Upstream new proofs and proof improvements #356
karthikbhargavanmldsa-hax.yml
on: pull_request
extract
1m 58s
mldsa-extract-hax-status
0s
mldsa-diff-hax-status
0s
mldsa-lax-hax-status
0s
Annotations
4 warnings
|
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)
|
Artifacts
Produced during runtime
| Name | Size | Digest | |
|---|---|---|---|
|
fstar-extraction-mldsa
|
199 KB |
sha256:d4c9bbe6deff99f41eceedcef550ffc08ffb41464a58d40e76becdff6eb426c0
|
|