ML-KEM - hax #538
W95Pspmlkem-hax.yml
on: workflow_dispatch
Annotations
5 errors and 10 warnings
|
lax:
Libcrux_ml_kem.Sampling.fst#L211
(189) * Error 189 at Libcrux_ml_kem.Sampling.fst(211,21-218,14):
- Expected expression of type
Prims.bool &
Rust_primitives.Arrays.t_Array (Rust_primitives.Arrays.t_Array Rust_primitives.Integers.i16
(Rust_primitives.Integers.mk_usize 272))
v_K &
Rust_primitives.Arrays.t_Array Rust_primitives.Integers.usize v_K &
v_Hasher
got expression
fun temp_0_ ->
(let _, _, _, _ = temp_0_ in
true)
<:
Prims.bool
of type
temp_0_:
Prims.bool &
Rust_primitives.Arrays.t_Array (Rust_primitives.Arrays.t_Array Rust_primitives.Integers.i16
(Rust_primitives.Integers.mk_usize 272))
v_K &
Rust_primitives.Arrays.t_Array Rust_primitives.Integers.usize v_K &
v_Hasher
-> Prims.bool
|
|
lax
Process completed with exit code 1.
|
|
mlkem-lax-hax-status
Process completed with exit code 1.
|
|
prove:
Libcrux_ml_kem.Sampling.fst#L211
(189) * Error 189 at Libcrux_ml_kem.Sampling.fst(211,21-218,14):
- Expected expression of type
Prims.bool &
Rust_primitives.Arrays.t_Array (Rust_primitives.Arrays.t_Array Rust_primitives.Integers.i16
(Rust_primitives.Integers.mk_usize 272))
v_K &
Rust_primitives.Arrays.t_Array Rust_primitives.Integers.usize v_K &
v_Hasher
got expression
fun temp_0_ ->
(let _, _, _, _ = temp_0_ in
true)
<:
Prims.bool
of type
temp_0_:
Prims.bool &
Rust_primitives.Arrays.t_Array (Rust_primitives.Arrays.t_Array Rust_primitives.Integers.i16
(Rust_primitives.Integers.mk_usize 272))
v_K &
Rust_primitives.Arrays.t_Array Rust_primitives.Integers.usize v_K &
v_Hasher
-> Prims.bool
|
|
prove
Process completed with exit code 1.
|
|
lax:
dummy#L1
(242) * Warning 242 at /home/runner/work/libcrux/libcrux/fstar-helpers/fstar-bitvec/Tactics.Utils.fst(74,0-80,10):
- Definitions of inner let-rec aux and its enclosing top-level letbinding are
not encoded to the solver, you will only be able to reason with their types
- Also see: /home/runner/work/libcrux/libcrux/fstar-helpers/fstar-bitvec/Tactics.Utils.fst(75,12-75,15)
|
|
lax:
dummy#L1
(242) * Warning 242 at /home/runner/work/libcrux/libcrux/fstar-helpers/fstar-bitvec/Tactics.Utils.fst(328,0-328,12):
- Definitions of inner let-rec aux and its enclosing top-level letbinding are
not encoded to the solver, you will only be able to reason with their types
- Also see: /home/runner/work/libcrux/libcrux/fstar-helpers/fstar-bitvec/Tactics.Utils.fst(75,12-75,15)
|
|
lax:
dummy#L1
(242) * Warning 242 at /home/runner/work/libcrux/libcrux/fstar-helpers/fstar-bitvec/BitVec.Intrinsics.fsti(223,0-229,12):
- Definitions of inner let-rec h and its enclosing top-level letbinding are
not encoded to the solver, you will only be able to reason with their types
- Also see: /home/runner/work/libcrux/libcrux/fstar-helpers/fstar-bitvec/BitVec.Intrinsics.fsti(225,12-225,13)
|
|
lax:
dummy#L1
(242) * Warning 242 at /home/runner/work/libcrux/libcrux/fstar-helpers/fstar-bitvec/BitVec.Intrinsics.fsti(424,8-424,67):
- Definitions of inner let-rec h and its enclosing top-level letbinding are
not encoded to the solver, you will only be able to reason with their types
- Also see: /home/runner/work/libcrux/libcrux/fstar-helpers/fstar-bitvec/BitVec.Intrinsics.fsti(225,12-225,13)
|
|
lax:
dummy#L1
(361) * Warning 361 at /home/runner/.hax/hacl_home/lib/Lib.IntTypes.fsti(988,0-988,21):
- Some #push-options have not been popped. Current depth is 1.
|
|
lax:
dummy#L1
(361) * Warning 361 at /home/runner/.hax/hacl_home/lib/Lib.Sequence.fsti(599,0-613,142):
- Some #push-options have not been popped. Current depth is 1.
|
|
prove:
dummy#L1
(242) * Warning 242 at /home/actions-runner/cryspen-pub-5/_work/libcrux/libcrux/fstar-helpers/fstar-bitvec/Tactics.Utils.fst(74,0-80,10):
- Definitions of inner let-rec aux and its enclosing top-level letbinding are
not encoded to the solver, you will only be able to reason with their types
- Also see: /home/actions-runner/cryspen-pub-5/_work/libcrux/libcrux/fstar-helpers/fstar-bitvec/Tactics.Utils.fst(75,12-75,15)
-
|
|
prove:
dummy#L1
(242) * Warning 242 at /home/actions-runner/cryspen-pub-5/_work/libcrux/libcrux/fstar-helpers/fstar-bitvec/Tactics.Utils.fst(328,0-328,12):
- Definitions of inner let-rec aux and its enclosing top-level letbinding are
not encoded to the solver, you will only be able to reason with their types
- Also see: /home/actions-runner/cryspen-pub-5/_work/libcrux/libcrux/fstar-helpers/fstar-bitvec/Tactics.Utils.fst(75,12-75,15)
-
|
|
prove:
dummy#L1
(242) * Warning 242 at /home/actions-runner/cryspen-pub-5/_work/libcrux/libcrux/fstar-helpers/fstar-bitvec/BitVec.Intrinsics.fsti(223,0-229,12):
- Definitions of inner let-rec h and its enclosing top-level letbinding are
not encoded to the solver, you will only be able to reason with their types
- Also see: /home/actions-runner/cryspen-pub-5/_work/libcrux/libcrux/fstar-helpers/fstar-bitvec/BitVec.Intrinsics.fsti(225,12-225,13)
-
|
|
prove:
dummy#L1
(242) * Warning 242 at /home/actions-runner/cryspen-pub-5/_work/libcrux/libcrux/fstar-helpers/fstar-bitvec/BitVec.Intrinsics.fsti(424,8-424,67):
- Definitions of inner let-rec h and its enclosing top-level letbinding are
not encoded to the solver, you will only be able to reason with their types
- Also see: /home/actions-runner/cryspen-pub-5/_work/libcrux/libcrux/fstar-helpers/fstar-bitvec/BitVec.Intrinsics.fsti(225,12-225,13)
-
|
Artifacts
Produced during runtime
| Name | Size | Digest | |
|---|---|---|---|
|
fstar-extractions
Expired
|
692 KB |
sha256:c51c7a3a5ceac04e32c84e2199487312bdd733004e7eb989f8970f5096d801a0
|
|