Merge pull request #555 from hacspec/explicit_len_arrow_of_list

feat(f*): `array_of_list`: inline the length of the array
cryspen · Mar 6, 2024 · 625ea90 · 625ea90
2 parents 0753253 + fa5c3ba
commit 625ea90
Show file tree

Hide file tree

Showing 5 changed files with 14 additions and 10 deletions.
diff --git a/engine/backends/fstar/fstar_backend.ml b/engine/backends/fstar/fstar_backend.ml
@@ -440,7 +440,6 @@ struct
         in
         let list_ident = F.id "list" in
         let list = F.term_of_lid [ "list" ] in
-        let array = F.mk_e_app array_of_list [ list ] in
         let assert_norm =
           F.term_of_lid [ "FStar"; "Pervasives"; "assert_norm" ]
         in
@@ -450,6 +449,7 @@ struct
         let len =
           F.term @@ F.AST.Const (F.Const.Const_int (Int.to_string len, None))
         in
+        let array = F.mk_e_app array_of_list [ len; list ] in
         let formula = F.mk_e_app equality [ length; len ] in
         let assertion = F.mk_e_app assert_norm [ formula ] in
         let pat = F.AST.PatVar (list_ident, None, []) |> F.pat in

diff --git a/proof-libs/fstar/rust_primitives/Rust_primitives.Hax.fst b/proof-libs/fstar/rust_primitives/Rust_primitives.Hax.fst
@@ -33,5 +33,7 @@ instance update_at_tc_array t l n: update_at_tc (t_Array t l) (int_t n) = {
 let (.[]<-) #self #idx {| update_at_tc self idx |} (s: self) (i: idx {f_index_pre s i})
   = update_at s i
 
-let array_of_list #t = Rust_primitives.Arrays.of_list #t
-
+let array_of_list (#t:Type)
+  (n: nat {n < maxint Lib.IntTypes.U16})
+  (l: list t {FStar.List.Tot.length l == n})
+  : t_Array t (sz n) = Rust_primitives.Arrays.of_list #t l
diff --git a/test-harness/src/snapshots/toolchain__generics into-fstar.snap b/test-harness/src/snapshots/toolchain__generics into-fstar.snap
@@ -90,7 +90,7 @@ let call_g (_: Prims.unit) : usize =
   (g (sz 3)
       (let list = [sz 42; sz 3; sz 49] in
         FStar.Pervasives.assert_norm (Prims.eq2 (List.Tot.length list) 3);
-        Rust_primitives.Hax.array_of_list list)
+        Rust_primitives.Hax.array_of_list 3 list)
     <:
     usize) +!
   sz 3

diff --git a/test-harness/src/snapshots/toolchain__mut-ref-functionalization into-fstar.snap b/test-harness/src/snapshots/toolchain__mut-ref-functionalization into-fstar.snap
@@ -83,7 +83,7 @@ let build_vec (_: Prims.unit) : Alloc.Vec.t_Vec u8 Alloc.Alloc.t_Global =
                 [1uy; 2uy; 3uy]
               in
               FStar.Pervasives.assert_norm (Prims.eq2 (List.Tot.length list) 3);
-              Rust_primitives.Hax.array_of_list list)
+              Rust_primitives.Hax.array_of_list 3 list)
           <:
           Alloc.Boxed.t_Box (t_Array u8 (sz 3)) Alloc.Alloc.t_Global)
       <:
@@ -95,7 +95,7 @@ let index_mutation (x: Core.Ops.Range.t_Range usize) (a: t_Slice u8) : Prims.uni
                   [1uy]
                 in
                 FStar.Pervasives.assert_norm (Prims.eq2 (List.Tot.length list) 1);
-                Rust_primitives.Hax.array_of_list list)
+                Rust_primitives.Hax.array_of_list 1 list)
             <:
             Alloc.Boxed.t_Box (t_Array u8 (sz 1)) Alloc.Alloc.t_Global)
         <:
@@ -127,7 +127,7 @@ let index_mutation_unsize (x: t_Array u8 (sz 12)) : u8 =
             t_Slice u8)
           (Rust_primitives.unsize (let list = [1uy; 2uy] in
                 FStar.Pervasives.assert_norm (Prims.eq2 (List.Tot.length list) 2);
-                Rust_primitives.Hax.array_of_list list)
+                Rust_primitives.Hax.array_of_list 2 list)
             <:
             t_Slice u8)
         <:
@@ -142,7 +142,7 @@ let test_append (_: Prims.unit) : Alloc.Vec.t_Vec u8 Alloc.Alloc.t_Global =
                   [1uy; 2uy; 3uy]
                 in
                 FStar.Pervasives.assert_norm (Prims.eq2 (List.Tot.length list) 3);
-                Rust_primitives.Hax.array_of_list list)
+                Rust_primitives.Hax.array_of_list 3 list)
             <:
             Alloc.Boxed.t_Box (t_Array u8 (sz 3)) Alloc.Alloc.t_Global)
         <:

diff --git a/test-harness/src/snapshots/toolchain__naming into-fstar.snap b/test-harness/src/snapshots/toolchain__naming into-fstar.snap
@@ -17,6 +17,8 @@ info:
     snapshot:
       stderr: false
       stdout: true
+    include_flag: ~
+    backend_options: ~
 ---
 exit = 0
 
@@ -36,7 +38,7 @@ let debug (label value: u32) : Prims.unit =
                   ["["; "] a="; "\n"]
                 in
                 FStar.Pervasives.assert_norm (Prims.eq2 (List.Tot.length list) 3);
-                Rust_primitives.Hax.array_of_list list)
+                Rust_primitives.Hax.array_of_list 3 list)
             <:
             t_Slice string)
           (Rust_primitives.unsize (let list =
@@ -46,7 +48,7 @@ let debug (label value: u32) : Prims.unit =
                   ]
                 in
                 FStar.Pervasives.assert_norm (Prims.eq2 (List.Tot.length list) 2);
-                Rust_primitives.Hax.array_of_list list)
+                Rust_primitives.Hax.array_of_list 2 list)
             <:
             t_Slice Core.Fmt.Rt.t_Argument)
         <: