From f5871c3044d8af0cf33755ca7f98155fe59878bc Mon Sep 17 00:00:00 2001 From: Lucas Franceschino Date: Wed, 10 Apr 2024 09:18:55 +0200 Subject: [PATCH 1/2] fix(f*/lax): latest hax: fixes let-rec and types on empty lists --- proofs/fstar/README.md | 2 - proofs/fstar/extraction-lax.patch | 295 +++----- .../extraction-lax/Bertie.Tls13formats.fst | 2 +- proofs/fstar/extraction-panic-free.patch | 669 +++++++++--------- .../Bertie.Tls13formats.Handshake_data.fst | 2 +- .../fstar/extraction/Bertie.Tls13formats.fst | 8 +- .../fstar/extraction/Bertie.Tls13record.fst | 2 +- proofs/fstar/patches.sh | 2 +- 8 files changed, 454 insertions(+), 528 deletions(-) diff --git a/proofs/fstar/README.md b/proofs/fstar/README.md index 43efafe5..4ae58174 100644 --- 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 index 610024db..c992f99a 100644 --- a/proofs/fstar/extraction-lax.patch +++ b/proofs/fstar/extraction-lax.patch @@ -1,6 +1,6 @@ diff -ruN extraction/Bertie.Tls13crypto.fsti extraction-lax/Bertie.Tls13crypto.fsti ---- extraction/Bertie.Tls13crypto.fsti 2024-04-05 08:35:02 -+++ extraction-lax/Bertie.Tls13crypto.fsti 2024-04-05 08:35:03 +--- extraction/Bertie.Tls13crypto.fsti 2024-04-10 09:10:50.119985620 +0200 ++++ extraction-lax/Bertie.Tls13crypto.fsti 2024-04-10 09:10:50.159963761 +0200 @@ -46,10 +46,12 @@ val valid_rsa_exponent (e: Alloc.Vec.t_Vec u8 Alloc.Alloc.t_Global) : Prims.Pure bool Prims.l_True (fun _ -> Prims.l_True) @@ -55,21 +55,9 @@ diff -ruN extraction/Bertie.Tls13crypto.fsti extraction-lax/Bertie.Tls13crypto.f val impl__AeadKey__new (bytes: Bertie.Tls13utils.t_Bytes) (alg: t_AeadAlgorithm) : Prims.Pure t_AeadKey Prims.l_True (fun _ -> Prims.l_True) -diff -ruN extraction/Bertie.Tls13formats.Handshake_data.fst extraction-lax/Bertie.Tls13formats.Handshake_data.fst ---- extraction/Bertie.Tls13formats.Handshake_data.fst 2024-04-05 08:35:02 -+++ extraction-lax/Bertie.Tls13formats.Handshake_data.fst 2024-04-05 08:35:03 -@@ -245,7 +245,7 @@ - | 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 -ruN extraction/Bertie.Tls13formats.fst extraction-lax/Bertie.Tls13formats.fst ---- extraction/Bertie.Tls13formats.fst 2024-04-05 08:35:02 -+++ extraction-lax/Bertie.Tls13formats.fst 2024-04-05 08:35:03 +--- extraction/Bertie.Tls13formats.fst 2024-04-10 09:10:50.124982888 +0200 ++++ extraction-lax/Bertie.Tls13formats.fst 2024-04-10 09:10:50.149969226 +0200 @@ -104,16 +104,18 @@ let check_psk_key_exchange_modes (client_hello: t_Slice u8) = match Bertie.Tls13utils.check_length_encoding_u8_slice client_hello with @@ -147,16 +135,16 @@ diff -ruN extraction/Bertie.Tls13formats.fst extraction-lax/Bertie.Tls13formats. (match - Bertie.Tls13utils.check_eq_with_slice (Bertie.Tls13utils.impl__Bytes__as_raw hoist21 + Bertie.Tls13utils.check_eq_slice (Bertie.Tls13utils.impl__Bytes__as_raw hoist21 ++ <: ++ t_Slice u8) ++ (b.[ { Core.Ops.Range.f_start = sz 0; Core.Ops.Range.f_end = sz 2 } ++ <: ++ Core.Ops.Range.t_Range usize ] <: t_Slice u8) - b - (sz 0) - (sz 2) -+ (b.[ { Core.Ops.Range.f_start = sz 0; Core.Ops.Range.f_end = sz 2 } -+ <: -+ Core.Ops.Range.t_Range usize ] -+ <: -+ t_Slice u8) with | Core.Result.Result_Ok _ -> (match @@ -212,6 +200,19 @@ diff -ruN extraction/Bertie.Tls13formats.fst extraction-lax/Bertie.Tls13formats. - } - <: - Core.Ops.Range.t_Range usize ] +- <: +- t_Slice u8) +- with +- | Core.Result.Result_Ok ok -> +- Core.Ops.Control_flow.ControlFlow_Continue out +- <: +- Core.Ops.Control_flow.t_ControlFlow +- (Core.Result.t_Result (usize & Core.Option.t_Option Bertie.Tls13utils.t_Bytes) +- u8) (Core.Option.t_Option Bertie.Tls13utils.t_Bytes) +- | Core.Result.Result_Err err -> +- let! _:Prims.unit = +- Core.Ops.Control_flow.ControlFlow_Break +- (Core.Result.Result_Err err + Core.Ops.Range.t_Range usize ] + <: + t_Slice u8) @@ -230,10 +231,34 @@ diff -ruN extraction/Bertie.Tls13formats.fst extraction-lax/Bertie.Tls13formats. + Core.Ops.Range.f_end = sz 4 +! len <: usize + } <: +- Core.Result.t_Result (usize & Core.Option.t_Option Bertie.Tls13utils.t_Bytes) +- u8) ++ Core.Ops.Range.t_Range usize ] + <: +- Core.Ops.Control_flow.t_ControlFlow +- (Core.Result.t_Result (usize & Core.Option.t_Option Bertie.Tls13utils.t_Bytes) +- u8) Prims.unit +- in +- Core.Ops.Control_flow.ControlFlow_Continue out +- <: +- Core.Ops.Control_flow.t_ControlFlow +- (Core.Result.t_Result (usize & Core.Option.t_Option Bertie.Tls13utils.t_Bytes) +- u8) (Core.Option.t_Option Bertie.Tls13utils.t_Bytes)) +- | 0uy, 51uy -> +- (match +- check_server_key_share algs +- (b.[ { +- Core.Ops.Range.f_start = sz 4; +- Core.Ops.Range.f_end = sz 4 +! len <: usize +- } +- <: +- Core.Ops.Range.t_Range usize ] +- <: - t_Slice u8) - with -- | Core.Result.Result_Ok ok -> -- Core.Ops.Control_flow.ControlFlow_Continue out +- | Core.Result.Result_Ok gx -> +- Core.Ops.Control_flow.ControlFlow_Continue +- (Core.Option.Option_Some gx <: Core.Option.t_Option Bertie.Tls13utils.t_Bytes) - <: - Core.Ops.Control_flow.t_ControlFlow - (Core.Result.t_Result (usize & Core.Option.t_Option Bertie.Tls13utils.t_Bytes) @@ -245,13 +270,6 @@ diff -ruN extraction/Bertie.Tls13formats.fst extraction-lax/Bertie.Tls13formats. - <: - Core.Result.t_Result (usize & Core.Option.t_Option Bertie.Tls13utils.t_Bytes) - u8) -+ Core.Ops.Range.t_Range usize ] - <: -- Core.Ops.Control_flow.t_ControlFlow -- (Core.Result.t_Result (usize & Core.Option.t_Option Bertie.Tls13utils.t_Bytes) -- u8) Prims.unit -- in -- Core.Ops.Control_flow.ControlFlow_Continue out + t_Slice u8) + with + | Core.Result.Result_Ok ok -> @@ -264,16 +282,21 @@ diff -ruN extraction/Bertie.Tls13formats.fst extraction-lax/Bertie.Tls13formats. + let! _:Prims.unit = + Core.Ops.Control_flow.ControlFlow_Break + (Core.Result.Result_Err err -+ <: + <: +- Core.Ops.Control_flow.t_ControlFlow +- (Core.Result.t_Result (usize & Core.Option.t_Option Bertie.Tls13utils.t_Bytes) +- u8) Prims.unit +- in +- Core.Ops.Control_flow.ControlFlow_Continue out + Core.Result.t_Result (usize & Core.Option.t_Option Bertie.Tls13utils.t_Bytes) u8 + ) <: Core.Ops.Control_flow.t_ControlFlow (Core.Result.t_Result (usize & Core.Option.t_Option Bertie.Tls13utils.t_Bytes) - u8) (Core.Option.t_Option Bertie.Tls13utils.t_Bytes)) -- | 0uy, 51uy -> +- | 0uy, 41uy -> - (match -- check_server_key_share algs +- check_server_psk_shared_key algs - (b.[ { - Core.Ops.Range.f_start = sz 4; - Core.Ops.Range.f_end = sz 4 +! len <: usize @@ -297,27 +320,10 @@ diff -ruN extraction/Bertie.Tls13formats.fst extraction-lax/Bertie.Tls13formats. <: - t_Slice u8) - with -- | Core.Result.Result_Ok gx -> -- Core.Ops.Control_flow.ControlFlow_Continue -- (Core.Option.Option_Some gx <: Core.Option.t_Option Bertie.Tls13utils.t_Bytes) -- <: -- Core.Ops.Control_flow.t_ControlFlow -- (Core.Result.t_Result (usize & Core.Option.t_Option Bertie.Tls13utils.t_Bytes) -- u8) (Core.Option.t_Option Bertie.Tls13utils.t_Bytes) -- | Core.Result.Result_Err err -> -- let! _:Prims.unit = -- Core.Ops.Control_flow.ControlFlow_Break -- (Core.Result.Result_Err err -- <: -- Core.Result.t_Result (usize & Core.Option.t_Option Bertie.Tls13utils.t_Bytes) -- u8) -+ Core.Ops.Range.t_Range usize ] - <: -- Core.Ops.Control_flow.t_ControlFlow -- (Core.Result.t_Result (usize & Core.Option.t_Option Bertie.Tls13utils.t_Bytes) -- u8) Prims.unit -- in +- | Core.Result.Result_Ok ok -> - Core.Ops.Control_flow.ControlFlow_Continue out ++ Core.Ops.Range.t_Range usize ] ++ <: + t_Slice u8) + with + | Core.Result.Result_Ok gx -> @@ -337,16 +343,11 @@ diff -ruN extraction/Bertie.Tls13formats.fst extraction-lax/Bertie.Tls13formats. <: Core.Ops.Control_flow.t_ControlFlow (Core.Result.t_Result (usize & Core.Option.t_Option Bertie.Tls13utils.t_Bytes) -- u8) (Core.Option.t_Option Bertie.Tls13utils.t_Bytes)) -- | 0uy, 41uy -> -- (match -- check_server_psk_shared_key algs -- (b.[ { -- Core.Ops.Range.f_start = sz 4; -- Core.Ops.Range.f_end = sz 4 +! len <: usize -- } -- <: -- Core.Ops.Range.t_Range usize ] +- u8) (Core.Option.t_Option Bertie.Tls13utils.t_Bytes) +- | Core.Result.Result_Err err -> +- let! _:Prims.unit = +- Core.Ops.Control_flow.ControlFlow_Break +- (Core.Result.Result_Err err + u8) Prims.unit + in + Core.Ops.Control_flow.ControlFlow_Continue out @@ -362,19 +363,6 @@ diff -ruN extraction/Bertie.Tls13formats.fst extraction-lax/Bertie.Tls13formats. + Core.Ops.Range.f_end = sz 4 +! len <: usize + } <: -- t_Slice u8) -- with -- | Core.Result.Result_Ok ok -> -- Core.Ops.Control_flow.ControlFlow_Continue out -- <: -- Core.Ops.Control_flow.t_ControlFlow -- (Core.Result.t_Result (usize & Core.Option.t_Option Bertie.Tls13utils.t_Bytes) -- u8) (Core.Option.t_Option Bertie.Tls13utils.t_Bytes) -- | Core.Result.Result_Err err -> -- let! _:Prims.unit = -- Core.Ops.Control_flow.ControlFlow_Break -- (Core.Result.Result_Err err -- <: - Core.Result.t_Result (usize & Core.Option.t_Option Bertie.Tls13utils.t_Bytes) - u8) + Core.Ops.Range.t_Range usize ] @@ -584,15 +572,6 @@ diff -ruN extraction/Bertie.Tls13formats.fst extraction-lax/Bertie.Tls13formats. let check_handshake_record (p: Bertie.Tls13utils.t_Bytes) = Rust_primitives.Hax.Control_flow_monad.Mexception.run (if -@@ -1185,7 +1211,7 @@ - (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) @@ -1235,8 +1261,8 @@ with | Core.Result.Result_Ok legacy_session_id -> @@ -621,15 +600,6 @@ diff -ruN extraction/Bertie.Tls13formats.fst extraction-lax/Bertie.Tls13formats. <: Bertie.Tls13formats.Handshake_data.t_HandshakeData) <: -@@ -1464,7 +1490,7 @@ - <: - 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 @@ -1528,8 +1554,8 @@ match Bertie.Tls13utils.check_length_encoding_u16_slice ch with | Core.Result.Result_Ok _ -> @@ -737,6 +707,23 @@ diff -ruN extraction/Bertie.Tls13formats.fst extraction-lax/Bertie.Tls13formats. + Core.Ops.Range.t_Range usize ] <: - (usize & t_Extensions)) +- <: +- Core.Result.t_Result (usize & t_Extensions) u8 +- | Core.Result.Result_Err err -> +- Core.Result.Result_Err err <: Core.Result.t_Result (usize & t_Extensions) u8) +- | 0uy, 45uy -> +- (match +- check_psk_key_exchange_modes (bytes.[ { +- Core.Ops.Range.f_start = sz 4; +- Core.Ops.Range.f_end = sz 4 +! len <: usize +- } +- <: +- Core.Ops.Range.t_Range usize ] +- <: +- t_Slice u8) +- with +- | Core.Result.Result_Ok _ -> +- Core.Result.Result_Ok (sz 4 +! len, out <: (usize & t_Extensions)) + t_Slice u8) + with + | Core.Result.Result_Ok hoist152 -> @@ -762,9 +749,9 @@ diff -ruN extraction/Bertie.Tls13formats.fst extraction-lax/Bertie.Tls13formats. - Core.Result.t_Result (usize & t_Extensions) u8 - | Core.Result.Result_Err err -> - Core.Result.Result_Err err <: Core.Result.t_Result (usize & t_Extensions) u8) -- | 0uy, 45uy -> +- | 0uy, 43uy -> - (match -- check_psk_key_exchange_modes (bytes.[ { +- check_supported_versions (bytes.[ { - Core.Ops.Range.f_start = sz 4; - Core.Ops.Range.f_end = sz 4 +! len <: usize - } @@ -790,9 +777,10 @@ diff -ruN extraction/Bertie.Tls13formats.fst extraction-lax/Bertie.Tls13formats. - Core.Result.t_Result (usize & t_Extensions) u8 - | Core.Result.Result_Err err -> - Core.Result.Result_Err err <: Core.Result.t_Result (usize & t_Extensions) u8) -- | 0uy, 43uy -> +- | 0uy, 10uy -> - (match -- check_supported_versions (bytes.[ { +- check_supported_groups algs +- (bytes.[ { - Core.Ops.Range.f_start = sz 4; - Core.Ops.Range.f_end = sz 4 +! len <: usize - } @@ -823,9 +811,9 @@ diff -ruN extraction/Bertie.Tls13formats.fst extraction-lax/Bertie.Tls13formats. - Core.Result.t_Result (usize & t_Extensions) u8 - | Core.Result.Result_Err err -> - Core.Result.Result_Err err <: Core.Result.t_Result (usize & t_Extensions) u8) -- | 0uy, 10uy -> +- | 0uy, 13uy -> - (match -- check_supported_groups algs +- check_signature_algorithms algs - (bytes.[ { - Core.Ops.Range.f_start = sz 4; - Core.Ops.Range.f_end = sz 4 +! len <: usize @@ -858,9 +846,9 @@ diff -ruN extraction/Bertie.Tls13formats.fst extraction-lax/Bertie.Tls13formats. - Core.Result.t_Result (usize & t_Extensions) u8 - | Core.Result.Result_Err err -> - Core.Result.Result_Err err <: Core.Result.t_Result (usize & t_Extensions) u8) -- | 0uy, 13uy -> +- | 0uy, 51uy -> - (match -- check_signature_algorithms algs +- check_key_shares algs - (bytes.[ { - Core.Ops.Range.f_start = sz 4; - Core.Ops.Range.f_end = sz 4 +! len <: usize @@ -887,24 +875,6 @@ diff -ruN extraction/Bertie.Tls13formats.fst extraction-lax/Bertie.Tls13formats. <: - t_Slice u8) - with -- | Core.Result.Result_Ok _ -> -- Core.Result.Result_Ok (sz 4 +! len, out <: (usize & t_Extensions)) -- <: -- Core.Result.t_Result (usize & t_Extensions) u8 -- | Core.Result.Result_Err err -> -- Core.Result.Result_Err err <: Core.Result.t_Result (usize & t_Extensions) u8) -- | 0uy, 51uy -> -- (match -- check_key_shares algs -- (bytes.[ { -- Core.Ops.Range.f_start = sz 4; -- Core.Ops.Range.f_end = sz 4 +! len <: usize -- } -- <: -- Core.Ops.Range.t_Range usize ] -- <: -- t_Slice u8) -- with - | Core.Result.Result_Ok gx -> - Core.Result.Result_Ok - (sz 4 +! len, @@ -941,8 +911,7 @@ diff -ruN extraction/Bertie.Tls13formats.fst extraction-lax/Bertie.Tls13formats. <: - t_Extensions) + Core.Ops.Range.t_Range usize ] - <: -- (usize & t_Extensions)) ++ <: + t_Slice u8) + with + | Core.Result.Result_Ok gx -> @@ -960,7 +929,8 @@ diff -ruN extraction/Bertie.Tls13formats.fst extraction-lax/Bertie.Tls13formats. + = + Core.Option.Option_None <: Core.Option.t_Option Bertie.Tls13utils.t_Bytes + } -+ <: + <: +- (usize & t_Extensions)) + t_Extensions) <: - Core.Result.t_Result (usize & t_Extensions) u8 @@ -1096,7 +1066,7 @@ diff -ruN extraction/Bertie.Tls13formats.fst extraction-lax/Bertie.Tls13formats. Core.Ops.Range.f_end = Bertie.Tls13utils.impl__Bytes__len sc <: usize } <: -@@ -2005,159 +2022,199 @@ +@@ -2005,157 +2022,197 @@ (algs: Bertie.Tls13crypto.t_Algorithms) (server_hello: Bertie.Tls13formats.Handshake_data.t_HandshakeData) = @@ -1270,9 +1240,7 @@ diff -ruN extraction/Bertie.Tls13formats.fst extraction-lax/Bertie.Tls13formats. <: - t_Slice u8) + Bertie.Tls13utils.t_Bytes) - with -- | Core.Result.Result_Ok sidlen -> -- let next:usize = (next +! sz 1 <: usize) +! sidlen in ++ with + | Core.Result.Result_Ok _ -> + Core.Ops.Control_flow.ControlFlow_Continue (() <: Prims.unit) + <: @@ -1313,7 +1281,9 @@ diff -ruN extraction/Bertie.Tls13formats.fst extraction-lax/Bertie.Tls13formats. + Core.Ops.Range.t_Range usize) + <: + Bertie.Tls13utils.t_Bytes) -+ with + with +- | Core.Result.Result_Ok sidlen -> +- let next:usize = (next +! sz 1 <: usize) +! sidlen in + | Core.Result.Result_Ok _ -> + let next:usize = next +! sz 2 in (match @@ -1424,16 +1394,14 @@ diff -ruN extraction/Bertie.Tls13formats.fst extraction-lax/Bertie.Tls13formats. + | Core.Option.Option_Some gy -> + Core.Result.Result_Ok + (srand, gy <: (Bertie.Tls13utils.t_Bytes & Bertie.Tls13utils.t_Bytes)) - <: - Core.Result.t_Result ++ <: ++ Core.Result.t_Result + (Bertie.Tls13utils.t_Bytes & Bertie.Tls13utils.t_Bytes) u8 + | _ -> + Core.Result.Result_Err Bertie.Tls13utils.v_MISSING_KEY_SHARE -+ <: -+ Core.Result.t_Result + <: + Core.Result.t_Result (Bertie.Tls13utils.t_Bytes & Bertie.Tls13utils.t_Bytes) u8) - | Core.Result.Result_Err err -> - Core.Result.Result_Err err @@ -2168,26 +2225,41 @@ Core.Result.Result_Err err <: @@ -1482,20 +1450,11 @@ diff -ruN extraction/Bertie.Tls13formats.fst extraction-lax/Bertie.Tls13formats. 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 + Bertie.Tls13utils.encode_length_u8 (Rust_primitives.unsize (let list : list u8 = [] in FStar.Pervasives.assert_norm (Prims.eq2 (List.Tot.length list) 0); Rust_primitives.Hax.array_of_list 0 list) <: -@@ -2484,7 +2556,7 @@ - <: - 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) @@ -2533,33 +2605,29 @@ (ciphersuite: Bertie.Tls13crypto.t_Algorithms) (client_hello: Bertie.Tls13formats.Handshake_data.t_HandshakeData) @@ -1649,7 +1608,7 @@ diff -ruN extraction/Bertie.Tls13formats.fst extraction-lax/Bertie.Tls13formats. ({ Core.Ops.Range.f_start = next; Core.Ops.Range.f_end -@@ -2634,194 +2760,158 @@ +@@ -2634,194 +2760,168 @@ <: Bertie.Tls13utils.t_Bytes) with @@ -1983,16 +1942,6 @@ diff -ruN extraction/Bertie.Tls13formats.fst extraction-lax/Bertie.Tls13formats. + Core.Option.t_Option Bertie.Tls13utils.t_Bytes & + Core.Option.t_Option Bertie.Tls13utils.t_Bytes & + usize)) - <: - Core.Result.t_Result - (Bertie.Tls13utils.t_Bytes & Bertie.Tls13utils.t_Bytes & -@@ -2829,6 +2919,16 @@ - Bertie.Tls13utils.t_Bytes & - Core.Option.t_Option Bertie.Tls13utils.t_Bytes & - Core.Option.t_Option Bertie.Tls13utils.t_Bytes & -+ usize) u8 -+ | _ -> -+ Core.Result.Result_Err (Bertie.Tls13utils.parse_failed ()) + <: + Core.Result.t_Result + (Bertie.Tls13utils.t_Bytes & Bertie.Tls13utils.t_Bytes & @@ -2000,9 +1949,12 @@ diff -ruN extraction/Bertie.Tls13formats.fst extraction-lax/Bertie.Tls13formats. + Bertie.Tls13utils.t_Bytes & + Core.Option.t_Option Bertie.Tls13utils.t_Bytes & + Core.Option.t_Option Bertie.Tls13utils.t_Bytes & - usize) u8) - | Core.Result.Result_Err err -> - Core.Result.Result_Err err ++ usize) u8 ++ | _ -> ++ Core.Result.Result_Err (Bertie.Tls13utils.parse_failed ()) + <: + Core.Result.t_Result + (Bertie.Tls13utils.t_Bytes & Bertie.Tls13utils.t_Bytes & @@ -2850,49 +2950,121 @@ Core.Option.t_Option Bertie.Tls13utils.t_Bytes & Core.Option.t_Option Bertie.Tls13utils.t_Bytes & @@ -2154,8 +2106,8 @@ diff -ruN extraction/Bertie.Tls13formats.fst extraction-lax/Bertie.Tls13formats. + Core.Option.t_Option Bertie.Tls13utils.t_Bytes & + usize) u8)) diff -ruN extraction/Bertie.Tls13formats.fsti extraction-lax/Bertie.Tls13formats.fsti ---- extraction/Bertie.Tls13formats.fsti 2024-04-05 08:35:02 -+++ extraction-lax/Bertie.Tls13formats.fsti 2024-04-05 08:35:03 +--- extraction/Bertie.Tls13formats.fsti 2024-04-10 09:10:50.113988899 +0200 ++++ extraction-lax/Bertie.Tls13formats.fsti 2024-04-10 09:10:50.156965400 +0200 @@ -408,7 +408,7 @@ | _ -> Bertie.Tls13utils.tlserr (Bertie.Tls13utils.parse_failed () <: u8) } @@ -2165,21 +2117,9 @@ diff -ruN extraction/Bertie.Tls13formats.fsti extraction-lax/Bertie.Tls13formats : Prims.Pure (Core.Result.t_Result Prims.unit u8) Prims.l_True (fun _ -> Prims.l_True) val check_server_psk_shared_key (v__algs: Bertie.Tls13crypto.t_Algorithms) (b: t_Slice u8) -diff -ruN extraction/Bertie.Tls13record.fst extraction-lax/Bertie.Tls13record.fst ---- extraction/Bertie.Tls13record.fst 2024-04-05 08:35:02 -+++ extraction-lax/Bertie.Tls13record.fst 2024-04-05 08:35:03 -@@ -54,7 +54,7 @@ - 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 -ruN extraction/Bertie.Tls13utils.fsti extraction-lax/Bertie.Tls13utils.fsti ---- extraction/Bertie.Tls13utils.fsti 2024-04-05 08:35:02 -+++ extraction-lax/Bertie.Tls13utils.fsti 2024-04-05 08:35:03 +--- extraction/Bertie.Tls13utils.fsti 2024-04-10 09:10:50.129980156 +0200 ++++ extraction-lax/Bertie.Tls13utils.fsti 2024-04-10 09:10:50.165960482 +0200 @@ -129,9 +129,6 @@ val check_eq_slice (b1 b2: t_Slice u8) : Prims.Pure (Core.Result.t_Result Prims.unit u8) Prims.l_True (fun _ -> Prims.l_True) @@ -2199,7 +2139,7 @@ diff -ruN extraction/Bertie.Tls13utils.fsti extraction-lax/Bertie.Tls13utils.fst f_index_post = (fun (self: t_Bytes) (x: usize) (out: u8) -> true); f_index = fun (self: t_Bytes) (x: usize) -> self._0.[ x ] } -@@ -212,10 +209,22 @@ +@@ -212,11 +209,23 @@ let impl_9: Core.Ops.Index.t_Index t_Bytes (Core.Ops.Range.t_Range usize) = { f_Output = t_Slice u8; @@ -2212,7 +2152,7 @@ diff -ruN extraction/Bertie.Tls13utils.fsti extraction-lax/Bertie.Tls13utils.fst f_index_post = (fun (self: t_Bytes) (x: Core.Ops.Range.t_Range usize) (out: t_Slice u8) -> true); f_index = fun (self: t_Bytes) (x: Core.Ops.Range.t_Range usize) -> self._0.[ x ] } -+ + +[@@ FStar.Tactics.Typeclasses.tcinstance] +let upd_10: Rust_primitives.Hax.update_at_tc t_Bytes usize = + { @@ -2220,6 +2160,7 @@ diff -ruN extraction/Bertie.Tls13utils.fsti extraction-lax/Bertie.Tls13utils.fst + update_at = fun s (i:usize{v i < Seq.length s._0}) x -> Bytes (Seq.upd s._0 (v i) x) + } + - ++ val impl__Bytes__append (self x: t_Bytes) : Prims.Pure t_Bytes Prims.l_True (fun _ -> Prims.l_True) + val impl__Bytes__concat (self other: t_Bytes) diff --git a/proofs/fstar/extraction-lax/Bertie.Tls13formats.fst b/proofs/fstar/extraction-lax/Bertie.Tls13formats.fst index 4ee71852..023334e0 100644 --- 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 index 211b9196..a9773ab5 100644 --- a/proofs/fstar/extraction-panic-free.patch +++ b/proofs/fstar/extraction-panic-free.patch @@ -1,6 +1,6 @@ diff -ruN extraction-lax/Bertie.Tls13api.fst extraction-panic-free/Bertie.Tls13api.fst ---- extraction-lax/Bertie.Tls13api.fst 2024-04-05 08:35:03 -+++ extraction-panic-free/Bertie.Tls13api.fst 2024-04-05 08:35:03 +--- extraction-lax/Bertie.Tls13api.fst 2024-04-10 09:10:50.153967040 +0200 ++++ extraction-panic-free/Bertie.Tls13api.fst 2024-04-10 09:10:50.195944087 +0200 @@ -72,6 +72,7 @@ (impl_916461611_ & Core.Result.t_Result (Bertie.Tls13utils.t_Bytes & t_Client) u8) @@ -56,8 +56,8 @@ diff -ruN extraction-lax/Bertie.Tls13api.fst extraction-panic-free/Bertie.Tls13a let hax_temp_output:Core.Result.t_Result (Bertie.Tls13utils.t_Bytes & Bertie.Tls13utils.t_Bytes & t_Server) u8 = diff -ruN extraction-lax/Bertie.Tls13api.fsti extraction-panic-free/Bertie.Tls13api.fsti ---- extraction-lax/Bertie.Tls13api.fsti 2024-04-05 08:35:03 -+++ extraction-panic-free/Bertie.Tls13api.fsti 2024-04-05 08:35:03 +--- extraction-lax/Bertie.Tls13api.fsti 2024-04-10 09:10:50.168958842 +0200 ++++ extraction-panic-free/Bertie.Tls13api.fsti 2024-04-10 09:10:50.194944634 +0200 @@ -42,7 +42,7 @@ (session_ticket psk: Core.Option.t_Option Bertie.Tls13utils.t_Bytes) (rng: impl_916461611_) @@ -90,8 +90,8 @@ diff -ruN extraction-lax/Bertie.Tls13api.fsti extraction-panic-free/Bertie.Tls13 + (Seq.length client_hello._0 >= 3) (fun _ -> Prims.l_True) diff -ruN extraction-lax/Bertie.Tls13cert.fst extraction-panic-free/Bertie.Tls13cert.fst ---- extraction-lax/Bertie.Tls13cert.fst 2024-04-05 08:35:03 -+++ extraction-panic-free/Bertie.Tls13cert.fst 2024-04-05 08:35:03 +--- extraction-lax/Bertie.Tls13cert.fst 2024-04-10 09:10:50.155965947 +0200 ++++ extraction-panic-free/Bertie.Tls13cert.fst 2024-04-10 09:10:50.185949552 +0200 @@ -1,5 +1,5 @@ module Bertie.Tls13cert -#set-options "--fuel 0 --ifuel 1 --z3rlimit 15" @@ -132,7 +132,7 @@ diff -ruN extraction-lax/Bertie.Tls13cert.fst extraction-panic-free/Bertie.Tls13 let short_length (b: Bertie.Tls13utils.t_Bytes) (offset: usize) = if ((Bertie.Tls13utils.f_declassify (b.[ offset ] <: u8) <: u8) &. 128uy <: u8) =. 0uy then -@@ -131,26 +144,20 @@ +@@ -131,25 +144,19 @@ | Core.Result.Result_Err err -> Core.Result.Result_Err err <: Core.Result.t_Result (usize & usize) u8 @@ -146,14 +146,7 @@ diff -ruN extraction-lax/Bertie.Tls13cert.fst extraction-panic-free/Bertie.Tls13 - Core.Result.Result_Ok (offset +! length) <: Core.Result.t_Result usize u8 - | Core.Result.Result_Err err -> Core.Result.Result_Err err <: Core.Result.t_Result usize u8) - | Core.Result.Result_Err err -> Core.Result.Result_Err err <: Core.Result.t_Result usize u8 -+ Core.Result.Result_Ok (Bertie.Tls13utils.impl__Bytes__slice b offset length) -+ <: -+ Core.Result.t_Result Bertie.Tls13utils.t_Bytes u8 -+ | Core.Result.Result_Err err -> -+ Core.Result.Result_Err err <: Core.Result.t_Result Bertie.Tls13utils.t_Bytes u8) -+ | Core.Result.Result_Err err -> -+ Core.Result.Result_Err err <: Core.Result.t_Result Bertie.Tls13utils.t_Bytes u8 - +- -let skip_sequence (b: Bertie.Tls13utils.t_Bytes) (offset: usize) = - match check_tag b offset 48uy with - | Core.Result.Result_Ok _ -> @@ -163,10 +156,16 @@ diff -ruN extraction-lax/Bertie.Tls13cert.fst extraction-panic-free/Bertie.Tls13 - Core.Result.Result_Ok (offset +! length) <: Core.Result.t_Result usize u8 - | Core.Result.Result_Err err -> Core.Result.Result_Err err <: Core.Result.t_Result usize u8) - | Core.Result.Result_Err err -> Core.Result.Result_Err err <: Core.Result.t_Result usize u8 -- ++ Core.Result.Result_Ok (Bertie.Tls13utils.impl__Bytes__slice b offset length) ++ <: ++ Core.Result.t_Result Bertie.Tls13utils.t_Bytes u8 ++ | Core.Result.Result_Err err -> ++ Core.Result.Result_Err err <: Core.Result.t_Result Bertie.Tls13utils.t_Bytes u8) ++ | Core.Result.Result_Err err -> ++ Core.Result.Result_Err err <: Core.Result.t_Result Bertie.Tls13utils.t_Bytes u8 + let read_spki (cert: Bertie.Tls13utils.t_Bytes) (offset: usize) = Rust_primitives.Hax.Control_flow_monad.Mexception.run (match - check_tag cert offset 48uy <: Core.Result.t_Result Prims.unit u8 @@ -527,30 +534,98 @@ (Core.Result.t_Result (Bertie.Tls13crypto.t_SignatureScheme & t_CertificateKey) u8) (Core.Result.t_Result (Bertie.Tls13crypto.t_SignatureScheme & t_CertificateKey) u8)) @@ -280,11 +279,10 @@ diff -ruN extraction-lax/Bertie.Tls13cert.fst extraction-panic-free/Bertie.Tls13 read_spki cert offset | Core.Result.Result_Err err -> Core.Result.Result_Err err -@@ -588,79 +663,6 @@ - Core.Result.Result_Err err +@@ -589,79 +664,6 @@ <: Core.Result.t_Result (Bertie.Tls13crypto.t_SignatureScheme & t_CertificateKey) u8 -- + -let ecdsa_public_key (cert: Bertie.Tls13utils.t_Bytes) (indices: t_CertificateKey) = - let CertificateKey offset len:t_CertificateKey = indices in - match check_tag cert offset 4uy with @@ -357,12 +355,13 @@ diff -ruN extraction-lax/Bertie.Tls13cert.fst extraction-panic-free/Bertie.Tls13 - Core.Result.Result_Err err <: Core.Result.t_Result Bertie.Tls13utils.t_Bytes u8) - | Core.Result.Result_Err err -> - Core.Result.Result_Err err <: Core.Result.t_Result Bertie.Tls13utils.t_Bytes u8 - +- let rsa_public_key (cert: Bertie.Tls13utils.t_Bytes) (indices: t_CertificateKey) = let CertificateKey offset v__len:t_CertificateKey = indices in + match check_tag cert offset 48uy with diff -ruN extraction-lax/Bertie.Tls13cert.fsti extraction-panic-free/Bertie.Tls13cert.fsti ---- extraction-lax/Bertie.Tls13cert.fsti 2024-04-05 08:35:03 -+++ extraction-panic-free/Bertie.Tls13cert.fsti 2024-04-05 08:35:03 +--- extraction-lax/Bertie.Tls13cert.fsti 2024-04-10 09:10:50.167959389 +0200 ++++ extraction-panic-free/Bertie.Tls13cert.fsti 2024-04-10 09:10:50.183950645 +0200 @@ -37,16 +37,30 @@ -> Prims.Pure Bertie.Tls13utils.t_Bytes Prims.l_True (fun _ -> Prims.l_True) @@ -371,13 +370,13 @@ diff -ruN extraction-lax/Bertie.Tls13cert.fsti extraction-panic-free/Bertie.Tls1 + : Prims.Pure (Core.Result.t_Result Prims.unit u8) + (v offset < Seq.length b._0) + (fun _ -> Prims.l_True) - ++ +val ecdsa_public_key (cert: Bertie.Tls13utils.t_Bytes) (indices: t_CertificateKey) + : Prims.Pure (Core.Result.t_Result Bertie.Tls13utils.t_Bytes u8) + (v indices._0 < Seq.length cert._0 /\ + v indices._0 < pow2 31 - 1 /\ v indices._1 > 0) + (fun _ -> Prims.l_True) -+ + val length_length (b: Bertie.Tls13utils.t_Bytes) (offset: usize) - : Prims.Pure usize Prims.l_True (fun _ -> Prims.l_True) + : Prims.Pure usize @@ -445,8 +444,8 @@ diff -ruN extraction-lax/Bertie.Tls13cert.fsti extraction-panic-free/Bertie.Tls1 (fun _ -> Prims.l_True) diff -ruN extraction-lax/Bertie.Tls13crypto.fsti extraction-panic-free/Bertie.Tls13crypto.fsti ---- extraction-lax/Bertie.Tls13crypto.fsti 2024-04-05 08:35:03 -+++ extraction-panic-free/Bertie.Tls13crypto.fsti 2024-04-05 08:35:03 +--- extraction-lax/Bertie.Tls13crypto.fsti 2024-04-10 09:10:50.159963761 +0200 ++++ extraction-panic-free/Bertie.Tls13crypto.fsti 2024-04-10 09:10:50.199941901 +0200 @@ -54,10 +54,12 @@ *) @@ -473,7 +472,7 @@ diff -ruN extraction-lax/Bertie.Tls13crypto.fsti extraction-panic-free/Bertie.Tl val hkdf_expand (alg: t_HashAlgorithm) (prk info: Bertie.Tls13utils.t_Bytes) (len: usize) : Prims.Pure (Core.Result.t_Result Bertie.Tls13utils.t_Bytes u8) -@@ -314,21 +318,32 @@ +@@ -314,20 +318,31 @@ val impl__Algorithms__ciphersuite (self: t_Algorithms) : Prims.Pure (Core.Result.t_Result Bertie.Tls13utils.t_Bytes u8) Prims.l_True @@ -488,8 +487,8 @@ diff -ruN extraction-lax/Bertie.Tls13crypto.fsti extraction-panic-free/Bertie.Tl + (fun res -> match res with + | Core.Result.Result_Ok len -> v len < 256 /\ Seq.length bytes >= v len + | _ -> True) - + + val impl__Algorithms__signature_algorithm (self: t_Algorithms) : Prims.Pure (Core.Result.t_Result Bertie.Tls13utils.t_Bytes u8) Prims.l_True @@ -505,11 +504,10 @@ diff -ruN extraction-lax/Bertie.Tls13crypto.fsti extraction-panic-free/Bertie.Tl + (fun res -> match res with + | Core.Result.Result_Ok b -> Seq.length b._0 == 2 + | _ -> True) - + + val sign (#impl_916461611_: Type) - {| i1: Rand_core.t_CryptoRng impl_916461611_ |} @@ -372,7 +387,9 @@ (impl_916461611_ & Core.Result.t_Result (Bertie.Tls13utils.t_Bytes & Bertie.Tls13utils.t_Bytes) u8) @@ -557,78 +555,9 @@ diff -ruN extraction-lax/Bertie.Tls13crypto.fsti extraction-panic-free/Bertie.Tl } val impl__AeadKeyIV__new (key: t_AeadKey) (iv: Bertie.Tls13utils.t_Bytes) -diff -ruN extraction-lax/Bertie.Tls13formats.Handshake_data.fst extraction-panic-free/Bertie.Tls13formats.Handshake_data.fst ---- extraction-lax/Bertie.Tls13formats.Handshake_data.fst 2024-04-05 08:35:03 -+++ extraction-panic-free/Bertie.Tls13formats.Handshake_data.fst 2024-04-05 08:35:03 -@@ -82,7 +82,7 @@ - <: - t_Slice u8) - with -- | Core.Result.Result_Ok len -> -+ | Core.Result.Result_Ok len -> ( - let message:Bertie.Tls13utils.t_Bytes = - Bertie.Tls13utils.impl__Bytes__slice_range self._0 - ({ Core.Ops.Range.f_start = sz 0; Core.Ops.Range.f_end = sz 4 +! len <: usize } -@@ -103,7 +103,7 @@ - <: - (t_HandshakeData & t_HandshakeData)) - <: -- Core.Result.t_Result (t_HandshakeData & t_HandshakeData) u8 -+ Core.Result.t_Result (t_HandshakeData & t_HandshakeData) u8) - | Core.Result.Result_Err err -> - Core.Result.Result_Err err <: Core.Result.t_Result (t_HandshakeData & t_HandshakeData) u8 - -@@ -154,7 +154,6 @@ - | Core.Result.Result_Err err -> - Core.Result.Result_Err err <: Core.Result.t_Result t_HandshakeData u8 - --let impl__HandshakeData__to_bytes (self: t_HandshakeData) = Core.Clone.f_clone self._0 - - let impl__HandshakeData__to_four (self: t_HandshakeData) = - match impl__HandshakeData__next_handshake_message self with -@@ -244,12 +243,13 @@ - Core.Result.t_Result t_HandshakeData u8 - | Core.Result.Result_Err err -> - Core.Result.Result_Err err <: Core.Result.t_Result t_HandshakeData u8 -- -+ - let rec impl__HandshakeData__find_handshake_message - (self: t_HandshakeData) - (handshake_type: t_HandshakeType) - (start: usize) - = -+ assume (v start + 4 < max_usize); - if (impl__HandshakeData__len self <: usize) <. (start +! sz 4 <: usize) - then false - else -diff -ruN extraction-lax/Bertie.Tls13formats.Handshake_data.fsti extraction-panic-free/Bertie.Tls13formats.Handshake_data.fsti ---- extraction-lax/Bertie.Tls13formats.Handshake_data.fsti 2024-04-05 08:35:03 -+++ extraction-panic-free/Bertie.Tls13formats.Handshake_data.fsti 2024-04-05 08:35:03 -@@ -57,10 +57,9 @@ - val impl__HandshakeData__as_handshake_message - (self: t_HandshakeData) - (expected_type: t_HandshakeType) -- : Prims.Pure (Core.Result.t_Result t_HandshakeData u8) Prims.l_True (fun _ -> Prims.l_True) -+ : Prims.Pure (Core.Result.t_Result t_HandshakeData u8) Prims.l_True (fun _ -> Prims.l_True) - --val impl__HandshakeData__to_bytes (self: t_HandshakeData) -- : Prims.Pure Bertie.Tls13utils.t_Bytes Prims.l_True (fun _ -> Prims.l_True) -+let impl__HandshakeData__to_bytes (self: t_HandshakeData) = self._0 - - val impl__HandshakeData__to_four (self: t_HandshakeData) - : Prims.Pure -@@ -92,4 +91,7 @@ - (self: t_HandshakeData) - (handshake_type: t_HandshakeType) - (start: usize) -- : Prims.Pure bool Prims.l_True (fun _ -> Prims.l_True) -+ : Prims.Pure bool -+ (v start <= v (impl__HandshakeData__len self)) -+ (fun _ -> Prims.l_True) -+ (decreases (v (impl__HandshakeData__len self) - v start)) diff -ruN extraction-lax/Bertie.Tls13formats.fst extraction-panic-free/Bertie.Tls13formats.fst ---- extraction-lax/Bertie.Tls13formats.fst 2024-04-05 08:35:03 -+++ extraction-panic-free/Bertie.Tls13formats.fst 2024-04-05 08:35:03 +--- extraction-lax/Bertie.Tls13formats.fst 2024-04-10 09:10:50.149969226 +0200 ++++ extraction-panic-free/Bertie.Tls13formats.fst 2024-04-10 09:10:50.192945727 +0200 @@ -47,6 +47,8 @@ | ContentType_Handshake -> discriminant_ContentType_Handshake | ContentType_ApplicationData -> discriminant_ContentType_ApplicationData @@ -700,14 +629,14 @@ diff -ruN extraction-lax/Bertie.Tls13formats.fst extraction-panic-free/Bertie.Tl | Core.Result.Result_Ok hoist21 -> (match - Bertie.Tls13utils.check_eq_slice (Bertie.Tls13utils.impl__Bytes__as_raw hoist21 -+ Bertie.Tls13utils.check_eq_with_slice (Bertie.Tls13utils.impl__Bytes__as_raw hoist21 - <: - t_Slice u8) +- <: +- t_Slice u8) - (b.[ { Core.Ops.Range.f_start = sz 0; Core.Ops.Range.f_end = sz 2 } - <: - Core.Ops.Range.t_Range usize ] -- <: -- t_Slice u8) ++ Bertie.Tls13utils.check_eq_with_slice (Bertie.Tls13utils.impl__Bytes__as_raw hoist21 + <: + t_Slice u8) + b + (sz 0) + (sz 2) @@ -785,22 +714,7 @@ diff -ruN extraction-lax/Bertie.Tls13formats.fst extraction-panic-free/Bertie.Tl + Core.Ops.Range.t_Range usize ] <: - Core.Ops.Range.t_Range usize ] -+ t_Slice u8) -+ with -+ | Core.Result.Result_Ok ok -> -+ Core.Ops.Control_flow.ControlFlow_Continue out -+ <: -+ Core.Ops.Control_flow.t_ControlFlow -+ (Core.Result.t_Result (usize & Core.Option.t_Option Bertie.Tls13utils.t_Bytes) -+ u8) (Core.Option.t_Option Bertie.Tls13utils.t_Bytes) -+ | Core.Result.Result_Err err -> -+ let! _:Prims.unit = -+ Core.Ops.Control_flow.ControlFlow_Break -+ (Core.Result.Result_Err err -+ <: -+ Core.Result.t_Result (usize & Core.Option.t_Option Bertie.Tls13utils.t_Bytes) -+ u8) - <: +- <: - t_Slice u8) - with - | Core.Result.Result_Ok ok -> @@ -816,10 +730,9 @@ diff -ruN extraction-lax/Bertie.Tls13formats.fst extraction-panic-free/Bertie.Tl - <: - Core.Result.t_Result (usize & Core.Option.t_Option Bertie.Tls13utils.t_Bytes) u8 - ) -+ Core.Ops.Control_flow.t_ControlFlow -+ (Core.Result.t_Result (usize & Core.Option.t_Option Bertie.Tls13utils.t_Bytes) -+ u8) Prims.unit -+ in ++ t_Slice u8) ++ with ++ | Core.Result.Result_Ok ok -> + Core.Ops.Control_flow.ControlFlow_Continue out <: Core.Ops.Control_flow.t_ControlFlow @@ -838,35 +751,14 @@ diff -ruN extraction-lax/Bertie.Tls13formats.fst extraction-panic-free/Bertie.Tl - Core.Ops.Range.f_start = sz 4; - Core.Ops.Range.f_end = sz 4 +! len <: usize - } -+ u8) (Core.Option.t_Option Bertie.Tls13utils.t_Bytes)) -+ | 0uy, 51uy -> -+ (match -+ check_server_key_share algs -+ (b.[ { -+ Core.Ops.Range.f_start = sz 4; -+ Core.Ops.Range.f_end = sz 4 +! len <: usize -+ } -+ <: -+ Core.Ops.Range.t_Range usize ] - <: -- Core.Ops.Range.t_Range usize ] -+ t_Slice u8) -+ with -+ | Core.Result.Result_Ok gx -> -+ Core.Ops.Control_flow.ControlFlow_Continue -+ (Core.Option.Option_Some gx <: Core.Option.t_Option Bertie.Tls13utils.t_Bytes) -+ <: -+ Core.Ops.Control_flow.t_ControlFlow -+ (Core.Result.t_Result (usize & Core.Option.t_Option Bertie.Tls13utils.t_Bytes) + u8) (Core.Option.t_Option Bertie.Tls13utils.t_Bytes) + | Core.Result.Result_Err err -> + let! _:Prims.unit = + Core.Ops.Control_flow.ControlFlow_Break + (Core.Result.Result_Err err -+ <: -+ Core.Result.t_Result (usize & Core.Option.t_Option Bertie.Tls13utils.t_Bytes) -+ u8) - <: + <: +- Core.Ops.Range.t_Range usize ] +- <: - t_Slice u8) - with - | Core.Result.Result_Ok gx -> @@ -880,7 +772,9 @@ diff -ruN extraction-lax/Bertie.Tls13formats.fst extraction-panic-free/Bertie.Tl - let! _:Prims.unit = - Core.Ops.Control_flow.ControlFlow_Break - (Core.Result.Result_Err err -- <: ++ Core.Result.t_Result (usize & Core.Option.t_Option Bertie.Tls13utils.t_Bytes) ++ u8) + <: - Core.Result.t_Result (usize & Core.Option.t_Option Bertie.Tls13utils.t_Bytes) u8 - ) + Core.Ops.Control_flow.t_ControlFlow @@ -906,9 +800,9 @@ diff -ruN extraction-lax/Bertie.Tls13formats.fst extraction-panic-free/Bertie.Tl - Core.Ops.Range.f_end = sz 4 +! len <: usize - } + u8) (Core.Option.t_Option Bertie.Tls13utils.t_Bytes)) -+ | 0uy, 41uy -> ++ | 0uy, 51uy -> + (match -+ check_server_psk_shared_key algs ++ check_server_key_share algs + (b.[ { + Core.Ops.Range.f_start = sz 4; + Core.Ops.Range.f_end = sz 4 +! len <: usize @@ -919,8 +813,9 @@ diff -ruN extraction-lax/Bertie.Tls13formats.fst extraction-panic-free/Bertie.Tl - Core.Ops.Range.t_Range usize ] + t_Slice u8) + with -+ | Core.Result.Result_Ok ok -> -+ Core.Ops.Control_flow.ControlFlow_Continue out ++ | Core.Result.Result_Ok gx -> ++ Core.Ops.Control_flow.ControlFlow_Continue ++ (Core.Option.Option_Some gx <: Core.Option.t_Option Bertie.Tls13utils.t_Bytes) + <: + Core.Ops.Control_flow.t_ControlFlow + (Core.Result.t_Result (usize & Core.Option.t_Option Bertie.Tls13utils.t_Bytes) @@ -945,7 +840,41 @@ diff -ruN extraction-lax/Bertie.Tls13formats.fst extraction-panic-free/Bertie.Tl - let! _:Prims.unit = - Core.Ops.Control_flow.ControlFlow_Break - (Core.Result.Result_Err err -- <: ++ Core.Ops.Control_flow.t_ControlFlow ++ (Core.Result.t_Result (usize & Core.Option.t_Option Bertie.Tls13utils.t_Bytes) ++ u8) Prims.unit ++ in ++ Core.Ops.Control_flow.ControlFlow_Continue out ++ <: ++ Core.Ops.Control_flow.t_ControlFlow ++ (Core.Result.t_Result (usize & Core.Option.t_Option Bertie.Tls13utils.t_Bytes) ++ u8) (Core.Option.t_Option Bertie.Tls13utils.t_Bytes)) ++ | 0uy, 41uy -> ++ (match ++ check_server_psk_shared_key algs ++ (b.[ { ++ Core.Ops.Range.f_start = sz 4; ++ Core.Ops.Range.f_end = sz 4 +! len <: usize ++ } ++ <: ++ Core.Ops.Range.t_Range usize ] ++ <: ++ t_Slice u8) ++ with ++ | Core.Result.Result_Ok ok -> ++ Core.Ops.Control_flow.ControlFlow_Continue out ++ <: ++ Core.Ops.Control_flow.t_ControlFlow ++ (Core.Result.t_Result (usize & Core.Option.t_Option Bertie.Tls13utils.t_Bytes) ++ u8) (Core.Option.t_Option Bertie.Tls13utils.t_Bytes) ++ | Core.Result.Result_Err err -> ++ let! _:Prims.unit = ++ Core.Ops.Control_flow.ControlFlow_Break ++ (Core.Result.Result_Err err ++ <: ++ Core.Result.t_Result (usize & Core.Option.t_Option Bertie.Tls13utils.t_Bytes) ++ u8) + <: - Core.Result.t_Result (usize & Core.Option.t_Option Bertie.Tls13utils.t_Bytes) u8 - ) + Core.Ops.Control_flow.t_ControlFlow @@ -1124,8 +1053,7 @@ diff -ruN extraction-lax/Bertie.Tls13formats.fst extraction-panic-free/Bertie.Tl - (match ecdsa_signature cv with - | Core.Result.Result_Ok ok -> - Core.Ops.Control_flow.ControlFlow_Continue ok -+ Bertie.Tls13formats.Handshake_data.impl__HandshakeData__from_bytes (Bertie.Tls13formats.Handshake_data.HandshakeType_CertificateVerify - <: +- <: - Core.Ops.Control_flow.t_ControlFlow - (Core.Result.t_Result Bertie.Tls13formats.Handshake_data.t_HandshakeData u8) - Bertie.Tls13utils.t_Bytes @@ -1141,7 +1069,8 @@ diff -ruN extraction-lax/Bertie.Tls13formats.fst extraction-panic-free/Bertie.Tl - | Bertie.Tls13crypto.SignatureScheme_ED25519 -> - Core.Ops.Control_flow.ControlFlow_Continue - (Rust_primitives.Hax.never_to_any (Core.Panicking.panic "not implemented" -- <: ++ Bertie.Tls13formats.Handshake_data.impl__HandshakeData__from_bytes (Bertie.Tls13formats.Handshake_data.HandshakeType_CertificateVerify + <: - Rust_primitives.Hax.t_Never)) - <: - Core.Ops.Control_flow.t_ControlFlow @@ -1230,60 +1159,7 @@ diff -ruN extraction-lax/Bertie.Tls13formats.fst extraction-panic-free/Bertie.Tl - let len:usize = - len +! - (Bertie.Tls13utils.impl__Bytes__len legacy_session_id -+ let trunc_len:usize = sz 0 in -+ (match Bertie.Tls13utils.encode_length_u16 extensions with -+ | Core.Result.Result_Ok encoded_extensions -> -+ let len:usize = -+ (Bertie.Tls13utils.impl__Bytes__len version <: usize) +! -+ (Bertie.Tls13utils.impl__Bytes__len client_random <: usize) -+ in -+ let len:usize = -+ len +! -+ (Bertie.Tls13utils.impl__Bytes__len legacy_session_id <: usize -+ ) -+ in -+ let len:usize = -+ len +! -+ (Bertie.Tls13utils.impl__Bytes__len cipher_suites <: usize) -+ in -+ let len:usize = -+ len +! -+ (Bertie.Tls13utils.impl__Bytes__len compression_methods -+ <: -+ usize) -+ in -+ let len:usize = -+ len +! -+ (Bertie.Tls13utils.impl__Bytes__len encoded_extensions -+ <: -+ usize) -+ in -+ let out:Bertie.Tls13utils.t_Bytes = -+ Bertie.Tls13utils.impl__Bytes__new_alloc len -+ in -+ let out:Bertie.Tls13utils.t_Bytes = -+ Bertie.Tls13utils.impl__Bytes__append out version -+ in -+ let out:Bertie.Tls13utils.t_Bytes = -+ Bertie.Tls13utils.impl__Bytes__append out client_random -+ in -+ let out:Bertie.Tls13utils.t_Bytes = -+ Bertie.Tls13utils.impl__Bytes__append out legacy_session_id -+ in -+ let out:Bertie.Tls13utils.t_Bytes = -+ Bertie.Tls13utils.impl__Bytes__append out cipher_suites -+ in -+ let out:Bertie.Tls13utils.t_Bytes = -+ Bertie.Tls13utils.impl__Bytes__append out compression_methods -+ in -+ let out:Bertie.Tls13utils.t_Bytes = -+ Bertie.Tls13utils.impl__Bytes__append out encoded_extensions -+ in -+ let handshake_bytes:Bertie.Tls13utils.t_Bytes = out in -+ (match -+ Bertie.Tls13formats.Handshake_data.impl__HandshakeData__from_bytes -+ (Bertie.Tls13formats.Handshake_data.HandshakeType_ClientHello - <: +- <: - usize) - in - let len:usize = @@ -1347,7 +1223,60 @@ diff -ruN extraction-lax/Bertie.Tls13formats.fst extraction-panic-free/Bertie.Tl - usize) u8 - | Core.Result.Result_Err err -> - Core.Result.Result_Err err -- <: ++ let trunc_len:usize = sz 0 in ++ (match Bertie.Tls13utils.encode_length_u16 extensions with ++ | Core.Result.Result_Ok encoded_extensions -> ++ let len:usize = ++ (Bertie.Tls13utils.impl__Bytes__len version <: usize) +! ++ (Bertie.Tls13utils.impl__Bytes__len client_random <: usize) ++ in ++ let len:usize = ++ len +! ++ (Bertie.Tls13utils.impl__Bytes__len legacy_session_id <: usize ++ ) ++ in ++ let len:usize = ++ len +! ++ (Bertie.Tls13utils.impl__Bytes__len cipher_suites <: usize) ++ in ++ let len:usize = ++ len +! ++ (Bertie.Tls13utils.impl__Bytes__len compression_methods ++ <: ++ usize) ++ in ++ let len:usize = ++ len +! ++ (Bertie.Tls13utils.impl__Bytes__len encoded_extensions ++ <: ++ usize) ++ in ++ let out:Bertie.Tls13utils.t_Bytes = ++ Bertie.Tls13utils.impl__Bytes__new_alloc len ++ in ++ let out:Bertie.Tls13utils.t_Bytes = ++ Bertie.Tls13utils.impl__Bytes__append out version ++ in ++ let out:Bertie.Tls13utils.t_Bytes = ++ Bertie.Tls13utils.impl__Bytes__append out client_random ++ in ++ let out:Bertie.Tls13utils.t_Bytes = ++ Bertie.Tls13utils.impl__Bytes__append out legacy_session_id ++ in ++ let out:Bertie.Tls13utils.t_Bytes = ++ Bertie.Tls13utils.impl__Bytes__append out cipher_suites ++ in ++ let out:Bertie.Tls13utils.t_Bytes = ++ Bertie.Tls13utils.impl__Bytes__append out compression_methods ++ in ++ let out:Bertie.Tls13utils.t_Bytes = ++ Bertie.Tls13utils.impl__Bytes__append out encoded_extensions ++ in ++ let handshake_bytes:Bertie.Tls13utils.t_Bytes = out in ++ (match ++ Bertie.Tls13formats.Handshake_data.impl__HandshakeData__from_bytes ++ (Bertie.Tls13formats.Handshake_data.HandshakeType_ClientHello + <: - Core.Result.t_Result - (Bertie.Tls13formats.Handshake_data.t_HandshakeData & - usize) u8) @@ -1367,7 +1296,7 @@ diff -ruN extraction-lax/Bertie.Tls13formats.fst extraction-panic-free/Bertie.Tl | Core.Result.Result_Err err -> Core.Result.Result_Err err <: -@@ -1570,196 +1492,207 @@ +@@ -1570,195 +1492,206 @@ Core.Result.Result_Err err <: Core.Result.t_Result Bertie.Tls13utils.t_Bytes u8 let check_extension (algs: Bertie.Tls13crypto.t_Algorithms) (bytes: t_Slice u8) = @@ -1460,8 +1389,7 @@ diff -ruN extraction-lax/Bertie.Tls13formats.fst extraction-panic-free/Bertie.Tl } <: - Core.Ops.Range.t_Range usize ] -+ t_Extensions) - <: +- <: - t_Slice u8) - with - | Core.Result.Result_Ok hoist152 -> @@ -1481,7 +1409,8 @@ diff -ruN extraction-lax/Bertie.Tls13formats.fst extraction-panic-free/Bertie.Tl - = - Core.Option.Option_None <: Core.Option.t_Option Bertie.Tls13utils.t_Bytes - } -- <: ++ t_Extensions) + <: - t_Extensions) + (usize & t_Extensions)) <: @@ -1666,8 +1595,7 @@ diff -ruN extraction-lax/Bertie.Tls13formats.fst extraction-panic-free/Bertie.Tl } <: - Core.Ops.Range.t_Range usize ] -+ t_Extensions) - <: +- <: - t_Slice u8) - with - | Core.Result.Result_Ok gx -> @@ -1685,7 +1613,8 @@ diff -ruN extraction-lax/Bertie.Tls13formats.fst extraction-panic-free/Bertie.Tl - = - Core.Option.Option_None <: Core.Option.t_Option Bertie.Tls13utils.t_Bytes - } -- <: ++ t_Extensions) + <: - t_Extensions) + (usize & t_Extensions)) <: @@ -1744,11 +1673,10 @@ diff -ruN extraction-lax/Bertie.Tls13formats.fst extraction-panic-free/Bertie.Tl + Core.Result.t_Result (usize & t_Extensions) u8) + | Core.Result.Result_Err err -> + Core.Result.Result_Err err <: Core.Result.t_Result (usize & t_Extensions) u8 - + + let finished (vd: Bertie.Tls13utils.t_Bytes) = Bertie.Tls13formats.Handshake_data.impl__HandshakeData__from_bytes (Bertie.Tls13formats.Handshake_data.HandshakeType_Finished - <: @@ -1815,15 +1748,14 @@ Bertie.Tls13crypto.impl__Algorithms__signature algs in @@ -1809,7 +1737,7 @@ diff -ruN extraction-lax/Bertie.Tls13formats.fst extraction-panic-free/Bertie.Tl Core.Ops.Range.f_end = Bertie.Tls13utils.impl__Bytes__len sc <: usize } <: -@@ -2022,199 +1954,159 @@ +@@ -2022,197 +1954,157 @@ (algs: Bertie.Tls13crypto.t_Algorithms) (server_hello: Bertie.Tls13formats.Handshake_data.t_HandshakeData) = @@ -1853,6 +1781,15 @@ diff -ruN extraction-lax/Bertie.Tls13formats.fst extraction-panic-free/Bertie.Tl - match protocol_version_alert () with - | Core.Result.Result_Ok ok -> - Core.Ops.Control_flow.ControlFlow_Continue ok +- <: +- Core.Ops.Control_flow.t_ControlFlow +- (Core.Result.t_Result (Bertie.Tls13utils.t_Bytes & Bertie.Tls13utils.t_Bytes) u8 +- ) Prims.unit +- | Core.Result.Result_Err err -> +- Core.Ops.Control_flow.ControlFlow_Break +- (Core.Result.Result_Err err +- <: +- Core.Result.t_Result (Bertie.Tls13utils.t_Bytes & Bertie.Tls13utils.t_Bytes) u8) + Bertie.Tls13formats.Handshake_data.t_HandshakeType) + with + | Core.Result.Result_Ok (Bertie.Tls13formats.Handshake_data.HandshakeData server_hello) -> @@ -1868,15 +1805,6 @@ diff -ruN extraction-lax/Bertie.Tls13formats.fst extraction-panic-free/Bertie.Tl - Core.Ops.Control_flow.t_ControlFlow - (Core.Result.t_Result (Bertie.Tls13utils.t_Bytes & Bertie.Tls13utils.t_Bytes) u8 - ) Prims.unit -- | Core.Result.Result_Err err -> -- Core.Ops.Control_flow.ControlFlow_Break -- (Core.Result.Result_Err err -- <: -- Core.Result.t_Result (Bertie.Tls13utils.t_Bytes & Bertie.Tls13utils.t_Bytes) u8) -- <: -- Core.Ops.Control_flow.t_ControlFlow -- (Core.Result.t_Result (Bertie.Tls13utils.t_Bytes & Bertie.Tls13utils.t_Bytes) u8 -- ) Prims.unit - in + t_Slice u8) + (Bertie.Tls13utils.impl__Bytes__as_raw server_hello <: t_Slice u8) @@ -1898,26 +1826,19 @@ diff -ruN extraction-lax/Bertie.Tls13formats.fst extraction-panic-free/Bertie.Tl - let next:usize = next +! sz 32 in (match - Bertie.Tls13utils.length_u8_encoded (server_hello.[ { -+ Bertie.Tls13utils.check ((Bertie.Tls13utils.impl__Bytes__len server_hello <: usize) >=. -+ (next +! sz 32 <: usize) -+ <: -+ bool) -+ with -+ | Core.Result.Result_Ok _ -> -+ let srand:Bertie.Tls13utils.t_Bytes = -+ Bertie.Tls13utils.impl__Bytes__slice_range server_hello -+ ({ - Core.Ops.Range.f_start = next; +- Core.Ops.Range.f_start = next; - Core.Ops.Range.f_end - = - Bertie.Tls13utils.impl__Bytes__len server_hello <: usize -+ Core.Ops.Range.f_end = next +! sz 32 <: usize - } - <: +- } +- <: - Core.Ops.Range.t_Range usize ] -- <: ++ Bertie.Tls13utils.check ((Bertie.Tls13utils.impl__Bytes__len server_hello <: usize) >=. ++ (next +! sz 32 <: usize) + <: - t_Slice u8) -- with ++ bool) + with - | Core.Result.Result_Ok sidlen -> - let next:usize = (next +! sz 1 <: usize) +! sidlen in - let! _:Prims.unit = @@ -1957,8 +1878,7 @@ diff -ruN extraction-lax/Bertie.Tls13formats.fst extraction-panic-free/Bertie.Tl - Core.Ops.Control_flow.t_ControlFlow - (Core.Result.t_Result - (Bertie.Tls13utils.t_Bytes & Bertie.Tls13utils.t_Bytes) u8) Prims.unit -+ Core.Ops.Range.t_Range usize) - in +- in - let next:usize = next +! sz 2 in - let! _:Prims.unit = - match @@ -1970,20 +1890,9 @@ diff -ruN extraction-lax/Bertie.Tls13formats.fst extraction-panic-free/Bertie.Tl - } - <: - Core.Ops.Range.t_Range usize) -+ let next:usize = next +! sz 32 in -+ (match -+ Bertie.Tls13utils.length_u8_encoded (server_hello.[ { -+ Core.Ops.Range.f_start = next; -+ Core.Ops.Range.f_end -+ = -+ Bertie.Tls13utils.impl__Bytes__len server_hello <: usize -+ } -+ <: -+ Core.Ops.Range.t_Range usize ] - <: +- <: - Bertie.Tls13utils.t_Bytes) -+ t_Slice u8) - with +- with - | Core.Result.Result_Ok _ -> - Core.Ops.Control_flow.ControlFlow_Continue (() <: Prims.unit) - <: @@ -2004,11 +1913,19 @@ diff -ruN extraction-lax/Bertie.Tls13formats.fst extraction-panic-free/Bertie.Tl - <: - Core.Result.t_Result (Bertie.Tls13utils.t_Bytes & Bertie.Tls13utils.t_Bytes) - u8) -- <: ++ | Core.Result.Result_Ok _ -> ++ let srand:Bertie.Tls13utils.t_Bytes = ++ Bertie.Tls13utils.impl__Bytes__slice_range server_hello ++ ({ ++ Core.Ops.Range.f_start = next; ++ Core.Ops.Range.f_end = next +! sz 32 <: usize ++ } + <: - Core.Ops.Control_flow.t_ControlFlow - (Core.Result.t_Result - (Bertie.Tls13utils.t_Bytes & Bertie.Tls13utils.t_Bytes) u8) Prims.unit -- in ++ Core.Ops.Range.t_Range usize) + in - Core.Ops.Control_flow.ControlFlow_Continue - (let next:usize = next +! sz 1 in - match @@ -2022,9 +1939,20 @@ diff -ruN extraction-lax/Bertie.Tls13formats.fst extraction-panic-free/Bertie.Tl - } - <: - Core.Ops.Range.t_Range usize) -- <: ++ let next:usize = next +! sz 32 in ++ (match ++ Bertie.Tls13utils.length_u8_encoded (server_hello.[ { ++ Core.Ops.Range.f_start = next; ++ Core.Ops.Range.f_end ++ = ++ Bertie.Tls13utils.impl__Bytes__len server_hello <: usize ++ } ++ <: ++ Core.Ops.Range.t_Range usize ] + <: - Bertie.Tls13utils.t_Bytes) -- with ++ t_Slice u8) + with - | Core.Result.Result_Ok _ -> - let next:usize = next +! sz 2 in + | Core.Result.Result_Ok sidlen -> @@ -2060,6 +1988,11 @@ diff -ruN extraction-lax/Bertie.Tls13formats.fst extraction-panic-free/Bertie.Tl - | Core.Option.Option_Some gy -> - Core.Result.Result_Ok - (srand, gy <: (Bertie.Tls13utils.t_Bytes & Bertie.Tls13utils.t_Bytes)) +- <: +- Core.Result.t_Result +- (Bertie.Tls13utils.t_Bytes & Bertie.Tls13utils.t_Bytes) u8 +- | _ -> +- Core.Result.Result_Err Bertie.Tls13utils.v_MISSING_KEY_SHARE + | Core.Result.Result_Ok _ -> + let next:usize = next +! sz 2 in + (match @@ -2139,15 +2072,8 @@ diff -ruN extraction-lax/Bertie.Tls13formats.fst extraction-panic-free/Bertie.Tl + Core.Result.Result_Err err <: Core.Result.t_Result -- (Bertie.Tls13utils.t_Bytes & Bertie.Tls13utils.t_Bytes) u8 -- | _ -> -- Core.Result.Result_Err Bertie.Tls13utils.v_MISSING_KEY_SHARE -- <: -- Core.Result.t_Result (Bertie.Tls13utils.t_Bytes & Bertie.Tls13utils.t_Bytes) u8) - | Core.Result.Result_Err err -> - Core.Result.Result_Err err -@@ -2225,38 +2117,24 @@ +@@ -2225,37 +2117,23 @@ Core.Result.Result_Err err <: Core.Result.t_Result (Bertie.Tls13utils.t_Bytes & Bertie.Tls13utils.t_Bytes) u8) @@ -2192,11 +2118,10 @@ diff -ruN extraction-lax/Bertie.Tls13formats.fst extraction-panic-free/Bertie.Tl + Core.Result.Result_Err err + <: + Core.Result.t_Result (Bertie.Tls13utils.t_Bytes & Bertie.Tls13utils.t_Bytes) u8 - + + 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 @@ -2302,155 +2180,86 @@ Core.Result.t_Result Bertie.Tls13formats.Handshake_data.t_HandshakeData u8 @@ -2321,6 +2246,11 @@ diff -ruN extraction-lax/Bertie.Tls13formats.fst extraction-panic-free/Bertie.Tl - with - | Core.Result.Result_Ok sh -> - Core.Result.Result_Ok sh +- <: +- Core.Result.t_Result Bertie.Tls13formats.Handshake_data.t_HandshakeData +- u8 +- | Core.Result.Result_Err err -> +- Core.Result.Result_Err err + let out:Bertie.Tls13utils.t_Bytes = + Bertie.Tls13utils.impl__Bytes__new_alloc len + in @@ -2346,11 +2276,6 @@ diff -ruN extraction-lax/Bertie.Tls13formats.fst extraction-panic-free/Bertie.Tl + Bertie.Tls13formats.Handshake_data.impl__HandshakeData__from_bytes (Bertie.Tls13formats.Handshake_data.HandshakeType_ServerHello <: - Core.Result.t_Result Bertie.Tls13formats.Handshake_data.t_HandshakeData -- u8 -- | Core.Result.Result_Err err -> -- Core.Result.Result_Err err -- <: -- Core.Result.t_Result Bertie.Tls13formats.Handshake_data.t_HandshakeData - u8) + Bertie.Tls13formats.Handshake_data.t_HandshakeType) + out @@ -2544,19 +2469,7 @@ diff -ruN extraction-lax/Bertie.Tls13formats.fst extraction-panic-free/Bertie.Tl - match invalid_compression_list () with - | Core.Result.Result_Ok ok -> - Core.Ops.Control_flow.ControlFlow_Continue ok -+ (match -+ match -+ Bertie.Tls13utils.check_eq_with_slice (Bertie.Tls13utils.impl__Bytes__as_raw -+ comp -+ <: -+ t_Slice u8) -+ (Bertie.Tls13utils.impl__Bytes__as_raw ch <: t_Slice u8) -+ next -+ (next +! sz 2 <: usize) -+ with -+ | Core.Result.Result_Ok _ -> -+ Core.Result.Result_Ok (() <: Prims.unit) - <: +- <: - Core.Ops.Control_flow.t_ControlFlow - (Core.Result.t_Result - (Bertie.Tls13utils.t_Bytes & Bertie.Tls13utils.t_Bytes & @@ -2576,7 +2489,19 @@ diff -ruN extraction-lax/Bertie.Tls13formats.fst extraction-panic-free/Bertie.Tl - Core.Option.t_Option Bertie.Tls13utils.t_Bytes & - Core.Option.t_Option Bertie.Tls13utils.t_Bytes & - usize) u8) -- <: ++ (match ++ match ++ Bertie.Tls13utils.check_eq_with_slice (Bertie.Tls13utils.impl__Bytes__as_raw ++ comp ++ <: ++ t_Slice u8) ++ (Bertie.Tls13utils.impl__Bytes__as_raw ch <: t_Slice u8) ++ next ++ (next +! sz 2 <: usize) ++ with ++ | Core.Result.Result_Ok _ -> ++ Core.Result.Result_Ok (() <: Prims.unit) + <: - Core.Ops.Control_flow.t_ControlFlow - (Core.Result.t_Result - (Bertie.Tls13utils.t_Bytes & Bertie.Tls13utils.t_Bytes & @@ -2614,7 +2539,7 @@ diff -ruN extraction-lax/Bertie.Tls13formats.fst extraction-panic-free/Bertie.Tl ({ Core.Ops.Range.f_start = next; Core.Ops.Range.f_end -@@ -2760,158 +2522,195 @@ +@@ -2760,168 +2522,195 @@ <: Bertie.Tls13utils.t_Bytes) with @@ -2940,6 +2865,16 @@ diff -ruN extraction-lax/Bertie.Tls13formats.fst extraction-panic-free/Bertie.Tl - Core.Option.t_Option Bertie.Tls13utils.t_Bytes & - Core.Option.t_Option Bertie.Tls13utils.t_Bytes & - usize)) +- <: +- Core.Result.t_Result +- (Bertie.Tls13utils.t_Bytes & Bertie.Tls13utils.t_Bytes & +- Bertie.Tls13utils.t_Bytes & +- Bertie.Tls13utils.t_Bytes & +- Core.Option.t_Option Bertie.Tls13utils.t_Bytes & +- Core.Option.t_Option Bertie.Tls13utils.t_Bytes & +- usize) u8 +- | _ -> +- Core.Result.Result_Err (Bertie.Tls13utils.parse_failed ()) + Core.Result.t_Result + (Bertie.Tls13utils.t_Bytes & Bertie.Tls13utils.t_Bytes & + Bertie.Tls13utils.t_Bytes & @@ -2952,23 +2887,6 @@ diff -ruN extraction-lax/Bertie.Tls13formats.fst extraction-panic-free/Bertie.Tl <: Core.Result.t_Result (Bertie.Tls13utils.t_Bytes & Bertie.Tls13utils.t_Bytes & -@@ -2919,16 +2718,6 @@ - Bertie.Tls13utils.t_Bytes & - Core.Option.t_Option Bertie.Tls13utils.t_Bytes & - Core.Option.t_Option Bertie.Tls13utils.t_Bytes & -- usize) u8 -- | _ -> -- Core.Result.Result_Err (Bertie.Tls13utils.parse_failed ()) -- <: -- Core.Result.t_Result -- (Bertie.Tls13utils.t_Bytes & Bertie.Tls13utils.t_Bytes & -- Bertie.Tls13utils.t_Bytes & -- Bertie.Tls13utils.t_Bytes & -- Core.Option.t_Option Bertie.Tls13utils.t_Bytes & -- Core.Option.t_Option Bertie.Tls13utils.t_Bytes & - usize) u8) - | Core.Result.Result_Err err -> - Core.Result.Result_Err err @@ -2950,121 +2739,50 @@ Core.Option.t_Option Bertie.Tls13utils.t_Bytes & Core.Option.t_Option Bertie.Tls13utils.t_Bytes & @@ -3121,8 +3039,8 @@ diff -ruN extraction-lax/Bertie.Tls13formats.fst extraction-panic-free/Bertie.Tl + usize) u8 + diff -ruN extraction-lax/Bertie.Tls13formats.fsti extraction-panic-free/Bertie.Tls13formats.fsti ---- extraction-lax/Bertie.Tls13formats.fsti 2024-04-05 08:35:03 -+++ extraction-panic-free/Bertie.Tls13formats.fsti 2024-04-05 08:35:03 +--- extraction-lax/Bertie.Tls13formats.fsti 2024-04-10 09:10:50.156965400 +0200 ++++ extraction-panic-free/Bertie.Tls13formats.fsti 2024-04-10 09:10:50.177953924 +0200 @@ -234,6 +234,8 @@ FStar.Pervasives.assert_norm (Prims.eq2 (List.Tot.length list) 2); Rust_primitives.Hax.array_of_list 2 list @@ -3291,9 +3209,78 @@ diff -ruN extraction-lax/Bertie.Tls13formats.fsti extraction-panic-free/Bertie.T val check_extensions (algs: Bertie.Tls13crypto.t_Algorithms) (b: Bertie.Tls13utils.t_Bytes) : Prims.Pure (Core.Result.t_Result t_Extensions u8) Prims.l_True (fun _ -> Prims.l_True) +diff -ruN extraction-lax/Bertie.Tls13formats.Handshake_data.fst extraction-panic-free/Bertie.Tls13formats.Handshake_data.fst +--- extraction-lax/Bertie.Tls13formats.Handshake_data.fst 2024-04-10 09:10:50.143972505 +0200 ++++ extraction-panic-free/Bertie.Tls13formats.Handshake_data.fst 2024-04-10 09:10:50.188947913 +0200 +@@ -82,7 +82,7 @@ + <: + t_Slice u8) + with +- | Core.Result.Result_Ok len -> ++ | Core.Result.Result_Ok len -> ( + let message:Bertie.Tls13utils.t_Bytes = + Bertie.Tls13utils.impl__Bytes__slice_range self._0 + ({ Core.Ops.Range.f_start = sz 0; Core.Ops.Range.f_end = sz 4 +! len <: usize } +@@ -103,7 +103,7 @@ + <: + (t_HandshakeData & t_HandshakeData)) + <: +- Core.Result.t_Result (t_HandshakeData & t_HandshakeData) u8 ++ Core.Result.t_Result (t_HandshakeData & t_HandshakeData) u8) + | Core.Result.Result_Err err -> + Core.Result.Result_Err err <: Core.Result.t_Result (t_HandshakeData & t_HandshakeData) u8 + +@@ -154,7 +154,6 @@ + | Core.Result.Result_Err err -> + Core.Result.Result_Err err <: Core.Result.t_Result t_HandshakeData u8 + +-let impl__HandshakeData__to_bytes (self: t_HandshakeData) = Core.Clone.f_clone self._0 + + let impl__HandshakeData__to_four (self: t_HandshakeData) = + match impl__HandshakeData__next_handshake_message self with +@@ -244,12 +243,13 @@ + Core.Result.t_Result t_HandshakeData u8 + | Core.Result.Result_Err err -> + Core.Result.Result_Err err <: Core.Result.t_Result t_HandshakeData u8 +- ++ + let rec impl__HandshakeData__find_handshake_message + (self: t_HandshakeData) + (handshake_type: t_HandshakeType) + (start: usize) + = ++ assume (v start + 4 < max_usize); + if (impl__HandshakeData__len self <: usize) <. (start +! sz 4 <: usize) + then false + else +diff -ruN extraction-lax/Bertie.Tls13formats.Handshake_data.fsti extraction-panic-free/Bertie.Tls13formats.Handshake_data.fsti +--- extraction-lax/Bertie.Tls13formats.Handshake_data.fsti 2024-04-10 09:10:50.145971412 +0200 ++++ extraction-panic-free/Bertie.Tls13formats.Handshake_data.fsti 2024-04-10 09:10:50.180952285 +0200 +@@ -57,10 +57,9 @@ + val impl__HandshakeData__as_handshake_message + (self: t_HandshakeData) + (expected_type: t_HandshakeType) +- : Prims.Pure (Core.Result.t_Result t_HandshakeData u8) Prims.l_True (fun _ -> Prims.l_True) ++ : Prims.Pure (Core.Result.t_Result t_HandshakeData u8) Prims.l_True (fun _ -> Prims.l_True) + +-val impl__HandshakeData__to_bytes (self: t_HandshakeData) +- : Prims.Pure Bertie.Tls13utils.t_Bytes Prims.l_True (fun _ -> Prims.l_True) ++let impl__HandshakeData__to_bytes (self: t_HandshakeData) = self._0 + + val impl__HandshakeData__to_four (self: t_HandshakeData) + : Prims.Pure +@@ -92,4 +91,7 @@ + (self: t_HandshakeData) + (handshake_type: t_HandshakeType) + (start: usize) +- : Prims.Pure bool Prims.l_True (fun _ -> Prims.l_True) ++ : Prims.Pure bool ++ (v start <= v (impl__HandshakeData__len self)) ++ (fun _ -> Prims.l_True) ++ (decreases (v (impl__HandshakeData__len self) - v start)) diff -ruN extraction-lax/Bertie.Tls13handshake.fst extraction-panic-free/Bertie.Tls13handshake.fst ---- extraction-lax/Bertie.Tls13handshake.fst 2024-04-05 08:35:03 -+++ extraction-panic-free/Bertie.Tls13handshake.fst 2024-04-05 08:35:03 +--- extraction-lax/Bertie.Tls13handshake.fst 2024-04-10 09:10:50.151968133 +0200 ++++ extraction-panic-free/Bertie.Tls13handshake.fst 2024-04-10 09:10:50.175955017 +0200 @@ -22,13 +22,14 @@ Bertie.Tls13utils.u16_as_be_bytes (Bertie.Tls13utils.v_U16 (cast (len <: usize) <: u16) <: u16 ) @@ -3341,8 +3328,8 @@ diff -ruN extraction-lax/Bertie.Tls13handshake.fst extraction-panic-free/Bertie. bindero with diff -ruN extraction-lax/Bertie.Tls13handshake.fsti extraction-panic-free/Bertie.Tls13handshake.fsti ---- extraction-lax/Bertie.Tls13handshake.fsti 2024-04-05 08:35:03 -+++ extraction-panic-free/Bertie.Tls13handshake.fsti 2024-04-05 08:35:03 +--- extraction-lax/Bertie.Tls13handshake.fsti 2024-04-10 09:10:50.147970319 +0200 ++++ extraction-panic-free/Bertie.Tls13handshake.fsti 2024-04-10 09:10:50.178953378 +0200 @@ -13,7 +13,7 @@ (key label context: Bertie.Tls13utils.t_Bytes) (len: usize) @@ -3386,8 +3373,8 @@ diff -ruN extraction-lax/Bertie.Tls13handshake.fsti extraction-panic-free/Bertie : Prims.Pure (Core.Result.t_Result diff -ruN extraction-lax/Bertie.Tls13record.fst extraction-panic-free/Bertie.Tls13record.fst ---- extraction-lax/Bertie.Tls13record.fst 2024-04-05 08:35:03 -+++ extraction-panic-free/Bertie.Tls13record.fst 2024-04-05 08:35:03 +--- extraction-lax/Bertie.Tls13record.fst 2024-04-10 09:10:50.161962668 +0200 ++++ extraction-panic-free/Bertie.Tls13record.fst 2024-04-10 09:10:50.186949006 +0200 @@ -7,10 +7,11 @@ let (counter: Bertie.Tls13utils.t_Bytes):Bertie.Tls13utils.t_Bytes = Core.Convert.f_into (Core.Num.impl__u64__to_be_bytes n <: t_Array u8 (sz 8)) @@ -3508,8 +3495,8 @@ diff -ruN extraction-lax/Bertie.Tls13record.fst extraction-panic-free/Bertie.Tls (v_rec, (ClientCipherState0 ae kiv (n +! 1uL) exp <: t_ClientCipherState0) <: diff -ruN extraction-lax/Bertie.Tls13record.fsti extraction-panic-free/Bertie.Tls13record.fsti ---- extraction-lax/Bertie.Tls13record.fsti 2024-04-05 08:35:03 -+++ extraction-panic-free/Bertie.Tls13record.fsti 2024-04-05 08:35:03 +--- extraction-lax/Bertie.Tls13record.fsti 2024-04-10 09:10:50.164961028 +0200 ++++ extraction-panic-free/Bertie.Tls13record.fsti 2024-04-10 09:10:50.173956110 +0200 @@ -4,10 +4,15 @@ open FStar.Mul @@ -3602,8 +3589,8 @@ diff -ruN extraction-lax/Bertie.Tls13record.fsti extraction-panic-free/Bertie.Tl val server_cipher_state0 diff -ruN extraction-lax/Bertie.Tls13utils.fsti extraction-panic-free/Bertie.Tls13utils.fsti ---- extraction-lax/Bertie.Tls13utils.fsti 2024-04-05 08:35:03 -+++ extraction-panic-free/Bertie.Tls13utils.fsti 2024-04-05 08:35:03 +--- extraction-lax/Bertie.Tls13utils.fsti 2024-04-10 09:10:50.165960482 +0200 ++++ extraction-panic-free/Bertie.Tls13utils.fsti 2024-04-10 09:10:50.189947366 +0200 @@ -61,6 +61,8 @@ let v_ZERO_RTT_DISABLED: u8 = 129uy @@ -3622,8 +3609,8 @@ diff -ruN extraction-lax/Bertie.Tls13utils.fsti extraction-panic-free/Bertie.Tls + (fun res -> match res with + | Core.Result.Result_Ok l -> b == true + | _ -> True) - + + val check_eq1 (b1 b2: u8) : Prims.Pure (Core.Result.t_Result Prims.unit u8) Prims.l_True (fun _ -> Prims.l_True) @@ -3640,8 +3627,8 @@ diff -ruN extraction-lax/Bertie.Tls13utils.fsti extraction-panic-free/Bertie.Tls + (fun res -> match res with + | Core.Result.Result_Ok l -> v l <= 65536 /\ v l + 2 <= Seq.length bytes + | _ -> True) - + + val length_u24_encoded (bytes: t_Slice u8) - : Prims.Pure (Core.Result.t_Result usize u8) Prims.l_True (fun _ -> Prims.l_True) + : Prims.Pure (Core.Result.t_Result usize u8) @@ -3656,8 +3643,8 @@ diff -ruN extraction-lax/Bertie.Tls13utils.fsti extraction-panic-free/Bertie.Tls + (fun res -> match res with + | Core.Result.Result_Ok l -> v l <= 256 /\ v l + 1 <= Seq.length bytes + | _ -> True) - + + val check_length_encoding_u16_slice (bytes: t_Slice u8) - : Prims.Pure (Core.Result.t_Result Prims.unit u8) Prims.l_True (fun _ -> Prims.l_True) + : Prims.Pure (Core.Result.t_Result Prims.unit u8) Prims.l_True @@ -3684,8 +3671,8 @@ diff -ruN extraction-lax/Bertie.Tls13utils.fsti extraction-panic-free/Bertie.Tls + Seq.length bytes > 0 /\ + v (Seq.index bytes 0) + 1 == Seq.length bytes + | _ -> True) - + + val eq_slice (b1 b2: t_Slice u8) : Prims.Pure bool Prims.l_True (fun _ -> Prims.l_True) val check_eq_slice (b1 b2: t_Slice u8) @@ -3762,11 +3749,11 @@ diff -ruN extraction-lax/Bertie.Tls13utils.fsti extraction-panic-free/Bertie.Tls -val impl__Bytes__concat_array (v_N: usize) (self: t_Bytes) (other: t_Array u8 v_N) - : Prims.Pure t_Bytes Prims.l_True (fun _ -> Prims.l_True) - ++ +val impl__Bytes__concat_array (v_N: usize) (self: t_Bytes{Seq.length self._0 + v v_N <= max_usize}) (other: t_Array u8 v_N) + : Prims.Pure t_Bytes Prims.l_True + (fun res -> Seq.length res._0 == Seq.length self._0 + v v_N) -+ + val impl__Bytes__extend_from_slice (self x: t_Bytes) : Prims.Pure t_Bytes Prims.l_True (fun _ -> Prims.l_True) @@ -3807,7 +3794,7 @@ diff -ruN extraction-lax/Bertie.Tls13utils.fsti extraction-panic-free/Bertie.Tls +val impl__Bytes__slice_range (self: t_Bytes) (range: Core.Ops.Range.t_Range usize{Core.Ops.Index.f_index_pre self._0 range}) + : Prims.Pure t_Bytes Prims.l_True + (fun res -> res == Bytes (self._0.[ range ])) - ++ +val impl__Bytes__zeroes (len: usize) : Prims.Pure t_Bytes Prims.l_True + (fun res -> Seq.length res._0 == v len) + @@ -3819,7 +3806,7 @@ diff -ruN extraction-lax/Bertie.Tls13utils.fsti extraction-panic-free/Bertie.Tls + f_index_post = (fun (self: t_Bytes) (x: usize) (out: u8) -> true); + f_index = fun (self: t_Bytes) (x: usize) -> self._0.[ x ] + } -+ + val impl__Bytes__update_slice (self: t_Bytes) (start: usize) (other: t_Bytes) (beg len: usize) - : Prims.Pure t_Bytes Prims.l_True (fun _ -> Prims.l_True) + : Prims.Pure t_Bytes @@ -3839,8 +3826,7 @@ diff -ruN extraction-lax/Bertie.Tls13utils.fsti extraction-panic-free/Bertie.Tls + f_index_post = (fun (self: t_Bytes) (x: Core.Ops.Range.t_Range usize) (out: t_Slice u8) -> true); + f_index = fun (self: t_Bytes) (x: Core.Ops.Range.t_Range usize) -> self._0.[ x ] + } - --val bytes (x: t_Slice u8) : Prims.Pure t_Bytes Prims.l_True (fun _ -> Prims.l_True) ++ +[@@ FStar.Tactics.Typeclasses.tcinstance] +let upd_22: Rust_primitives.Hax.update_at_tc t_Bytes usize = + { @@ -3848,15 +3834,16 @@ diff -ruN extraction-lax/Bertie.Tls13utils.fsti extraction-panic-free/Bertie.Tls + update_at = fun s (i:usize{v i < Seq.length s._0}) x -> Bytes (Seq.upd s._0 (v i) x) + } --val bytes1 (x: u8) : Prims.Pure t_Bytes Prims.l_True (fun _ -> Prims.l_True) +-val bytes (x: t_Slice u8) : Prims.Pure t_Bytes Prims.l_True (fun _ -> Prims.l_True) --val bytes2 (x y: u8) : Prims.Pure t_Bytes Prims.l_True (fun _ -> Prims.l_True) +-val bytes1 (x: u8) : Prims.Pure t_Bytes Prims.l_True (fun _ -> Prims.l_True) +let bytes (x: t_Slice u8) = Bytes x +-val bytes2 (x y: u8) : Prims.Pure t_Bytes Prims.l_True (fun _ -> Prims.l_True) +val bytes1 (x: u8) : Prims.Pure t_Bytes Prims.l_True (fun res -> Seq.length res._0 == 1) + +val bytes2 (x y: u8) : Prims.Pure t_Bytes Prims.l_True (fun res -> Seq.length res._0 == 2) -+ + val check_eq (b1 b2: t_Bytes) : Prims.Pure (Core.Result.t_Result Prims.unit u8) Prims.l_True (fun _ -> Prims.l_True) @@ -3866,8 +3853,8 @@ diff -ruN extraction-lax/Bertie.Tls13utils.fsti extraction-panic-free/Bertie.Tls + (fun res -> match res with + | Core.Result.Result_Ok _ -> Seq.length bytes._0 >= 2 + | _ -> True) - + + val check_length_encoding_u8 (bytes: t_Bytes) - : Prims.Pure (Core.Result.t_Result Prims.unit u8) Prims.l_True (fun _ -> Prims.l_True) + : Prims.Pure (Core.Result.t_Result Prims.unit u8) Prims.l_True diff --git a/proofs/fstar/extraction/Bertie.Tls13formats.Handshake_data.fst b/proofs/fstar/extraction/Bertie.Tls13formats.Handshake_data.fst index 94b6b13f..aecfddf0 100644 --- 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 index d32736cb..53c34922 100644 --- 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 index a15f7192..6f434c99 100644 --- 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 index 17576f0c..3e2de8dd 100755 --- a/proofs/fstar/patches.sh +++ b/proofs/fstar/patches.sh @@ -11,7 +11,7 @@ DENYLIST="" 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 From fa5b7853c221bd31d31b8239cd19a2f4b7e8a6ed Mon Sep 17 00:00:00 2001 From: Lucas Franceschino Date: Wed, 10 Apr 2024 09:32:50 +0200 Subject: [PATCH 2/2] fix: `patches.sh`: use `gcp` if installed, `cp` otherwise --- proofs/fstar/patches.sh | 7 ++++++- 1 file changed, 6 insertions(+), 1 deletion(-) diff --git a/proofs/fstar/patches.sh b/proofs/fstar/patches.sh index 3e2de8dd..4ba1b451 100755 --- 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/ prepare_folder() { original="$1" workdir="$2" - find "$original" \( -name '*.fst' -o -name '*.fsti' \) -exec cp --parents \{\} "$workdir" \; + find "$original" \( -name '*.fst' -o -name '*.fsti' \) -exec "$CP" --parents \{\} "$workdir" \; } # `patch_folder ORIGINAL DESTINATION PATCH` creates the folder