Skip to content

Commit

Permalink
new F*
Browse files Browse the repository at this point in the history
  • Loading branch information
@franziskuskiefer
franziskuskiefer committed Jan 12, 2024
1 parent 1d372bd commit b9d532b
Show file tree
Hide file tree
Showing 10 changed files with 1,238 additions and 1,187 deletions.
12 changes: 11 additions & 1 deletion hax-driver.py
View file
Original file line number Diff line number Diff line change
Expand Up @@ -58,7 +58,17 @@ def shell(command, expect=0, cwd=None, env={}):

options = parser.parse_args()

cargo_hax_into = ["cargo", "hax", "-C", "-p", "bertie", ";", "into"]
cargo_hax_into = [
"cargo",
"hax",
"-C",
"-p",
"bertie",
"--features",
"secret_integers",
";",
"into",
]
hax_env = {}

if options.sub == "extract":
Expand Down
4 changes: 2 additions & 2 deletions proofs/fstar/extraction/Bertie.Server.fst
View file
Original file line number Diff line number Diff line change
Expand Up @@ -49,13 +49,13 @@ let lookup_db
Core.Result.t_Result Prims.unit u8)
with
| Core.Ops.Control_flow.ControlFlow_Break residual ->
let* hoist256:Rust_primitives.Hax.t_Never =
let* hoist253: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 hoist256)
Core.Ops.Control_flow.ControlFlow_Continue (Rust_primitives.Hax.never_to_any hoist253)
<:
Core.Ops.Control_flow.t_ControlFlow (Core.Result.t_Result t_ServerInfo u8) Prims.unit
| Core.Ops.Control_flow.ControlFlow_Continue v_val ->
Expand Down
84 changes: 42 additions & 42 deletions proofs/fstar/extraction/Bertie.Tls13api.fst
View file

Large diffs are not rendered by default.

262 changes: 131 additions & 131 deletions proofs/fstar/extraction/Bertie.Tls13cert.fst
View file

Large diffs are not rendered by default.

224 changes: 110 additions & 114 deletions proofs/fstar/extraction/Bertie.Tls13crypto.fst
View file

Large diffs are not rendered by default.

68 changes: 36 additions & 32 deletions proofs/fstar/extraction/Bertie.Tls13formats.Handshake_data.fst
View file
Original file line number Diff line number Diff line change
Expand Up @@ -99,12 +99,12 @@ let impl__HandshakeData__next_handshake_message (self: t_HandshakeData)
Core.Result.t_Result usize u8)
with
| Core.Ops.Control_flow.ControlFlow_Break residual ->
let* hoist307:Rust_primitives.Hax.t_Never =
let* hoist304: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_HandshakeData & t_HandshakeData) u8)
in
Core.Ops.Control_flow.ControlFlow_Continue (Rust_primitives.Hax.never_to_any hoist307)
Core.Ops.Control_flow.ControlFlow_Continue (Rust_primitives.Hax.never_to_any hoist304)
<:
Core.Ops.Control_flow.t_ControlFlow
(Core.Result.t_Result (t_HandshakeData & t_HandshakeData) u8) usize
Expand Down Expand Up @@ -153,12 +153,12 @@ let impl__HandshakeData__as_handshake_message
Core.Result.t_Result (t_HandshakeData & t_HandshakeData) u8)
with
| Core.Ops.Control_flow.ControlFlow_Break residual ->
let* hoist308:Rust_primitives.Hax.t_Never =
let* hoist305: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_HandshakeData u8)
in
Core.Ops.Control_flow.ControlFlow_Continue (Rust_primitives.Hax.never_to_any hoist308)
Core.Ops.Control_flow.ControlFlow_Continue (Rust_primitives.Hax.never_to_any hoist305)
<:
Core.Ops.Control_flow.t_ControlFlow (Core.Result.t_Result t_HandshakeData u8)
(t_HandshakeData & t_HandshakeData)
Expand All @@ -179,12 +179,12 @@ let impl__HandshakeData__as_handshake_message
else Core.Result.Result_Ok message <: Core.Result.t_Result t_HandshakeData u8)
with
| Core.Ops.Control_flow.ControlFlow_Break residual ->
let* hoist309:Rust_primitives.Hax.t_Never =
let* hoist306: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_HandshakeData u8)
in
Core.Ops.Control_flow.ControlFlow_Continue (Rust_primitives.Hax.never_to_any hoist309)
Core.Ops.Control_flow.ControlFlow_Continue (Rust_primitives.Hax.never_to_any hoist306)
<:
Core.Ops.Control_flow.t_ControlFlow (Core.Result.t_Result t_HandshakeData u8)
t_HandshakeData
Expand All @@ -210,12 +210,12 @@ let impl__HandshakeData__as_handshake_message
Core.Result.t_Result Prims.unit u8)
with
| Core.Ops.Control_flow.ControlFlow_Break residual ->
let* hoist310:Rust_primitives.Hax.t_Never =
let* hoist307: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_HandshakeData u8)
in
Core.Ops.Control_flow.ControlFlow_Continue (Rust_primitives.Hax.never_to_any hoist310)
Core.Ops.Control_flow.ControlFlow_Continue (Rust_primitives.Hax.never_to_any hoist307)
<:
Core.Ops.Control_flow.t_ControlFlow (Core.Result.t_Result t_HandshakeData u8) Prims.unit
| Core.Ops.Control_flow.ControlFlow_Continue v_val ->
Expand Down Expand Up @@ -257,13 +257,13 @@ let impl__HandshakeData__to_four (self: t_HandshakeData)
Core.Result.t_Result (t_HandshakeData & t_HandshakeData) u8)
with
| Core.Ops.Control_flow.ControlFlow_Break residual ->
let* hoist311:Rust_primitives.Hax.t_Never =
let* hoist308: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_HandshakeData & t_HandshakeData & t_HandshakeData & t_HandshakeData) u8)
in
Core.Ops.Control_flow.ControlFlow_Continue (Rust_primitives.Hax.never_to_any hoist311)
Core.Ops.Control_flow.ControlFlow_Continue (Rust_primitives.Hax.never_to_any hoist308)
<:
Core.Ops.Control_flow.t_ControlFlow
(Core.Result.t_Result
Expand All @@ -284,13 +284,13 @@ let impl__HandshakeData__to_four (self: t_HandshakeData)
Core.Result.t_Result (t_HandshakeData & t_HandshakeData) u8)
with
| Core.Ops.Control_flow.ControlFlow_Break residual ->
let* hoist312:Rust_primitives.Hax.t_Never =
let* hoist309: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_HandshakeData & t_HandshakeData & t_HandshakeData & t_HandshakeData) u8)
in
Core.Ops.Control_flow.ControlFlow_Continue (Rust_primitives.Hax.never_to_any hoist312)
Core.Ops.Control_flow.ControlFlow_Continue (Rust_primitives.Hax.never_to_any hoist309)
<:
Core.Ops.Control_flow.t_ControlFlow
(Core.Result.t_Result
Expand All @@ -311,13 +311,13 @@ let impl__HandshakeData__to_four (self: t_HandshakeData)
Core.Result.t_Result (t_HandshakeData & t_HandshakeData) u8)
with
| Core.Ops.Control_flow.ControlFlow_Break residual ->
let* hoist313:Rust_primitives.Hax.t_Never =
let* hoist310: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_HandshakeData & t_HandshakeData & t_HandshakeData & t_HandshakeData) u8)
in
Core.Ops.Control_flow.ControlFlow_Continue (Rust_primitives.Hax.never_to_any hoist313)
Core.Ops.Control_flow.ControlFlow_Continue (Rust_primitives.Hax.never_to_any hoist310)
<:
Core.Ops.Control_flow.t_ControlFlow
(Core.Result.t_Result
Expand All @@ -338,13 +338,13 @@ let impl__HandshakeData__to_four (self: t_HandshakeData)
Core.Result.t_Result (t_HandshakeData & t_HandshakeData) u8)
with
| Core.Ops.Control_flow.ControlFlow_Break residual ->
let* hoist314:Rust_primitives.Hax.t_Never =
let* hoist311: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_HandshakeData & t_HandshakeData & t_HandshakeData & t_HandshakeData) u8)
in
Core.Ops.Control_flow.ControlFlow_Continue (Rust_primitives.Hax.never_to_any hoist314)
Core.Ops.Control_flow.ControlFlow_Continue (Rust_primitives.Hax.never_to_any hoist311)
<:
Core.Ops.Control_flow.t_ControlFlow
(Core.Result.t_Result
Expand Down Expand Up @@ -386,12 +386,12 @@ let impl__HandshakeData__to_two (self: t_HandshakeData)
Core.Result.t_Result (t_HandshakeData & t_HandshakeData) u8)
with
| Core.Ops.Control_flow.ControlFlow_Break residual ->
let* hoist315:Rust_primitives.Hax.t_Never =
let* hoist312: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_HandshakeData & t_HandshakeData) u8)
in
Core.Ops.Control_flow.ControlFlow_Continue (Rust_primitives.Hax.never_to_any hoist315)
Core.Ops.Control_flow.ControlFlow_Continue (Rust_primitives.Hax.never_to_any hoist312)
<:
Core.Ops.Control_flow.t_ControlFlow
(Core.Result.t_Result (t_HandshakeData & t_HandshakeData) u8)
Expand All @@ -410,12 +410,12 @@ let impl__HandshakeData__to_two (self: t_HandshakeData)
Core.Result.t_Result (t_HandshakeData & t_HandshakeData) u8)
with
| Core.Ops.Control_flow.ControlFlow_Break residual ->
let* hoist316:Rust_primitives.Hax.t_Never =
let* hoist313: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_HandshakeData & t_HandshakeData) u8)
in
Core.Ops.Control_flow.ControlFlow_Continue (Rust_primitives.Hax.never_to_any hoist316)
Core.Ops.Control_flow.ControlFlow_Continue (Rust_primitives.Hax.never_to_any hoist313)
<:
Core.Ops.Control_flow.t_ControlFlow
(Core.Result.t_Result (t_HandshakeData & t_HandshakeData) u8)
Expand Down Expand Up @@ -455,19 +455,19 @@ let impl__HandshakeData__from_bytes
(handshake_type: t_HandshakeType)
(handshake_bytes: Bertie.Tls13utils.t_Bytes)
: Core.Result.t_Result t_HandshakeData u8 =
Rust_primitives.Hax.Control_flow_monad.Mexception.run (let* hoist318:Bertie.Tls13utils.t_Bytes =
Rust_primitives.Hax.Control_flow_monad.Mexception.run (let* hoist315:Bertie.Tls13utils.t_Bytes =
match
Core.Ops.Try_trait.f_branch (Bertie.Tls13utils.encode_length_u24 handshake_bytes
<:
Core.Result.t_Result Bertie.Tls13utils.t_Bytes u8)
with
| Core.Ops.Control_flow.ControlFlow_Break residual ->
let* hoist317:Rust_primitives.Hax.t_Never =
let* hoist314: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_HandshakeData u8)
in
Core.Ops.Control_flow.ControlFlow_Continue (Rust_primitives.Hax.never_to_any hoist317)
Core.Ops.Control_flow.ControlFlow_Continue (Rust_primitives.Hax.never_to_any hoist314)
<:
Core.Ops.Control_flow.t_ControlFlow (Core.Result.t_Result t_HandshakeData u8)
Bertie.Tls13utils.t_Bytes
Expand All @@ -478,18 +478,22 @@ let impl__HandshakeData__from_bytes
Bertie.Tls13utils.t_Bytes
in
Core.Ops.Control_flow.ControlFlow_Continue
(let hoist319:Bertie.Tls13utils.t_Bytes =
Bertie.Tls13utils.impl__Bytes__concat (Bertie.Tls13utils.bytes1 (cast (handshake_type
(let hoist316:Bertie.Tls13utils.t_Bytes =
Bertie.Tls13utils.impl__Bytes__prefix hoist315
(Rust_primitives.unsize (let list =
[
Bertie.Tls13utils.U8 (cast (handshake_type <: t_HandshakeType) <: u8)
<:
t_HandshakeType)
<:
u8)
Bertie.Tls13utils.t_U8
]
in
FStar.Pervasives.assert_norm (Prims.eq2 (List.Tot.length list) 1);
Rust_primitives.Hax.array_of_list list)
<:
Bertie.Tls13utils.t_Bytes)
hoist318
t_Slice Bertie.Tls13utils.t_U8)
in
let hoist320:t_HandshakeData = Core.Convert.f_from hoist319 in
Core.Result.Result_Ok hoist320 <: Core.Result.t_Result t_HandshakeData u8)
let hoist317:t_HandshakeData = Core.Convert.f_from hoist316 in
Core.Result.Result_Ok hoist317 <: Core.Result.t_Result t_HandshakeData u8)
<:
Core.Ops.Control_flow.t_ControlFlow (Core.Result.t_Result t_HandshakeData u8)
(Core.Result.t_Result t_HandshakeData u8))
Expand Down
Loading

0 comments on commit b9d532b

Please sign in to comment.