Merge pull request #679 from hacspec/fix-667-explicits-types

Engine: F*: fix #677 by always extracting implicit types
hacspec · May 22, 2024 · 9da5c6c · 9da5c6c
2 parents 455fbeb + ecc3a12
commit 9da5c6c
Show file tree

Hide file tree

Showing 21 changed files with 436 additions and 274 deletions.
diff --git a/engine/backends/fstar/fstar_ast.ml b/engine/backends/fstar/fstar_ast.ml
@@ -53,6 +53,7 @@ let mk_e_abs args body =
 let mk_e_app base args =
   AST.mkApp base (List.map ~f:(fun arg -> (arg, AST.Nothing)) args) dummyRange
 
+let mk_app base args = AST.mkApp base args dummyRange
 let unit = term AST.(Const Const_unit)
 
 let tc_solve =

diff --git a/engine/backends/fstar/fstar_backend.ml b/engine/backends/fstar/fstar_backend.ml
@@ -450,14 +450,17 @@ struct
             @@ "pexpr: expected a integer, found the following non-digit \
                 chars: '" ^ s ^ "'");
         F.AST.Const (F.Const.Const_int (s, None)) |> F.term
-    | App { f; args; generic_args } ->
-        let const_generics =
-          List.filter_map
-            ~f:(function GConst e -> Some e | _ -> None)
-            generic_args
+    | App { f; args; generic_args; bounds_impls = _; impl = _ } ->
+        let generic_args =
+          generic_args
+          |> List.filter ~f:(function GType (TArrow _) -> false | _ -> true)
+          |> List.map ~f:(function
+               | GConst const -> (pexpr const, F.AST.Nothing)
+               | GLifetime _ -> .
+               | GType ty -> (pty e.span ty, F.AST.Hash))
         in
-        let args = const_generics @ args in
-        F.mk_e_app (pexpr f) @@ List.map ~f:pexpr args
+        let args = List.map ~f:(pexpr &&& Fn.const F.AST.Nothing) args in
+        F.mk_app (pexpr f) (generic_args @ args)
     | If { cond; then_; else_ } ->
         F.term
         @@ F.AST.If

diff --git a/examples/Cargo.lock b/examples/Cargo.lock
diff --git a/examples/barrett/proofs/fstar/extraction/Makefile b/examples/barrett/proofs/fstar/extraction/Makefile
@@ -53,7 +53,7 @@ all:
 	rm -f .depend && $(MAKE) .depend
 	$(MAKE) verify
 
-HAX_CLI = "cargo hax into fstar --z3rlimit 500"
+HAX_CLI = "cargo hax into fstar --z3rlimit 1000"
 
 # If $HACL_HOME doesn't exist, clone it
 ${HACL_HOME}:

diff --git a/examples/chacha20/proofs/fstar/extraction/Chacha20.Hacspec_helper.fst b/examples/chacha20/proofs/fstar/extraction/Chacha20.Hacspec_helper.fst
@@ -5,10 +5,9 @@ open FStar.Mul
 
 let add_state (state other: t_Array u32 (sz 16)) : t_Array u32 (sz 16) =
   let state:t_Array u32 (sz 16) =
-    Core.Iter.Traits.Iterator.f_fold (Core.Iter.Traits.Collect.f_into_iter ({
-              Core.Ops.Range.f_start = sz 0;
-              Core.Ops.Range.f_end = sz 16
-            }
+    Core.Iter.Traits.Iterator.f_fold (Core.Iter.Traits.Collect.f_into_iter #(Core.Ops.Range.t_Range
+            usize)
+          ({ Core.Ops.Range.f_start = sz 0; Core.Ops.Range.f_end = sz 16 }
             <:
             Core.Ops.Range.t_Range usize)
         <:
@@ -27,16 +26,18 @@ let add_state (state other: t_Array u32 (sz 16)) : t_Array u32 (sz 16) =
 
 let update_array (array: t_Array u8 (sz 64)) (v_val: t_Slice u8) : t_Array u8 (sz 64) =
   let _:Prims.unit =
-    if ~.(sz 64 >=. (Core.Slice.impl__len v_val <: usize) <: bool)
+    if ~.(sz 64 >=. (Core.Slice.impl__len #u8 v_val <: usize) <: bool)
     then
       Rust_primitives.Hax.never_to_any (Core.Panicking.panic "assertion failed: 64 >= val.len()"
           <:
           Rust_primitives.Hax.t_Never)
   in
   let array:t_Array u8 (sz 64) =
-    Core.Iter.Traits.Iterator.f_fold (Core.Iter.Traits.Collect.f_into_iter ({
+    Core.Iter.Traits.Iterator.f_fold (Core.Iter.Traits.Collect.f_into_iter #(Core.Ops.Range.t_Range
+            usize)
+          ({
               Core.Ops.Range.f_start = sz 0;
-              Core.Ops.Range.f_end = Core.Slice.impl__len v_val <: usize
+              Core.Ops.Range.f_end = Core.Slice.impl__len #u8 v_val <: usize
             }
             <:
             Core.Ops.Range.t_Range usize)
@@ -54,10 +55,9 @@ let update_array (array: t_Array u8 (sz 64)) (v_val: t_Slice u8) : t_Array u8 (s
 
 let xor_state (state other: t_Array u32 (sz 16)) : t_Array u32 (sz 16) =
   let state:t_Array u32 (sz 16) =
-    Core.Iter.Traits.Iterator.f_fold (Core.Iter.Traits.Collect.f_into_iter ({
-              Core.Ops.Range.f_start = sz 0;
-              Core.Ops.Range.f_end = sz 16
-            }
+    Core.Iter.Traits.Iterator.f_fold (Core.Iter.Traits.Collect.f_into_iter #(Core.Ops.Range.t_Range
+            usize)
+          ({ Core.Ops.Range.f_start = sz 0; Core.Ops.Range.f_end = sz 16 }
             <:
             Core.Ops.Range.t_Range usize)
         <:
@@ -77,10 +77,9 @@ let xor_state (state other: t_Array u32 (sz 16)) : t_Array u32 (sz 16) =
 let to_le_u32s_16_ (bytes: t_Slice u8) : t_Array u32 (sz 16) =
   let out:t_Array u32 (sz 16) = Rust_primitives.Hax.repeat 0ul (sz 16) in
   let out:t_Array u32 (sz 16) =
-    Core.Iter.Traits.Iterator.f_fold (Core.Iter.Traits.Collect.f_into_iter ({
-              Core.Ops.Range.f_start = sz 0;
-              Core.Ops.Range.f_end = sz 16
-            }
+    Core.Iter.Traits.Iterator.f_fold (Core.Iter.Traits.Collect.f_into_iter #(Core.Ops.Range.t_Range
+            usize)
+          ({ Core.Ops.Range.f_start = sz 0; Core.Ops.Range.f_end = sz 16 }
             <:
             Core.Ops.Range.t_Range usize)
         <:
@@ -91,8 +90,11 @@ let to_le_u32s_16_ (bytes: t_Slice u8) : t_Array u32 (sz 16) =
           let i:usize = i in
           Rust_primitives.Hax.Monomorphized_update_at.update_at_usize out
             i
-            (Core.Num.impl__u32__from_le_bytes (Core.Result.impl__unwrap (Core.Convert.f_try_into (bytes.[
-                            {
+            (Core.Num.impl__u32__from_le_bytes (Core.Result.impl__unwrap #(t_Array u8 (sz 4))
+                    #Core.Array.t_TryFromSliceError
+                    (Core.Convert.f_try_into #(t_Slice u8)
+                        #(t_Array u8 (sz 4))
+                        (bytes.[ {
                               Core.Ops.Range.f_start = sz 4 *! i <: usize;
                               Core.Ops.Range.f_end = (sz 4 *! i <: usize) +! sz 4 <: usize
                             }
@@ -114,10 +116,9 @@ let to_le_u32s_16_ (bytes: t_Slice u8) : t_Array u32 (sz 16) =
 let to_le_u32s_3_ (bytes: t_Slice u8) : t_Array u32 (sz 3) =
   let out:t_Array u32 (sz 3) = Rust_primitives.Hax.repeat 0ul (sz 3) in
   let out:t_Array u32 (sz 3) =
-    Core.Iter.Traits.Iterator.f_fold (Core.Iter.Traits.Collect.f_into_iter ({
-              Core.Ops.Range.f_start = sz 0;
-              Core.Ops.Range.f_end = sz 3
-            }
+    Core.Iter.Traits.Iterator.f_fold (Core.Iter.Traits.Collect.f_into_iter #(Core.Ops.Range.t_Range
+            usize)
+          ({ Core.Ops.Range.f_start = sz 0; Core.Ops.Range.f_end = sz 3 }
             <:
             Core.Ops.Range.t_Range usize)
         <:
@@ -128,8 +129,11 @@ let to_le_u32s_3_ (bytes: t_Slice u8) : t_Array u32 (sz 3) =
           let i:usize = i in
           Rust_primitives.Hax.Monomorphized_update_at.update_at_usize out
             i
-            (Core.Num.impl__u32__from_le_bytes (Core.Result.impl__unwrap (Core.Convert.f_try_into (bytes.[
-                            {
+            (Core.Num.impl__u32__from_le_bytes (Core.Result.impl__unwrap #(t_Array u8 (sz 4))
+                    #Core.Array.t_TryFromSliceError
+                    (Core.Convert.f_try_into #(t_Slice u8)
+                        #(t_Array u8 (sz 4))
+                        (bytes.[ {
                               Core.Ops.Range.f_start = sz 4 *! i <: usize;
                               Core.Ops.Range.f_end = (sz 4 *! i <: usize) +! sz 4 <: usize
                             }
@@ -151,10 +155,9 @@ let to_le_u32s_3_ (bytes: t_Slice u8) : t_Array u32 (sz 3) =
 let to_le_u32s_8_ (bytes: t_Slice u8) : t_Array u32 (sz 8) =
   let out:t_Array u32 (sz 8) = Rust_primitives.Hax.repeat 0ul (sz 8) in
   let out:t_Array u32 (sz 8) =
-    Core.Iter.Traits.Iterator.f_fold (Core.Iter.Traits.Collect.f_into_iter ({
-              Core.Ops.Range.f_start = sz 0;
-              Core.Ops.Range.f_end = sz 8
-            }
+    Core.Iter.Traits.Iterator.f_fold (Core.Iter.Traits.Collect.f_into_iter #(Core.Ops.Range.t_Range
+            usize)
+          ({ Core.Ops.Range.f_start = sz 0; Core.Ops.Range.f_end = sz 8 }
             <:
             Core.Ops.Range.t_Range usize)
         <:
@@ -165,8 +168,11 @@ let to_le_u32s_8_ (bytes: t_Slice u8) : t_Array u32 (sz 8) =
           let i:usize = i in
           Rust_primitives.Hax.Monomorphized_update_at.update_at_usize out
             i
-            (Core.Num.impl__u32__from_le_bytes (Core.Result.impl__unwrap (Core.Convert.f_try_into (bytes.[
-                            {
+            (Core.Num.impl__u32__from_le_bytes (Core.Result.impl__unwrap #(t_Array u8 (sz 4))
+                    #Core.Array.t_TryFromSliceError
+                    (Core.Convert.f_try_into #(t_Slice u8)
+                        #(t_Array u8 (sz 4))
+                        (bytes.[ {
                               Core.Ops.Range.f_start = sz 4 *! i <: usize;
                               Core.Ops.Range.f_end = (sz 4 *! i <: usize) +! sz 4 <: usize
                             }
@@ -188,11 +194,13 @@ let to_le_u32s_8_ (bytes: t_Slice u8) : t_Array u32 (sz 8) =
 let u32s_to_le_bytes (state: t_Array u32 (sz 16)) : t_Array u8 (sz 64) =
   let out:t_Array u8 (sz 64) = Rust_primitives.Hax.repeat 0uy (sz 64) in
   let out:t_Array u8 (sz 64) =
-    Core.Iter.Traits.Iterator.f_fold (Core.Iter.Traits.Collect.f_into_iter ({
+    Core.Iter.Traits.Iterator.f_fold (Core.Iter.Traits.Collect.f_into_iter #(Core.Ops.Range.t_Range
+            usize)
+          ({
               Core.Ops.Range.f_start = sz 0;
               Core.Ops.Range.f_end
               =
-              Core.Slice.impl__len (Rust_primitives.unsize state <: t_Slice u32) <: usize
+              Core.Slice.impl__len #u32 (Rust_primitives.unsize state <: t_Slice u32) <: usize
             }
             <:
             Core.Ops.Range.t_Range usize)
@@ -203,10 +211,9 @@ let u32s_to_le_bytes (state: t_Array u32 (sz 16)) : t_Array u8 (sz 64) =
           let out:t_Array u8 (sz 64) = out in
           let i:usize = i in
           let tmp:t_Array u8 (sz 4) = Core.Num.impl__u32__to_le_bytes (state.[ i ] <: u32) in
-          Core.Iter.Traits.Iterator.f_fold (Core.Iter.Traits.Collect.f_into_iter ({
-                    Core.Ops.Range.f_start = sz 0;
-                    Core.Ops.Range.f_end = sz 4
-                  }
+          Core.Iter.Traits.Iterator.f_fold (Core.Iter.Traits.Collect.f_into_iter #(Core.Ops.Range.t_Range
+                  usize)
+                ({ Core.Ops.Range.f_start = sz 0; Core.Ops.Range.f_end = sz 4 }
                   <:
                   Core.Ops.Range.t_Range usize)
               <:

diff --git a/examples/chacha20/proofs/fstar/extraction/Chacha20.fst b/examples/chacha20/proofs/fstar/extraction/Chacha20.fst
@@ -107,12 +107,10 @@ let chacha20_double_round (state: t_Array u32 (sz 16)) : t_Array u32 (sz 16) =
 let chacha20_rounds (state: t_Array u32 (sz 16)) : t_Array u32 (sz 16) =
   let st:t_Array u32 (sz 16) = state in
   let st:t_Array u32 (sz 16) =
-    Core.Iter.Traits.Iterator.f_fold (Core.Iter.Traits.Collect.f_into_iter ({
-              Core.Ops.Range.f_start = 0l;
-              Core.Ops.Range.f_end = 10l
-            }
-            <:
-            Core.Ops.Range.t_Range i32)
+    Core.Iter.Traits.Iterator.f_fold (Core.Iter.Traits.Collect.f_into_iter #(Core.Ops.Range.t_Range
+            i32)
+          ({ Core.Ops.Range.f_start = 0l; Core.Ops.Range.f_end = 10l } <: Core.Ops.Range.t_Range i32
+          )
         <:
         Core.Ops.Range.t_Range i32)
       st
@@ -144,14 +142,15 @@ let chacha20_encrypt_block (st0: t_Array u32 (sz 16)) (ctr: u32) (plain: t_Array
 
 let chacha20_encrypt_last (st0: t_Array u32 (sz 16)) (ctr: u32) (plain: t_Slice u8)
     : Prims.Pure (Alloc.Vec.t_Vec u8 Alloc.Alloc.t_Global)
-      (requires (Core.Slice.impl__len plain <: usize) <=. sz 64)
+      (requires (Core.Slice.impl__len #u8 plain <: usize) <=. sz 64)
       (fun _ -> Prims.l_True) =
   let (b: t_Array u8 (sz 64)):t_Array u8 (sz 64) = Rust_primitives.Hax.repeat 0uy (sz 64) in
   let b:t_Array u8 (sz 64) = Chacha20.Hacspec_helper.update_array b plain in
   let b:t_Array u8 (sz 64) = chacha20_encrypt_block st0 ctr b in
-  Alloc.Slice.impl__to_vec (b.[ {
+  Alloc.Slice.impl__to_vec #u8
+    (b.[ {
           Core.Ops.Range.f_start = sz 0;
-          Core.Ops.Range.f_end = Core.Slice.impl__len plain <: usize
+          Core.Ops.Range.f_end = Core.Slice.impl__len #u8 plain <: usize
         }
         <:
         Core.Ops.Range.t_Range usize ]
@@ -186,14 +185,13 @@ let chacha20_key_block0 (key: t_Array u8 (sz 32)) (iv: t_Array u8 (sz 12)) : t_A
 
 let chacha20_update (st0: t_Array u32 (sz 16)) (m: t_Slice u8)
     : Alloc.Vec.t_Vec u8 Alloc.Alloc.t_Global =
-  let blocks_out:Alloc.Vec.t_Vec u8 Alloc.Alloc.t_Global = Alloc.Vec.impl__new () in
-  let num_blocks:usize = (Core.Slice.impl__len m <: usize) /! sz 64 in
-  let remainder_len:usize = (Core.Slice.impl__len m <: usize) %! sz 64 in
+  let blocks_out:Alloc.Vec.t_Vec u8 Alloc.Alloc.t_Global = Alloc.Vec.impl__new #u8 () in
+  let num_blocks:usize = (Core.Slice.impl__len #u8 m <: usize) /! sz 64 in
+  let remainder_len:usize = (Core.Slice.impl__len #u8 m <: usize) %! sz 64 in
   let blocks_out:Alloc.Vec.t_Vec u8 Alloc.Alloc.t_Global =
-    Core.Iter.Traits.Iterator.f_fold (Core.Iter.Traits.Collect.f_into_iter ({
-              Core.Ops.Range.f_start = sz 0;
-              Core.Ops.Range.f_end = num_blocks
-            }
+    Core.Iter.Traits.Iterator.f_fold (Core.Iter.Traits.Collect.f_into_iter #(Core.Ops.Range.t_Range
+            usize)
+          ({ Core.Ops.Range.f_start = sz 0; Core.Ops.Range.f_end = num_blocks }
             <:
             Core.Ops.Range.t_Range usize)
         <:
@@ -205,7 +203,11 @@ let chacha20_update (st0: t_Array u32 (sz 16)) (m: t_Slice u8)
           let b:t_Array u8 (sz 64) =
             chacha20_encrypt_block st0
               (cast (i <: usize) <: u32)
-              (Core.Result.impl__unwrap (Core.Convert.f_try_into (m.[ {
+              (Core.Result.impl__unwrap #(t_Array u8 (sz 64))
+                  #Core.Array.t_TryFromSliceError
+                  (Core.Convert.f_try_into #(t_Slice u8)
+                      #(t_Array u8 (sz 64))
+                      (m.[ {
                             Core.Ops.Range.f_start = sz 64 *! i <: usize;
                             Core.Ops.Range.f_end = (sz 64 *! i <: usize) +! sz 64 <: usize
                           }
@@ -219,17 +221,22 @@ let chacha20_update (st0: t_Array u32 (sz 16)) (m: t_Slice u8)
                 t_Array u8 (sz 64))
           in
           let _:Prims.unit =
-            Hax_lib.v_assume ((Alloc.Vec.impl_1__len blocks_out <: usize) =. (i *! sz 64 <: usize)
+            Hax_lib.v_assume ((Alloc.Vec.impl_1__len #u8 #Alloc.Alloc.t_Global blocks_out <: usize) =.
+                (i *! sz 64 <: usize)
                 <:
                 bool)
           in
           let blocks_out:Alloc.Vec.t_Vec u8 Alloc.Alloc.t_Global =
-            Alloc.Vec.impl_2__extend_from_slice blocks_out (Rust_primitives.unsize b <: t_Slice u8)
+            Alloc.Vec.impl_2__extend_from_slice #u8
+              #Alloc.Alloc.t_Global
+              blocks_out
+              (Rust_primitives.unsize b <: t_Slice u8)
           in
           blocks_out)
   in
   let _:Prims.unit =
-    Hax_lib.v_assume ((Alloc.Vec.impl_1__len blocks_out <: usize) =. (num_blocks *! sz 64 <: usize)
+    Hax_lib.v_assume ((Alloc.Vec.impl_1__len #u8 #Alloc.Alloc.t_Global blocks_out <: usize) =.
+        (num_blocks *! sz 64 <: usize)
         <:
         bool)
   in
@@ -241,15 +248,18 @@ let chacha20_update (st0: t_Array u32 (sz 16)) (m: t_Slice u8)
           (cast (num_blocks <: usize) <: u32)
           (m.[ {
                 Core.Ops.Range.f_start = sz 64 *! num_blocks <: usize;
-                Core.Ops.Range.f_end = Core.Slice.impl__len m <: usize
+                Core.Ops.Range.f_end = Core.Slice.impl__len #u8 m <: usize
               }
               <:
               Core.Ops.Range.t_Range usize ]
             <:
             t_Slice u8)
       in
       let blocks_out:Alloc.Vec.t_Vec u8 Alloc.Alloc.t_Global =
-        Alloc.Vec.impl_2__extend_from_slice blocks_out (Core.Ops.Deref.f_deref b <: t_Slice u8)
+        Alloc.Vec.impl_2__extend_from_slice #u8
+          #Alloc.Alloc.t_Global
+          blocks_out
+          (Core.Ops.Deref.f_deref #(Alloc.Vec.t_Vec u8 Alloc.Alloc.t_Global) b <: t_Slice u8)
       in
       blocks_out
     else blocks_out