From ce4c80571ba19ede0b232dee9e1e57903520a941 Mon Sep 17 00:00:00 2001 From: Nadrieril Date: Fri, 16 Jan 2026 17:04:51 +0100 Subject: [PATCH 1/3] Reformat a teeny bit --- lib/Cleanup2.ml | 66 ++++++++++++++++++++++++++++++------------------- 1 file changed, 40 insertions(+), 26 deletions(-) diff --git a/lib/Cleanup2.ml b/lib/Cleanup2.ml index c2521b7c..d196faf8 100644 --- a/lib/Cleanup2.ml +++ b/lib/Cleanup2.ml @@ -627,13 +627,17 @@ let resugar_loops = let open Krml.Helpers in let w = match t1 with TInt w -> w | _ -> assert false in let e_some_i = with_type (Builtin.mk_option t1) (ECons ("Some", [with_type t1 (EBound 0)])) in - with_type e.typ @@ ESequence (with_type TUnit (EFor (fresh_binder ~mut:true "i" t1, - e_start, - mk_lt w (Krml.DeBruijn.lift 1 e_end), - (* XXX seems like the increment is always size_t here ?! *) - mk_incr_e w (with_type t1 (ECast (e_increment, t1))), - self#visit_expr env (Krml.DeBruijn.subst e_some_i 0 e_body))) :: - List.map (fun e -> self#visit_expr env (Krml.DeBruijn.subst eunit 0 e)) rest) + with_type e.typ @@ + ESequence ( + with_type TUnit (EFor ( + fresh_binder ~mut:true "i" t1, + e_start, + mk_lt w (Krml.DeBruijn.lift 1 e_end), + (* XXX seems like the increment is always size_t here ?! *) + mk_incr_e w (with_type t1 (ECast (e_increment, t1))), + self#visit_expr env (Krml.DeBruijn.subst e_some_i 0 e_body) + )) :: List.map (fun e -> self#visit_expr env (Krml.DeBruijn.subst eunit 0 e)) rest + ) | [%cremepat {| let iter = @@ -654,13 +658,17 @@ let resugar_loops = |}] -> let open Krml.Helpers in let w = match t1 with TInt w -> w | _ -> assert false in - with_type e.typ @@ ESequence (with_type TUnit (EFor (fresh_binder ~mut:true "i" t1, - e_start, - mk_lt w (Krml.DeBruijn.lift 1 e_end), - (* XXX seems like the increment is always size_t here ?! *) - mk_incr_e w (with_type t1 (ECast (e_increment, t1))), - self#visit_expr env e_body)) :: - List.map (fun e -> self#visit_expr env (Krml.DeBruijn.subst eunit 0 e)) rest) + with_type e.typ @@ + ESequence ( + with_type TUnit (EFor ( + fresh_binder ~mut:true "i" t1, + e_start, + mk_lt w (Krml.DeBruijn.lift 1 e_end), + (* XXX seems like the increment is always size_t here ?! *) + mk_incr_e w (with_type t1 (ECast (e_increment, t1))), + self#visit_expr env e_body + )) :: List.map (fun e -> self#visit_expr env (Krml.DeBruijn.subst eunit 0 e)) rest + ) (* Terminal position (step-by for-loop) *) | [%cremepat {| @@ -683,12 +691,15 @@ let resugar_loops = let open Krml.Helpers in let w = match t1 with TInt w -> w | _ -> assert false in let e_some_i = with_type (Builtin.mk_option t1) (ECons ("Some", [with_type t1 (EBound 0)])) in - with_type e.typ @@ EFor (fresh_binder ~mut:true "i" t1, - e_start, - mk_lt w (Krml.DeBruijn.lift 1 e_end), - (* XXX seems like the increment is always size_t here ?! *) - mk_incr_e w (with_type t1 (ECast (e_increment, t1))), - self#visit_expr env (Krml.DeBruijn.subst e_some_i 0 e_body)) + with_type e.typ @@ + EFor ( + fresh_binder ~mut:true "i" t1, + e_start, + mk_lt w (Krml.DeBruijn.lift 1 e_end), + (* XXX seems like the increment is always size_t here ?! *) + mk_incr_e w (with_type t1 (ECast (e_increment, t1))), + self#visit_expr env (Krml.DeBruijn.subst e_some_i 0 e_body) + ) | [%cremepat {| let iter = @@ -708,12 +719,15 @@ let resugar_loops = |}] -> let open Krml.Helpers in let w = match t1 with TInt w -> w | _ -> assert false in - with_type e.typ @@ EFor (fresh_binder ~mut:true "i" t1, - e_start, - mk_lt w (Krml.DeBruijn.lift 1 e_end), - (* XXX seems like the increment is always size_t here ?! *) - mk_incr_e w (with_type t1 (ECast (e_increment, t1))), - self#visit_expr env e_body) + with_type e.typ @@ + EFor ( + fresh_binder ~mut:true "i" t1, + e_start, + mk_lt w (Krml.DeBruijn.lift 1 e_end), + (* XXX seems like the increment is always size_t here ?! *) + mk_incr_e w (with_type t1 (ECast (e_increment, t1))), + self#visit_expr env e_body + ) (* Terminal position (regular range for-loop) *) | [%cremepat {| From 437966a7c67f2f421561c067b9c9f8d9f6a6aab0 Mon Sep 17 00:00:00 2001 From: Nadrieril Date: Fri, 16 Jan 2026 18:00:29 +0100 Subject: [PATCH 2/3] Deduplicate the special iterator reconstructions --- lib/Cleanup2.ml | 413 +++++++++++++++++++++--------------------------- 1 file changed, 183 insertions(+), 230 deletions(-) diff --git a/lib/Cleanup2.ml b/lib/Cleanup2.ml index d196faf8..0000dd88 100644 --- a/lib/Cleanup2.ml +++ b/lib/Cleanup2.ml @@ -604,29 +604,182 @@ let resugar_loops = inherit [_] map as super method! visit_expr ((), _ as env) e = - (* Non-terminal position (step-by for-loop) *) - match e with - | [%cremepat {| - let iter = - core::iter::traits::collect::?::into_iter< - core::iter::adapters::step_by::StepBy>, - ?.. - >(core::iter::range::?::step_by( - { start: ?e_start, end: ?e_end }, - ?e_increment - )); - while true { - let x = core::iter::adapters::step_by::?::next(&iter); - match x { - None -> break, - Some ? -> ?e_body + let open Krml.Helpers in + let step_by = match e with + (* Non-terminal position (step-by for-loop) *) + | [%cremepat {| + let iter = + core::iter::traits::collect::?::into_iter< + core::iter::adapters::step_by::StepBy>, + ?.. + >(core::iter::range::?::step_by( + { start: ?e_start, end: ?e_end }, + ?e_increment + )); + while true { + let x = core::iter::adapters::step_by::?::next(&iter); + match x { + None -> break, + Some ? -> ?e_body + } + }; + ?rest.. + |}] -> + let e_some_i = with_type (Builtin.mk_option t1) (ECons ("Some", [with_type t1 (EBound 0)])) in + let e_body = Krml.DeBruijn.subst e_some_i 0 e_body in + Some (t1, e_start, e_end, e_increment, e_body, rest) + + | [%cremepat {| + let iter = + core::iter::traits::collect::?::into_iter< + core::iter::adapters::step_by::StepBy>, + ?.. + >(core::iter::range::?::step_by( + { start: ?e_start, end: ?e_end }, + ?e_increment + )); + while true { + match (core::iter::adapters::step_by::?::next(&iter)) { + None -> break, + Some ? -> ?e_body + } + }; + ?rest.. + |}] -> Some (t1, e_start, e_end, e_increment, e_body, rest) + + (* Terminal position (step-by for-loop) *) + | [%cremepat {| + let iter = + core::iter::traits::collect::?::into_iter< + core::iter::adapters::step_by::StepBy>, + ?.. + >(core::iter::range::?::step_by( + { start: ?e_start, end: ?e_end }, + ?e_increment + )); + while true { + let x = core::iter::adapters::step_by::?::next(&iter); + match x { + None -> break, + Some ? -> ?e_body + } + } + |}] -> + let e_some_i = with_type (Builtin.mk_option t1) (ECons ("Some", [with_type t1 (EBound 0)])) in + let e_body = Krml.DeBruijn.subst e_some_i 0 e_body in + Some (t1, e_start, e_end, e_increment, e_body, []) + + | [%cremepat {| + let iter = + core::iter::traits::collect::?::into_iter< + core::iter::adapters::step_by::StepBy>, + ?.. + >(core::iter::range::?::step_by( + { start: ?e_start, end: ?e_end }, + ?e_increment + )); + while true { + match (core::iter::adapters::step_by::?::next(&iter)) { + None -> break, + Some ? -> ?e_body + } } - }; - ?rest.. - |}] -> - let open Krml.Helpers in + |}] -> Some (t1, e_start, e_end, e_increment, e_body, []) + | _ -> None + in + + let range_iter = match e with + (* Terminal position (regular range for-loop) *) + | [%cremepat {| + let iter = + core::iter::traits::collect::?::into_iter + , ?..> + ({ start: ?e_start, end: ?e_end }); + while true { + let x = core::iter::range::?::next(&iter); + match x { + None -> break, + Some ? -> ?e_body + } + } + |}] -> + let e_some_i = with_type (Builtin.mk_option t1) (ECons ("Some", [with_type t1 (EBound 0)])) in + let e_body = Krml.DeBruijn.subst e_some_i 0 e_body in + Some (t1, e_start, e_end, e_body, []) + + | [%cremepat {| + let iter = + core::iter::traits::collect::?::into_iter + , ?..> + ({ start: ?e_start, end: ?e_end }); + while true { + match (core::iter::range::?::next(&iter)) { + None -> break, + Some ? -> ?e_body + } + } + |}] -> Some (t1, e_start, e_end, e_body, []) + + (* Non-terminal position (regular range for-loop) *) + | [%cremepat {| + let iter = + core::iter::traits::collect::?::into_iter + , ?..> + ({ start: ?e_start, end: ?e_end }); + while true { + let x = core::iter::range::?::next(&iter); + match x { + None -> break, + Some ? -> ?e_body + } + }; + ?rest.. + |}] -> + let e_some_i = with_type (Builtin.mk_option t1) (ECons ("Some", [with_type t1 (EBound 0)])) in + let e_body = Krml.DeBruijn.subst e_some_i 0 e_body in + Some (t1, e_start, e_end, e_body, rest) + + (* Special variant that appears in external crates -- TODO: do we need variants of all other + patterns? *) + | [%cremepat {| + let iter = + core::iter::traits::collect::?::into_iter + , ?..> + ({ start: ?e_start, end: ?e_end }); + while true { + let x = core::iter::range::?::next(&iter); + match x { + None -> ?e2, + Some ? -> ?e_body + }; + abort + } + |}] when ends_with_return e2 && ends_with_continue e_body + (* && x does not appear in e2 *) -> + let e_some_i = with_type (Builtin.mk_option t1) (ECons ("Some", [with_type t1 (EBound 0)])) in + let e_body = Krml.DeBruijn.subst e_some_i 0 e_body in + Some (t1, e_start, e_end, e_body, []) + + | [%cremepat {| + let iter = + core::iter::traits::collect::?::into_iter + , ?..> + ({ start: ?e_start, end: ?e_end }); + while true { + match (core::iter::range::?::next(&iter)) { + None -> break, + Some ? -> ?e_body + } + }; + ?rest.. + |}] -> Some (t1, e_start, e_end, e_body, rest) + + | _ -> None + in + + match step_by with + | Some (t1, e_start, e_end, e_increment, e_body, rest) -> let w = match t1 with TInt w -> w | _ -> assert false in - let e_some_i = with_type (Builtin.mk_option t1) (ECons ("Some", [with_type t1 (EBound 0)])) in with_type e.typ @@ ESequence ( with_type TUnit (EFor ( @@ -635,223 +788,23 @@ let resugar_loops = mk_lt w (Krml.DeBruijn.lift 1 e_end), (* XXX seems like the increment is always size_t here ?! *) mk_incr_e w (with_type t1 (ECast (e_increment, t1))), - self#visit_expr env (Krml.DeBruijn.subst e_some_i 0 e_body) + self#visit_expr env e_body )) :: List.map (fun e -> self#visit_expr env (Krml.DeBruijn.subst eunit 0 e)) rest ) - - | [%cremepat {| - let iter = - core::iter::traits::collect::?::into_iter< - core::iter::adapters::step_by::StepBy>, - ?.. - >(core::iter::range::?::step_by( - { start: ?e_start, end: ?e_end }, - ?e_increment - )); - while true { - match (core::iter::adapters::step_by::?::next(&iter)) { - None -> break, - Some ? -> ?e_body - } - }; - ?rest.. - |}] -> - let open Krml.Helpers in - let w = match t1 with TInt w -> w | _ -> assert false in - with_type e.typ @@ - ESequence ( + | None -> begin match range_iter with + | Some (t1, e_start, e_end, e_body, rest) -> + let w = match t1 with TInt w -> w | _ -> assert false in + with_type e.typ @@ ESequence ( with_type TUnit (EFor ( fresh_binder ~mut:true "i" t1, e_start, mk_lt w (Krml.DeBruijn.lift 1 e_end), - (* XXX seems like the increment is always size_t here ?! *) - mk_incr_e w (with_type t1 (ECast (e_increment, t1))), + mk_incr w, self#visit_expr env e_body )) :: List.map (fun e -> self#visit_expr env (Krml.DeBruijn.subst eunit 0 e)) rest - ) - - (* Terminal position (step-by for-loop) *) - | [%cremepat {| - let iter = - core::iter::traits::collect::?::into_iter< - core::iter::adapters::step_by::StepBy>, - ?.. - >(core::iter::range::?::step_by( - { start: ?e_start, end: ?e_end }, - ?e_increment - )); - while true { - let x = core::iter::adapters::step_by::?::next(&iter); - match x { - None -> break, - Some ? -> ?e_body - } - } - |}] -> - let open Krml.Helpers in - let w = match t1 with TInt w -> w | _ -> assert false in - let e_some_i = with_type (Builtin.mk_option t1) (ECons ("Some", [with_type t1 (EBound 0)])) in - with_type e.typ @@ - EFor ( - fresh_binder ~mut:true "i" t1, - e_start, - mk_lt w (Krml.DeBruijn.lift 1 e_end), - (* XXX seems like the increment is always size_t here ?! *) - mk_incr_e w (with_type t1 (ECast (e_increment, t1))), - self#visit_expr env (Krml.DeBruijn.subst e_some_i 0 e_body) - ) - - | [%cremepat {| - let iter = - core::iter::traits::collect::?::into_iter< - core::iter::adapters::step_by::StepBy>, - ?.. - >(core::iter::range::?::step_by( - { start: ?e_start, end: ?e_end }, - ?e_increment - )); - while true { - match (core::iter::adapters::step_by::?::next(&iter)) { - None -> break, - Some ? -> ?e_body - } - } - |}] -> - let open Krml.Helpers in - let w = match t1 with TInt w -> w | _ -> assert false in - with_type e.typ @@ - EFor ( - fresh_binder ~mut:true "i" t1, - e_start, - mk_lt w (Krml.DeBruijn.lift 1 e_end), - (* XXX seems like the increment is always size_t here ?! *) - mk_incr_e w (with_type t1 (ECast (e_increment, t1))), - self#visit_expr env e_body - ) - - (* Terminal position (regular range for-loop) *) - | [%cremepat {| - let iter = - core::iter::traits::collect::?::into_iter - , ?..> - ({ start: ?e_start, end: ?e_end }); - while true { - let x = core::iter::range::?::next(&iter); - match x { - None -> break, - Some ? -> ?e_body - } - } - |}] -> - let open Krml.Helpers in - let w = match t1 with TInt w -> w | _ -> assert false in - let e_some_i = with_type (Builtin.mk_option t1) (ECons ("Some", [with_type t1 (EBound 0)])) in - with_type e.typ @@ EFor (fresh_binder ~mut:true "i" t1, - e_start, - mk_lt w (Krml.DeBruijn.lift 1 e_end), - mk_incr w, - self#visit_expr env (Krml.DeBruijn.subst e_some_i 0 e_body)) - - | [%cremepat {| - let iter = - core::iter::traits::collect::?::into_iter - , ?..> - ({ start: ?e_start, end: ?e_end }); - while true { - match (core::iter::range::?::next(&iter)) { - None -> break, - Some ? -> ?e_body - } - } - |}] -> - let open Krml.Helpers in - let w = match t1 with TInt w -> w | _ -> assert false in - with_type e.typ @@ EFor (fresh_binder ~mut:true "i" t1, - e_start, - mk_lt w (Krml.DeBruijn.lift 1 e_end), - mk_incr w, - self#visit_expr env e_body) - - (* Non-terminal position (regular range for-loop) *) - | [%cremepat {| - let iter = - core::iter::traits::collect::?::into_iter - , ?..> - ({ start: ?e_start, end: ?e_end }); - while true { - let x = core::iter::range::?::next(&iter); - match x { - None -> break, - Some ? -> ?e_body - } - }; - ?rest.. - |}] -> - let open Krml.Helpers in - let w = match t1 with TInt w -> w | _ -> assert false in - let e_some_i = with_type (Builtin.mk_option t1) (ECons ("Some", [with_type t1 (EBound 0)])) in - with_type e.typ @@ ESequence (with_type TUnit (EFor (fresh_binder ~mut:true "i" t1, - e_start, - mk_lt w (Krml.DeBruijn.lift 1 e_end), - mk_incr w, - self#visit_expr env (Krml.DeBruijn.subst e_some_i 0 e_body)) - ) :: List.map (fun e -> self#visit_expr env (Krml.DeBruijn.subst eunit 0 e)) rest) - - (* Special variant that appears in external crates -- TODO: do we need variants of all other - patterns? *) - | [%cremepat {| - let iter = - core::iter::traits::collect::?::into_iter - , ?..> - ({ start: ?e_start, end: ?e_end }); - while true { - let x = core::iter::range::?::next(&iter); - match x { - None -> ?e2, - Some ? -> ?e_body - }; - abort - } - |}] when ends_with_return e2 && ends_with_continue e_body - (* && x does not appear in e2 *) -> - let open Krml.Helpers in - let w = match t1 with TInt w -> w | _ -> assert false in - let e_some_i = with_type (Builtin.mk_option t1) (ECons ("Some", [with_type t1 (EBound 0)])) in - with_type e.typ @@ ESequence [ - with_type TUnit (EFor (fresh_binder ~mut:true "i" t1, - e_start, - mk_lt w (Krml.DeBruijn.lift 1 e_end), - mk_incr w, - self#visit_expr env (Krml.DeBruijn.subst e_some_i 0 e_body)) - ); - self#visit_expr env (Krml.DeBruijn.(subst eunit 0 (subst eunit 0 e2))) - ] - - | [%cremepat {| - let iter = - core::iter::traits::collect::?::into_iter - , ?..> - ({ start: ?e_start, end: ?e_end }); - while true { - match (core::iter::range::?::next(&iter)) { - None -> break, - Some ? -> ?e_body - } - }; - ?rest.. - |}] -> - let open Krml.Helpers in - let w = match t1 with TInt w -> w | _ -> assert false in - with_type e.typ @@ ESequence (with_type TUnit (EFor (fresh_binder ~mut:true "i" t1, - e_start, - mk_lt w (Krml.DeBruijn.lift 1 e_end), - mk_incr w, - self#visit_expr env e_body) - ) :: List.map (fun e -> self#visit_expr env (Krml.DeBruijn.subst eunit 0 e)) rest) - - | _ -> - super#visit_expr env e - + ) + | None -> super#visit_expr env e + end end [@ocamlformat "disable"] From eed427a399e91eeae4bfad153f0ca03082cd4d7f Mon Sep 17 00:00:00 2001 From: Nadrieril Date: Sat, 17 Jan 2026 01:05:10 +0100 Subject: [PATCH 3/3] Update charon --- flake.lock | 6 +- lib/Cleanup2.ml | 168 +++++++- out/test-for/for.c | 5 +- out/test-libcrux-no-const/libcrux_sha3_avx2.c | 362 ++++++++---------- .../libcrux_sha3_portable.c | 289 ++++++-------- out/test-libcrux/libcrux_sha3_avx2.c | 362 ++++++++---------- out/test-libcrux/libcrux_sha3_portable.c | 289 ++++++-------- 7 files changed, 716 insertions(+), 765 deletions(-) diff --git a/flake.lock b/flake.lock index 3864e8e3..b6c9193b 100644 --- a/flake.lock +++ b/flake.lock @@ -26,11 +26,11 @@ "rust-overlay": "rust-overlay" }, "locked": { - "lastModified": 1768389534, - "narHash": "sha256-XFEO8NXtHp7oReVetcPcNhf1V5BF6YVn8vgXzQwL/jk=", + "lastModified": 1768574799, + "narHash": "sha256-cgEeDmfK78v+rICgvp+K5I9k23l02HoKxGIwNhGQdeA=", "owner": "aeneasverif", "repo": "charon", - "rev": "cb7e773a836cd1463208b4587d463d654e7ff7ed", + "rev": "57ce772f5f02bd0b709a216bdcf847dcafb61d9c", "type": "github" }, "original": { diff --git a/lib/Cleanup2.ml b/lib/Cleanup2.ml index 0000dd88..bd4addb5 100644 --- a/lib/Cleanup2.ml +++ b/lib/Cleanup2.ml @@ -627,6 +627,29 @@ let resugar_loops = |}] -> let e_some_i = with_type (Builtin.mk_option t1) (ECons ("Some", [with_type t1 (EBound 0)])) in let e_body = Krml.DeBruijn.subst e_some_i 0 e_body in + Some (t1, e_start, e_end, e_increment, [e_body], rest) + + | [%cremepat {| + let iter = + core::iter::traits::collect::?::into_iter< + core::iter::adapters::step_by::StepBy>, + ?.. + >(core::iter::range::?::step_by( + { start: ?e_start, end: ?e_end }, + ?e_increment + )); + while true { + let x = core::iter::adapters::step_by::?::next(&iter); + match x { + None -> break, + Some ? -> ?e_body + }; + ?loop_rest.. + }; + ?rest.. + |}] -> + let e_some_i = with_type (Builtin.mk_option t1) (ECons ("Some", [with_type t1 (EBound 0)])) in + let e_body = List.map (Krml.DeBruijn.subst e_some_i 0) (e_body :: loop_rest) in Some (t1, e_start, e_end, e_increment, e_body, rest) | [%cremepat {| @@ -645,7 +668,26 @@ let resugar_loops = } }; ?rest.. - |}] -> Some (t1, e_start, e_end, e_increment, e_body, rest) + |}] -> Some (t1, e_start, e_end, e_increment, [e_body], rest) + + | [%cremepat {| + let iter = + core::iter::traits::collect::?::into_iter< + core::iter::adapters::step_by::StepBy>, + ?.. + >(core::iter::range::?::step_by( + { start: ?e_start, end: ?e_end }, + ?e_increment + )); + while true { + match (core::iter::adapters::step_by::?::next(&iter)) { + None -> break, + Some ? -> ?e_body + }; + ?loop_rest.. + }; + ?rest.. + |}] -> Some (t1, e_start, e_end, e_increment, e_body :: loop_rest, rest) (* Terminal position (step-by for-loop) *) | [%cremepat {| @@ -667,6 +709,28 @@ let resugar_loops = |}] -> let e_some_i = with_type (Builtin.mk_option t1) (ECons ("Some", [with_type t1 (EBound 0)])) in let e_body = Krml.DeBruijn.subst e_some_i 0 e_body in + Some (t1, e_start, e_end, e_increment, [e_body], []) + + | [%cremepat {| + let iter = + core::iter::traits::collect::?::into_iter< + core::iter::adapters::step_by::StepBy>, + ?.. + >(core::iter::range::?::step_by( + { start: ?e_start, end: ?e_end }, + ?e_increment + )); + while true { + let x = core::iter::adapters::step_by::?::next(&iter); + match x { + None -> break, + Some ? -> ?e_body + }; + ?loop_rest.. + } + |}] -> + let e_some_i = with_type (Builtin.mk_option t1) (ECons ("Some", [with_type t1 (EBound 0)])) in + let e_body = List.map (Krml.DeBruijn.subst e_some_i 0) (e_body :: loop_rest) in Some (t1, e_start, e_end, e_increment, e_body, []) | [%cremepat {| @@ -684,7 +748,26 @@ let resugar_loops = Some ? -> ?e_body } } - |}] -> Some (t1, e_start, e_end, e_increment, e_body, []) + |}] -> Some (t1, e_start, e_end, e_increment, [e_body], []) + + | [%cremepat {| + let iter = + core::iter::traits::collect::?::into_iter< + core::iter::adapters::step_by::StepBy>, + ?.. + >(core::iter::range::?::step_by( + { start: ?e_start, end: ?e_end }, + ?e_increment + )); + while true { + match (core::iter::adapters::step_by::?::next(&iter)) { + None -> break, + Some ? -> ?e_body + }; + ?loop_rest.. + } + |}] -> Some (t1, e_start, e_end, e_increment, e_body :: loop_rest, []) + | _ -> None in @@ -705,6 +788,24 @@ let resugar_loops = |}] -> let e_some_i = with_type (Builtin.mk_option t1) (ECons ("Some", [with_type t1 (EBound 0)])) in let e_body = Krml.DeBruijn.subst e_some_i 0 e_body in + Some (t1, e_start, e_end, [e_body], []) + + | [%cremepat {| + let iter = + core::iter::traits::collect::?::into_iter + , ?..> + ({ start: ?e_start, end: ?e_end }); + while true { + let x = core::iter::range::?::next(&iter); + match x { + None -> break, + Some ? -> ?e_body + }; + ?loop_rest.. + } + |}] -> + let e_some_i = with_type (Builtin.mk_option t1) (ECons ("Some", [with_type t1 (EBound 0)])) in + let e_body = List.map (Krml.DeBruijn.subst e_some_i 0) (e_body :: loop_rest) in Some (t1, e_start, e_end, e_body, []) | [%cremepat {| @@ -718,7 +819,21 @@ let resugar_loops = Some ? -> ?e_body } } - |}] -> Some (t1, e_start, e_end, e_body, []) + |}] -> Some (t1, e_start, e_end, [e_body], []) + + | [%cremepat {| + let iter = + core::iter::traits::collect::?::into_iter + , ?..> + ({ start: ?e_start, end: ?e_end }); + while true { + match (core::iter::range::?::next(&iter)) { + None -> break, + Some ? -> ?e_body + }; + ?loop_rest.. + } + |}] -> Some (t1, e_start, e_end, e_body :: loop_rest, []) (* Non-terminal position (regular range for-loop) *) | [%cremepat {| @@ -737,6 +852,26 @@ let resugar_loops = |}] -> let e_some_i = with_type (Builtin.mk_option t1) (ECons ("Some", [with_type t1 (EBound 0)])) in let e_body = Krml.DeBruijn.subst e_some_i 0 e_body in + Some (t1, e_start, e_end, [e_body], rest) + + (* Non-terminal position (regular range for-loop) *) + | [%cremepat {| + let iter = + core::iter::traits::collect::?::into_iter + , ?..> + ({ start: ?e_start, end: ?e_end }); + while true { + let x = core::iter::range::?::next(&iter); + match x { + None -> break, + Some ? -> ?e_body + }; + ?loop_rest.. + }; + ?rest.. + |}] -> + let e_some_i = with_type (Builtin.mk_option t1) (ECons ("Some", [with_type t1 (EBound 0)])) in + let e_body = List.map (Krml.DeBruijn.subst e_some_i 0) (e_body :: loop_rest) in Some (t1, e_start, e_end, e_body, rest) (* Special variant that appears in external crates -- TODO: do we need variants of all other @@ -758,7 +893,7 @@ let resugar_loops = (* && x does not appear in e2 *) -> let e_some_i = with_type (Builtin.mk_option t1) (ECons ("Some", [with_type t1 (EBound 0)])) in let e_body = Krml.DeBruijn.subst e_some_i 0 e_body in - Some (t1, e_start, e_end, e_body, []) + Some (t1, e_start, e_end, [e_body], []) | [%cremepat {| let iter = @@ -772,7 +907,22 @@ let resugar_loops = } }; ?rest.. - |}] -> Some (t1, e_start, e_end, e_body, rest) + |}] -> Some (t1, e_start, e_end, [e_body], rest) + + | [%cremepat {| + let iter = + core::iter::traits::collect::?::into_iter + , ?..> + ({ start: ?e_start, end: ?e_end }); + while true { + match (core::iter::range::?::next(&iter)) { + None -> break, + Some ? -> ?e_body + }; + ?loop_rest.. + }; + ?rest.. + |}] -> Some (t1, e_start, e_end, e_body :: loop_rest, rest) | _ -> None in @@ -788,7 +938,9 @@ let resugar_loops = mk_lt w (Krml.DeBruijn.lift 1 e_end), (* XXX seems like the increment is always size_t here ?! *) mk_incr_e w (with_type t1 (ECast (e_increment, t1))), - self#visit_expr env e_body + with_type TUnit (ESequence ( + List.map (self#visit_expr env) e_body + )) )) :: List.map (fun e -> self#visit_expr env (Krml.DeBruijn.subst eunit 0 e)) rest ) | None -> begin match range_iter with @@ -800,7 +952,9 @@ let resugar_loops = e_start, mk_lt w (Krml.DeBruijn.lift 1 e_end), mk_incr w, - self#visit_expr env e_body + with_type TUnit (ESequence ( + List.map (self#visit_expr env) e_body + )) )) :: List.map (fun e -> self#visit_expr env (Krml.DeBruijn.subst eunit 0 e)) rest ) | None -> super#visit_expr env e diff --git a/out/test-for/for.c b/out/test-for/for.c index 3c36497f..635be9cc 100644 --- a/out/test-for/for.c +++ b/out/test-for/for.c @@ -17,11 +17,10 @@ uint8_t for_other(Eurydice_borrow_slice_u8 input) for (int32_t i = (int32_t)0; i < (int32_t)5; i++) { int32_t i0 = i; - if (!(i0 == (int32_t)2)) + if (i0 == (int32_t)2) { - continue; + return 6U; } - return 6U; } return input.ptr[0U]; } diff --git a/out/test-libcrux-no-const/libcrux_sha3_avx2.c b/out/test-libcrux-no-const/libcrux_sha3_avx2.c index a647c754..8143a737 100644 --- a/out/test-libcrux-no-const/libcrux_sha3_avx2.c +++ b/out/test-libcrux-no-const/libcrux_sha3_avx2.c @@ -1641,46 +1641,24 @@ with const generics static KRML_MUSTINLINE void chi_80_a6(Eurydice_arr_05 *self) { Eurydice_arr_05 old = self[0U]; - core_ops_range_Range_08 - iter = - core_iter_traits_collect__core__iter__traits__collect__IntoIterator_Clause1_Item__I__for_I__into_iter(( - KRML_CLITERAL(core_ops_range_Range_08){ .start = (size_t)0U, .end = (size_t)5U } - ), - core_ops_range_Range_08, - size_t, - core_ops_range_Range_08); - while (true) - { - core_option_Option_08 - uu____0 = - core_iter_range__core__iter__traits__iterator__Iterator_A__for_core__ops__range__Range_A__TraitClause_0___next(&iter, - size_t, - core_option_Option_08); - if (uu____0.tag == core_option_None) - { - break; - } - else - { - size_t i0 = uu____0.f0; - KRML_MAYBE_FOR5(i, - (size_t)0U, - (size_t)5U, - (size_t)1U, - size_t j = i; - set_80_a6(self, - i0, - j, - and_not_xor_b0(index_c2_a6(self, (KRML_CLITERAL(size_t_x2){ .fst = i0, .snd = j }))[0U], - index_c2_a6(&old, - (KRML_CLITERAL(size_t_x2){ .fst = i0, .snd = (j + (size_t)2U) % (size_t)5U }))[0U], - index_c2_a6(&old, - (KRML_CLITERAL(size_t_x2){ .fst = i0, .snd = (j + (size_t)1U) % (size_t)5U }))[0U]));); - continue; - } - KRML_HOST_EPRINTF("KaRaMeL abort at %s:%d\n%s\n", __FILE__, __LINE__, "panic!"); - KRML_HOST_EXIT(255U); - } + KRML_MAYBE_FOR5(i0, + (size_t)0U, + (size_t)5U, + (size_t)1U, + size_t i1 = i0; + KRML_MAYBE_FOR5(i, + (size_t)0U, + (size_t)5U, + (size_t)1U, + size_t j = i; + set_80_a6(self, + i1, + j, + and_not_xor_b0(index_c2_a6(self, (KRML_CLITERAL(size_t_x2){ .fst = i1, .snd = j }))[0U], + index_c2_a6(&old, + (KRML_CLITERAL(size_t_x2){ .fst = i1, .snd = (j + (size_t)2U) % (size_t)5U }))[0U], + index_c2_a6(&old, + (KRML_CLITERAL(size_t_x2){ .fst = i1, .snd = (j + (size_t)1U) % (size_t)5U }))[0U])););); } /** @@ -1893,85 +1871,78 @@ store_block_5b( )), uint8_t); } - return; } - else - { - return; - } - } - else - { - size_t i = uu____0.f0; - size_t i0 = (size_t)4U * i / (size_t)5U; - size_t j0 = (size_t)4U * i % (size_t)5U; - size_t i1 = ((size_t)4U * i + (size_t)1U) / (size_t)5U; - size_t j1 = ((size_t)4U * i + (size_t)1U) % (size_t)5U; - size_t i2 = ((size_t)4U * i + (size_t)2U) / (size_t)5U; - size_t j2 = ((size_t)4U * i + (size_t)2U) % (size_t)5U; - size_t i3 = ((size_t)4U * i + (size_t)3U) / (size_t)5U; - size_t j3 = ((size_t)4U * i + (size_t)3U) % (size_t)5U; - __m256i - v0l = - mm256_permute2x128_si256((int32_t)32, - get_ij_a6(s, i0, j0)[0U], - get_ij_a6(s, i2, j2)[0U], - __m256i); - __m256i - v1h = - mm256_permute2x128_si256((int32_t)32, - get_ij_a6(s, i1, j1)[0U], - get_ij_a6(s, i3, j3)[0U], - __m256i); - __m256i - v2l = - mm256_permute2x128_si256((int32_t)49, - get_ij_a6(s, i0, j0)[0U], - get_ij_a6(s, i2, j2)[0U], - __m256i); - __m256i - v3h = - mm256_permute2x128_si256((int32_t)49, - get_ij_a6(s, i1, j1)[0U], - get_ij_a6(s, i3, j3)[0U], - __m256i); - __m256i v0 = mm256_unpacklo_epi64(v0l, v1h); - __m256i v1 = mm256_unpackhi_epi64(v0l, v1h); - __m256i v2 = mm256_unpacklo_epi64(v2l, v3h); - __m256i v3 = mm256_unpackhi_epi64(v2l, v3h); - mm256_storeu_si256_u8(Eurydice_slice_subslice_mut_7e(out0, - ( - KRML_CLITERAL(core_ops_range_Range_08){ - .start = start + (size_t)32U * i, - .end = start + (size_t)32U * (i + (size_t)1U) - } - )), - v0); - mm256_storeu_si256_u8(Eurydice_slice_subslice_mut_7e(out1, - ( - KRML_CLITERAL(core_ops_range_Range_08){ - .start = start + (size_t)32U * i, - .end = start + (size_t)32U * (i + (size_t)1U) - } - )), - v1); - mm256_storeu_si256_u8(Eurydice_slice_subslice_mut_7e(out2, - ( - KRML_CLITERAL(core_ops_range_Range_08){ - .start = start + (size_t)32U * i, - .end = start + (size_t)32U * (i + (size_t)1U) - } - )), - v2); - mm256_storeu_si256_u8(Eurydice_slice_subslice_mut_7e(out3, - ( - KRML_CLITERAL(core_ops_range_Range_08){ - .start = start + (size_t)32U * i, - .end = start + (size_t)32U * (i + (size_t)1U) - } - )), - v3); + return; } + size_t i = uu____0.f0; + size_t i0 = (size_t)4U * i / (size_t)5U; + size_t j0 = (size_t)4U * i % (size_t)5U; + size_t i1 = ((size_t)4U * i + (size_t)1U) / (size_t)5U; + size_t j1 = ((size_t)4U * i + (size_t)1U) % (size_t)5U; + size_t i2 = ((size_t)4U * i + (size_t)2U) / (size_t)5U; + size_t j2 = ((size_t)4U * i + (size_t)2U) % (size_t)5U; + size_t i3 = ((size_t)4U * i + (size_t)3U) / (size_t)5U; + size_t j3 = ((size_t)4U * i + (size_t)3U) % (size_t)5U; + __m256i + v0l = + mm256_permute2x128_si256((int32_t)32, + get_ij_a6(s, i0, j0)[0U], + get_ij_a6(s, i2, j2)[0U], + __m256i); + __m256i + v1h = + mm256_permute2x128_si256((int32_t)32, + get_ij_a6(s, i1, j1)[0U], + get_ij_a6(s, i3, j3)[0U], + __m256i); + __m256i + v2l = + mm256_permute2x128_si256((int32_t)49, + get_ij_a6(s, i0, j0)[0U], + get_ij_a6(s, i2, j2)[0U], + __m256i); + __m256i + v3h = + mm256_permute2x128_si256((int32_t)49, + get_ij_a6(s, i1, j1)[0U], + get_ij_a6(s, i3, j3)[0U], + __m256i); + __m256i v0 = mm256_unpacklo_epi64(v0l, v1h); + __m256i v1 = mm256_unpackhi_epi64(v0l, v1h); + __m256i v2 = mm256_unpacklo_epi64(v2l, v3h); + __m256i v3 = mm256_unpackhi_epi64(v2l, v3h); + mm256_storeu_si256_u8(Eurydice_slice_subslice_mut_7e(out0, + ( + KRML_CLITERAL(core_ops_range_Range_08){ + .start = start + (size_t)32U * i, + .end = start + (size_t)32U * (i + (size_t)1U) + } + )), + v0); + mm256_storeu_si256_u8(Eurydice_slice_subslice_mut_7e(out1, + ( + KRML_CLITERAL(core_ops_range_Range_08){ + .start = start + (size_t)32U * i, + .end = start + (size_t)32U * (i + (size_t)1U) + } + )), + v1); + mm256_storeu_si256_u8(Eurydice_slice_subslice_mut_7e(out2, + ( + KRML_CLITERAL(core_ops_range_Range_08){ + .start = start + (size_t)32U * i, + .end = start + (size_t)32U * (i + (size_t)1U) + } + )), + v2); + mm256_storeu_si256_u8(Eurydice_slice_subslice_mut_7e(out3, + ( + KRML_CLITERAL(core_ops_range_Range_08){ + .start = start + (size_t)32U * i, + .end = start + (size_t)32U * (i + (size_t)1U) + } + )), + v3); } KRML_HOST_EPRINTF("KaRaMeL abort at %s:%d\n%s\n", __FILE__, __LINE__, "panic!"); KRML_HOST_EXIT(255U); @@ -2074,7 +2045,6 @@ keccak4_ad( if (blocks == (size_t)0U) { squeeze4_17_5b(&s, out0, out1, out2, out3, (size_t)0U, outlen); - return; } else { @@ -2090,14 +2060,11 @@ keccak4_ad( keccakf1600_80_a6(&s); squeeze4_17_5b(&s, out0, out1, out2, out3, last, outlen - last); } - return; } + return; } - else - { - size_t i = uu____0.f0; - absorb_block_80_97(&s, data, i * (size_t)136U); - } + size_t i = uu____0.f0; + absorb_block_80_97(&s, data, i * (size_t)136U); } KRML_HOST_EPRINTF("KaRaMeL abort at %s:%d\n%s\n", __FILE__, __LINE__, "panic!"); KRML_HOST_EXIT(255U); @@ -2508,85 +2475,78 @@ store_block_3a( )), uint8_t); } - return; - } - else - { - return; } + return; } - else - { - size_t i = uu____0.f0; - size_t i0 = (size_t)4U * i / (size_t)5U; - size_t j0 = (size_t)4U * i % (size_t)5U; - size_t i1 = ((size_t)4U * i + (size_t)1U) / (size_t)5U; - size_t j1 = ((size_t)4U * i + (size_t)1U) % (size_t)5U; - size_t i2 = ((size_t)4U * i + (size_t)2U) / (size_t)5U; - size_t j2 = ((size_t)4U * i + (size_t)2U) % (size_t)5U; - size_t i3 = ((size_t)4U * i + (size_t)3U) / (size_t)5U; - size_t j3 = ((size_t)4U * i + (size_t)3U) % (size_t)5U; - __m256i - v0l = - mm256_permute2x128_si256((int32_t)32, - get_ij_a6(s, i0, j0)[0U], - get_ij_a6(s, i2, j2)[0U], - __m256i); - __m256i - v1h = - mm256_permute2x128_si256((int32_t)32, - get_ij_a6(s, i1, j1)[0U], - get_ij_a6(s, i3, j3)[0U], - __m256i); - __m256i - v2l = - mm256_permute2x128_si256((int32_t)49, - get_ij_a6(s, i0, j0)[0U], - get_ij_a6(s, i2, j2)[0U], - __m256i); - __m256i - v3h = - mm256_permute2x128_si256((int32_t)49, - get_ij_a6(s, i1, j1)[0U], - get_ij_a6(s, i3, j3)[0U], - __m256i); - __m256i v0 = mm256_unpacklo_epi64(v0l, v1h); - __m256i v1 = mm256_unpackhi_epi64(v0l, v1h); - __m256i v2 = mm256_unpacklo_epi64(v2l, v3h); - __m256i v3 = mm256_unpackhi_epi64(v2l, v3h); - mm256_storeu_si256_u8(Eurydice_slice_subslice_mut_7e(out0, - ( - KRML_CLITERAL(core_ops_range_Range_08){ - .start = start + (size_t)32U * i, - .end = start + (size_t)32U * (i + (size_t)1U) - } - )), - v0); - mm256_storeu_si256_u8(Eurydice_slice_subslice_mut_7e(out1, - ( - KRML_CLITERAL(core_ops_range_Range_08){ - .start = start + (size_t)32U * i, - .end = start + (size_t)32U * (i + (size_t)1U) - } - )), - v1); - mm256_storeu_si256_u8(Eurydice_slice_subslice_mut_7e(out2, - ( - KRML_CLITERAL(core_ops_range_Range_08){ - .start = start + (size_t)32U * i, - .end = start + (size_t)32U * (i + (size_t)1U) - } - )), - v2); - mm256_storeu_si256_u8(Eurydice_slice_subslice_mut_7e(out3, - ( - KRML_CLITERAL(core_ops_range_Range_08){ - .start = start + (size_t)32U * i, - .end = start + (size_t)32U * (i + (size_t)1U) - } - )), - v3); - } + size_t i = uu____0.f0; + size_t i0 = (size_t)4U * i / (size_t)5U; + size_t j0 = (size_t)4U * i % (size_t)5U; + size_t i1 = ((size_t)4U * i + (size_t)1U) / (size_t)5U; + size_t j1 = ((size_t)4U * i + (size_t)1U) % (size_t)5U; + size_t i2 = ((size_t)4U * i + (size_t)2U) / (size_t)5U; + size_t j2 = ((size_t)4U * i + (size_t)2U) % (size_t)5U; + size_t i3 = ((size_t)4U * i + (size_t)3U) / (size_t)5U; + size_t j3 = ((size_t)4U * i + (size_t)3U) % (size_t)5U; + __m256i + v0l = + mm256_permute2x128_si256((int32_t)32, + get_ij_a6(s, i0, j0)[0U], + get_ij_a6(s, i2, j2)[0U], + __m256i); + __m256i + v1h = + mm256_permute2x128_si256((int32_t)32, + get_ij_a6(s, i1, j1)[0U], + get_ij_a6(s, i3, j3)[0U], + __m256i); + __m256i + v2l = + mm256_permute2x128_si256((int32_t)49, + get_ij_a6(s, i0, j0)[0U], + get_ij_a6(s, i2, j2)[0U], + __m256i); + __m256i + v3h = + mm256_permute2x128_si256((int32_t)49, + get_ij_a6(s, i1, j1)[0U], + get_ij_a6(s, i3, j3)[0U], + __m256i); + __m256i v0 = mm256_unpacklo_epi64(v0l, v1h); + __m256i v1 = mm256_unpackhi_epi64(v0l, v1h); + __m256i v2 = mm256_unpacklo_epi64(v2l, v3h); + __m256i v3 = mm256_unpackhi_epi64(v2l, v3h); + mm256_storeu_si256_u8(Eurydice_slice_subslice_mut_7e(out0, + ( + KRML_CLITERAL(core_ops_range_Range_08){ + .start = start + (size_t)32U * i, + .end = start + (size_t)32U * (i + (size_t)1U) + } + )), + v0); + mm256_storeu_si256_u8(Eurydice_slice_subslice_mut_7e(out1, + ( + KRML_CLITERAL(core_ops_range_Range_08){ + .start = start + (size_t)32U * i, + .end = start + (size_t)32U * (i + (size_t)1U) + } + )), + v1); + mm256_storeu_si256_u8(Eurydice_slice_subslice_mut_7e(out2, + ( + KRML_CLITERAL(core_ops_range_Range_08){ + .start = start + (size_t)32U * i, + .end = start + (size_t)32U * (i + (size_t)1U) + } + )), + v2); + mm256_storeu_si256_u8(Eurydice_slice_subslice_mut_7e(out3, + ( + KRML_CLITERAL(core_ops_range_Range_08){ + .start = start + (size_t)32U * i, + .end = start + (size_t)32U * (i + (size_t)1U) + } + )), + v3); } KRML_HOST_EPRINTF("KaRaMeL abort at %s:%d\n%s\n", __FILE__, __LINE__, "panic!"); KRML_HOST_EXIT(255U); diff --git a/out/test-libcrux-no-const/libcrux_sha3_portable.c b/out/test-libcrux-no-const/libcrux_sha3_portable.c index 9c70d22c..c95e306d 100644 --- a/out/test-libcrux-no-const/libcrux_sha3_portable.c +++ b/out/test-libcrux-no-const/libcrux_sha3_portable.c @@ -189,22 +189,19 @@ libcrux_sha3_simd_portable_load_block_f8( } return; } - else - { - size_t i = uu____0.f0; - size_t offset = start + (size_t)8U * i; - Eurydice_array_u8x8 arr; - memcpy(arr.data, - Eurydice_slice_subslice_mut_7e(blocks, - (KRML_CLITERAL(core_ops_range_Range_08){ .start = offset, .end = offset + (size_t)8U })).ptr, - (size_t)8U * sizeof (uint8_t)); - Eurydice_array_u8x8 - uu____1 = - core_result_unwrap_26_ab(( - KRML_CLITERAL(core_result_Result_8e){ .tag = core_result_Ok, .val = { .case_Ok = arr } } - )); - state_flat.data[i] = core_num__u64__from_le_bytes(uu____1); - } + size_t i = uu____0.f0; + size_t offset = start + (size_t)8U * i; + Eurydice_array_u8x8 arr; + memcpy(arr.data, + Eurydice_slice_subslice_mut_7e(blocks, + (KRML_CLITERAL(core_ops_range_Range_08){ .start = offset, .end = offset + (size_t)8U })).ptr, + (size_t)8U * sizeof (uint8_t)); + Eurydice_array_u8x8 + uu____1 = + core_result_unwrap_26_ab(( + KRML_CLITERAL(core_result_Result_8e){ .tag = core_result_Ok, .val = { .case_Ok = arr } } + )); + state_flat.data[i] = core_num__u64__from_le_bytes(uu____1); } KRML_HOST_EPRINTF("KaRaMeL abort at %s:%d\n%s\n", __FILE__, __LINE__, "panic!"); KRML_HOST_EXIT(255U); @@ -1565,47 +1562,25 @@ with const generics KRML_MUSTINLINE void libcrux_sha3_generic_keccak_chi_80_04(Eurydice_arr_26 *self) { Eurydice_arr_26 old = self[0U]; - core_ops_range_Range_08 - iter = - core_iter_traits_collect__core__iter__traits__collect__IntoIterator_Clause1_Item__I__for_I__into_iter(( - KRML_CLITERAL(core_ops_range_Range_08){ .start = (size_t)0U, .end = (size_t)5U } - ), - core_ops_range_Range_08, - size_t, - core_ops_range_Range_08); - while (true) - { - core_option_Option_08 - uu____0 = - core_iter_range__core__iter__traits__iterator__Iterator_A__for_core__ops__range__Range_A__TraitClause_0___next(&iter, - size_t, - core_option_Option_08); - if (uu____0.tag == core_option_None) - { - break; - } - else - { - size_t i0 = uu____0.f0; - KRML_MAYBE_FOR5(i, - (size_t)0U, - (size_t)5U, - (size_t)1U, - size_t j = i; - libcrux_sha3_generic_keccak_set_80_04(self, - i0, - j, - libcrux_sha3_simd_portable_and_not_xor_d2(libcrux_sha3_generic_keccak_index_c2_04(self, - (KRML_CLITERAL(size_t_x2){ .fst = i0, .snd = j }))[0U], - libcrux_sha3_generic_keccak_index_c2_04(&old, - (KRML_CLITERAL(size_t_x2){ .fst = i0, .snd = (j + (size_t)2U) % (size_t)5U }))[0U], - libcrux_sha3_generic_keccak_index_c2_04(&old, - (KRML_CLITERAL(size_t_x2){ .fst = i0, .snd = (j + (size_t)1U) % (size_t)5U }))[0U]));); - continue; - } - KRML_HOST_EPRINTF("KaRaMeL abort at %s:%d\n%s\n", __FILE__, __LINE__, "panic!"); - KRML_HOST_EXIT(255U); - } + KRML_MAYBE_FOR5(i0, + (size_t)0U, + (size_t)5U, + (size_t)1U, + size_t i1 = i0; + KRML_MAYBE_FOR5(i, + (size_t)0U, + (size_t)5U, + (size_t)1U, + size_t j = i; + libcrux_sha3_generic_keccak_set_80_04(self, + i1, + j, + libcrux_sha3_simd_portable_and_not_xor_d2(libcrux_sha3_generic_keccak_index_c2_04(self, + (KRML_CLITERAL(size_t_x2){ .fst = i1, .snd = j }))[0U], + libcrux_sha3_generic_keccak_index_c2_04(&old, + (KRML_CLITERAL(size_t_x2){ .fst = i1, .snd = (j + (size_t)2U) % (size_t)5U }))[0U], + libcrux_sha3_generic_keccak_index_c2_04(&old, + (KRML_CLITERAL(size_t_x2){ .fst = i1, .snd = (j + (size_t)1U) % (size_t)5U }))[0U])););); } /** @@ -1830,7 +1805,6 @@ libcrux_sha3_generic_keccak_portable_keccak1_96( if (blocks == (size_t)0U) { libcrux_sha3_simd_portable_squeeze_13_f8(&s, out, (size_t)0U, outlen); - return; } else { @@ -1846,16 +1820,13 @@ libcrux_sha3_generic_keccak_portable_keccak1_96( libcrux_sha3_generic_keccak_keccakf1600_80_04(&s); libcrux_sha3_simd_portable_squeeze_13_f8(&s, out, last, outlen - last); } - return; } + return; } - else - { - size_t i = uu____0.f0; - /* original Rust expression is not an lvalue in C */ - Eurydice_arr_f9 lvalue = { .data = { data } }; - libcrux_sha3_generic_keccak_absorb_block_80_c6(&s, &lvalue, i * (size_t)72U); - } + size_t i = uu____0.f0; + /* original Rust expression is not an lvalue in C */ + Eurydice_arr_f9 lvalue = { .data = { data } }; + libcrux_sha3_generic_keccak_absorb_block_80_c6(&s, &lvalue, i * (size_t)72U); } KRML_HOST_EPRINTF("KaRaMeL abort at %s:%d\n%s\n", __FILE__, __LINE__, "panic!"); KRML_HOST_EXIT(255U); @@ -1917,22 +1888,19 @@ libcrux_sha3_simd_portable_load_block_5b( } return; } - else - { - size_t i = uu____0.f0; - size_t offset = start + (size_t)8U * i; - Eurydice_array_u8x8 arr; - memcpy(arr.data, - Eurydice_slice_subslice_mut_7e(blocks, - (KRML_CLITERAL(core_ops_range_Range_08){ .start = offset, .end = offset + (size_t)8U })).ptr, - (size_t)8U * sizeof (uint8_t)); - Eurydice_array_u8x8 - uu____1 = - core_result_unwrap_26_ab(( - KRML_CLITERAL(core_result_Result_8e){ .tag = core_result_Ok, .val = { .case_Ok = arr } } - )); - state_flat.data[i] = core_num__u64__from_le_bytes(uu____1); - } + size_t i = uu____0.f0; + size_t offset = start + (size_t)8U * i; + Eurydice_array_u8x8 arr; + memcpy(arr.data, + Eurydice_slice_subslice_mut_7e(blocks, + (KRML_CLITERAL(core_ops_range_Range_08){ .start = offset, .end = offset + (size_t)8U })).ptr, + (size_t)8U * sizeof (uint8_t)); + Eurydice_array_u8x8 + uu____1 = + core_result_unwrap_26_ab(( + KRML_CLITERAL(core_result_Result_8e){ .tag = core_result_Ok, .val = { .case_Ok = arr } } + )); + state_flat.data[i] = core_num__u64__from_le_bytes(uu____1); } KRML_HOST_EPRINTF("KaRaMeL abort at %s:%d\n%s\n", __FILE__, __LINE__, "panic!"); KRML_HOST_EXIT(255U); @@ -2170,7 +2138,6 @@ libcrux_sha3_generic_keccak_portable_keccak1_ad( if (blocks == (size_t)0U) { libcrux_sha3_simd_portable_squeeze_13_5b(&s, out, (size_t)0U, outlen); - return; } else { @@ -2186,16 +2153,13 @@ libcrux_sha3_generic_keccak_portable_keccak1_ad( libcrux_sha3_generic_keccak_keccakf1600_80_04(&s); libcrux_sha3_simd_portable_squeeze_13_5b(&s, out, last, outlen - last); } - return; } + return; } - else - { - size_t i = uu____0.f0; - /* original Rust expression is not an lvalue in C */ - Eurydice_arr_f9 lvalue = { .data = { data } }; - libcrux_sha3_generic_keccak_absorb_block_80_c60(&s, &lvalue, i * (size_t)136U); - } + size_t i = uu____0.f0; + /* original Rust expression is not an lvalue in C */ + Eurydice_arr_f9 lvalue = { .data = { data } }; + libcrux_sha3_generic_keccak_absorb_block_80_c60(&s, &lvalue, i * (size_t)136U); } KRML_HOST_EPRINTF("KaRaMeL abort at %s:%d\n%s\n", __FILE__, __LINE__, "panic!"); KRML_HOST_EXIT(255U); @@ -2328,7 +2292,6 @@ libcrux_sha3_generic_keccak_portable_keccak1_ad0( if (blocks == (size_t)0U) { libcrux_sha3_simd_portable_squeeze_13_5b(&s, out, (size_t)0U, outlen); - return; } else { @@ -2344,16 +2307,13 @@ libcrux_sha3_generic_keccak_portable_keccak1_ad0( libcrux_sha3_generic_keccak_keccakf1600_80_04(&s); libcrux_sha3_simd_portable_squeeze_13_5b(&s, out, last, outlen - last); } - return; } + return; } - else - { - size_t i = uu____0.f0; - /* original Rust expression is not an lvalue in C */ - Eurydice_arr_f9 lvalue = { .data = { data } }; - libcrux_sha3_generic_keccak_absorb_block_80_c60(&s, &lvalue, i * (size_t)136U); - } + size_t i = uu____0.f0; + /* original Rust expression is not an lvalue in C */ + Eurydice_arr_f9 lvalue = { .data = { data } }; + libcrux_sha3_generic_keccak_absorb_block_80_c60(&s, &lvalue, i * (size_t)136U); } KRML_HOST_EPRINTF("KaRaMeL abort at %s:%d\n%s\n", __FILE__, __LINE__, "panic!"); KRML_HOST_EXIT(255U); @@ -2423,22 +2383,19 @@ libcrux_sha3_simd_portable_load_block_3a( } return; } - else - { - size_t i = uu____0.f0; - size_t offset = start + (size_t)8U * i; - Eurydice_array_u8x8 arr; - memcpy(arr.data, - Eurydice_slice_subslice_mut_7e(blocks, - (KRML_CLITERAL(core_ops_range_Range_08){ .start = offset, .end = offset + (size_t)8U })).ptr, - (size_t)8U * sizeof (uint8_t)); - Eurydice_array_u8x8 - uu____1 = - core_result_unwrap_26_ab(( - KRML_CLITERAL(core_result_Result_8e){ .tag = core_result_Ok, .val = { .case_Ok = arr } } - )); - state_flat.data[i] = core_num__u64__from_le_bytes(uu____1); - } + size_t i = uu____0.f0; + size_t offset = start + (size_t)8U * i; + Eurydice_array_u8x8 arr; + memcpy(arr.data, + Eurydice_slice_subslice_mut_7e(blocks, + (KRML_CLITERAL(core_ops_range_Range_08){ .start = offset, .end = offset + (size_t)8U })).ptr, + (size_t)8U * sizeof (uint8_t)); + Eurydice_array_u8x8 + uu____1 = + core_result_unwrap_26_ab(( + KRML_CLITERAL(core_result_Result_8e){ .tag = core_result_Ok, .val = { .case_Ok = arr } } + )); + state_flat.data[i] = core_num__u64__from_le_bytes(uu____1); } KRML_HOST_EPRINTF("KaRaMeL abort at %s:%d\n%s\n", __FILE__, __LINE__, "panic!"); KRML_HOST_EXIT(255U); @@ -2747,22 +2704,19 @@ libcrux_sha3_simd_portable_load_block_2c( } return; } - else - { - size_t i = uu____0.f0; - size_t offset = start + (size_t)8U * i; - Eurydice_array_u8x8 arr; - memcpy(arr.data, - Eurydice_slice_subslice_mut_7e(blocks, - (KRML_CLITERAL(core_ops_range_Range_08){ .start = offset, .end = offset + (size_t)8U })).ptr, - (size_t)8U * sizeof (uint8_t)); - Eurydice_array_u8x8 - uu____1 = - core_result_unwrap_26_ab(( - KRML_CLITERAL(core_result_Result_8e){ .tag = core_result_Ok, .val = { .case_Ok = arr } } - )); - state_flat.data[i] = core_num__u64__from_le_bytes(uu____1); - } + size_t i = uu____0.f0; + size_t offset = start + (size_t)8U * i; + Eurydice_array_u8x8 arr; + memcpy(arr.data, + Eurydice_slice_subslice_mut_7e(blocks, + (KRML_CLITERAL(core_ops_range_Range_08){ .start = offset, .end = offset + (size_t)8U })).ptr, + (size_t)8U * sizeof (uint8_t)); + Eurydice_array_u8x8 + uu____1 = + core_result_unwrap_26_ab(( + KRML_CLITERAL(core_result_Result_8e){ .tag = core_result_Ok, .val = { .case_Ok = arr } } + )); + state_flat.data[i] = core_num__u64__from_le_bytes(uu____1); } KRML_HOST_EPRINTF("KaRaMeL abort at %s:%d\n%s\n", __FILE__, __LINE__, "panic!"); KRML_HOST_EXIT(255U); @@ -3000,7 +2954,6 @@ libcrux_sha3_generic_keccak_portable_keccak1_1e( if (blocks == (size_t)0U) { libcrux_sha3_simd_portable_squeeze_13_2c(&s, out, (size_t)0U, outlen); - return; } else { @@ -3016,16 +2969,13 @@ libcrux_sha3_generic_keccak_portable_keccak1_1e( libcrux_sha3_generic_keccak_keccakf1600_80_04(&s); libcrux_sha3_simd_portable_squeeze_13_2c(&s, out, last, outlen - last); } - return; } + return; } - else - { - size_t i = uu____0.f0; - /* original Rust expression is not an lvalue in C */ - Eurydice_arr_f9 lvalue = { .data = { data } }; - libcrux_sha3_generic_keccak_absorb_block_80_c61(&s, &lvalue, i * (size_t)144U); - } + size_t i = uu____0.f0; + /* original Rust expression is not an lvalue in C */ + Eurydice_arr_f9 lvalue = { .data = { data } }; + libcrux_sha3_generic_keccak_absorb_block_80_c61(&s, &lvalue, i * (size_t)144U); } KRML_HOST_EPRINTF("KaRaMeL abort at %s:%d\n%s\n", __FILE__, __LINE__, "panic!"); KRML_HOST_EXIT(255U); @@ -3087,22 +3037,19 @@ libcrux_sha3_simd_portable_load_block_7a( } return; } - else - { - size_t i = uu____0.f0; - size_t offset = start + (size_t)8U * i; - Eurydice_array_u8x8 arr; - memcpy(arr.data, - Eurydice_slice_subslice_mut_7e(blocks, - (KRML_CLITERAL(core_ops_range_Range_08){ .start = offset, .end = offset + (size_t)8U })).ptr, - (size_t)8U * sizeof (uint8_t)); - Eurydice_array_u8x8 - uu____1 = - core_result_unwrap_26_ab(( - KRML_CLITERAL(core_result_Result_8e){ .tag = core_result_Ok, .val = { .case_Ok = arr } } - )); - state_flat.data[i] = core_num__u64__from_le_bytes(uu____1); - } + size_t i = uu____0.f0; + size_t offset = start + (size_t)8U * i; + Eurydice_array_u8x8 arr; + memcpy(arr.data, + Eurydice_slice_subslice_mut_7e(blocks, + (KRML_CLITERAL(core_ops_range_Range_08){ .start = offset, .end = offset + (size_t)8U })).ptr, + (size_t)8U * sizeof (uint8_t)); + Eurydice_array_u8x8 + uu____1 = + core_result_unwrap_26_ab(( + KRML_CLITERAL(core_result_Result_8e){ .tag = core_result_Ok, .val = { .case_Ok = arr } } + )); + state_flat.data[i] = core_num__u64__from_le_bytes(uu____1); } KRML_HOST_EPRINTF("KaRaMeL abort at %s:%d\n%s\n", __FILE__, __LINE__, "panic!"); KRML_HOST_EXIT(255U); @@ -3340,7 +3287,6 @@ libcrux_sha3_generic_keccak_portable_keccak1_7c( if (blocks == (size_t)0U) { libcrux_sha3_simd_portable_squeeze_13_7a(&s, out, (size_t)0U, outlen); - return; } else { @@ -3356,16 +3302,13 @@ libcrux_sha3_generic_keccak_portable_keccak1_7c( libcrux_sha3_generic_keccak_keccakf1600_80_04(&s); libcrux_sha3_simd_portable_squeeze_13_7a(&s, out, last, outlen - last); } - return; } + return; } - else - { - size_t i = uu____0.f0; - /* original Rust expression is not an lvalue in C */ - Eurydice_arr_f9 lvalue = { .data = { data } }; - libcrux_sha3_generic_keccak_absorb_block_80_c62(&s, &lvalue, i * (size_t)104U); - } + size_t i = uu____0.f0; + /* original Rust expression is not an lvalue in C */ + Eurydice_arr_f9 lvalue = { .data = { data } }; + libcrux_sha3_generic_keccak_absorb_block_80_c62(&s, &lvalue, i * (size_t)104U); } KRML_HOST_EPRINTF("KaRaMeL abort at %s:%d\n%s\n", __FILE__, __LINE__, "panic!"); KRML_HOST_EXIT(255U); @@ -3557,7 +3500,6 @@ libcrux_sha3_generic_keccak_portable_keccak1_c6( if (blocks == (size_t)0U) { libcrux_sha3_simd_portable_squeeze_13_3a(&s, out, (size_t)0U, outlen); - return; } else { @@ -3573,16 +3515,13 @@ libcrux_sha3_generic_keccak_portable_keccak1_c6( libcrux_sha3_generic_keccak_keccakf1600_80_04(&s); libcrux_sha3_simd_portable_squeeze_13_3a(&s, out, last, outlen - last); } - return; } + return; } - else - { - size_t i = uu____0.f0; - /* original Rust expression is not an lvalue in C */ - Eurydice_arr_f9 lvalue = { .data = { data } }; - libcrux_sha3_generic_keccak_absorb_block_80_c63(&s, &lvalue, i * (size_t)168U); - } + size_t i = uu____0.f0; + /* original Rust expression is not an lvalue in C */ + Eurydice_arr_f9 lvalue = { .data = { data } }; + libcrux_sha3_generic_keccak_absorb_block_80_c63(&s, &lvalue, i * (size_t)168U); } KRML_HOST_EPRINTF("KaRaMeL abort at %s:%d\n%s\n", __FILE__, __LINE__, "panic!"); KRML_HOST_EXIT(255U); diff --git a/out/test-libcrux/libcrux_sha3_avx2.c b/out/test-libcrux/libcrux_sha3_avx2.c index 1f865d78..e6babf52 100644 --- a/out/test-libcrux/libcrux_sha3_avx2.c +++ b/out/test-libcrux/libcrux_sha3_avx2.c @@ -1641,46 +1641,24 @@ with const generics static KRML_MUSTINLINE void chi_80_a6(Eurydice_arr_05 *self) { Eurydice_arr_05 old = self[0U]; - core_ops_range_Range_08 - iter = - core_iter_traits_collect__core__iter__traits__collect__IntoIterator_Clause1_Item__I__for_I__into_iter(( - KRML_CLITERAL(core_ops_range_Range_08){ .start = (size_t)0U, .end = (size_t)5U } - ), - core_ops_range_Range_08, - size_t, - core_ops_range_Range_08); - while (true) - { - core_option_Option_08 - uu____0 = - core_iter_range__core__iter__traits__iterator__Iterator_A__for_core__ops__range__Range_A__TraitClause_0___next(&iter, - size_t, - core_option_Option_08); - if (uu____0.tag == core_option_None) - { - break; - } - else - { - size_t i0 = uu____0.f0; - KRML_MAYBE_FOR5(i, - (size_t)0U, - (size_t)5U, - (size_t)1U, - size_t j = i; - set_80_a6(self, - i0, - j, - and_not_xor_b0(index_c2_a6(self, (KRML_CLITERAL(size_t_x2){ .fst = i0, .snd = j }))[0U], - index_c2_a6(&old, - (KRML_CLITERAL(size_t_x2){ .fst = i0, .snd = (j + (size_t)2U) % (size_t)5U }))[0U], - index_c2_a6(&old, - (KRML_CLITERAL(size_t_x2){ .fst = i0, .snd = (j + (size_t)1U) % (size_t)5U }))[0U]));); - continue; - } - KRML_HOST_EPRINTF("KaRaMeL abort at %s:%d\n%s\n", __FILE__, __LINE__, "panic!"); - KRML_HOST_EXIT(255U); - } + KRML_MAYBE_FOR5(i0, + (size_t)0U, + (size_t)5U, + (size_t)1U, + size_t i1 = i0; + KRML_MAYBE_FOR5(i, + (size_t)0U, + (size_t)5U, + (size_t)1U, + size_t j = i; + set_80_a6(self, + i1, + j, + and_not_xor_b0(index_c2_a6(self, (KRML_CLITERAL(size_t_x2){ .fst = i1, .snd = j }))[0U], + index_c2_a6(&old, + (KRML_CLITERAL(size_t_x2){ .fst = i1, .snd = (j + (size_t)2U) % (size_t)5U }))[0U], + index_c2_a6(&old, + (KRML_CLITERAL(size_t_x2){ .fst = i1, .snd = (j + (size_t)1U) % (size_t)5U }))[0U])););); } /** @@ -1898,85 +1876,78 @@ store_block_5b( )), uint8_t); } - return; } - else - { - return; - } - } - else - { - size_t i = uu____0.f0; - size_t i0 = (size_t)4U * i / (size_t)5U; - size_t j0 = (size_t)4U * i % (size_t)5U; - size_t i1 = ((size_t)4U * i + (size_t)1U) / (size_t)5U; - size_t j1 = ((size_t)4U * i + (size_t)1U) % (size_t)5U; - size_t i2 = ((size_t)4U * i + (size_t)2U) / (size_t)5U; - size_t j2 = ((size_t)4U * i + (size_t)2U) % (size_t)5U; - size_t i3 = ((size_t)4U * i + (size_t)3U) / (size_t)5U; - size_t j3 = ((size_t)4U * i + (size_t)3U) % (size_t)5U; - __m256i - v0l = - mm256_permute2x128_si256((int32_t)32, - get_ij_a6(s, i0, j0)[0U], - get_ij_a6(s, i2, j2)[0U], - __m256i); - __m256i - v1h = - mm256_permute2x128_si256((int32_t)32, - get_ij_a6(s, i1, j1)[0U], - get_ij_a6(s, i3, j3)[0U], - __m256i); - __m256i - v2l = - mm256_permute2x128_si256((int32_t)49, - get_ij_a6(s, i0, j0)[0U], - get_ij_a6(s, i2, j2)[0U], - __m256i); - __m256i - v3h = - mm256_permute2x128_si256((int32_t)49, - get_ij_a6(s, i1, j1)[0U], - get_ij_a6(s, i3, j3)[0U], - __m256i); - __m256i v0 = mm256_unpacklo_epi64(v0l, v1h); - __m256i v1 = mm256_unpackhi_epi64(v0l, v1h); - __m256i v2 = mm256_unpacklo_epi64(v2l, v3h); - __m256i v3 = mm256_unpackhi_epi64(v2l, v3h); - mm256_storeu_si256_u8(Eurydice_slice_subslice_mut_7e(out0, - ( - KRML_CLITERAL(core_ops_range_Range_08){ - .start = start + (size_t)32U * i, - .end = start + (size_t)32U * (i + (size_t)1U) - } - )), - v0); - mm256_storeu_si256_u8(Eurydice_slice_subslice_mut_7e(out1, - ( - KRML_CLITERAL(core_ops_range_Range_08){ - .start = start + (size_t)32U * i, - .end = start + (size_t)32U * (i + (size_t)1U) - } - )), - v1); - mm256_storeu_si256_u8(Eurydice_slice_subslice_mut_7e(out2, - ( - KRML_CLITERAL(core_ops_range_Range_08){ - .start = start + (size_t)32U * i, - .end = start + (size_t)32U * (i + (size_t)1U) - } - )), - v2); - mm256_storeu_si256_u8(Eurydice_slice_subslice_mut_7e(out3, - ( - KRML_CLITERAL(core_ops_range_Range_08){ - .start = start + (size_t)32U * i, - .end = start + (size_t)32U * (i + (size_t)1U) - } - )), - v3); + return; } + size_t i = uu____0.f0; + size_t i0 = (size_t)4U * i / (size_t)5U; + size_t j0 = (size_t)4U * i % (size_t)5U; + size_t i1 = ((size_t)4U * i + (size_t)1U) / (size_t)5U; + size_t j1 = ((size_t)4U * i + (size_t)1U) % (size_t)5U; + size_t i2 = ((size_t)4U * i + (size_t)2U) / (size_t)5U; + size_t j2 = ((size_t)4U * i + (size_t)2U) % (size_t)5U; + size_t i3 = ((size_t)4U * i + (size_t)3U) / (size_t)5U; + size_t j3 = ((size_t)4U * i + (size_t)3U) % (size_t)5U; + __m256i + v0l = + mm256_permute2x128_si256((int32_t)32, + get_ij_a6(s, i0, j0)[0U], + get_ij_a6(s, i2, j2)[0U], + __m256i); + __m256i + v1h = + mm256_permute2x128_si256((int32_t)32, + get_ij_a6(s, i1, j1)[0U], + get_ij_a6(s, i3, j3)[0U], + __m256i); + __m256i + v2l = + mm256_permute2x128_si256((int32_t)49, + get_ij_a6(s, i0, j0)[0U], + get_ij_a6(s, i2, j2)[0U], + __m256i); + __m256i + v3h = + mm256_permute2x128_si256((int32_t)49, + get_ij_a6(s, i1, j1)[0U], + get_ij_a6(s, i3, j3)[0U], + __m256i); + __m256i v0 = mm256_unpacklo_epi64(v0l, v1h); + __m256i v1 = mm256_unpackhi_epi64(v0l, v1h); + __m256i v2 = mm256_unpacklo_epi64(v2l, v3h); + __m256i v3 = mm256_unpackhi_epi64(v2l, v3h); + mm256_storeu_si256_u8(Eurydice_slice_subslice_mut_7e(out0, + ( + KRML_CLITERAL(core_ops_range_Range_08){ + .start = start + (size_t)32U * i, + .end = start + (size_t)32U * (i + (size_t)1U) + } + )), + v0); + mm256_storeu_si256_u8(Eurydice_slice_subslice_mut_7e(out1, + ( + KRML_CLITERAL(core_ops_range_Range_08){ + .start = start + (size_t)32U * i, + .end = start + (size_t)32U * (i + (size_t)1U) + } + )), + v1); + mm256_storeu_si256_u8(Eurydice_slice_subslice_mut_7e(out2, + ( + KRML_CLITERAL(core_ops_range_Range_08){ + .start = start + (size_t)32U * i, + .end = start + (size_t)32U * (i + (size_t)1U) + } + )), + v2); + mm256_storeu_si256_u8(Eurydice_slice_subslice_mut_7e(out3, + ( + KRML_CLITERAL(core_ops_range_Range_08){ + .start = start + (size_t)32U * i, + .end = start + (size_t)32U * (i + (size_t)1U) + } + )), + v3); } KRML_HOST_EPRINTF("KaRaMeL abort at %s:%d\n%s\n", __FILE__, __LINE__, "panic!"); KRML_HOST_EXIT(255U); @@ -2079,7 +2050,6 @@ keccak4_ad( if (blocks == (size_t)0U) { squeeze4_17_5b(&s, out0, out1, out2, out3, (size_t)0U, outlen); - return; } else { @@ -2095,14 +2065,11 @@ keccak4_ad( keccakf1600_80_a6(&s); squeeze4_17_5b(&s, out0, out1, out2, out3, last, outlen - last); } - return; } + return; } - else - { - size_t i = uu____0.f0; - absorb_block_80_97(&s, data, i * (size_t)136U); - } + size_t i = uu____0.f0; + absorb_block_80_97(&s, data, i * (size_t)136U); } KRML_HOST_EPRINTF("KaRaMeL abort at %s:%d\n%s\n", __FILE__, __LINE__, "panic!"); KRML_HOST_EXIT(255U); @@ -2518,85 +2485,78 @@ store_block_3a( )), uint8_t); } - return; - } - else - { - return; } + return; } - else - { - size_t i = uu____0.f0; - size_t i0 = (size_t)4U * i / (size_t)5U; - size_t j0 = (size_t)4U * i % (size_t)5U; - size_t i1 = ((size_t)4U * i + (size_t)1U) / (size_t)5U; - size_t j1 = ((size_t)4U * i + (size_t)1U) % (size_t)5U; - size_t i2 = ((size_t)4U * i + (size_t)2U) / (size_t)5U; - size_t j2 = ((size_t)4U * i + (size_t)2U) % (size_t)5U; - size_t i3 = ((size_t)4U * i + (size_t)3U) / (size_t)5U; - size_t j3 = ((size_t)4U * i + (size_t)3U) % (size_t)5U; - __m256i - v0l = - mm256_permute2x128_si256((int32_t)32, - get_ij_a6(s, i0, j0)[0U], - get_ij_a6(s, i2, j2)[0U], - __m256i); - __m256i - v1h = - mm256_permute2x128_si256((int32_t)32, - get_ij_a6(s, i1, j1)[0U], - get_ij_a6(s, i3, j3)[0U], - __m256i); - __m256i - v2l = - mm256_permute2x128_si256((int32_t)49, - get_ij_a6(s, i0, j0)[0U], - get_ij_a6(s, i2, j2)[0U], - __m256i); - __m256i - v3h = - mm256_permute2x128_si256((int32_t)49, - get_ij_a6(s, i1, j1)[0U], - get_ij_a6(s, i3, j3)[0U], - __m256i); - __m256i v0 = mm256_unpacklo_epi64(v0l, v1h); - __m256i v1 = mm256_unpackhi_epi64(v0l, v1h); - __m256i v2 = mm256_unpacklo_epi64(v2l, v3h); - __m256i v3 = mm256_unpackhi_epi64(v2l, v3h); - mm256_storeu_si256_u8(Eurydice_slice_subslice_mut_7e(out0, - ( - KRML_CLITERAL(core_ops_range_Range_08){ - .start = start + (size_t)32U * i, - .end = start + (size_t)32U * (i + (size_t)1U) - } - )), - v0); - mm256_storeu_si256_u8(Eurydice_slice_subslice_mut_7e(out1, - ( - KRML_CLITERAL(core_ops_range_Range_08){ - .start = start + (size_t)32U * i, - .end = start + (size_t)32U * (i + (size_t)1U) - } - )), - v1); - mm256_storeu_si256_u8(Eurydice_slice_subslice_mut_7e(out2, - ( - KRML_CLITERAL(core_ops_range_Range_08){ - .start = start + (size_t)32U * i, - .end = start + (size_t)32U * (i + (size_t)1U) - } - )), - v2); - mm256_storeu_si256_u8(Eurydice_slice_subslice_mut_7e(out3, - ( - KRML_CLITERAL(core_ops_range_Range_08){ - .start = start + (size_t)32U * i, - .end = start + (size_t)32U * (i + (size_t)1U) - } - )), - v3); - } + size_t i = uu____0.f0; + size_t i0 = (size_t)4U * i / (size_t)5U; + size_t j0 = (size_t)4U * i % (size_t)5U; + size_t i1 = ((size_t)4U * i + (size_t)1U) / (size_t)5U; + size_t j1 = ((size_t)4U * i + (size_t)1U) % (size_t)5U; + size_t i2 = ((size_t)4U * i + (size_t)2U) / (size_t)5U; + size_t j2 = ((size_t)4U * i + (size_t)2U) % (size_t)5U; + size_t i3 = ((size_t)4U * i + (size_t)3U) / (size_t)5U; + size_t j3 = ((size_t)4U * i + (size_t)3U) % (size_t)5U; + __m256i + v0l = + mm256_permute2x128_si256((int32_t)32, + get_ij_a6(s, i0, j0)[0U], + get_ij_a6(s, i2, j2)[0U], + __m256i); + __m256i + v1h = + mm256_permute2x128_si256((int32_t)32, + get_ij_a6(s, i1, j1)[0U], + get_ij_a6(s, i3, j3)[0U], + __m256i); + __m256i + v2l = + mm256_permute2x128_si256((int32_t)49, + get_ij_a6(s, i0, j0)[0U], + get_ij_a6(s, i2, j2)[0U], + __m256i); + __m256i + v3h = + mm256_permute2x128_si256((int32_t)49, + get_ij_a6(s, i1, j1)[0U], + get_ij_a6(s, i3, j3)[0U], + __m256i); + __m256i v0 = mm256_unpacklo_epi64(v0l, v1h); + __m256i v1 = mm256_unpackhi_epi64(v0l, v1h); + __m256i v2 = mm256_unpacklo_epi64(v2l, v3h); + __m256i v3 = mm256_unpackhi_epi64(v2l, v3h); + mm256_storeu_si256_u8(Eurydice_slice_subslice_mut_7e(out0, + ( + KRML_CLITERAL(core_ops_range_Range_08){ + .start = start + (size_t)32U * i, + .end = start + (size_t)32U * (i + (size_t)1U) + } + )), + v0); + mm256_storeu_si256_u8(Eurydice_slice_subslice_mut_7e(out1, + ( + KRML_CLITERAL(core_ops_range_Range_08){ + .start = start + (size_t)32U * i, + .end = start + (size_t)32U * (i + (size_t)1U) + } + )), + v1); + mm256_storeu_si256_u8(Eurydice_slice_subslice_mut_7e(out2, + ( + KRML_CLITERAL(core_ops_range_Range_08){ + .start = start + (size_t)32U * i, + .end = start + (size_t)32U * (i + (size_t)1U) + } + )), + v2); + mm256_storeu_si256_u8(Eurydice_slice_subslice_mut_7e(out3, + ( + KRML_CLITERAL(core_ops_range_Range_08){ + .start = start + (size_t)32U * i, + .end = start + (size_t)32U * (i + (size_t)1U) + } + )), + v3); } KRML_HOST_EPRINTF("KaRaMeL abort at %s:%d\n%s\n", __FILE__, __LINE__, "panic!"); KRML_HOST_EXIT(255U); diff --git a/out/test-libcrux/libcrux_sha3_portable.c b/out/test-libcrux/libcrux_sha3_portable.c index 66f36402..a018565d 100644 --- a/out/test-libcrux/libcrux_sha3_portable.c +++ b/out/test-libcrux/libcrux_sha3_portable.c @@ -190,22 +190,19 @@ libcrux_sha3_simd_portable_load_block_f8( } return; } - else - { - size_t i = uu____0.f0; - size_t offset = start + (size_t)8U * i; - Eurydice_array_u8x8 arr; - memcpy(arr.data, - Eurydice_slice_subslice_shared_7e(blocks, - (KRML_CLITERAL(core_ops_range_Range_08){ .start = offset, .end = offset + (size_t)8U })).ptr, - (size_t)8U * sizeof (uint8_t)); - Eurydice_array_u8x8 - uu____1 = - core_result_unwrap_26_ab(( - KRML_CLITERAL(core_result_Result_8e){ .tag = core_result_Ok, .val = { .case_Ok = arr } } - )); - state_flat.data[i] = core_num__u64__from_le_bytes(uu____1); - } + size_t i = uu____0.f0; + size_t offset = start + (size_t)8U * i; + Eurydice_array_u8x8 arr; + memcpy(arr.data, + Eurydice_slice_subslice_shared_7e(blocks, + (KRML_CLITERAL(core_ops_range_Range_08){ .start = offset, .end = offset + (size_t)8U })).ptr, + (size_t)8U * sizeof (uint8_t)); + Eurydice_array_u8x8 + uu____1 = + core_result_unwrap_26_ab(( + KRML_CLITERAL(core_result_Result_8e){ .tag = core_result_Ok, .val = { .case_Ok = arr } } + )); + state_flat.data[i] = core_num__u64__from_le_bytes(uu____1); } KRML_HOST_EPRINTF("KaRaMeL abort at %s:%d\n%s\n", __FILE__, __LINE__, "panic!"); KRML_HOST_EXIT(255U); @@ -1568,47 +1565,25 @@ with const generics KRML_MUSTINLINE void libcrux_sha3_generic_keccak_chi_80_04(Eurydice_arr_26 *self) { Eurydice_arr_26 old = self[0U]; - core_ops_range_Range_08 - iter = - core_iter_traits_collect__core__iter__traits__collect__IntoIterator_Clause1_Item__I__for_I__into_iter(( - KRML_CLITERAL(core_ops_range_Range_08){ .start = (size_t)0U, .end = (size_t)5U } - ), - core_ops_range_Range_08, - size_t, - core_ops_range_Range_08); - while (true) - { - core_option_Option_08 - uu____0 = - core_iter_range__core__iter__traits__iterator__Iterator_A__for_core__ops__range__Range_A__TraitClause_0___next(&iter, - size_t, - core_option_Option_08); - if (uu____0.tag == core_option_None) - { - break; - } - else - { - size_t i0 = uu____0.f0; - KRML_MAYBE_FOR5(i, - (size_t)0U, - (size_t)5U, - (size_t)1U, - size_t j = i; - libcrux_sha3_generic_keccak_set_80_04(self, - i0, - j, - libcrux_sha3_simd_portable_and_not_xor_d2(libcrux_sha3_generic_keccak_index_c2_04(self, - (KRML_CLITERAL(size_t_x2){ .fst = i0, .snd = j }))[0U], - libcrux_sha3_generic_keccak_index_c2_04(&old, - (KRML_CLITERAL(size_t_x2){ .fst = i0, .snd = (j + (size_t)2U) % (size_t)5U }))[0U], - libcrux_sha3_generic_keccak_index_c2_04(&old, - (KRML_CLITERAL(size_t_x2){ .fst = i0, .snd = (j + (size_t)1U) % (size_t)5U }))[0U]));); - continue; - } - KRML_HOST_EPRINTF("KaRaMeL abort at %s:%d\n%s\n", __FILE__, __LINE__, "panic!"); - KRML_HOST_EXIT(255U); - } + KRML_MAYBE_FOR5(i0, + (size_t)0U, + (size_t)5U, + (size_t)1U, + size_t i1 = i0; + KRML_MAYBE_FOR5(i, + (size_t)0U, + (size_t)5U, + (size_t)1U, + size_t j = i; + libcrux_sha3_generic_keccak_set_80_04(self, + i1, + j, + libcrux_sha3_simd_portable_and_not_xor_d2(libcrux_sha3_generic_keccak_index_c2_04(self, + (KRML_CLITERAL(size_t_x2){ .fst = i1, .snd = j }))[0U], + libcrux_sha3_generic_keccak_index_c2_04(&old, + (KRML_CLITERAL(size_t_x2){ .fst = i1, .snd = (j + (size_t)2U) % (size_t)5U }))[0U], + libcrux_sha3_generic_keccak_index_c2_04(&old, + (KRML_CLITERAL(size_t_x2){ .fst = i1, .snd = (j + (size_t)1U) % (size_t)5U }))[0U])););); } /** @@ -1833,7 +1808,6 @@ libcrux_sha3_generic_keccak_portable_keccak1_96( if (blocks == (size_t)0U) { libcrux_sha3_simd_portable_squeeze_13_f8(&s, out, (size_t)0U, outlen); - return; } else { @@ -1849,16 +1823,13 @@ libcrux_sha3_generic_keccak_portable_keccak1_96( libcrux_sha3_generic_keccak_keccakf1600_80_04(&s); libcrux_sha3_simd_portable_squeeze_13_f8(&s, out, last, outlen - last); } - return; } + return; } - else - { - size_t i = uu____0.f0; - /* original Rust expression is not an lvalue in C */ - Eurydice_arr_06 lvalue = { .data = { data } }; - libcrux_sha3_generic_keccak_absorb_block_80_c6(&s, &lvalue, i * (size_t)72U); - } + size_t i = uu____0.f0; + /* original Rust expression is not an lvalue in C */ + Eurydice_arr_06 lvalue = { .data = { data } }; + libcrux_sha3_generic_keccak_absorb_block_80_c6(&s, &lvalue, i * (size_t)72U); } KRML_HOST_EPRINTF("KaRaMeL abort at %s:%d\n%s\n", __FILE__, __LINE__, "panic!"); KRML_HOST_EXIT(255U); @@ -1920,22 +1891,19 @@ libcrux_sha3_simd_portable_load_block_5b( } return; } - else - { - size_t i = uu____0.f0; - size_t offset = start + (size_t)8U * i; - Eurydice_array_u8x8 arr; - memcpy(arr.data, - Eurydice_slice_subslice_shared_7e(blocks, - (KRML_CLITERAL(core_ops_range_Range_08){ .start = offset, .end = offset + (size_t)8U })).ptr, - (size_t)8U * sizeof (uint8_t)); - Eurydice_array_u8x8 - uu____1 = - core_result_unwrap_26_ab(( - KRML_CLITERAL(core_result_Result_8e){ .tag = core_result_Ok, .val = { .case_Ok = arr } } - )); - state_flat.data[i] = core_num__u64__from_le_bytes(uu____1); - } + size_t i = uu____0.f0; + size_t offset = start + (size_t)8U * i; + Eurydice_array_u8x8 arr; + memcpy(arr.data, + Eurydice_slice_subslice_shared_7e(blocks, + (KRML_CLITERAL(core_ops_range_Range_08){ .start = offset, .end = offset + (size_t)8U })).ptr, + (size_t)8U * sizeof (uint8_t)); + Eurydice_array_u8x8 + uu____1 = + core_result_unwrap_26_ab(( + KRML_CLITERAL(core_result_Result_8e){ .tag = core_result_Ok, .val = { .case_Ok = arr } } + )); + state_flat.data[i] = core_num__u64__from_le_bytes(uu____1); } KRML_HOST_EPRINTF("KaRaMeL abort at %s:%d\n%s\n", __FILE__, __LINE__, "panic!"); KRML_HOST_EXIT(255U); @@ -2173,7 +2141,6 @@ libcrux_sha3_generic_keccak_portable_keccak1_ad( if (blocks == (size_t)0U) { libcrux_sha3_simd_portable_squeeze_13_5b(&s, out, (size_t)0U, outlen); - return; } else { @@ -2189,16 +2156,13 @@ libcrux_sha3_generic_keccak_portable_keccak1_ad( libcrux_sha3_generic_keccak_keccakf1600_80_04(&s); libcrux_sha3_simd_portable_squeeze_13_5b(&s, out, last, outlen - last); } - return; } + return; } - else - { - size_t i = uu____0.f0; - /* original Rust expression is not an lvalue in C */ - Eurydice_arr_06 lvalue = { .data = { data } }; - libcrux_sha3_generic_keccak_absorb_block_80_c60(&s, &lvalue, i * (size_t)136U); - } + size_t i = uu____0.f0; + /* original Rust expression is not an lvalue in C */ + Eurydice_arr_06 lvalue = { .data = { data } }; + libcrux_sha3_generic_keccak_absorb_block_80_c60(&s, &lvalue, i * (size_t)136U); } KRML_HOST_EPRINTF("KaRaMeL abort at %s:%d\n%s\n", __FILE__, __LINE__, "panic!"); KRML_HOST_EXIT(255U); @@ -2331,7 +2295,6 @@ libcrux_sha3_generic_keccak_portable_keccak1_ad0( if (blocks == (size_t)0U) { libcrux_sha3_simd_portable_squeeze_13_5b(&s, out, (size_t)0U, outlen); - return; } else { @@ -2347,16 +2310,13 @@ libcrux_sha3_generic_keccak_portable_keccak1_ad0( libcrux_sha3_generic_keccak_keccakf1600_80_04(&s); libcrux_sha3_simd_portable_squeeze_13_5b(&s, out, last, outlen - last); } - return; } + return; } - else - { - size_t i = uu____0.f0; - /* original Rust expression is not an lvalue in C */ - Eurydice_arr_06 lvalue = { .data = { data } }; - libcrux_sha3_generic_keccak_absorb_block_80_c60(&s, &lvalue, i * (size_t)136U); - } + size_t i = uu____0.f0; + /* original Rust expression is not an lvalue in C */ + Eurydice_arr_06 lvalue = { .data = { data } }; + libcrux_sha3_generic_keccak_absorb_block_80_c60(&s, &lvalue, i * (size_t)136U); } KRML_HOST_EPRINTF("KaRaMeL abort at %s:%d\n%s\n", __FILE__, __LINE__, "panic!"); KRML_HOST_EXIT(255U); @@ -2426,22 +2386,19 @@ libcrux_sha3_simd_portable_load_block_3a( } return; } - else - { - size_t i = uu____0.f0; - size_t offset = start + (size_t)8U * i; - Eurydice_array_u8x8 arr; - memcpy(arr.data, - Eurydice_slice_subslice_shared_7e(blocks, - (KRML_CLITERAL(core_ops_range_Range_08){ .start = offset, .end = offset + (size_t)8U })).ptr, - (size_t)8U * sizeof (uint8_t)); - Eurydice_array_u8x8 - uu____1 = - core_result_unwrap_26_ab(( - KRML_CLITERAL(core_result_Result_8e){ .tag = core_result_Ok, .val = { .case_Ok = arr } } - )); - state_flat.data[i] = core_num__u64__from_le_bytes(uu____1); - } + size_t i = uu____0.f0; + size_t offset = start + (size_t)8U * i; + Eurydice_array_u8x8 arr; + memcpy(arr.data, + Eurydice_slice_subslice_shared_7e(blocks, + (KRML_CLITERAL(core_ops_range_Range_08){ .start = offset, .end = offset + (size_t)8U })).ptr, + (size_t)8U * sizeof (uint8_t)); + Eurydice_array_u8x8 + uu____1 = + core_result_unwrap_26_ab(( + KRML_CLITERAL(core_result_Result_8e){ .tag = core_result_Ok, .val = { .case_Ok = arr } } + )); + state_flat.data[i] = core_num__u64__from_le_bytes(uu____1); } KRML_HOST_EPRINTF("KaRaMeL abort at %s:%d\n%s\n", __FILE__, __LINE__, "panic!"); KRML_HOST_EXIT(255U); @@ -2750,22 +2707,19 @@ libcrux_sha3_simd_portable_load_block_2c( } return; } - else - { - size_t i = uu____0.f0; - size_t offset = start + (size_t)8U * i; - Eurydice_array_u8x8 arr; - memcpy(arr.data, - Eurydice_slice_subslice_shared_7e(blocks, - (KRML_CLITERAL(core_ops_range_Range_08){ .start = offset, .end = offset + (size_t)8U })).ptr, - (size_t)8U * sizeof (uint8_t)); - Eurydice_array_u8x8 - uu____1 = - core_result_unwrap_26_ab(( - KRML_CLITERAL(core_result_Result_8e){ .tag = core_result_Ok, .val = { .case_Ok = arr } } - )); - state_flat.data[i] = core_num__u64__from_le_bytes(uu____1); - } + size_t i = uu____0.f0; + size_t offset = start + (size_t)8U * i; + Eurydice_array_u8x8 arr; + memcpy(arr.data, + Eurydice_slice_subslice_shared_7e(blocks, + (KRML_CLITERAL(core_ops_range_Range_08){ .start = offset, .end = offset + (size_t)8U })).ptr, + (size_t)8U * sizeof (uint8_t)); + Eurydice_array_u8x8 + uu____1 = + core_result_unwrap_26_ab(( + KRML_CLITERAL(core_result_Result_8e){ .tag = core_result_Ok, .val = { .case_Ok = arr } } + )); + state_flat.data[i] = core_num__u64__from_le_bytes(uu____1); } KRML_HOST_EPRINTF("KaRaMeL abort at %s:%d\n%s\n", __FILE__, __LINE__, "panic!"); KRML_HOST_EXIT(255U); @@ -3003,7 +2957,6 @@ libcrux_sha3_generic_keccak_portable_keccak1_1e( if (blocks == (size_t)0U) { libcrux_sha3_simd_portable_squeeze_13_2c(&s, out, (size_t)0U, outlen); - return; } else { @@ -3019,16 +2972,13 @@ libcrux_sha3_generic_keccak_portable_keccak1_1e( libcrux_sha3_generic_keccak_keccakf1600_80_04(&s); libcrux_sha3_simd_portable_squeeze_13_2c(&s, out, last, outlen - last); } - return; } + return; } - else - { - size_t i = uu____0.f0; - /* original Rust expression is not an lvalue in C */ - Eurydice_arr_06 lvalue = { .data = { data } }; - libcrux_sha3_generic_keccak_absorb_block_80_c61(&s, &lvalue, i * (size_t)144U); - } + size_t i = uu____0.f0; + /* original Rust expression is not an lvalue in C */ + Eurydice_arr_06 lvalue = { .data = { data } }; + libcrux_sha3_generic_keccak_absorb_block_80_c61(&s, &lvalue, i * (size_t)144U); } KRML_HOST_EPRINTF("KaRaMeL abort at %s:%d\n%s\n", __FILE__, __LINE__, "panic!"); KRML_HOST_EXIT(255U); @@ -3090,22 +3040,19 @@ libcrux_sha3_simd_portable_load_block_7a( } return; } - else - { - size_t i = uu____0.f0; - size_t offset = start + (size_t)8U * i; - Eurydice_array_u8x8 arr; - memcpy(arr.data, - Eurydice_slice_subslice_shared_7e(blocks, - (KRML_CLITERAL(core_ops_range_Range_08){ .start = offset, .end = offset + (size_t)8U })).ptr, - (size_t)8U * sizeof (uint8_t)); - Eurydice_array_u8x8 - uu____1 = - core_result_unwrap_26_ab(( - KRML_CLITERAL(core_result_Result_8e){ .tag = core_result_Ok, .val = { .case_Ok = arr } } - )); - state_flat.data[i] = core_num__u64__from_le_bytes(uu____1); - } + size_t i = uu____0.f0; + size_t offset = start + (size_t)8U * i; + Eurydice_array_u8x8 arr; + memcpy(arr.data, + Eurydice_slice_subslice_shared_7e(blocks, + (KRML_CLITERAL(core_ops_range_Range_08){ .start = offset, .end = offset + (size_t)8U })).ptr, + (size_t)8U * sizeof (uint8_t)); + Eurydice_array_u8x8 + uu____1 = + core_result_unwrap_26_ab(( + KRML_CLITERAL(core_result_Result_8e){ .tag = core_result_Ok, .val = { .case_Ok = arr } } + )); + state_flat.data[i] = core_num__u64__from_le_bytes(uu____1); } KRML_HOST_EPRINTF("KaRaMeL abort at %s:%d\n%s\n", __FILE__, __LINE__, "panic!"); KRML_HOST_EXIT(255U); @@ -3343,7 +3290,6 @@ libcrux_sha3_generic_keccak_portable_keccak1_7c( if (blocks == (size_t)0U) { libcrux_sha3_simd_portable_squeeze_13_7a(&s, out, (size_t)0U, outlen); - return; } else { @@ -3359,16 +3305,13 @@ libcrux_sha3_generic_keccak_portable_keccak1_7c( libcrux_sha3_generic_keccak_keccakf1600_80_04(&s); libcrux_sha3_simd_portable_squeeze_13_7a(&s, out, last, outlen - last); } - return; } + return; } - else - { - size_t i = uu____0.f0; - /* original Rust expression is not an lvalue in C */ - Eurydice_arr_06 lvalue = { .data = { data } }; - libcrux_sha3_generic_keccak_absorb_block_80_c62(&s, &lvalue, i * (size_t)104U); - } + size_t i = uu____0.f0; + /* original Rust expression is not an lvalue in C */ + Eurydice_arr_06 lvalue = { .data = { data } }; + libcrux_sha3_generic_keccak_absorb_block_80_c62(&s, &lvalue, i * (size_t)104U); } KRML_HOST_EPRINTF("KaRaMeL abort at %s:%d\n%s\n", __FILE__, __LINE__, "panic!"); KRML_HOST_EXIT(255U); @@ -3548,7 +3491,6 @@ libcrux_sha3_generic_keccak_portable_keccak1_c6( if (blocks == (size_t)0U) { libcrux_sha3_simd_portable_squeeze_13_3a(&s, out, (size_t)0U, outlen); - return; } else { @@ -3564,16 +3506,13 @@ libcrux_sha3_generic_keccak_portable_keccak1_c6( libcrux_sha3_generic_keccak_keccakf1600_80_04(&s); libcrux_sha3_simd_portable_squeeze_13_3a(&s, out, last, outlen - last); } - return; } + return; } - else - { - size_t i = uu____0.f0; - /* original Rust expression is not an lvalue in C */ - Eurydice_arr_06 lvalue = { .data = { data } }; - libcrux_sha3_generic_keccak_absorb_block_80_c63(&s, &lvalue, i * (size_t)168U); - } + size_t i = uu____0.f0; + /* original Rust expression is not an lvalue in C */ + Eurydice_arr_06 lvalue = { .data = { data } }; + libcrux_sha3_generic_keccak_absorb_block_80_c63(&s, &lvalue, i * (size_t)168U); } KRML_HOST_EPRINTF("KaRaMeL abort at %s:%d\n%s\n", __FILE__, __LINE__, "panic!"); KRML_HOST_EXIT(255U);