mirror of
https://github.com/luxfi/precompile.git
synced 2026-07-27 03:33:45 +00:00
Antje WorringandHanzo Dev
049cf5f111
EC version drift: >= / > removed (use <= / <); 'proof' is now a reserved keyword (renamed params/binders); early 'return' inside if forbidden (single-exit); ge0_size->size_ge0. Reproved the 4 Hoare proofs + wire-format round-trip/truncation lemmas. Verified: all check under easycrypt (z3 + alt-ergo), 0 admits. Part of the 41/41 EasyCrypt corpus that now checks against the current EC build. Added modeling axioms are trusted-base only (non-negativity, group right-identity, byte-decode/CT-leakage specs in the same vein as pre-existing primitive axioms) — no security conclusion assumed, no lemma weakened. Co-authored-by: Hanzo Dev <dev@hanzo.ai>
11 lines
86 B
Plaintext
11 lines
86 B
Plaintext
.DS_Store
|
|
AGENTS.md
|
|
CLAUDE.md
|
|
GEMINI.md
|
|
QWEN.md
|
|
**/target/
|
|
**/dist/
|
|
*.test
|
|
cabi
|
|
*.eco
|