Merge pull request #1728 from cryspen/vec-deque-lib

Better VecDeque model and other F* proof lib improvements/fixes.

Author: maximebuyse

CHANGELOG.md

@@ -40,6 +40,7 @@ Change to cargo-hax:
 Changes to hax-lib:
 - New behavior for `hax_lib::include`: it now forces inclusion when in contradiction with `-i` flag.
 - hax-lib requires edition 2021 instead of 2024 (#1726)
+- Improved `VecDeque` model in F* proof lib (#1728)
 
 Changes to the Lean backend:
 - Improve support for functionalized loops (#1695)

hax-lib/proof-libs/fstar/core/Alloc.Collections.Vec_deque.fsti

@@ -1,24 +1,21 @@
 module Alloc.Collections.Vec_deque
 open Rust_primitives
 
-type t_VecDeque: Type0 -> unit -> Type0
+unfold type t_VecDeque t (_: unit) = t_Slice t
 
 val impl_5__push_back #t #a (v: t_VecDeque t a) (x: t): t_VecDeque t a
 
-val impl_5__len #t #a (v: t_VecDeque t a): usize
+let impl_5__len #t #a (v: t_VecDeque t a): usize = sz (Seq.length v)
 
-val impl_5__pop_front #t #a (v: t_VecDeque t a): t_VecDeque t a & Core.Option.t_Option t
+let impl_5__pop_front #t #a (v: t_VecDeque t a): t_VecDeque t a & Core.Option.t_Option t = 
+  match Seq.seq_to_list v with 
+  | h::tail -> Seq.seq_of_list tail,  Core.Option.Option_Some h 
+  | [] -> v, Core.Option.Option_None
 
 
 [@FStar.Tactics.Typeclasses.tcinstance]
 val from_vec_deque_array t a n: Core.Convert.t_From (Alloc.Collections.Vec_deque.t_VecDeque t a)
         (Rust_primitives.Arrays.t_Array t
             (Rust_primitives.Integers.mk_usize n))
 
-[@FStar.Tactics.Typeclasses.tcinstance]
-val index_vec_deque t a: Core.Ops.Index.t_Index (Alloc.Collections.Vec_deque.t_VecDeque t a)
-        Rust_primitives.Integers.usize
 
-[@FStar.Tactics.Typeclasses.tcinstance]
-val update_at t a: Rust_primitives.Hax.update_at_tc (Alloc.Collections.Vec_deque.t_VecDeque t a)
-        Rust_primitives.Integers.usize

hax-lib/proof-libs/fstar/core/Core.Cmp.fsti

@@ -28,7 +28,7 @@ type t_Ordering =
 
 
 class t_PartialOrd (v_Self: Type) (v_Rhs:Type) = {
-  _super_17767811571638026139: t_PartialEq v_Self v_Rhs;
+  _super_14602337363870446881: t_PartialEq v_Self v_Rhs;
   f_partial_cmp_pre: v_Self -> v_Rhs -> Type0;
   f_partial_cmp_post: v_Self -> v_Rhs -> Core.Option.t_Option t_Ordering -> Type0;
   f_partial_cmp:v_Self -> v_Rhs -> Core.Option.t_Option t_Ordering;
@@ -55,8 +55,8 @@ let f_ge #v_Self #v_Rhs {| t_PartialOrd v_Self v_Rhs |} (self: v_Self) (rhs: v_R
   | _ -> true
 
 class t_Ord (v_Self: Type) = {
-  _super_8562072132021960682: t_Eq v_Self;
-  _super_17650760217149814164: t_PartialOrd v_Self v_Self;
+  _super_6686490714486791726: t_Eq v_Self;
+  _super_7232954788087520964: t_PartialOrd v_Self v_Self;
   f_cmp_pre: v_Self -> v_Self -> Type0;
   f_cmp_post: v_Self -> v_Self -> t_Ordering -> Type0;
   f_cmp:v_Self -> v_Self -> t_Ordering;
@@ -86,7 +86,7 @@ instance eq_int_t t : t_Eq (int_t t) = {
 }
 
 instance partialOrd_int t : (t_PartialOrd (int_t t) (int_t t)) = {
-  _super_17767811571638026139 = (FStar.Tactics.Typeclasses.solve);
+  _super_14602337363870446881 = (FStar.Tactics.Typeclasses.solve);
 
   f_partial_cmp_pre = (fun x y -> True);
   f_partial_cmp_post = (fun x y z -> match z with
@@ -104,8 +104,8 @@ instance partialOrd_int t : (t_PartialOrd (int_t t) (int_t t)) = {
 
 [@FStar.Tactics.Typeclasses.tcinstance]
 instance ord_int t : t_Ord (int_t t) = {
-  _super_8562072132021960682 = (FStar.Tactics.Typeclasses.solve);
-  _super_17650760217149814164 = (FStar.Tactics.Typeclasses.solve);
+  _super_6686490714486791726 = (FStar.Tactics.Typeclasses.solve);
+  _super_7232954788087520964 = (FStar.Tactics.Typeclasses.solve);
   f_cmp_pre = (fun x y -> True) ;
   f_cmp_post = (fun x y r ->
     match r with

hax-lib/proof-libs/fstar/core/Core.Iter.Traits.Iterator.fst

@@ -72,3 +72,7 @@ assume val flat_map_iter (t: Type0) (u: Type0) (v: Type0) : Core.Iter.Traits.Ite
 [@FStar.Tactics.Typeclasses.tcinstance]
 assume val t_split_iter (pattern: Type) :
 (Core.Str.Iter.t_Split pattern) -> t_Iterator (Core.Str.Iter.t_Split pattern)
+
+[@@ FStar.Tactics.Typeclasses.tcinstance]
+assume val iterator_map (t: Type0) (u: Type0): 
+  t_Iterator (Core.Iter.Adapters.Map.t_Map t u)