Upstream fstar core changes from cryspen-sandwich.

examples/chacha20/proofs/fstar/extraction/Makefile

@@ -54,7 +54,7 @@ all:
 	$(MAKE) verify
 
 # Default hax invocation
-HAX_CLI = "cargo hax into fstar"
+HAX_CLI = "cargo hax into fstar --z3rlimit 40"
 
 # If $HACL_HOME doesn't exist, clone it
 ${HACL_HOME}:

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

@@ -0,0 +1,3 @@
+module Alloc.Borrow
+
+type t_Cow t = t

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

@@ -0,0 +1,3 @@
+module Alloc.Boxed
+
+type t_Box t t_Global = t

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

@@ -3,7 +3,7 @@ open Rust_primitives
 
 include Core.Fmt
 
-val impl_2__new_v1 (pieces: t_Slice string) (args: Core.Fmt.Rt.t_Argument): t_Arguments
+val impl_2__new_v1 (sz1:usize) (sz2: usize) (pieces: t_Slice string) (args: Core.Fmt.Rt.t_Argument): t_Arguments
 val impl_7__write_fmt (fmt: t_Formatter) (args: t_Arguments): t_Result
 
 val format (args: t_Arguments): string

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

@@ -2,4 +2,16 @@ module Alloc.String
 
 type t_String = string
 
+let impl__String__new (): t_String = ""
 
+let impl__String__push_str (self: t_String) (s: t_String): t_String =
+    self ^ s
+
+let impl__String__push (self: t_String) (ch: FStar.Char.char) = 
+    self ^ (FStar.String.string_of_char ch)
+
+let impl__String__pop (self: t_String): (Alloc.String.t_String & Core.Option.t_Option FStar.Char.char) = 
+    let l = FStar.String.length self in 
+    if l > 0 then 
+        (FStar.String.sub self 0 (l - 1), Core.Option.Option_Some (FStar.String.index self (l - 1)))
+    else (self, Core.Option.Option_None)

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

@@ -35,3 +35,6 @@ instance update_at_tc_array t n: update_at_tc (t_Vec t ()) (int_t n) = {
   update_at = (fun arr i x -> FStar.Seq.upd arr (v i) x);
 }
 
+
+let impl_1__is_empty #t (#[(Tactics.exact (`()))]alloc:unit) (v: t_Vec t alloc): bool =
+  Seq.length v = 0

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

@@ -0,0 +1,5 @@
+module Core.Borrow
+
+class t_Borrow (v_Self: Type0) (v_Borrowed: Type0) = {
+    f__hax_placeholder:unit
+}

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

@@ -72,4 +72,10 @@ class t_AsRef self t = {
   f_as_ref: self -> t;
 }
 
+instance as_ref_id a: t_AsRef a a = {
+  f_as_ref_pre = (fun _ -> true);
+  f_as_ref_post = (fun _ _ -> true);
+  f_as_ref = (fun x -> x)
+}
+
 type t_Infallible = _:unit{False}

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

@@ -0,0 +1,10 @@
+module Core.Error
+
+open FStar.Mul
+
+class t_Error (v_Self: Type0) = {
+  [@@@ FStar.Tactics.Typeclasses.no_method]_super_11603873402755071380:Core.Fmt.t_Debug v_Self;
+  [@@@ FStar.Tactics.Typeclasses.no_method]_super_7348497752681407507:Core.Fmt.t_Display v_Self;
+
+  f__hax_placeholder:unit
+}

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

@@ -12,8 +12,14 @@ class t_Display t_Self = {
   f_fmt: t_Self -> t_Formatter -> (t_Formatter & Core.Result.t_Result Prims.unit t_Error)
 }
 
+class t_Debug t_Self = {
+  f_dbg_fmt_pre: t_Self -> Core.Fmt.t_Formatter -> bool;
+  f_dbg_fmt_post: t_Self -> Core.Fmt.t_Formatter -> (Core.Fmt.t_Formatter & Core.Result.t_Result Prims.unit Core.Fmt.t_Error) -> bool;
+  f_dbg_fmt: t_Self -> Core.Fmt.t_Formatter -> (Core.Fmt.t_Formatter & Core.Result.t_Result Prims.unit Core.Fmt.t_Error)
+}
+
 val t_Arguments: Type0
-val impl_2__new_v1 (pieces: t_Slice string) (args: t_Slice Core.Fmt.Rt.t_Argument): t_Arguments
+val impl_2__new_v1 (sz1: usize) (sz2: usize) (pieces: t_Slice string) (args: t_Slice Core.Fmt.Rt.t_Argument): t_Arguments
 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.Iter.Traits.Iterator.fst

@@ -39,3 +39,4 @@ class iterator (self: Type u#0): Type u#1 = {
   f_all:       self -> (f_Item -> bool) -> self * bool;
 }
 
+let t_Iterator = iterator

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

@@ -1,5 +1,25 @@
 module Core.Marker
 
+type t_PhantomData (t: Type) = t
+
+class t_Send (h: Type) = {
+  dummy_send_field: unit
+}
+
+(** we consider everything to be send *)
+instance t_Send_all t: t_Send t = {
+  dummy_send_field = ()
+}
+
+class t_Sync (h: Type) = {
+  dummy_sync_field: unit
+}
+
+(** we consider everything to be sync *)
+instance t_Sync_all t: t_Sync t = {
+  dummy_sync_field = ()
+}
+
 class t_Sized (h: Type) = {
   dummy_field: unit
 }
@@ -17,3 +37,12 @@ class t_Copy (h: Type) = {
 instance t_Copy_all t: t_Copy t = {
   dummy_copy_field = ()
 }
+
+class t_Clone (h: Type) = {
+  dummy_clone_field: unit
+}
+
+(** we consider everything to be clonable *)
+instance t_Clone_all t: t_Clone t = {
+  dummy_clone_field = ()
+}

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

@@ -0,0 +1,6 @@
+module Core.Ops.Bit
+open FStar.Mul
+
+class t_Shr (v_Self: Type0) (v_Rhs: Type0) = {
+  f_Output:Type0;
+}

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

@@ -16,3 +16,33 @@ let impl__unwrap #t (x: t_Option t {Option_Some? x}): t = Option_Some?._0 x
 
 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__as_ref #t_Self (self: t_Option t_Self): t_Option t_Self = self
+
+let impl__unwrap_or_default 
+      #t {| i1: Core.Default.t_Default t |}
+      (self: t_Option t)
+      =
+  match self with
+  | Option_Some inner -> inner
+  | Core.Option.Option_None  -> Core.Default.f_default #t ()
+
+let impl__unwrap_or
+      #t
+      (self: t_Option t)
+      (def: t)
+      =
+  match self with
+  | Option_Some inner -> inner
+  | Core.Option.Option_None  -> def
+
+let impl__ok_or_else #t_Self #e (self: t_Option t_Self) (err: unit -> e): Core.Result.t_Result t_Self e =
+  match self with 
+  | Option_Some inner -> Core.Result.Result_Ok inner
+  | Option_None -> Core.Result.Result_Err (err ())
+
+let impl__ok_or #t_Self #e (self: t_Option t_Self) (err: e): Core.Result.t_Result t_Self e =
+  match self with 
+  | Option_Some inner -> Core.Result.Result_Ok inner
+  | Option_None -> Core.Result.Result_Err err

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

@@ -8,4 +8,16 @@ let impl__map_err #e1 #e2 (x: t_Result 't e1) (f: e1 -> e2): t_Result 't e2
   = match x with
   | Result_Ok v -> Result_Ok v
   | Result_Err e -> Result_Err (f e)
+
+let impl__is_ok #t #e (self: t_Result t e): bool
+  = Result_Ok? self
 
+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)
+  | Result_Err e -> Result_Err e
+
+let impl__and_then #t #e #u (self: t_Result t e) (op: t -> t_Result u e): t_Result u e =
+  match self with 
+  | Result_Ok v -> op v 
+  | Result_Err e -> Result_Err e

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

@@ -0,0 +1,8 @@
+module Std.Collections.Hash.Map
+
+open Core
+open FStar.Mul
+
+type t_HashMap (v_K: Type0) (v_V: Type0) (v_S: Type0) = {
+  f__hax_placeholder:unit
+}

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

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

proof-libs/fstar/core/Std.Io.Error.fsti

@@ -0,0 +1,6 @@
+module Std.Io.Error
+
+open Core
+open FStar.Mul
+
+type t_Error = { f__hax_placeholder:Prims.unit }

proof-libs/fstar/core/Std.Io.fsti

@@ -0,0 +1,29 @@
+module Std.Io
+
+open Core
+open FStar.Mul
+
+class t_Read (v_Self: Type0) = {
+  f_read_pre:v_Self -> t_Slice u8 -> bool;
+  f_read_post:v_Self -> t_Slice u8 -> (v_Self & t_Slice u8 & Core.Result.t_Result usize Std.Io.Error.t_Error)
+    -> bool;
+  f_read:x0: v_Self -> x1: t_Slice u8
+    -> Prims.Pure (v_Self & t_Slice u8 & Core.Result.t_Result usize Std.Io.Error.t_Error)
+        (f_read_pre x0 x1)
+        (fun result -> f_read_post x0 x1 result)
+}
+
+class t_Write (v_Self: Type0) = {
+  f_write_pre:v_Self -> t_Slice u8 -> bool;
+  f_write_post:v_Self -> t_Slice u8 -> (v_Self & Core.Result.t_Result usize Std.Io.Error.t_Error) -> bool;
+  f_write:x0: v_Self -> x1: t_Slice u8
+    -> Prims.Pure (v_Self & Core.Result.t_Result usize Std.Io.Error.t_Error)
+        (f_write_pre x0 x1)
+        (fun result -> f_write_post x0 x1 result);
+  f_flush_pre:v_Self -> bool;
+  f_flush_post:v_Self -> (v_Self & Core.Result.t_Result Prims.unit Std.Io.Error.t_Error) -> bool;
+  f_flush:x0: v_Self
+    -> Prims.Pure (v_Self & Core.Result.t_Result Prims.unit Std.Io.Error.t_Error)
+        (f_flush_pre x0)
+        (fun result -> f_flush_post x0 result)
+}