Merge pull request #117 from cryspen/update-hax--let-rec--empty-list-…

…types fix(f*/lax): latest hax: fixes let-rec and types on empty lists
cryspen · Jul 3, 2024 · b5775ee · b5775ee
2 parents 7376ac8 + 7837018
commit b5775ee
Show file tree

Hide file tree

Showing 8 changed files with 459 additions and 528 deletions.
diff --git a/proofs/fstar/README.md b/proofs/fstar/README.md
@@ -45,9 +45,7 @@ create`) and regeneration of the `extraction` folder.
 
 The lax checking patch mainly performs the following fixes which will become unnecessary with future hax fixes:
 
-* Recursive functions are not produced with `let rec` in F*
 * IndexMut implementations need to implemented by hand in F*
-* Empty lists need type annotations in F*
 
 Finally, we edit the code in `extraction-lax` by hand to obtain panic-freedom proofs in `extraction-panic-free`.
 Eventually these hand-edits will be backported into Rust as pre- and post-conditions.

diff --git a/proofs/fstar/extraction-lax.patch b/proofs/fstar/extraction-lax.patch
diff --git a/proofs/fstar/extraction-lax/Bertie.Tls13formats.fst b/proofs/fstar/extraction-lax/Bertie.Tls13formats.fst
@@ -2259,7 +2259,7 @@ let parse_server_hello
 
 let server_certificate (v__algs: Bertie.Tls13crypto.t_Algorithms) (cert: Bertie.Tls13utils.t_Bytes) =
   match
-    Bertie.Tls13utils.encode_length_u8 (Rust_primitives.unsize (let list : list u8 = [] in
+    Bertie.Tls13utils.encode_length_u8 (Rust_primitives.unsize (let list:Prims.list u8 = [] in
             FStar.Pervasives.assert_norm (Prims.eq2 (List.Tot.length list) 0);
             Rust_primitives.Hax.array_of_list 0 list)
         <:

diff --git a/proofs/fstar/extraction-panic-free.patch b/proofs/fstar/extraction-panic-free.patch
diff --git a/proofs/fstar/extraction/Bertie.Tls13formats.Handshake_data.fst b/proofs/fstar/extraction/Bertie.Tls13formats.Handshake_data.fst
@@ -245,7 +245,7 @@ let impl__HandshakeData__from_bytes
   | Core.Result.Result_Err err ->
     Core.Result.Result_Err err <: Core.Result.t_Result t_HandshakeData u8
 
-let impl__HandshakeData__find_handshake_message
+let rec impl__HandshakeData__find_handshake_message
       (self: t_HandshakeData)
       (handshake_type: t_HandshakeType)
       (start: usize)

diff --git a/proofs/fstar/extraction/Bertie.Tls13formats.fst b/proofs/fstar/extraction/Bertie.Tls13formats.fst
@@ -1185,7 +1185,7 @@ let check_handshake_record (p: Bertie.Tls13utils.t_Bytes) =
           (Core.Result.t_Result (Bertie.Tls13formats.Handshake_data.t_HandshakeData & usize) u8)
           (Core.Result.t_Result (Bertie.Tls13formats.Handshake_data.t_HandshakeData & usize) u8))
 
-let check_server_extensions (algs: Bertie.Tls13crypto.t_Algorithms) (b: t_Slice u8) =
+let rec check_server_extensions (algs: Bertie.Tls13crypto.t_Algorithms) (b: t_Slice u8) =
   match check_server_extension algs b with
   | Core.Result.Result_Ok (len, out) ->
     if len =. (Core.Slice.impl__len b <: usize)
@@ -1464,7 +1464,7 @@ let encrypted_extensions (v__algs: Bertie.Tls13crypto.t_Algorithms) =
     <:
     Core.Result.t_Result Bertie.Tls13formats.Handshake_data.t_HandshakeData u8
 
-let find_key_share (g: Bertie.Tls13utils.t_Bytes) (ch: t_Slice u8) =
+let rec find_key_share (g: Bertie.Tls13utils.t_Bytes) (ch: t_Slice u8) =
   if (Core.Slice.impl__len ch <: usize) <. sz 4
   then Bertie.Tls13utils.tlserr (Bertie.Tls13utils.parse_failed () <: u8)
   else
@@ -2187,7 +2187,7 @@ let parse_server_hello
 
 let server_certificate (v__algs: Bertie.Tls13crypto.t_Algorithms) (cert: Bertie.Tls13utils.t_Bytes) =
   match
-    Bertie.Tls13utils.encode_length_u8 (Rust_primitives.unsize (let list = [] in
+    Bertie.Tls13utils.encode_length_u8 (Rust_primitives.unsize (let list:Prims.list u8 = [] in
             FStar.Pervasives.assert_norm (Prims.eq2 (List.Tot.length list) 0);
             Rust_primitives.Hax.array_of_list 0 list)
         <:
@@ -2484,7 +2484,7 @@ let impl__Transcript__transcript_hash_without_client_hello
       <:
       Bertie.Tls13utils.t_Bytes)
 
-let check_extensions_slice (algs: Bertie.Tls13crypto.t_Algorithms) (b: t_Slice u8) =
+let rec check_extensions_slice (algs: Bertie.Tls13crypto.t_Algorithms) (b: t_Slice u8) =
   match check_extension algs b with
   | Core.Result.Result_Ok (len, out) ->
     if len =. (Core.Slice.impl__len b <: usize)

diff --git a/proofs/fstar/extraction/Bertie.Tls13record.fst b/proofs/fstar/extraction/Bertie.Tls13record.fst
@@ -54,7 +54,7 @@ let derive_iv_ctr (iv: Bertie.Tls13utils.t_Bytes) (n: u64) =
   in
   iv_ctr
 
-let padlen (b: Bertie.Tls13utils.t_Bytes) (n: usize) =
+let rec padlen (b: Bertie.Tls13utils.t_Bytes) (n: usize) =
   if n >. sz 0 && (Bertie.Tls13utils.f_declassify (b.[ n -! sz 1 <: usize ] <: u8) <: u8) =. 0uy
   then sz 1 +! (padlen b (n -! sz 1 <: usize) <: usize)
   else sz 0

diff --git a/proofs/fstar/patches.sh b/proofs/fstar/patches.sh
@@ -7,11 +7,16 @@ cd "$SCRIPTPATH"
 
 DENYLIST=""
 
+CP="gcp"
+if ! command -v gcp &> /dev/null; then
+    CP="cp"
+fi
+
 # `prepare_folder SRC DEST` copies F* files from SRC to DEST/<basename SRC>
 prepare_folder() {
     original="$1"
     workdir="$2"
-    find "$original" \( -name '*.fst' -o -name '*.fsti' \) -exec gcp --parents \{\} "$workdir" \;
+    find "$original" \( -name '*.fst' -o -name '*.fsti' \) -exec "$CP" --parents \{\} "$workdir" \;
 }
 
 # `patch_folder ORIGINAL DESTINATION PATCH` creates the folder