Skip to content

Commit

Permalink
chore(hax/F*): update snapshot
Browse files Browse the repository at this point in the history
  • Loading branch information
@W95Psp
W95Psp committed Feb 1, 2024
1 parent e511395 commit 361deef
Show file tree
Hide file tree
Showing 10 changed files with 3,481 additions and 10,152 deletions.
47 changes: 14 additions & 33 deletions proofs/fstar/extraction/Bertie.Server.fst
View file
Original file line number Diff line number Diff line change
Expand Up @@ -28,7 +28,7 @@ let lookup_db
(sni: Bertie.Tls13utils.t_Bytes)
(tkt: Core.Option.t_Option Bertie.Tls13utils.t_Bytes)
: Core.Result.t_Result t_ServerInfo u8 =
Rust_primitives.Hax.Control_flow_monad.Mexception.run (if
Rust_primitives.Hax.Control_flow_monad.Mresult.run (if
(Bertie.Tls13utils.eq sni
(Bertie.Tls13utils.impl__Bytes__new () <: Bertie.Tls13utils.t_Bytes)
<:
Expand All @@ -42,28 +42,13 @@ let lookup_db
Core.Option.t_Option (Bertie.Tls13utils.t_Bytes & Bertie.Tls13utils.t_Bytes))
with
| true, Core.Option.Option_Some ctkt, Core.Option.Option_Some (stkt, psk) ->
let* _:Prims.unit =
match
Core.Ops.Try_trait.f_branch (Bertie.Tls13utils.check_eq ctkt stkt
<:
Core.Result.t_Result Prims.unit u8)
with
| Core.Ops.Control_flow.ControlFlow_Break residual ->
let* hoist245:Rust_primitives.Hax.t_Never =
Core.Ops.Control_flow.ControlFlow.v_Break (Core.Ops.Try_trait.f_from_residual residual

<:
Core.Result.t_Result t_ServerInfo u8)
in
Core.Ops.Control_flow.ControlFlow_Continue (Rust_primitives.Hax.never_to_any hoist245)
<:
Core.Ops.Control_flow.t_ControlFlow (Core.Result.t_Result t_ServerInfo u8) Prims.unit
| Core.Ops.Control_flow.ControlFlow_Continue v_val ->
Core.Ops.Control_flow.ControlFlow_Continue v_val
<:
Core.Ops.Control_flow.t_ControlFlow (Core.Result.t_Result t_ServerInfo u8) Prims.unit
let| _:Prims.unit =
Core.Result.impl__map_err (Bertie.Tls13utils.check_eq ctkt stkt
<:
Core.Result.t_Result Prims.unit u8)
(Core.Convert.f_from <: u8 -> u8)
in
Core.Ops.Control_flow.ControlFlow_Continue
Core.Result.Result_Ok
(let server:t_ServerInfo =
{
f_cert = Core.Clone.f_clone db.f_cert;
Expand All @@ -79,10 +64,9 @@ let lookup_db
in
Core.Result.Result_Ok server <: Core.Result.t_Result t_ServerInfo u8)
<:
Core.Ops.Control_flow.t_ControlFlow (Core.Result.t_Result t_ServerInfo u8)
(Core.Result.t_Result t_ServerInfo u8)
Core.Result.t_Result (Core.Result.t_Result t_ServerInfo u8) u8
| false, _, _ ->
Core.Ops.Control_flow.ControlFlow_Continue
Core.Result.Result_Ok
(let server:t_ServerInfo =
{
f_cert = Core.Clone.f_clone db.f_cert;
Expand All @@ -96,21 +80,18 @@ let lookup_db
in
Core.Result.Result_Ok server <: Core.Result.t_Result t_ServerInfo u8)
<:
Core.Ops.Control_flow.t_ControlFlow (Core.Result.t_Result t_ServerInfo u8)
(Core.Result.t_Result t_ServerInfo u8)
Core.Result.t_Result (Core.Result.t_Result t_ServerInfo u8) u8
| _ ->
Core.Ops.Control_flow.ControlFlow_Continue
Core.Result.Result_Ok
(Core.Result.Result_Err Bertie.Tls13utils.v_PSK_MODE_MISMATCH
<:
Core.Result.t_Result t_ServerInfo u8)
<:
Core.Ops.Control_flow.t_ControlFlow (Core.Result.t_Result t_ServerInfo u8)
(Core.Result.t_Result t_ServerInfo u8)
Core.Result.t_Result (Core.Result.t_Result t_ServerInfo u8) u8
else
Core.Ops.Control_flow.ControlFlow_Continue
Core.Result.Result_Ok
(Core.Result.Result_Err (Bertie.Tls13utils.parse_failed () <: u8)
<:
Core.Result.t_Result t_ServerInfo u8)
<:
Core.Ops.Control_flow.t_ControlFlow (Core.Result.t_Result t_ServerInfo u8)
(Core.Result.t_Result t_ServerInfo u8))
Core.Result.t_Result (Core.Result.t_Result t_ServerInfo u8) u8)
527 changes: 142 additions & 385 deletions proofs/fstar/extraction/Bertie.Tls13api.fst
View file

Large diffs are not rendered by default.

Loading

0 comments on commit 361deef

Please sign in to comment.