Merge branch 'main' into opaque-extensions

engine/backends/fstar/fstar_backend.ml

@@ -401,8 +401,9 @@ struct
     let ppat = ppat' false in
     match p.p with
     | PWild -> F.wild
-    | PAscription { typ; pat } ->
+    | PAscription { typ; pat = { p = PBinding _; _ } as pat } ->
         F.pat @@ F.AST.PatAscribed (ppat pat, (pty p.span typ, None))
+    | PAscription { pat; _ } -> ppat pat
     | PBinding
         {
           mut = Immutable;

engine/lib/ast_utils.ml

@@ -226,9 +226,11 @@ module Make (F : Features.T) = struct
             ((enabled, s) : bool * (string, string) Hashtbl.t) gc =
           match gc with
           | GCType { goal; name } when enabled ->
-              let data = "i" ^ Int.to_string (Hashtbl.length s) in
-              let _ = Hashtbl.add s ~key:name ~data in
-              GCType { goal; name = data }
+              let new_name =
+                Hashtbl.find_or_add s name ~default:(fun () ->
+                    "i" ^ Int.to_string (Hashtbl.length s))
+              in
+              GCType { goal; name = new_name }
           | _ -> super#visit_generic_constraint (enabled, s) gc
 
         method! visit_trait_item (_, s) = super#visit_trait_item (true, s)

proof-libs/fstar/core/Alloc.Collections.Btree.Set.fsti

@@ -0,0 +1,3 @@
+module Alloc.Collections.Btree.Set
+
+val t_BTreeSet (t:Type0) (u:unit): eqtype

proof-libs/fstar/core/Alloc.Slice.fst → proof-libs/fstar/core/Alloc.Slice.fsti

@@ -3,3 +3,5 @@ open Rust_primitives.Arrays
 open Alloc.Vec
 
 let impl__to_vec #a (s: t_Slice a): t_Vec a Alloc.Alloc.t_Global = s
+
+val impl__concat #t1 #t2 (s: t_Slice t1): t_Slice t2

proof-libs/fstar/core/Alloc.Vec.fst

@@ -1,7 +1,7 @@
 module Alloc.Vec
 open Rust_primitives
 
-unfold type t_Vec t (_: unit) = s:t_Slice t
+unfold type t_Vec t (_: unit) = t_Slice t
 
 let impl__new #t (): t_Vec t () = FStar.Seq.empty
 
@@ -26,6 +26,8 @@ let impl_1__len #t (#[(Tactics.exact (`()))]alloc:unit) (v: t_Vec t alloc) =
   assert (n <= maxint usize_inttype);
   mk_int #usize_inttype (Seq.length v)
 
+let impl_1__as_slice #t (#[(Tactics.exact (`()))]alloc:unit) (v: t_Vec t alloc) : t_Slice t = v
+
 let from_elem #a (item: a) (len: usize) = Seq.create (v len) item
 
 open Rust_primitives.Hax

proof-libs/fstar/core/Core.Array.fst → proof-libs/fstar/core/Core.Array.fsti

@@ -8,5 +8,6 @@ let impl_23__map #a n #b (arr: t_Array a n) (f: a -> b): t_Array b n
 
 let impl_23__as_slice #a len (arr: t_Array a len): t_Slice a = arr
 
-let from_fn #a len (f: usize -> a): t_Array a len = admit()
+val from_fn #a len (f: usize -> a): Pure (t_Array a len) (requires True) (ensures (fun a -> forall i. Seq.index a i == f (sz i)))
+
 

proof-libs/fstar/core/Core.Fmt.fsti

@@ -23,3 +23,4 @@ val impl_2__new_v1 (sz1: usize) (sz2: usize) (pieces: t_Slice string) (args: t_S
 val impl_7__write_fmt (fmt: t_Formatter) (args: t_Arguments): t_Formatter & t_Result
 val impl_2__new_const (args: t_Slice string): t_Arguments
 
+

proof-libs/fstar/core/Core.Marker.fst

@@ -1,6 +1,8 @@
+
 module Core.Marker
 
-type t_PhantomData (t: Type) = t
+type t_PhantomData (t:Type0) = 
+     | PhantomData: t_PhantomData t
 
 class t_Send (h: Type) = {
   dummy_send_field: unit

proof-libs/fstar/core/Core.Num.fsti

@@ -1,6 +1,8 @@
 module Core.Num
 open Rust_primitives
 
+let impl__u16__MAX: u16 = mk_u16 (maxint u16_inttype)
+
 let impl__u8__wrapping_add: u8 -> u8 -> u8 = add_mod
 let impl__u8__wrapping_sub: u8 -> u8 -> u8 = sub_mod
 let impl__u16__wrapping_add: u16 -> u16 ->  u16 = add_mod

proof-libs/fstar/core/Core.Ops.Arith.fsti

@@ -46,3 +46,16 @@ class t_SubAssign self rhs = {
   f_sub_assign: x:self -> y:rhs -> Pure self (f_sub_assign_pre x y) (fun r -> f_sub_assign_post x y r);
 }
 
+class t_MulAssign self rhs = {
+   f_mul_assign_pre: self -> rhs -> bool;
+   f_mul_assign_post: self -> rhs -> self -> bool;
+   f_mul_assign: x:self -> y:rhs -> Pure self (f_mul_assign_pre x y) (fun r -> f_mul_assign_post x y r);
+}
+
+class t_DivAssign self rhs = {
+   f_div_assign_pre: self -> rhs -> bool;
+   f_div_assign_post: self -> rhs -> self -> bool;
+   f_div_assign: x:self -> y:rhs -> Pure self (f_div_assign_pre x y) (fun r -> f_div_assign_post x y r);
+}
+
+

proof-libs/fstar/core/Core.Option.fst

@@ -18,6 +18,8 @@ let impl__is_some #t_Self (self: t_Option t_Self): bool =  Option_Some? self
 
 let impl__is_none #t_Self (self: t_Option t_Self): bool =  Option_None? self
 
+let impl__take #t (x: t_Option t) : (t_Option t & t_Option t) = (x, Option_None)
+
 let impl__as_ref #t_Self (self: t_Option t_Self): t_Option t_Self = self
 
 let impl__unwrap_or_default 

proof-libs/fstar/core/Core.Result.fst

@@ -12,6 +12,8 @@ let impl__map_err #e1 #e2 (x: t_Result 't e1) (f: e1 -> e2): t_Result 't e2
 let impl__is_ok #t #e (self: t_Result t e): bool
   = Result_Ok? self
 
+let impl__expect #t #e (x: t_Result t e {Result_Ok? x}) (y: string): t = Result_Ok?.v x
+
 let impl__map #t #e #u (self: t_Result t e) (f: t -> u): t_Result u e =
   match self with 
   | Result_Ok v -> Result_Ok (f v)
@@ -21,3 +23,4 @@ let impl__and_then #t #e #u (self: t_Result t e) (op: t -> t_Result u e): t_Resu
   match self with 
   | Result_Ok v -> op v 
   | Result_Err e -> Result_Err e
+

proof-libs/fstar/core/Rand_core.Os.fsti

@@ -0,0 +1,9 @@
+module Rand_core.Os
+
+type t_OsRng
+
+[@FStar.Tactics.Typeclasses.tcinstance]
+val impl_rng_core: Rand_core.t_RngCore t_OsRng
+
+[@FStar.Tactics.Typeclasses.tcinstance]
+val impl_crypto_rng_core: Rand_core.t_CryptoRngCore t_OsRng

proof-libs/fstar/core/Rand_core.fsti

@@ -10,3 +10,9 @@ class t_RngCore (t_Self: Type0) = {
 class t_CryptoRng (t_Self: Type0) = {
   marker_trait: unit
 }
+
+class t_CryptoRngCore (t_Self: Type0) = {
+  f_rngcore: t_Self -> t_Self
+}
+
+

proof-libs/fstar/core/Std.Collections.Hash.Map.fsti

@@ -1,8 +1,5 @@
 module Std.Collections.Hash.Map
 
-open Core
-open FStar.Mul
+type t_HashMap (k v s:Type0)
 
-type t_HashMap (v_K: Type0) (v_V: Type0) (v_S: Type0) = {
-  f__hax_placeholder:unit
-}
+val impl__new #k #v: unit -> t_HashMap k v Std.Hash.Random.t_RandomState

proof-libs/fstar/core/Std.Hash.Random.fsti

@@ -1,5 +1,3 @@
 module Std.Hash.Random
 
-type t_RandomState = {
-    dummy_random_state_field: unit
-}
+type t_RandomState

proof-libs/fstar/rust_primitives/Rust_primitives.Hax.Monomorphized_update_at.fsti

@@ -14,9 +14,6 @@ let update_at_usize
   (x: t)
   : t_Array t (length s)
   = Seq.upd #t s (v i) x
-  // : Pure (t_Array t (length s))
-  //   (requires (v i < Seq.length s))
-  //   (ensures (fun res -> res == Seq.upd s (v i) x))
 
 val update_at_range #n
   (#t: Type0)

proof-libs/fstar/rust_primitives/Rust_primitives.Integers.fsti

@@ -238,14 +238,9 @@ val decr_equiv_lemma: #t:inttype
   -> a:int_t t{minint t < v a}
   -> Lemma (decr a == LI.decr #t #LI.PUB a)
 
-let div (#t:inttype) (a:int_t t) (b:int_t t{v b <> 0}) =
-  assume(unsigned t \/ range (v a / v b) t); // see issue #423
+let div (#t:inttype) (a:int_t t) (b:int_t t{v b <> 0 /\ (unsigned t \/ range (v a / v b) t)}) =
+  assert (unsigned t \/ range (v a / v b) t);
   mk_int #t (v a / v b)
-
-val div_equiv_lemma: #t:inttype{~(LI.U128? t) /\ ~(LI.S128? t)}
-  -> a:int_t t
-  -> b:int_t t{v b <> 0 /\ (unsigned t \/ range FStar.Int.(v a / v b) t)}
-  -> Lemma (div a b == LI.div a b)
 
 let mod (#t:inttype) (a:int_t t) (b:int_t t{v b <> 0}) =
   mk_int #t (v a % v b)