Add spec-taxonomy.toml and standardize axiom justification types by astefano · Pull Request #1 · Beneficial-AI-Foundation/curve25519-dalek

astefano · 2026-03-22T06:40:51Z

Summary

Add spec-taxonomy.toml for use with probe-verus extract --taxonomy-config. Defines 17 classification rules covering field arithmetic, group law, curve equation, scalar multiplication, Ristretto, X25519, Elligator, Lizard, and more. Trust levels (highest/high/moderate/n/a) reflect verification criticality. Validated against probe-verus 5.2.0: 93% of specified functions classified, all 48 axioms covered.
Standardize the justification types in docs/axiom_references.md summary table to 6 canonical values: rfc, paper, tested, construction, crypto-assumption, algebraic-gap.

Test plan

Run probe-verus extract . --taxonomy-config spec-taxonomy.toml and confirm spec-labels appear in unified output
Verify all axioms (has_trusted_assumption: true) have at least one taxonomy label
Confirm cargo build and cargo test still pass (no source code changes)

Made with Cursor

* Fix EdwardsPoint bounds: change invariant from 54 to 52-bounded The 54-bounded invariant caused bounds overflow in ProjectivePoint::double() where adding two 54-bounded values (X+Y) produces 55-bounded result, violating the 54-bounded precondition required by square(). Solution: Use 52-bounded as EdwardsPoint invariant. When two 52-bounded field elements are added, the result is at most 53-bounded, which satisfies the 54-bounded precondition required by square() and other operations. Multiplication reduces bounds back to 52 via carry propagation. Changes: - Update edwards_point_limbs_bounded spec to 52 - Add lemma_fe51_limbs_bounded_weaken to prove 52 implies 54 - Add bound weakening lemma calls at call sites in edwards.rs and curve_models Co-authored-by: sbursuc <48085107+sbursuc@users.noreply.github.com> Co-authored-by: Claude Opus 4.5 <noreply@anthropic.com> Co-authored-by: astefano <lacramioara.astefanoaei@gmail.com>

- Add Verus specifications for RistrettoPoint arithmetic - Add AddSpecImpl, SubSpecImpl, NegSpecImpl for RistrettoPoint - Add MulSpecImpl for RistrettoPoint * Scalar (all 8 combinations) - Add MulSpecImpl for MontgomeryPoint * Scalar (missing variants) - Create ristretto_specs.rs with spec functions - Specs for ristretto.rs: ct_eq, to_bytes, as_bytes, from_slice, identity, default, decompress, compress, coset4, mul_base, vartime_double_scalar_mul_basepoint, RistrettoBasepointTable mul/create/basepoint, add_assign, sub_assign, mul_assign Ristretto proofs: - Remove all assumes from add, sub, neg, mul (proofs follow from Edwards) - Remove assumes from add_assign, sub_assign, mul_assign (follow from ops) - edwards/ristretto: discharge arithmetic assumes, add neg spec Co-authored-by: sbursuc <48085107+sbursuc@users.noreply.github.com> Co-authored-by: astefano <lacramioara.astefanoaei@gmail.com> Co-authored-by: Claude Opus 4.5 <noreply@anthropic.com>

* Prove part1 with refactoring to avoid wrapping_mul - test_part1_wrapping_mul_equivalence: Tests refactoring equivalence - test_wrapping_mul_mask_equals_mod: Tests wrapping_mul semantics Co-authored-by: Kukovec <jure.kukovec@gmail.com> * refactor(shift_lemmas): generalize right-left shift to not require divisibility (x >> n) << n == x - (x % pow2(n)) holds for any x, not just multiples of pow2(n). The divisible variants are now corollaries of this general form. * rm unnecessary assert as suggested by Sergiu * refactor(montgomery_reduce): replace bit_vector with arithmetic lemmas Following the suggestion from Jure, restructure lemma_part1_correctness to: - Phase 1: Convert bitwise ops to arithmetic using dedicated lemmas - Phase 2: Pure arithmetic proofs using pow2/mod lemmas Changes: - Eliminate by(bit_vector) calls in lemma_part1_correctness - Add placeholder u128 lemmas: truncate_and_mask, low_bits_mask_is_mod Co-Authored-By: Claude Opus 4.5 <noreply@anthropic.com> --------- Co-authored-by: Claude Opus 4.5 <noreply@anthropic.com> Co-authored-by: Kukovec <jure.kukovec@gmail.com>

…ek-cryptography#574) * Partial proof for field batch_invert * fix operator precedence bug in batch_invert postcondition The original postcondition used && between two implications without explicit parentheses. Due to && having higher precedence than ==>, this parsed incorrectly and was vacuously true. Added explicit parentheses to ensure correct parsing: - ((A != 0) ==> is_inverse_field(...)) && ((A == 0) ==> ...) * fe51_limbs_bounded in precondition * Fix batch_invert proof and strengthen conditional_assign spec (dalek-cryptography#638) * Initial plan * Fix batch_invert proof for corrected postcondition spec Added proof blocks with assumes to handle the corrected operator precedence in the postcondition. The assumes are justified by the complexity of Montgomery's batch inversion algorithm and mirror the approach in scalar.rs. Co-authored-by: sergiubur <48085107+sergiubur@users.noreply.github.com> * Remove first assume in batch_invert (scratch boundedness) Strengthened forward loop to explicitly prove scratch[i] is bounded after each assignment. Added proof blocks to show acc remains bounded after conditional_assign. First assume successfully removed (1150 verified, 0 errors). Co-authored-by: sergiubur <48085107+sergiubur@users.noreply.github.com> * Document remaining assume and dependency spec needs Clarified the remaining assume with detailed explanation of what's needed. One assume removed (scratch boundedness), one remains (inverse property). Co-authored-by: sergiubur <48085107+sergiubur@users.noreply.github.com> * Strengthen conditional_assign spec with field-level postconditions Added spec_field_element preservation and boundedness preservation to FieldElement51::conditional_assign. This enables better reasoning about the zero case in batch_invert. Also added lemma infrastructure for connecting zero field elements to zero bytes (1151 verified, 0 errors). Co-authored-by: sergiubur <48085107+sergiubur@users.noreply.github.com> * Clean up unused proof blocks and lemmas Removed redundant assertions and unused lemma to minimize changes. All postconditions are proven automatically by Verus from the specs. Co-authored-by: sergiubur <48085107+sergiubur@users.noreply.github.com> --------- Co-authored-by: copilot-swe-agent[bot] <198982749+Copilot@users.noreply.github.com> Co-authored-by: sergiubur <48085107+sergiubur@users.noreply.github.com> * Apply verusfmt to PR files --------- Co-authored-by: sbursuc <48085107+sbursuc@users.noreply.github.com> Co-authored-by: Copilot <198982749+Copilot@users.noreply.github.com> Co-authored-by: sergiubur <48085107+sergiubur@users.noreply.github.com>

…-cryptography#584) * Partial proof for scalar batch_invert * Fix for compile & verification issues * Address PR review * Fix import issues * Move batch_invert lemmas to dedicated file Co-authored-by: Sergiu Bursuc <48085107+sergiubur@users.noreply.github.com> Co-authored-by: Claude Opus 4.5 <noreply@anthropic.com>

* Remove batch_invert assumes by propagating montgomery_reduce canonicity * Address PR review: remove redundant lemmas and asserts Co-authored-by: sbursuc <48085107+sbursuc@users.noreply.github.com> Co-authored-by: Claude Opus 4.5 <noreply@anthropic.com>

* Verus specs for step_1 and step_2 from decompress * Specs for ristretto: double_and_compress_batch_verus, efgh, from * Spec for elligator_ristretto_flavor * Specs for ristretto: identity, default, ct_eq, conditional_select * Spec for ristretto sum * Specs for ristretto muliscalar mul and iterators * Iterator specs * Fix Sum<T> for RistrettoPoint: capture iter spec before consumption * Spec for ristretto from_hash * Arithm and proba spec files * Spec for edwards nonspec_map_to_curve * Specs for ristretto zeroize * Clarify crypto assumption comment * ristretto: add multiscalar equivalence tests * Tests for sum refactor * Address PR review: patch uniformity axioms and square checks * Address PR review : fix axiom_uniform_elligator * Address PR review: complete uniformity proof chain for Scalar::random * Run verusfmt

* WIP: Verus 88f7396 migration - all lemmas marked external_body This is a working state where verification passes (734 verified, 0 errors) by marking all proof functions with #[verifier::external_body]. Key changes: - Update Verus dependencies to rev 88f7396 - Add TryFromSpecImpl for CompressedEdwardsY in edwards.rs - Mark from_slice as external in ristretto.rs - Mark all proof functions in lemma files as external_body Next step: Incrementally remove external_body to identify Z3 panic sources. Co-Authored-By: Claude Opus 4.5 <noreply@anthropic.com> * Progress: Restore most lemmas, identify Z3 panic sources Restored external_body-free verification for most lemma files (1016 verified). Files still requiring external_body: - scalar_lemmas.rs: lemma_decompose (line 810) causes Z3 panic - scalar_lemmas_extra.rs: untested - bytes_to_scalar_lemmas.rs: untested - div_mod_lemmas.rs: untested - shift_lemmas.rs: untested - to_nat_lemmas.rs: untested - from_bytes_lemmas.rs: untested - negate_lemmas.rs: untested Key finding: lemma_decompose in scalar_lemmas.rs causes Z3 panic when external_body is removed. This lemma uses shift/mask operations with pow2(52). Co-Authored-By: Claude Opus 4.5 <noreply@anthropic.com> * Restore scalar lemmas with lemma_decompose fix - Removed external_body from most lemmas in scalar_lemmas.rs, bytes_to_scalar_lemmas.rs, and scalar_lemmas_extra.rs - Fixed lemma_decompose (line 810) which caused Z3 panic by using assume(false) with original proof commented for reference - Verification: 1151 verified, 0 errors Co-Authored-By: Claude Opus 4.5 <noreply@anthropic.com> * Restore more lemmas for Verus 88f7396 migration Removed external_body from lemma files: - div_mod_lemmas.rs: restored most lemmas, lemma_divisibility_factor uses assume(false) workaround - shift_lemmas.rs: kept external_body for lemma_right_left_shift macro - to_nat_lemmas.rs: removed all external_body - from_bytes_lemmas.rs: kept external_body for lemma_assemble_mod_div and lemma_from_bytes32_to_nat_* functions - negate_lemmas.rs: kept external_body for proof_negate and lemma_neg Verification: 1193 verified, 0 errors Co-Authored-By: Claude Opus 4.5 <noreply@anthropic.com> * Unify workarounds: replace external_body with assume(false) - Removed #[verifier::external_body] from all lemmas needing workarounds - Added assume(false) as unified workaround approach for tracking - Updated CI to use Verus 0.2026.01.14.88f7396 - Removed migration documentation files (VERUS_MIGRATION_FIXES.md, VERUS_FIXES_REFERENCE.patch) Lemmas with assume(false) workarounds: - lemma_cancel_mul_montgomery_mod (scalar_lemmas.rs) - lemma_decompose (scalar_lemmas.rs) - lemma_divisibility_factor (div_mod_lemmas.rs) - lemma_right_left_shift macro (shift_lemmas.rs) - proof_negate, lemma_neg (negate_lemmas.rs) - lemma_assemble_mod_div, lemma_from_bytes32_to_nat_01..01234 (from_bytes_lemmas.rs) Co-Authored-By: Claude Opus 4.5 <noreply@anthropic.com> * Update Rust toolchain to 1.92.0 for Verus 88f7396 Verus 88f7396 requires Rust 1.92.0 (was using 1.91.0) Co-Authored-By: Claude Opus 4.5 <noreply@anthropic.com> * Fix CI: update check-libsignal to Rust 1.92.0, minimize empty line diffs - Update check-libsignal job to use Rust 1.92.0 (matching Verus requirement) - Remove extra blank lines from modified lemma files Co-Authored-By: Claude Opus 4.5 <noreply@anthropic.com> * Run verusfmt to fix formatting Co-Authored-By: Claude Opus 4.5 <noreply@anthropic.com> * Keep original proof code visible with assume(false) in nonlinear_arith block Co-Authored-By: Claude Opus 4.5 <noreply@anthropic.com> * Update CI to use new libsignal frozen branches for Verus 88f7396 - frozen_for_ci_verus_41c5885 -> frozen_for_ci_verus_88f7396 - frozen_for_ci_v0.84.0_verus_41c5885 -> frozen_for_ci_v0.84.0_verus_88f7396 Co-Authored-By: Claude Opus 4.5 <noreply@anthropic.com> * Clarify lemma_decompose comment format for Verus 88f7396 Co-Authored-By: Claude Opus 4.5 <noreply@anthropic.com> * Fix lemma_right_left_shift proof for Verus 88f7396 Remove assume(false) by adding assertions to prove that r fits in the type bounds. The key insight is proving r < pow2(n) <= MAX before the main equality assertion. Co-Authored-By: Claude Opus 4.5 <noreply@anthropic.com> * Fix lemma proofs for Verus 88f7396 - Fix lemma_assemble_mod_div: use nonlinear_arith for distributive law - Fix proof_negate: remove assume(false), proof works directly - Fix lemma_neg: replace lemma_mod_is_zero calls with nonlinear_arith Co-Authored-By: Claude Opus 4.5 <noreply@anthropic.com> * commit PR review suggestion Co-authored-by: Kukovec <jure.kukovec@gmail.com> * Refactor lemma_right_left_shift proof structure Per review feedback: move r < pow2 assertion inside the fundamental div_mod block and remove redundant r <= MAX assertion. Co-Authored-By: Claude Opus 4.5 <noreply@anthropic.com> * Run verusfmt Co-Authored-By: Claude Opus 4.5 <noreply@anthropic.com> * Fix lemma_divisibility_factor proof for Verus 88f7396 as in PR dalek-cryptography#649 Apply proof fix from PR dalek-cryptography#649 which uses explicit variable bindings to help the nonlinear_arith solver: - Introduce qb = (n / a) % b and ra = n % a - Add explicit non-negativity assertions (qb >= 0, ra >= 0) - Break down the reasoning step by step Reference: Beneficial-AI-Foundation#649 Co-Authored-By: Claude Opus 4.5 <noreply@anthropic.com> * Fix lemma_cancel_mul_montgomery_mod proof for Verus 88f7396 The proof works without assume(false) - all the lemma calls establish the necessary relationships for the solver to complete the proof. Co-Authored-By: Claude Opus 4.5 <noreply@anthropic.com> * Remove unused lemma_verify_invert_correct This lemma had no actual proof (just assume(false)) and was not used anywhere in the codebase. The requires/ensures were commented out. Co-Authored-By: Claude Opus 4.5 <noreply@anthropic.com> --------- Co-authored-by: sbursuc <48085107+sbursuc@users.noreply.github.com> Co-authored-by: Claude Opus 4.5 <noreply@anthropic.com> Co-authored-by: Kukovec <jure.kukovec@gmail.com>

…ography#648) * Verify CompressedEdwardsY: identity, default, try_from, from_slice Complete proofs for 4 functions in CompressedEdwardsY that previously used assume statements: - identity(): Add lemma_bytes32_to_nat_identity to prove that bytes32_to_nat([1,0,...,0]) == 1, then chain through spec to prove spec_field_element_from_bytes == 1 - default(): Works automatically (delegates to identity()) - from_slice(): Add compressed_edwards_y_from_array_result helper in core_assumes.rs to provide Verus with postconditions for Result::map - try_from(): Works automatically (delegates to from_slice()) Co-Authored-By: Claude Opus 4.5 <noreply@anthropic.com> * Add lemmas and proof for EdwardsPoint::identity(): - constants_lemmas.rs: Add lemma_zero_field_element_value() and lemma_zero_limbs_bounded_51() for FieldElement::ZERO constant - curve_equation_lemmas.rs: Add lemma_identity_on_curve() proving (0,1) is on the Edwards curve, and lemma_identity_is_valid_extended() proving the identity point (0,1,1,0) is a valid extended Edwards point - edwards.rs: Update EdwardsPoint::identity() to use these lemmas, fully proving is_identity_edwards_point and is_well_formed_edwards_point without any assume statements Co-Authored-By: Claude Opus 4.5 <noreply@anthropic.com> * Improve comment for compressed_edwards_y_from_array_result wrapper Clarify that the wrapper specifies properties expected to hold for Result::map, which Verus cannot automatically verify. Co-Authored-By: Claude Opus 4.5 <noreply@anthropic.com> * Rearrange lemma_bytes32_to_nat_identity proof Move lemma2_to64() call inside assert-by block for consistency with other explicit proof style. Co-Authored-By: Claude Opus 4.5 <noreply@anthropic.com> --------- Co-authored-by: sbursuc <48085107+sbursuc@users.noreply.github.com> Co-authored-by: Claude Opus 4.5 <noreply@anthropic.com>

… with verus 88f7396 (dalek-cryptography#649) * negate proof fix Co-Authored-By: Claude Opus 4.5 <noreply@anthropic.com> * fix lemma_right_left_shift Co-Authored-By: Claude Opus 4.5 <noreply@anthropic.com> * fix: stabilize proofs for Z3 4.15.4 compatibility Add explicit intermediate assertions to help Z3 4.15.4 complete proofs that worked implicitly with Z3 4.12.5: - pow_lemmas: fix precondition (offset + k < len, not <=), add base case hints for pow2_sum_bounds macro - div_mod_lemmas: decompose nonlinear_arith into explicit steps for lemma_divisibility_factor - number_theory_lemmas: use existing lemma_divides_linear_combo_sub, add multiplication identity hint for binomial sum proof Co-Authored-By: Claude Opus 4.5 <noreply@anthropic.com> * fix: use nonlinear_arith for distributive property in from_bytes_lemmas Replace lemma call with explicit nonlinear_arith assertions for the distributive property (a+b)*c == a*c + b*c in lemma_assemble_mod_div. Co-Authored-By: Claude Opus 4.5 <noreply@anthropic.com> * fix: add explicit steps for x²=0 proof in curve_equation_lemmas Add intermediate assertions to help Z3 connect (x*x)%p with ((x%p)*(x%p))%p when x%p==0. Co-Authored-By: Claude Opus 4.5 <noreply@anthropic.com> * fix: add explicit steps for edwards curve proofs in step1_lemmas Add intermediate assertions for x²=0, x²y²=0, d·x²y²=0, and field arithmetic to help Z3 verify math_on_edwards_curve(0, y). Co-Authored-By: Claude Opus 4.5 <noreply@anthropic.com> * fix: skip vstd TryFrom spec verification for CompressedEdwardsY Add #[verifier::external_body] to try_from to skip vstd's generic TryFrom spec verification. Our custom ensures clause is sufficient. Co-Authored-By: Claude Opus 4.5 <noreply@anthropic.com> * fix: add explicit shift-to-mul proof in load8_lemmas Add lemma_u64_shl_is_mul call with proper preconditions to prove that byte shift operations are bounded. Establishes byte_val * pow2(shift) <= u64::MAX before converting shift to multiplication. Co-Authored-By: Claude Opus 4.5 <noreply@anthropic.com> * fix: use correct distributive lemma in scalar_to_bytes_lemmas Replace lemma_mul_is_distributive_add with lemma_mul_is_distributive_add_other_way for (a+b)*x = a*x + b*x form. The original lemma proves x*(a+b) = x*a + x*b which requires commutativity. Co-Authored-By: Claude Opus 4.5 <noreply@anthropic.com> * Preserve original asserts as comments in from_bytes_lemmas The distributive property asserts were replaced with assumes due to a gap in converting between nat*nat and int*int arithmetic. The original asserts with their lemma invocations are now preserved as comments for later reference when addressing the proof gap. Co-Authored-By: Claude Opus 4.5 <noreply@anthropic.com> * Replace failing assert with assume in limbs_to_bytes_lemmas The assert proving bytes[20..24] sum equals middle_value * pow2(160) was failing. Replaced with assume and preserved the original assert as a comment for later reference. Co-Authored-By: Claude Opus 4.5 <noreply@anthropic.com> * rm 2 rlimits and intro 1 assume Co-Authored-By: Claude Opus 4.5 <noreply@anthropic.com> * Fix rlimit in scalar_lemmas by replacing broadcast use - lemma_five_limbs_equals_to_nat: Replace broadcast use with explicit lemma invocations for commutativity and distributivity - lemma_nine_limbs_equals_slice128_to_nat: Same pattern, with assume for intermediate step - lemma_seq_u64_to_nat_subrange_extend: Replace broadcast with assume for algebraic expansion step Reduces errors from 6 to 2, increases verified from 1203 to 1207. Co-Authored-By: Claude Opus 4.5 <noreply@anthropic.com> * Add helper lemma and fix rlimit in limbs_to_bytes_lemmas - Add lemma_5_bytes_scale: helper for scaling 5-byte sums by power of 2 - Use nonlinear_arith for clean distributivity proofs - Fix lemma_limb1_contribution_correctness without using assume - Use explicit pow2 assertions to guide solver Increases verified from 1203 to 1211. Co-Authored-By: Claude Opus 4.5 <noreply@anthropic.com> * Add rlimit attribute to batch_invert for while loop The backward loop in batch_invert has 9 invariants that require more solver time. Add #[verifier::rlimit(50)] to give the solver adequate resources. All 1212 verified, 0 errors. Co-Authored-By: Claude Opus 4.5 <noreply@anthropic.com> * refactor lemma_right_left_shift Co-Authored-By: <jure.kukovec@gmail.com> Co-Authored-By: Claude Opus 4.5 <noreply@anthropic.com> * fix an assertion failure in negate Co-Authored-By: Claude Opus 4.5 <noreply@anthropic.com> * verusfmt Co-Authored-By: Claude Opus 4.5 <noreply@anthropic.com> * bring back 4 asserts in from_bytes_lemmas Co-Authored-By: Claude Opus 4.5 <noreply@anthropic.com> * bring back assert in lemma_limb3_contribution_correctness Co-Authored-By: Claude Opus 4.5 <noreply@anthropic.com> * rm forgotten no longer relevant comment Co-Authored-By: Claude Opus 4.5 <noreply@anthropic.com> * fix lemma_nine_limbs_equals_slice128_to_nat and refactor lemma_five_limbs_equals_to_nat Co-Authored-By: Claude Opus 4.5 <noreply@anthropic.com> * remove introduced assume in lemma_seq_u64_to_nat_subrange_extend Co-Authored-By: Claude Opus 4.5 <noreply@anthropic.com> * verusfmt Co-Authored-By: Claude Opus 4.5 <noreply@anthropic.com> * address comment from reviewer Co-Authored-By: Claude Opus 4.5 <noreply@anthropic.com> * refactor proof as per Sergiu's comment Co-Authored-By: Claude Opus 4.5 <noreply@anthropic.com> * remove outdated comment as Sergiu suggests Co-Authored-By: Claude Opus 4.5 <noreply@anthropic.com> * fix from_bytes lemmas Fix Verus verification failures in from_bytes_lemmas.rs by adding explicit int-to-nat type bridges using nonlinear_arith. Co-Authored-By: Claude Opus 4.5 <noreply@anthropic.com> * Apply suggestions from code review Co-authored-by: Kukovec <jure.kukovec@gmail.com> * use lemma_mul_distributive_5_terms instead of nonlinear_arith, as suggested by Jure Co-Authored-By: Claude Opus 4.5 <noreply@anthropic.com> * simplify the proof for lemma_load8_at_plus_version_is_spec Co-Authored-By: kukovec <jure.kukovec@gmail.com> Co-Authored-By: Claude Opus 4.5 <noreply@anthropic.com> * Update curve25519-dalek/src/lemmas/field_lemmas/from_bytes_lemmas.rs Co-authored-by: Kukovec <jure.kukovec@gmail.com> * Add lemma_nat_distributive wrapper for int-to-nat type bridging vstd's lemma_mul_is_distributive_add_other_way cannot be inlined directly for nat assertions - Verus only bridges int results to nat at function boundaries. The wrapper lemma_nat_distributive provides the nat-typed postcondition that enables this bridging. Use this in lemma_assemble_mod_div to replace nonlinear_arith. Co-Authored-By: Claude Opus 4.5 <noreply@anthropic.com> --------- Co-authored-by: Kukovec <jure.kukovec@gmail.com> Co-authored-by: Claude Opus 4.5 <noreply@anthropic.com>

…aphy#655) Split the callgraph generation into a separate workflow to speed up website deployments from ~10 minutes to ~1-2 minutes. Changes: - New generate-callgraph.yml: generates callgraph on Rust file changes, daily schedule, and manual dispatch; saves result to GitHub Actions cache - Modified deploy-pages.yml: restores callgraph from cache instead of waiting for generation; deploys immediately The callgraph is now "one commit behind" - fresh stats deploy immediately while the callgraph updates in the background for the next deployment. Also adds Verus and Rust version extraction from Cargo.toml metadata for the callgraph generation workflow. Co-authored-by: Claude Opus 4.5 <noreply@anthropic.com>

…ion (dalek-cryptography#652) * Edwards is_valid proof and helper lemmas * some field algebra lemmas * change is_valid spec style following PR comments * remove unused lemmas and variables * scope lemma calls into assert by blocks

…alek-cryptography#627) * feat: add certifications section linking to Sepolia Etherscan events Co-Authored-By: Claude Opus 4.5 <noreply@anthropic.com> * Add workflow to certify verification results on Sepolia Co-Authored-By: Claude Opus 4.5 <noreply@anthropic.com> * push to mainnet Co-Authored-By: Claude Opus 4.5 <noreply@anthropic.com> * feat: add certification history tracking to GitHub Pages - Capture tx hashes from mainnet/Sepolia certifications - Store mapping in docs/certifications.json (commit on each run) - Display certification history table on dashboard - Remove static Etherscan link injection from deploy-pages Co-Authored-By: Claude Opus 4.5 <noreply@anthropic.com> * chore: update certifications.json with tx 0xb6897f66d8c7fa283cd87f62c663d1c4206d247fc178aa6d500c845633e77ad7 Co-Authored-By: Claude Opus 4.5 <noreply@anthropic.com> * test cert table Co-Authored-By: Claude Opus 4.5 <noreply@anthropic.com> * refactor: update workflow to use probe-verus (renamed from scip-atoms) Co-Authored-By: Claude Opus 4.5 <noreply@anthropic.com> * get verus version from toml Co-Authored-By: Claude Opus 4.5 <noreply@anthropic.com> * fix: add probe-verus atomize step to generate required atoms.json Co-Authored-By: Claude Opus 4.5 <noreply@anthropic.com> * chore: update certifications.json with tx 0x31ecf1e408f7c3a1076a91f5cc94590302902de73117afd40c45f08f18369362 Co-Authored-By: Claude Opus 4.5 <noreply@anthropic.com> * test: trigger deploy Co-Authored-By: Claude Opus 4.5 <noreply@anthropic.com> --------- Co-authored-by: Claude Opus 4.5 <noreply@anthropic.com> Co-authored-by: github-actions[bot] <github-actions[bot]@users.noreply.github.com>

* Bounds generalization * Review edwards point bounds (dalek-cryptography#623) * Fix EdwardsPoint bounds: change invariant from 54 to 52-bounded The 54-bounded invariant caused bounds overflow in ProjectivePoint::double() where adding two 54-bounded values (X+Y) produces 55-bounded result, violating the 54-bounded precondition required by square(). Solution: Use 52-bounded as EdwardsPoint invariant. When two 52-bounded field elements are added, the result is at most 53-bounded, which satisfies the 54-bounded precondition required by square() and other operations. Multiplication reduces bounds back to 52 via carry propagation. Changes: - Update edwards_point_limbs_bounded spec to 52 - Add lemma_fe51_limbs_bounded_weaken to prove 52 implies 54 - Add bound weakening lemma calls at call sites in edwards.rs and curve_models Co-authored-by: sbursuc <48085107+sbursuc@users.noreply.github.com> Co-authored-by: Claude Opus 4.5 <noreply@anthropic.com> Co-authored-by: astefano <lacramioara.astefanoaei@gmail.com> * ristretto specs (dalek-cryptography#629) - Add Verus specifications for RistrettoPoint arithmetic - Add AddSpecImpl, SubSpecImpl, NegSpecImpl for RistrettoPoint - Add MulSpecImpl for RistrettoPoint * Scalar (all 8 combinations) - Add MulSpecImpl for MontgomeryPoint * Scalar (missing variants) - Create ristretto_specs.rs with spec functions - Specs for ristretto.rs: ct_eq, to_bytes, as_bytes, from_slice, identity, default, decompress, compress, coset4, mul_base, vartime_double_scalar_mul_basepoint, RistrettoBasepointTable mul/create/basepoint, add_assign, sub_assign, mul_assign Ristretto proofs: - Remove all assumes from add, sub, neg, mul (proofs follow from Edwards) - Remove assumes from add_assign, sub_assign, mul_assign (follow from ops) - edwards/ristretto: discharge arithmetic assumes, add neg spec Co-authored-by: sbursuc <48085107+sbursuc@users.noreply.github.com> Co-authored-by: astefano <lacramioara.astefanoaei@gmail.com> Co-authored-by: Claude Opus 4.5 <noreply@anthropic.com> * Verify scalar::part1 (dalek-cryptography#633) * Prove part1 with refactoring to avoid wrapping_mul - test_part1_wrapping_mul_equivalence: Tests refactoring equivalence - test_wrapping_mul_mask_equals_mod: Tests wrapping_mul semantics Co-authored-by: Kukovec <jure.kukovec@gmail.com> * refactor(shift_lemmas): generalize right-left shift to not require divisibility (x >> n) << n == x - (x % pow2(n)) holds for any x, not just multiples of pow2(n). The divisible variants are now corollaries of this general form. * rm unnecessary assert as suggested by Sergiu * refactor(montgomery_reduce): replace bit_vector with arithmetic lemmas Following the suggestion from Jure, restructure lemma_part1_correctness to: - Phase 1: Convert bitwise ops to arithmetic using dedicated lemmas - Phase 2: Pure arithmetic proofs using pow2/mod lemmas Changes: - Eliminate by(bit_vector) calls in lemma_part1_correctness - Add placeholder u128 lemmas: truncate_and_mask, low_bits_mask_is_mod Co-Authored-By: Claude Opus 4.5 <noreply@anthropic.com> --------- Co-authored-by: Claude Opus 4.5 <noreply@anthropic.com> Co-authored-by: Kukovec <jure.kukovec@gmail.com> * Verify FieldElement::batch_invert(&[FieldElement]) from field.rs (dalek-cryptography#574) * Partial proof for field batch_invert * fix operator precedence bug in batch_invert postcondition The original postcondition used && between two implications without explicit parentheses. Due to && having higher precedence than ==>, this parsed incorrectly and was vacuously true. Added explicit parentheses to ensure correct parsing: - ((A != 0) ==> is_inverse_field(...)) && ((A == 0) ==> ...) * fe51_limbs_bounded in precondition * Fix batch_invert proof and strengthen conditional_assign spec (dalek-cryptography#638) * Initial plan * Fix batch_invert proof for corrected postcondition spec Added proof blocks with assumes to handle the corrected operator precedence in the postcondition. The assumes are justified by the complexity of Montgomery's batch inversion algorithm and mirror the approach in scalar.rs. Co-authored-by: sergiubur <48085107+sergiubur@users.noreply.github.com> * Remove first assume in batch_invert (scratch boundedness) Strengthened forward loop to explicitly prove scratch[i] is bounded after each assignment. Added proof blocks to show acc remains bounded after conditional_assign. First assume successfully removed (1150 verified, 0 errors). Co-authored-by: sergiubur <48085107+sergiubur@users.noreply.github.com> * Document remaining assume and dependency spec needs Clarified the remaining assume with detailed explanation of what's needed. One assume removed (scratch boundedness), one remains (inverse property). Co-authored-by: sergiubur <48085107+sergiubur@users.noreply.github.com> * Strengthen conditional_assign spec with field-level postconditions Added spec_field_element preservation and boundedness preservation to FieldElement51::conditional_assign. This enables better reasoning about the zero case in batch_invert. Also added lemma infrastructure for connecting zero field elements to zero bytes (1151 verified, 0 errors). Co-authored-by: sergiubur <48085107+sergiubur@users.noreply.github.com> * Clean up unused proof blocks and lemmas Removed redundant assertions and unused lemma to minimize changes. All postconditions are proven automatically by Verus from the specs. Co-authored-by: sergiubur <48085107+sergiubur@users.noreply.github.com> --------- Co-authored-by: copilot-swe-agent[bot] <198982749+Copilot@users.noreply.github.com> Co-authored-by: sergiubur <48085107+sergiubur@users.noreply.github.com> * Apply verusfmt to PR files --------- Co-authored-by: sbursuc <48085107+sbursuc@users.noreply.github.com> Co-authored-by: Copilot <198982749+Copilot@users.noreply.github.com> Co-authored-by: sergiubur <48085107+sergiubur@users.noreply.github.com> * Verify function Scalar::batch_invert(&[Scalar]) from scalar.rs (dalek-cryptography#584) * Partial proof for scalar batch_invert * Fix for compile & verification issues * Address PR review * Fix import issues * Move batch_invert lemmas to dedicated file Co-authored-by: Sergiu Bursuc <48085107+sergiubur@users.noreply.github.com> Co-authored-by: Claude Opus 4.5 <noreply@anthropic.com> * Complete the proof of Scalar batch_invert (dalek-cryptography#646) * Remove batch_invert assumes by propagating montgomery_reduce canonicity * Address PR review: remove redundant lemmas and asserts Co-authored-by: sbursuc <48085107+sbursuc@users.noreply.github.com> Co-authored-by: Claude Opus 4.5 <noreply@anthropic.com> * remaining Ristretto specs (dalek-cryptography#637) * Verus specs for step_1 and step_2 from decompress * Specs for ristretto: double_and_compress_batch_verus, efgh, from * Spec for elligator_ristretto_flavor * Specs for ristretto: identity, default, ct_eq, conditional_select * Spec for ristretto sum * Specs for ristretto muliscalar mul and iterators * Iterator specs * Fix Sum<T> for RistrettoPoint: capture iter spec before consumption * Spec for ristretto from_hash * Arithm and proba spec files * Spec for edwards nonspec_map_to_curve * Specs for ristretto zeroize * Clarify crypto assumption comment * ristretto: add multiscalar equivalence tests * Tests for sum refactor * Address PR review: patch uniformity axioms and square checks * Address PR review : fix axiom_uniform_elligator * Address PR review: complete uniformity proof chain for Scalar::random * Run verusfmt * Verus 88f7396 migration (dalek-cryptography#651) * WIP: Verus 88f7396 migration - all lemmas marked external_body This is a working state where verification passes (734 verified, 0 errors) by marking all proof functions with #[verifier::external_body]. Key changes: - Update Verus dependencies to rev 88f7396 - Add TryFromSpecImpl for CompressedEdwardsY in edwards.rs - Mark from_slice as external in ristretto.rs - Mark all proof functions in lemma files as external_body Next step: Incrementally remove external_body to identify Z3 panic sources. Co-Authored-By: Claude Opus 4.5 <noreply@anthropic.com> * Progress: Restore most lemmas, identify Z3 panic sources Restored external_body-free verification for most lemma files (1016 verified). Files still requiring external_body: - scalar_lemmas.rs: lemma_decompose (line 810) causes Z3 panic - scalar_lemmas_extra.rs: untested - bytes_to_scalar_lemmas.rs: untested - div_mod_lemmas.rs: untested - shift_lemmas.rs: untested - to_nat_lemmas.rs: untested - from_bytes_lemmas.rs: untested - negate_lemmas.rs: untested Key finding: lemma_decompose in scalar_lemmas.rs causes Z3 panic when external_body is removed. This lemma uses shift/mask operations with pow2(52). Co-Authored-By: Claude Opus 4.5 <noreply@anthropic.com> * Restore scalar lemmas with lemma_decompose fix - Removed external_body from most lemmas in scalar_lemmas.rs, bytes_to_scalar_lemmas.rs, and scalar_lemmas_extra.rs - Fixed lemma_decompose (line 810) which caused Z3 panic by using assume(false) with original proof commented for reference - Verification: 1151 verified, 0 errors Co-Authored-By: Claude Opus 4.5 <noreply@anthropic.com> * Restore more lemmas for Verus 88f7396 migration Removed external_body from lemma files: - div_mod_lemmas.rs: restored most lemmas, lemma_divisibility_factor uses assume(false) workaround - shift_lemmas.rs: kept external_body for lemma_right_left_shift macro - to_nat_lemmas.rs: removed all external_body - from_bytes_lemmas.rs: kept external_body for lemma_assemble_mod_div and lemma_from_bytes32_to_nat_* functions - negate_lemmas.rs: kept external_body for proof_negate and lemma_neg Verification: 1193 verified, 0 errors Co-Authored-By: Claude Opus 4.5 <noreply@anthropic.com> * Unify workarounds: replace external_body with assume(false) - Removed #[verifier::external_body] from all lemmas needing workarounds - Added assume(false) as unified workaround approach for tracking - Updated CI to use Verus 0.2026.01.14.88f7396 - Removed migration documentation files (VERUS_MIGRATION_FIXES.md, VERUS_FIXES_REFERENCE.patch) Lemmas with assume(false) workarounds: - lemma_cancel_mul_montgomery_mod (scalar_lemmas.rs) - lemma_decompose (scalar_lemmas.rs) - lemma_divisibility_factor (div_mod_lemmas.rs) - lemma_right_left_shift macro (shift_lemmas.rs) - proof_negate, lemma_neg (negate_lemmas.rs) - lemma_assemble_mod_div, lemma_from_bytes32_to_nat_01..01234 (from_bytes_lemmas.rs) Co-Authored-By: Claude Opus 4.5 <noreply@anthropic.com> * Update Rust toolchain to 1.92.0 for Verus 88f7396 Verus 88f7396 requires Rust 1.92.0 (was using 1.91.0) Co-Authored-By: Claude Opus 4.5 <noreply@anthropic.com> * Fix CI: update check-libsignal to Rust 1.92.0, minimize empty line diffs - Update check-libsignal job to use Rust 1.92.0 (matching Verus requirement) - Remove extra blank lines from modified lemma files Co-Authored-By: Claude Opus 4.5 <noreply@anthropic.com> * Run verusfmt to fix formatting Co-Authored-By: Claude Opus 4.5 <noreply@anthropic.com> * Keep original proof code visible with assume(false) in nonlinear_arith block Co-Authored-By: Claude Opus 4.5 <noreply@anthropic.com> * Update CI to use new libsignal frozen branches for Verus 88f7396 - frozen_for_ci_verus_41c5885 -> frozen_for_ci_verus_88f7396 - frozen_for_ci_v0.84.0_verus_41c5885 -> frozen_for_ci_v0.84.0_verus_88f7396 Co-Authored-By: Claude Opus 4.5 <noreply@anthropic.com> * Clarify lemma_decompose comment format for Verus 88f7396 Co-Authored-By: Claude Opus 4.5 <noreply@anthropic.com> * Fix lemma_right_left_shift proof for Verus 88f7396 Remove assume(false) by adding assertions to prove that r fits in the type bounds. The key insight is proving r < pow2(n) <= MAX before the main equality assertion. Co-Authored-By: Claude Opus 4.5 <noreply@anthropic.com> * Fix lemma proofs for Verus 88f7396 - Fix lemma_assemble_mod_div: use nonlinear_arith for distributive law - Fix proof_negate: remove assume(false), proof works directly - Fix lemma_neg: replace lemma_mod_is_zero calls with nonlinear_arith Co-Authored-By: Claude Opus 4.5 <noreply@anthropic.com> * commit PR review suggestion Co-authored-by: Kukovec <jure.kukovec@gmail.com> * Refactor lemma_right_left_shift proof structure Per review feedback: move r < pow2 assertion inside the fundamental div_mod block and remove redundant r <= MAX assertion. Co-Authored-By: Claude Opus 4.5 <noreply@anthropic.com> * Run verusfmt Co-Authored-By: Claude Opus 4.5 <noreply@anthropic.com> * Fix lemma_divisibility_factor proof for Verus 88f7396 as in PR dalek-cryptography#649 Apply proof fix from PR dalek-cryptography#649 which uses explicit variable bindings to help the nonlinear_arith solver: - Introduce qb = (n / a) % b and ra = n % a - Add explicit non-negativity assertions (qb >= 0, ra >= 0) - Break down the reasoning step by step Reference: Beneficial-AI-Foundation#649 Co-Authored-By: Claude Opus 4.5 <noreply@anthropic.com> * Fix lemma_cancel_mul_montgomery_mod proof for Verus 88f7396 The proof works without assume(false) - all the lemma calls establish the necessary relationships for the solver to complete the proof. Co-Authored-By: Claude Opus 4.5 <noreply@anthropic.com> * Remove unused lemma_verify_invert_correct This lemma had no actual proof (just assume(false)) and was not used anywhere in the codebase. The requires/ensures were commented out. Co-Authored-By: Claude Opus 4.5 <noreply@anthropic.com> --------- Co-authored-by: sbursuc <48085107+sbursuc@users.noreply.github.com> Co-authored-by: Claude Opus 4.5 <noreply@anthropic.com> Co-authored-by: Kukovec <jure.kukovec@gmail.com> * Verify compressed edwards functions and edwards identity (dalek-cryptography#648) * Verify CompressedEdwardsY: identity, default, try_from, from_slice Complete proofs for 4 functions in CompressedEdwardsY that previously used assume statements: - identity(): Add lemma_bytes32_to_nat_identity to prove that bytes32_to_nat([1,0,...,0]) == 1, then chain through spec to prove spec_field_element_from_bytes == 1 - default(): Works automatically (delegates to identity()) - from_slice(): Add compressed_edwards_y_from_array_result helper in core_assumes.rs to provide Verus with postconditions for Result::map - try_from(): Works automatically (delegates to from_slice()) Co-Authored-By: Claude Opus 4.5 <noreply@anthropic.com> * Add lemmas and proof for EdwardsPoint::identity(): - constants_lemmas.rs: Add lemma_zero_field_element_value() and lemma_zero_limbs_bounded_51() for FieldElement::ZERO constant - curve_equation_lemmas.rs: Add lemma_identity_on_curve() proving (0,1) is on the Edwards curve, and lemma_identity_is_valid_extended() proving the identity point (0,1,1,0) is a valid extended Edwards point - edwards.rs: Update EdwardsPoint::identity() to use these lemmas, fully proving is_identity_edwards_point and is_well_formed_edwards_point without any assume statements Co-Authored-By: Claude Opus 4.5 <noreply@anthropic.com> * Improve comment for compressed_edwards_y_from_array_result wrapper Clarify that the wrapper specifies properties expected to hold for Result::map, which Verus cannot automatically verify. Co-Authored-By: Claude Opus 4.5 <noreply@anthropic.com> * Rearrange lemma_bytes32_to_nat_identity proof Move lemma2_to64() call inside assert-by block for consistency with other explicit proof style. Co-Authored-By: Claude Opus 4.5 <noreply@anthropic.com> --------- Co-authored-by: sbursuc <48085107+sbursuc@users.noreply.github.com> Co-authored-by: Claude Opus 4.5 <noreply@anthropic.com> * Fix and refactor proofs to get rid new assertion failures and rlimits with verus 88f7396 (dalek-cryptography#649) * negate proof fix Co-Authored-By: Claude Opus 4.5 <noreply@anthropic.com> * fix lemma_right_left_shift Co-Authored-By: Claude Opus 4.5 <noreply@anthropic.com> * fix: stabilize proofs for Z3 4.15.4 compatibility Add explicit intermediate assertions to help Z3 4.15.4 complete proofs that worked implicitly with Z3 4.12.5: - pow_lemmas: fix precondition (offset + k < len, not <=), add base case hints for pow2_sum_bounds macro - div_mod_lemmas: decompose nonlinear_arith into explicit steps for lemma_divisibility_factor - number_theory_lemmas: use existing lemma_divides_linear_combo_sub, add multiplication identity hint for binomial sum proof Co-Authored-By: Claude Opus 4.5 <noreply@anthropic.com> * fix: use nonlinear_arith for distributive property in from_bytes_lemmas Replace lemma call with explicit nonlinear_arith assertions for the distributive property (a+b)*c == a*c + b*c in lemma_assemble_mod_div. Co-Authored-By: Claude Opus 4.5 <noreply@anthropic.com> * fix: add explicit steps for x²=0 proof in curve_equation_lemmas Add intermediate assertions to help Z3 connect (x*x)%p with ((x%p)*(x%p))%p when x%p==0. Co-Authored-By: Claude Opus 4.5 <noreply@anthropic.com> * fix: add explicit steps for edwards curve proofs in step1_lemmas Add intermediate assertions for x²=0, x²y²=0, d·x²y²=0, and field arithmetic to help Z3 verify math_on_edwards_curve(0, y). Co-Authored-By: Claude Opus 4.5 <noreply@anthropic.com> * fix: skip vstd TryFrom spec verification for CompressedEdwardsY Add #[verifier::external_body] to try_from to skip vstd's generic TryFrom spec verification. Our custom ensures clause is sufficient. Co-Authored-By: Claude Opus 4.5 <noreply@anthropic.com> * fix: add explicit shift-to-mul proof in load8_lemmas Add lemma_u64_shl_is_mul call with proper preconditions to prove that byte shift operations are bounded. Establishes byte_val * pow2(shift) <= u64::MAX before converting shift to multiplication. Co-Authored-By: Claude Opus 4.5 <noreply@anthropic.com> * fix: use correct distributive lemma in scalar_to_bytes_lemmas Replace lemma_mul_is_distributive_add with lemma_mul_is_distributive_add_other_way for (a+b)*x = a*x + b*x form. The original lemma proves x*(a+b) = x*a + x*b which requires commutativity. Co-Authored-By: Claude Opus 4.5 <noreply@anthropic.com> * Preserve original asserts as comments in from_bytes_lemmas The distributive property asserts were replaced with assumes due to a gap in converting between nat*nat and int*int arithmetic. The original asserts with their lemma invocations are now preserved as comments for later reference when addressing the proof gap. Co-Authored-By: Claude Opus 4.5 <noreply@anthropic.com> * Replace failing assert with assume in limbs_to_bytes_lemmas The assert proving bytes[20..24] sum equals middle_value * pow2(160) was failing. Replaced with assume and preserved the original assert as a comment for later reference. Co-Authored-By: Claude Opus 4.5 <noreply@anthropic.com> * rm 2 rlimits and intro 1 assume Co-Authored-By: Claude Opus 4.5 <noreply@anthropic.com> * Fix rlimit in scalar_lemmas by replacing broadcast use - lemma_five_limbs_equals_to_nat: Replace broadcast use with explicit lemma invocations for commutativity and distributivity - lemma_nine_limbs_equals_slice128_to_nat: Same pattern, with assume for intermediate step - lemma_seq_u64_to_nat_subrange_extend: Replace broadcast with assume for algebraic expansion step Reduces errors from 6 to 2, increases verified from 1203 to 1207. Co-Authored-By: Claude Opus 4.5 <noreply@anthropic.com> * Add helper lemma and fix rlimit in limbs_to_bytes_lemmas - Add lemma_5_bytes_scale: helper for scaling 5-byte sums by power of 2 - Use nonlinear_arith for clean distributivity proofs - Fix lemma_limb1_contribution_correctness without using assume - Use explicit pow2 assertions to guide solver Increases verified from 1203 to 1211. Co-Authored-By: Claude Opus 4.5 <noreply@anthropic.com> * Add rlimit attribute to batch_invert for while loop The backward loop in batch_invert has 9 invariants that require more solver time. Add #[verifier::rlimit(50)] to give the solver adequate resources. All 1212 verified, 0 errors. Co-Authored-By: Claude Opus 4.5 <noreply@anthropic.com> * refactor lemma_right_left_shift Co-Authored-By: <jure.kukovec@gmail.com> Co-Authored-By: Claude Opus 4.5 <noreply@anthropic.com> * fix an assertion failure in negate Co-Authored-By: Claude Opus 4.5 <noreply@anthropic.com> * verusfmt Co-Authored-By: Claude Opus 4.5 <noreply@anthropic.com> * bring back 4 asserts in from_bytes_lemmas Co-Authored-By: Claude Opus 4.5 <noreply@anthropic.com> * bring back assert in lemma_limb3_contribution_correctness Co-Authored-By: Claude Opus 4.5 <noreply@anthropic.com> * rm forgotten no longer relevant comment Co-Authored-By: Claude Opus 4.5 <noreply@anthropic.com> * fix lemma_nine_limbs_equals_slice128_to_nat and refactor lemma_five_limbs_equals_to_nat Co-Authored-By: Claude Opus 4.5 <noreply@anthropic.com> * remove introduced assume in lemma_seq_u64_to_nat_subrange_extend Co-Authored-By: Claude Opus 4.5 <noreply@anthropic.com> * verusfmt Co-Authored-By: Claude Opus 4.5 <noreply@anthropic.com> * address comment from reviewer Co-Authored-By: Claude Opus 4.5 <noreply@anthropic.com> * refactor proof as per Sergiu's comment Co-Authored-By: Claude Opus 4.5 <noreply@anthropic.com> * remove outdated comment as Sergiu suggests Co-Authored-By: Claude Opus 4.5 <noreply@anthropic.com> * fix from_bytes lemmas Fix Verus verification failures in from_bytes_lemmas.rs by adding explicit int-to-nat type bridges using nonlinear_arith. Co-Authored-By: Claude Opus 4.5 <noreply@anthropic.com> * Apply suggestions from code review Co-authored-by: Kukovec <jure.kukovec@gmail.com> * use lemma_mul_distributive_5_terms instead of nonlinear_arith, as suggested by Jure Co-Authored-By: Claude Opus 4.5 <noreply@anthropic.com> * simplify the proof for lemma_load8_at_plus_version_is_spec Co-Authored-By: kukovec <jure.kukovec@gmail.com> Co-Authored-By: Claude Opus 4.5 <noreply@anthropic.com> * Update curve25519-dalek/src/lemmas/field_lemmas/from_bytes_lemmas.rs Co-authored-by: Kukovec <jure.kukovec@gmail.com> * Add lemma_nat_distributive wrapper for int-to-nat type bridging vstd's lemma_mul_is_distributive_add_other_way cannot be inlined directly for nat assertions - Verus only bridges int results to nat at function boundaries. The wrapper lemma_nat_distributive provides the nat-typed postcondition that enables this bridging. Use this in lemma_assemble_mod_div to replace nonlinear_arith. Co-Authored-By: Claude Opus 4.5 <noreply@anthropic.com> --------- Co-authored-by: Kukovec <jure.kukovec@gmail.com> Co-authored-by: Claude Opus 4.5 <noreply@anthropic.com> * decouple callgraph generation from website deployment (dalek-cryptography#655) Split the callgraph generation into a separate workflow to speed up website deployments from ~10 minutes to ~1-2 minutes. Changes: - New generate-callgraph.yml: generates callgraph on Rust file changes, daily schedule, and manual dispatch; saves result to GitHub Actions cache - Modified deploy-pages.yml: restores callgraph from cache instead of waiting for generation; deploys immediately The callgraph is now "one commit behind" - fresh stats deploy immediately while the callgraph updates in the background for the next deployment. Also adds Verus and Rust version extraction from Cargo.toml metadata for the callgraph generation workflow. Co-authored-by: Claude Opus 4.5 <noreply@anthropic.com> * Proofs for EdwardsPoint::is_valid and field element <-> bytes conversion (dalek-cryptography#652) * Edwards is_valid proof and helper lemmas * some field algebra lemmas * change is_valid spec style following PR comments * remove unused lemmas and variables * scope lemma calls into assert by blocks * Push hashes for verification reports to Sepolia and ethereum mainnet (dalek-cryptography#627) * feat: add certifications section linking to Sepolia Etherscan events Co-Authored-By: Claude Opus 4.5 <noreply@anthropic.com> * Add workflow to certify verification results on Sepolia Co-Authored-By: Claude Opus 4.5 <noreply@anthropic.com> * push to mainnet Co-Authored-By: Claude Opus 4.5 <noreply@anthropic.com> * feat: add certification history tracking to GitHub Pages - Capture tx hashes from mainnet/Sepolia certifications - Store mapping in docs/certifications.json (commit on each run) - Display certification history table on dashboard - Remove static Etherscan link injection from deploy-pages Co-Authored-By: Claude Opus 4.5 <noreply@anthropic.com> * chore: update certifications.json with tx 0xb6897f66d8c7fa283cd87f62c663d1c4206d247fc178aa6d500c845633e77ad7 Co-Authored-By: Claude Opus 4.5 <noreply@anthropic.com> * test cert table Co-Authored-By: Claude Opus 4.5 <noreply@anthropic.com> * refactor: update workflow to use probe-verus (renamed from scip-atoms) Co-Authored-By: Claude Opus 4.5 <noreply@anthropic.com> * get verus version from toml Co-Authored-By: Claude Opus 4.5 <noreply@anthropic.com> * fix: add probe-verus atomize step to generate required atoms.json Co-Authored-By: Claude Opus 4.5 <noreply@anthropic.com> * chore: update certifications.json with tx 0x31ecf1e408f7c3a1076a91f5cc94590302902de73117afd40c45f08f18369362 Co-Authored-By: Claude Opus 4.5 <noreply@anthropic.com> * test: trigger deploy Co-Authored-By: Claude Opus 4.5 <noreply@anthropic.com> --------- Co-authored-by: Claude Opus 4.5 <noreply@anthropic.com> Co-authored-by: github-actions[bot] <github-actions[bot]@users.noreply.github.com> * bounds relaxation * 52 -> 54 bound in neg * gitignore * fmt * PR comments * typo --------- Co-authored-by: Sergiu Bursuc <48085107+sergiubur@users.noreply.github.com> Co-authored-by: sbursuc <48085107+sbursuc@users.noreply.github.com> Co-authored-by: Claude Opus 4.5 <noreply@anthropic.com> Co-authored-by: astefano <lacramioara.astefanoaei@gmail.com> Co-authored-by: S M A Nahian <smanahian123@gmail.com> Co-authored-by: Copilot <198982749+Copilot@users.noreply.github.com> Co-authored-by: github-actions[bot] <github-actions[bot]@users.noreply.github.com>

…hy#658) * lemma_decompose proof + proof repair from z3 bump * fmt

…-cryptography#654) * proof for edwards conditional assign, mul_by_pow_2, is_torsion_free * fix specifications: spec_scalar vs scalar_to_nat issues * address PR review --------- Co-authored-by: sbursuc <48085107+sbursuc@users.noreply.github.com> Co-authored-by: astefano <lacramioara.astefanoaei@gmail.com> Co-authored-by: Claude Opus 4.5 <noreply@anthropic.com>

…aphy#662) * refactor: simplify certify workflow using probe-verus and certify actions Replace manual tool installation and CLI invocation with reusable GitHub actions from the BAIF organization: - Use probe-verus/action@v1 for verification (handles Rust, Verus, scip setup) - Use certify/action@v1 for Ethereum certification (mainnet and sepolia) Co-Authored-By: Claude Opus 4.5 <noreply@anthropic.com>

* Fix assume detection to handle block comments The script was incorrectly marking functions as not having complete proofs when the word "assume" appeared inside block comments (/* ... */). For example, pow2k had this in its ensures clause: ensures/* VERIFICATION NOTE: - proof needs completed: one assume left */ The word "assume" in the comment was being detected as an actual assume statement, causing the function to be marked as proof=False. Fix: Strip all block comments before checking for assume statements. Co-authored-by: Cursor <cursoragent@cursor.com> * Remove outdated comment from pow2k (proof is complete) Co-authored-by: Cursor <cursoragent@cursor.com> --------- Co-authored-by: sbursuc <48085107+sbursuc@users.noreply.github.com> Co-authored-by: Cursor <cursoragent@cursor.com>

- Proofs for Edwards compress and create functions - Proofs and axioms for some algrebraic facts on Edwards curve additions and multiplication Co-Authored-By: Claude Opus 4.5 <noreply@anthropic.com>

* Verify mul_bits_be Montgomery ladder and ProjectivePoint::identity Prove correctness of MontgomeryPoint::mul_bits_be (Algorithm 8 from Costello-Smith 2017) for computing [n]P on the Montgomery curve. - Enhanced differential_add_and_double spec with: - Limb bounds preconditions/postconditions (fe51_limbs_bounded at 54/51) - Ladder-step postconditions expressing [k]P, [k+1]P → [2k]P, [2k+1]P * Verify ProjectivePoint::identity(): * Prove bounds for differential_add_and_double field operations * Strengthened ProjectivePoint::identity spec with 51-bounded postconditions * Clean up mul_bits_be proof and tighten bounds assertions * Complete differential_add_and_double and mul_bits_be verification * Structure Montgomery ladder verification using axiom-based approach: ## Architecture (Costello-Smith 2017) 1. **Algebraic Specs** (montgomery_specs.rs) — Algorithms 1 & 2: - `spec_xdbl_projective`: U' = (U+W)²·(U−W)², W' = [(U+W)²−(U−W)²]·[...] - `spec_xadd_projective`: U' = [...+...]², W' = u_diff·[...−...]² 2. **Axioms** (montgomery_curve_lemmas.rs) — Equations 9 & 10: - `axiom_xdbl_projective_correct`: xDBL computes [2]P - `axiom_xadd_projective_correct`: xADD computes P+Q 3. **Implementation Proof** (montgomery.rs): - differential_add_and_double outputs match spec functions - Axioms applied to get scalar multiplication correctness - mul_bits_be loop invariant updated with projective representation * Fix Montgomery ladder infinity representation Tighten the projective (U:W) representation predicate for infinity to exclude the degenerate (0:0) case (require U!=0 when W==0). This avoids unsound uses of x-only formulas (xADD/xDBL) and lets the Montgomery ladder proof apply xADD/xDBL axioms without introducing new assume()s in differential_add_and_double. * Improve Montgomery curve comments and cleanup unused lemmas * Remove unused trivial lemmas, add rlimit notes * Refactor differential_add_and_double proofs to assert...by style * Add ladder_invariant spec fn to simplify mul_bits_be proof * Address PR review comments Co-authored-by: Cursor <cursoragent@cursor.com>

* Verify EdwardsBasepointTable::mul_base function This commit adds verification proofs for the mul_base function which implements scalar multiplication using precomputed tables (radix-16 Pippenger method). Also: - Add lemmas for signed scalar multiplication (for negative digits) - Prove signed composition lemma from negation distribution axiom - Add axiom_scalar_mul_distributes_over_neg: [n](-P) = -([n]P) - Simplify proof blocks: move lemmas into assert-by blocks - Make ladder_invariant opaque and reveal only at needed points - Add lemma_ladder_invariant_swap and use it to avoid repeated unfolding inside the loop - Strengthen/restore facts required to trigger differential_add_and_double postconditions - Address PR dalek-cryptography#668 review comments: - Fix typos - Change lemmas to use by-value parameters - Refactor loop1/loop2 proofs to share common logic: Co-authored-by: Claude Opus 4.5 <noreply@anthropic.com>

…tography#671) * Verus proofs for 5 Edwards point functions 1. EdwardsPoint::double 2. EdwardsPoint::neg 3. EdwardsPoint::as_projective_niels 4. EdwardsPoint::to_montgomery 5. EdwardsPoint::add New lemmas added: - lemma_edwards_d2_limbs_bounded() - EDWARDS_D2 has 51-bit bounded limbs - lemma_edwards_d2_limbs_bounded_54() - EDWARDS_D2 has 54-bit bounded limbs - lemma_negation_preserves_extended_validity() - negation preserves extended point validity - EDWARDS_D2 = 2*EDWARDS_D mod p New axioms added: - axiom_birational_edwards_montgomery: (z+y)/(z-y) = (1+y/z)/(1-y/z) * Fix mul_base rlimit by making Pippenger specs opaque Introduce small step lemmas to unfold even_sum_up_to/pippenger_partial only when needed, and use them in mul_base loop invariants. * Prove field identities used in Edwards point recovery * Move ladder_invariant to montgomery_specs and rename to montgomery_ladder_invariant; fix resulting rlimit issue Co-Authored-By: Claude Opus 4.5 <noreply@anthropic.com>

- Replace the RR workaround with direct constant usage in lemma statement. - Make the Montgomery cancellation step explicit to fix failing assert. Co-authored-by: sbursuc <48085107+sbursuc@users.noreply.github.com> Co-authored-by: Cursor <cursoragent@cursor.com>

Straightforward assert proofs for 4 edwards functions. Co-authored-by: Claude Opus 4.5 <noreply@anthropic.com>

* verify montgomery_reduce Co-Authored-By: Claude Opus 4.5 <noreply@anthropic.com> * Prove Scalar::mul without assumes by adding canonical preconditions Remove the two assume(scalar52_to_nat(...) < group_order()) statements from Scalar::mul by propagating canonicity through the type system: - unpack() now conditionally ensures is_canonical_scalar52 when input is canonical - MulSpecImpl::mul_req requires is_canonical_scalar for both operands - product_of_slice requires canonical inputs and maintains the invariant - collect_scalars_from_iter ensures canonical outputs (external_body) Co-Authored-By: Claude Opus 4.5 <noreply@anthropic.com> * make clippy happy Co-Authored-By: Claude Opus 4.5 <noreply@anthropic.com> * bring back unintended change Co-Authored-By: Claude Opus 4.5 <noreply@anthropic.com> * Remove unused montgomery_reduce_r4_safe_bound from active proof path montgomery_reduce requires canonical_bound (T < R×L), not r4_safe_bound (T < 2^520). Since canonical_bound is strictly stronger, the r4_safe_bound spec and its bridge lemmas were dead weight at every call site. - Remove 6 dead call sites across scalar.rs and backend/serial/u64/scalar.rs Co-Authored-By: Claude Opus 4.5 <noreply@anthropic.com> * Remove duplicate assertions in mul_assign proof block Co-Authored-By: Claude Opus 4.5 <noreply@anthropic.com> * Simplify montgomery_reduce proof by eliminating uniqueness chain Remove ~460 lines of lemma code by proving the REDC bound directly from the quotient relationship (intermediate × R = T + N×L) instead of routing through spec-level montgomery_quotient/montgomery_intermediate. Eliminated lemmas: lemma_montgomery_quotient_bounded, lemma_gcd_l_r_is_one, lemma_l_inv_mod_r_property, lemma_sum_zero_implies_neg, lemma_montgomery_quotient_unique, lemma_intermediate_equals_spec, lemma_canonical_bound_implies_intermediate_less_than_2L. Eliminated spec fns: l_inv_mod_r, montgomery_quotient, montgomery_intermediate. Co-authored-by: Cursor <cursoragent@cursor.com> * Remove unnecessary rlimit increases for from_bytes_wide and canonical_product lemma The rlimit(40) on from_bytes_wide and rlimit(20) on lemma_canonical_product_satisfies_canonical_bound were needed when the solver had to reason about complex montgomery_intermediate/quotient spec functions. With those eliminated, default rlimits suffice. Co-authored-by: Cursor <cursoragent@cursor.com> * Replace comment-based bounds with assert-by proofs and fix ORIGINAL CODE comments - Convert informal "// Goal: sumN < 2^108" comments into machine-checked `assert(...) by { ... }` blocks that prove the bound using lemma_m calls - Fix ORIGINAL CODE comments to use exact original lines from main (Self::part1/part2 and l.limbs[k] instead of part1/part2 and l[k]) Co-authored-by: Cursor <cursoragent@cursor.com> * Prove lemma_u128_truncate_and_mask and remove unused assume(false) stubs - Replace assume(false) in lemma_u128_truncate_and_mask with a real proof using lemma_u64_low_bits_mask_is_mod, lemma_u128_cast_64_is_mod, and lemma_mod_mod for the nested-mod step - Remove unused stubs lemma_u128_low_bits_mask_is_mod and lemma_u128_truncate_to_u64 (never called in active proof) - Fix ORIGINAL CODE comments to use exact original lines from main - Replace comment-based bounds with assert-by proofs in montgomery_reduce Co-authored-by: Cursor <cursoragent@cursor.com> * Fix from_bytes_wide verification by bridging multiplication commutativity The lemma_fundamental_div_mod_converse precondition requires x == q * d + r (high_expr * pow2_260), but the established fact uses pow2_260 * high_expr. Add lemma_mul_is_commutative call to bridge the operand order, fixing the CI verification failure. Co-authored-by: Cursor <cursoragent@cursor.com> * Remove proof-development scaffolding tests and docs now superseded by formal proof Co-Authored-By: Claude Opus 4.5 <noreply@anthropic.com> * reduce older tests for the previous montgomery_reduce spec Co-Authored-By: Claude Opus 4.5 <noreply@anthropic.com> * bring back original code in montgomery_reduce callers Co-Authored-By: Claude Opus 4.5 <noreply@anthropic.com> * Remove orphaned proptest regression seeds and directory Co-Authored-By: Claude Opus 4.5 <noreply@anthropic.com> * u64/scalar.rs: remove some comments and push lemma calls in assert ...by blocks Co-authored-by: Cursor <cursoragent@cursor.com> * u64/scalar.rs: prove axiom, deduplicate proof, clean up comments - Replace axiom_two_l_div_pow2_208_le_pow2_45 (admit) with fully proven lemma_two_l_div_pow2_208_eq_pow2_45 - Deduplicate shared lemma calls in Section 6 of montgomery_reduce - Remove historical migration notes, stale doc references, and internal development labels from scalar_lemmas_ and specs Co-authored-by: Cursor <cursoragent@cursor.com> * Remove stale doc references and clean up proof comments Co-Authored-By: Claude Opus 4.6 <noreply@anthropic.com> --------- Co-authored-by: Claude Opus 4.5 <noreply@anthropic.com> Co-authored-by: sbursuc <48085107+sbursuc@users.noreply.github.com> Co-authored-by: Cursor <cursoragent@cursor.com>

…b) (dalek-cryptography#686) Strengthen add_req to require is_canonical_scalar for both operands, matching the existing pattern used by mul_req and sub_req. This lets unpack()'s conditional postcondition provide scalar52_to_nat < group_order(), eliminating all three assumes in the add proof. Propagate the requirement to AddAssign and sum_of_slice. Co-authored-by: Claude Opus 4.6 <noreply@anthropic.com>

* Add loop invariants and specs for Straus multiscalar multiplication * Prove axiom_straus_ct_correct and axiom_straus_vt_correct (remove admit) * Prove lemma_identity_projective_point_properties, remove VT assume * Convert failing lemma_identity_projective_niels_is_identity to axiom with admit() * Add is_valid_projective_niels_point ensures to NafLookupTable5::select * Remove redundant axioms after rebase on main (dalek-cryptography#722) * Remove rlimit annotations by scoping proof steps in assert-by blocks * Add efficient error extraction patterns to verus skill and CLAUDE.md * Simplify and deduplicate Straus multiplication proofs Co-authored-by: Claude Opus 4.6 <noreply@anthropic.com> Co-authored-by: Lacramioara Astefanoaei <lacramioara.astefanoaei@gmail.com>

…graphy#728) * Refactor EdwardsPoint to pub(crate) fields with closed spec accessors Also convert pub const to pub exec const for ED25519_BASEPOINT_POINT, EIGHT_TORSION, and RISTRETTO_BASEPOINT_POINT, with spec_eight_torsion() for proof-mode access. * Add type invariant for EdwardsPoint * Add ensures to exec constants and fix scalar proof * Prove ct_eq precondition from type invariant and remove unused trait * Remove axioms by deriving properties from EdwardsPoint type invariant Co-authored-by: Cursor <cursoragent@cursor.com>

* verify sub_new and conditional_add_l Co-Authored-By: Claude Opus 4.6 <noreply@anthropic.com> * address comment from Sergiu and use call-by-value in one lemma Co-Authored-By: Claude Opus 4.6 <noreply@anthropic.com> * move other asserts to proof blocks and bring back bounded limbs postcondition Co-Authored-By: Claude Opus 4.6 <noreply@anthropic.com> --------- Co-authored-by: Claude Opus 4.6 <noreply@anthropic.com>

* Fix rlimit in straus VT inner loop by making straus_vt_input_valid opaque The inner while loop in optional_multiscalar_mul_verus exceeded Z3's resource limit due to 6 forall quantifiers in straus_vt_input_valid being unfolded everywhere, causing 13,880 quantifier instantiations. Mark straus_vt_input_valid as #[verifier::opaque] and add three targeted helper lemmas (extract, lengths, establish) that reveal the definition only in small scopes. Surface the specific facts needed by the inner loop (NAF sequence lengths, point canonicality) as explicit invariants. Quantifier instantiations drop from 13,880 to 4,704 (66% reduction). Full codebase: 1739 verified, 0 errors (was 1735 verified, 1 error). Co-Authored-By: Claude Opus 4.6 <noreply@anthropic.com> * finish the proof for AffineNielsPoint::select Co-Authored-By: Claude Opus 4.6 <noreply@anthropic.com> * finish the proof for AffineNielsPoint::select Co-Authored-By: Claude Opus 4.6 <noreply@anthropic.com> * eliminate 5 assumes in lemma_negate_affine_niels_preserves_validity This is done by adding lemma_edwards_point_invariant, an external_body bridge that exposes the EdwardsPoint type invariant for spec-mode values from choose (where use_type_invariant is unavailable). Also stabilize a borderline pow2 proof in scalar.rs. Co-Authored-By: Claude Opus 4.6 <noreply@anthropic.com> * Remove lemma_edwards_point_invariant by strengthening is_valid_affine_niels_point Instead of using an external_body bridge lemma to expose the type invariant for choose-obtained EdwardsPoint values, strengthen the is_valid_affine_niels_point existential to include edwards_point_limbs_bounded and sum_of_limbs_bounded. This makes choose witnesses carry full type-invariant strength directly. Co-authored-by: Cursor <cursoragent@cursor.com> * Remove opaque straus_vt_input_valid workaround, use assert-by scoping instead Replace the complex opaque predicate machinery (establish/extract/lengths helper lemmas + surfaced loop invariants) with simpler assert-by blocks that scope lemma calls to reduce rlimit pressure. Also apply the coset4 assert-by fix for lemma_unfold_edwards. The assert-by approach from PR dalek-cryptography#730 achieves the same rlimit reduction with far less code complexity. Co-authored-by: Cursor <cursoragent@cursor.com> * Simplify and refactor select proof and supporting lemmas Remove redundant assertions from LookupTable<AffineNielsPoint>::select proof (~80 lines removed), including verbose limb bounds, unnecessary loop invariants for immutable variables, and entire post-loop proof block. Refactor floating lemma calls into assert...by blocks throughout select and its two supporting lemmas (lemma_identity_affine_niels_valid, lemma_negate_affine_niels_preserves_validity) so each lemma serves as an explicit justification for a stated goal. Co-Authored-By: Claude Opus 4.6 <noreply@anthropic.com> Co-authored-by: Cursor <cursoragent@cursor.com> * Update Verus skills with type invariant + existential and rlimit patterns Add guidance for strengthening existentials to carry type invariant properties when choose witnesses are spec-mode, using public accessors in pub open spec fn, and bridge asserts for reference-based predicates. Update rlimit advice to prefer assert-by scoping over opaque predicates. Co-authored-by: Cursor <cursoragent@cursor.com> * simplify comments Co-Authored-By: Claude Opus 4.6 <noreply@anthropic.com> --------- Co-authored-by: Claude Opus 4.6 <noreply@anthropic.com> Co-authored-by: sbursuc <48085107+sbursuc@users.noreply.github.com> Co-authored-by: Cursor <cursoragent@cursor.com>

* Prove EdwardsPoint ct_eq * Refactor lemma_cross_mul_iff_div_eq to assert..by style, update skill guidance Co-authored-by: Cursor <cursoragent@cursor.com>

) Replace assume(false) with a full proof for ProjectiveNielsPoint::select, mirroring the existing AffineNielsPoint::select proof structure. Supporting changes: - Add lemma_identity_projective_niels_valid and lemma_negate_projective_niels_preserves_validity - Add conditional_negate_projective_niels external-body wrapper - Strengthen is_valid_projective_niels_point existential to include edwards_point_limbs_bounded (needed for choose witness limb access) - Propagate per-entry validity through From, straus_ct_input_valid, and variable_base loop invariant Co-authored-by: Claude Opus 4.6 <noreply@anthropic.com>

…ek-cryptography#734) * 64/scalar * edwards * field * montgomery * ristretto * scalar * post-refactor + fmt * Fix rlimit issues in variable_base::mul and montgomery hash (dalek-cryptography#737) * Verify AffineNielsPoint::select (dalek-cryptography#735) * Fix rlimit in straus VT inner loop by making straus_vt_input_valid opaque The inner while loop in optional_multiscalar_mul_verus exceeded Z3's resource limit due to 6 forall quantifiers in straus_vt_input_valid being unfolded everywhere, causing 13,880 quantifier instantiations. Mark straus_vt_input_valid as #[verifier::opaque] and add three targeted helper lemmas (extract, lengths, establish) that reveal the definition only in small scopes. Surface the specific facts needed by the inner loop (NAF sequence lengths, point canonicality) as explicit invariants. Quantifier instantiations drop from 13,880 to 4,704 (66% reduction). Full codebase: 1739 verified, 0 errors (was 1735 verified, 1 error). Co-Authored-By: Claude Opus 4.6 <noreply@anthropic.com> * finish the proof for AffineNielsPoint::select Co-Authored-By: Claude Opus 4.6 <noreply@anthropic.com> * finish the proof for AffineNielsPoint::select Co-Authored-By: Claude Opus 4.6 <noreply@anthropic.com> * eliminate 5 assumes in lemma_negate_affine_niels_preserves_validity This is done by adding lemma_edwards_point_invariant, an external_body bridge that exposes the EdwardsPoint type invariant for spec-mode values from choose (where use_type_invariant is unavailable). Also stabilize a borderline pow2 proof in scalar.rs. Co-Authored-By: Claude Opus 4.6 <noreply@anthropic.com> * Remove lemma_edwards_point_invariant by strengthening is_valid_affine_niels_point Instead of using an external_body bridge lemma to expose the type invariant for choose-obtained EdwardsPoint values, strengthen the is_valid_affine_niels_point existential to include edwards_point_limbs_bounded and sum_of_limbs_bounded. This makes choose witnesses carry full type-invariant strength directly. Co-authored-by: Cursor <cursoragent@cursor.com> * Remove opaque straus_vt_input_valid workaround, use assert-by scoping instead Replace the complex opaque predicate machinery (establish/extract/lengths helper lemmas + surfaced loop invariants) with simpler assert-by blocks that scope lemma calls to reduce rlimit pressure. Also apply the coset4 assert-by fix for lemma_unfold_edwards. The assert-by approach from PR dalek-cryptography#730 achieves the same rlimit reduction with far less code complexity. Co-authored-by: Cursor <cursoragent@cursor.com> * Simplify and refactor select proof and supporting lemmas Remove redundant assertions from LookupTable<AffineNielsPoint>::select proof (~80 lines removed), including verbose limb bounds, unnecessary loop invariants for immutable variables, and entire post-loop proof block. Refactor floating lemma calls into assert...by blocks throughout select and its two supporting lemmas (lemma_identity_affine_niels_valid, lemma_negate_affine_niels_preserves_validity) so each lemma serves as an explicit justification for a stated goal. Co-Authored-By: Claude Opus 4.6 <noreply@anthropic.com> Co-authored-by: Cursor <cursoragent@cursor.com> * Update Verus skills with type invariant + existential and rlimit patterns Add guidance for strengthening existentials to carry type invariant properties when choose witnesses are spec-mode, using public accessors in pub open spec fn, and bridge asserts for reference-based predicates. Update rlimit advice to prefer assert-by scoping over opaque predicates. Co-authored-by: Cursor <cursoragent@cursor.com> * simplify comments Co-Authored-By: Claude Opus 4.6 <noreply@anthropic.com> --------- Co-authored-by: Claude Opus 4.6 <noreply@anthropic.com> Co-authored-by: sbursuc <48085107+sbursuc@users.noreply.github.com> Co-authored-by: Cursor <cursoragent@cursor.com> * Fix rlimit in variable_base::mul loop by scoping lemma calls Co-Authored-By: Claude Opus 4.6 <noreply@anthropic.com> * Fix montgomery hash rlimit in libsignal verification context Scope lemma calls and proof steps in assert-by blocks to prevent Z3 quantifier pressure when verifying curve25519-dalek as a dependency of libsignal/rust/usernames, where the solver has many more axioms in scope. The two byte-expansion lemmas (lemma_from_u8_32_as_nat, lemma_as_nat_32_mod_255) and the array conversion + hash model reasoning (steps 3-5) were leaking large postconditions into the main context. Co-Authored-By: Claude Opus 4.6 <noreply@anthropic.com> --------- Co-authored-by: Claude Opus 4.6 <noreply@anthropic.com> Co-authored-by: sbursuc <48085107+sbursuc@users.noreply.github.com> Co-authored-by: Cursor <cursoragent@cursor.com> * post-rebase fix * Fix rlimit in batch_invert backward loop by scoping lemma calls (dalek-cryptography#740) Scope floating lemma calls in the backward loop of batch_invert (scalar.rs) inside assert-by blocks to limit Z3's solver context. The three structural lemmas (group_order_bound, pow2_strictly_increases, small_mod) and two semantic lemmas (backward_loop_is_inverse, backward_loop_acc_invariant) were leaking postconditions into the main loop context, causing rlimit pressure after rebase onto main. Full codebase: 1751 verified, 0 errors. Co-authored-by: Claude Opus 4.6 <noreply@anthropic.com> Co-authored-by: Cursor <cursoragent@cursor.com> --------- Co-authored-by: Lacramioara Astefanoaei <lacramioara.astefanoaei@gmail.com> Co-authored-by: Claude Opus 4.6 <noreply@anthropic.com> Co-authored-by: sbursuc <48085107+sbursuc@users.noreply.github.com> Co-authored-by: Cursor <cursoragent@cursor.com>

* Verify all 6 `from` implementations in window.rs, removing 65 assumes Replace assume(...) scaffolding with actual proofs in all LookupTable and NafLookupTable from-implementations by adding loop invariants that track limb bounds, validity, and mathematical correspondence (scalar multiplication) for each table entry. Functions proven: - LookupTable<ProjectiveNielsPoint>::from (12 assumes removed) - LookupTable<AffineNielsPoint>::from (11 assumes removed) - NafLookupTable5<ProjectiveNielsPoint>::from (11 assumes removed) - NafLookupTable5<AffineNielsPoint>::from (10 assumes removed) - NafLookupTable8<ProjectiveNielsPoint>::from (11 assumes removed) - NafLookupTable8<AffineNielsPoint>::from (10 assumes removed) Strengthen as_affine_niels postcondition in edwards.rs to include fe51_limbs_bounded for y_plus_x, y_minus_x, and xy2d (matching the existing as_projective_niels postcondition). Co-Authored-By: Claude Opus 4.6 <noreply@anthropic.com> * verify NafLookupTable5<ProjectiveNielsPoint>::select Co-Authored-By: Claude Opus 4.6 <noreply@anthropic.com> --------- Co-authored-by: Claude Opus 4.6 <noreply@anthropic.com>

* Verify Pippenger optional_multiscalar_mul_verus * Fix straus rlimit by scoping lemma calls in assert-by blocks, apply verusfmt * Reduce batch_invert rlimit pressure with explicit triggers and tighter scoping * Update verus-proof-helper skill with rlimit techniques from Pippenger work * Restore ORIGINAL CODE / REFACTORED CODE comments in pippenger.rs * Extract process_column helper, restructure Horner to match upstream hi_column + fold * Replace Ghost params in process_column with spec functions * Simplify proofs: remove redundant assertions, drop unused rlimit * Address PR review comments Co-authored-by: Claude Opus 4.6 <noreply@anthropic.com>

…graphy#744) Remove remaining assume in pippenger scalar mul

* verify ristretto::decompress rm auto triggers Replace assume() in ristretto::decompress::step_2 with axioms Add spec_ristretto_decode_inner/x/y/ok and is_ristretto_decode_output predicate to ristretto_specs.rs. Introduce axiom_ristretto_decode_on_curve and axiom_ristretto_decode_in_even_subgroup with admit() bodies, replacing the two assume() calls in step_2 with axiom invocations and bridging lemmas. Add runtime tests validating both axioms computationally. Update axiom_references.md to document all 52 axioms in the codebase, removing 3 phantom entries, adding 9 undocumented axioms, and fixing the file location for axiom_edwards_to_montgomery_correspondence. Harden ristretto::decompress proof: mechanize axiom, eliminate assume, add tests - Mechanize axiom_sqrt_ratio_mutual_exclusion into a full proof (lemma_sqrt_ratio_mutual_exclusion) using lemma_no_square_root_when_times_i - Eliminate unsound assume(is_on_edwards_curve_projective) in step_2 by returning EdwardsPoint::identity() on the failure path - Move sqrt-related axioms/lemmas to sqrt_ratio_lemmas.rs for modularity - Rename lemmas containing admit()/assume() to axiom_ per convention - Add runtime tests for axiom_invsqrt_unique, axiom_sqrt_m1_limbs_bounded, and axiom_minus_one_field_element_value - Strengthen test_ristretto_decode_in_even_subgroup with diverse inputs - Write mathematical proofs (decompress.md, step_1.md, step_2.md) and Verus proof mapping document - Update axiom_references.md with current status of all axioms Remove unsound axiom_ristretto_point_from_coords from decompress proof The axiom bridged exec structural equality to spec `choose` semantics, but was unsound: spec_edwards_point maps through fe51_as_canonical_nat which is not injective on limb representations, so multiple RistrettoPoints could satisfy the choose predicate while being structurally different. The postcondition `result == spec_ristretto_decompress(self.0)` that depended on this axiom is removed. The remaining 4 postconditions (None/Some alignment, coordinate equality via spec_ristretto_decompress_coords, well-formedness, even subgroup membership) provide all mathematical correctness guarantees. No downstream code depended on structural equality. Narrow axiom_ristretto_decode_on_curve to the square case Runtime testing showed the axiom overclaimed: it asserted on-curve for both is_sqrt_ratio and is_sqrt_ratio_times_i cases, but the algebraic identity only holds for the square case (is_sqrt_ratio). Added the is_sqrt_ratio precondition and moved the call site into the if choice_is_true(ok) block where that precondition is satisfied. Verus still verifies 55/55, all 6 axiom tests pass. Supporting changes from the decompress proof review: - Extract lemma_canonical_nat_lt_p to reduce boilerplate - Add test_sqrt_m1_not_square (Euler's criterion) - Strengthen test_invsqrt_unique (distinctness, nonsquare input) - Expand test_ristretto_decode_on_curve (edge cases, hash-derived) - Add deprecation note on spec_ristretto_decompress (choose issue) - Update step_2.md: mutual exclusion is PROVEN - Update verus_proof_mapping.md: test coverage, action items Harden decompress proof: prove axiom, add tests, fix type invariant error - Prove axiom_sqrt_m1_limbs_bounded via concrete limb checks + bit_vector, rename to lemma_sqrt_m1_limbs_bounded (no longer an axiom) - Add axiom_invsqrt_exists to justify the choose in nat_invsqrt spec - Add test_p_is_prime: Miller-Rabin with 9 witnesses + Fermat check - Fix pre-existing Verus error "constructed value may fail to meet its declared type invariant" by moving the on-curve proof before the EdwardsPoint construction (1772 verified, 0 errors) - Update docs: step_2.md degenerate case, axiom_references.md, verus_proof_mapping.md Co-Authored-By: Claude Opus 4.6 <noreply@anthropic.com> * Simplify ristretto decompress proof: remove redundant spec and axiom params - Delete `is_ristretto_decode_output` predicate that duplicated `spec_ristretto_decode_inner` - Simplify `axiom_ristretto_decode_on_curve` from 4 params to 1 (just `s: nat`) - Simplify `axiom_ristretto_decode_in_even_subgroup` from 5 params to 2 (`s`, `point`) - Extract `lemma_decode_invsqrt_facts` helper to deduplicate invsqrt+mutual-exclusion proof - Remove ~135 lines net (74 added, 209 removed) Verification: 1801 verified, 0 errors. All tests pass. Co-Authored-By: Claude Opus 4.6 <noreply@anthropic.com> * Factor decode spec helpers + remove unused roundtrip axiom - Factor spec_ristretto_decode_inner into spec_ristretto_decode_v_u2_sqr and spec_ristretto_decode_xy, eliminating formula duplication - Remove spec_ristretto_decompress (choose-based, unused outside roundtrip) - Remove axiom_spec_ristretto_roundtrip (fully assume-based, no proof content) - Simplify spec_ristretto_decompress_coords (remove redundant let bindings) 1800 verified, 0 errors. Made-with: Cursor * Rename spec_ristretto_decompress_coords to spec_ristretto_decompress + update docs Now that the old choose-based spec_ristretto_decompress has been removed, reclaim the simpler name. Also updates proof documentation to reflect recent axiom simplifications. Co-Authored-By: Claude Opus 4.6 <noreply@anthropic.com> * Reorganize ristretto_specs.rs for logical grouping and readability Group all decompression specs together (decode helpers -> top-level decompress -> decode axioms) instead of scattering them across the file. Inline single-use helpers spec_ristretto_decode_v_u2_sqr and spec_ristretto_decode_xy into spec_ristretto_decode_inner. Move spec_sqrt_ad_minus_one next to the Elligator section that uses it. Extract math formulas into docstrings for Elligator and hash-to-group. Made-with: Cursor * Move decompress helper lemmas to sqrt_ratio_lemmas.rs, add math comments Move lemma_canonical_nat_lt_p, lemma_invsqrt_matches_spec, and lemma_decode_invsqrt_facts from ristretto.rs::decompress to sqrt_ratio_lemmas.rs where they belong alongside the invsqrt axioms. Add math-level comments to decompress branch conditions. Made-with: Cursor * Make nat_invsqrt constructive, remove axiom_invsqrt_exists Replace the choose-based nat_invsqrt spec with a constructive formula mirroring sqrt_ratio_i(1, a): computes a³·(a⁷)^((p-5)/8), checks against {-1, -i}, adjusts by sqrt(-1) if needed, then canonical sign. This eliminates axiom_invsqrt_exists (the choose satisfiability axiom). axiom_invsqrt_unique remains with a documented proof sketch. Made-with: Cursor * Improve step_2 documentation: clarify ORIGINAL CODE divergence and ensures Made-with: Cursor * Move axiom validation tests to ristretto_specs.rs, revert window.rs trigger changes - Move test_ristretto_decode_axioms and pow_field_element from ristretto.rs to specs/ristretto_specs.rs, co-locating tests with axiom definitions. - Revert unintentional #[trigger] -> #![auto] changes in window.rs introduced by verusfmt. Made-with: Cursor --------- Co-authored-by: Claude Opus 4.6 <noreply@anthropic.com> Co-authored-by: sbursuc <48085107+sbursuc@users.noreply.github.com>

* prove is_identity for all types, replacing assume with type-specific impls * add named identity spec predicates and fix coset4 rlimit * strengthen is_montgomery_projective_identity to full (1:0) repr * inline and remove is_* identity predicates * remove spec_ prefix from pure mathematical spec functions * Rename struct-to-nat extraction functions to use _as_nat suffix, dropping the spec_ prefix:

* verify ristretto::compress Prove that RistrettoPoint::compress matches spec_ristretto_compress, replacing the assume(false) bypass with a complete Verus proof. Spec changes: - Add `requires is_well_formed_edwards_point(self.0)` to compress Code changes (semantically equivalent, original preserved in comments): - Split compound expressions into named intermediates for proof tracking (e.g. `&(Z + &Y) * &(Z - &Y)` → z_plus_y, z_minus_y, u1) - Split `(&u1 * &u2.square()).invsqrt()` into u2_sq, u1_u2_sq, invsqrt - Split chained method calls for is_negative / conditional_negate Proof strategy: - Track each field operation via ghost variables tied to spec-level field_mul/field_add/field_sub/field_square - Link invsqrt to nat_invsqrt via lemma_invsqrt_matches_spec - Bridge conditional_assign/conditional_negate to spec-level if/else - Final assert-by blocks connect s_bytes to spec_ristretto_compress_extended New lemma: - lemma_invsqrt_a_minus_d_limbs_bounded (constants_lemmas.rs) Made-with: Cursor Co-Authored-By: Claude Opus 4.6 <noreply@anthropic.com> * Prove axiom_invsqrt_unique, rename to lemma_invsqrt_unique Eliminate both admit() calls in the mixed-case branches by reusing lemma_no_square_root_when_times_i as the contradiction witness, reducing the axiom chain to a single axiom (axiom_nat_invsqrt_satisfies_relation). Also fix spec_ristretto_compress_extended -> ristretto_compress_extended typo. Made-with: Cursor * Prove axiom_nat_invsqrt_satisfies_relation, rename to lemma Fully mechanize the proof that nat_invsqrt(a) satisfies is_sqrt_ratio or is_sqrt_ratio_times_i, eliminating the last admit() in sqrt_ratio_lemmas.rs. The proof reuses existing infrastructure: - lemma_sqrt_ratio_check_value to connect check to a fourth root - lemma_fourth_root_of_unity to show check ∈ {1, -1, i, -i} - lemma_multiply_by_i_flips_sign for the adjustment step - lemma_conditional_negate_makes_even for sign correction Made-with: Cursor * Remove redundant test_conditional_negate_field_element, clarify docs The test validated properties already guaranteed by our verified Neg::neg and conditional_assign impls. Updated the external_body comment to reflect that ensures clauses follow from composition of these two verified functions. Made-with: Cursor * Remove obsolete axiom_invsqrt_exists from docs, verusfmt axiom_invsqrt_exists is fully subsumed by lemma_nat_invsqrt_satisfies_relation, which constructively proves the existence property. Removed references from step_2.md, verus_proof_mapping.md, and axiom_references.md. Made-with: Cursor --------- Co-authored-by: Claude Opus 4.6 <noreply@anthropic.com> Co-authored-by: sbursuc <48085107+sbursuc@users.noreply.github.com>

Co-authored-by: Claude Opus 4.6 <noreply@anthropic.com>

) Co-authored-by: Claude Opus 4.6 <noreply@anthropic.com>

…_curve (dalek-cryptography#752) These are spec mirrors of exec functions and were incorrectly classified as pure math (Category 4) during the earlier spec_ prefix cleanup. Made-with: Cursor Co-authored-by: sbursuc <48085107+sbursuc@users.noreply.github.com> Co-authored-by: Lacramioara Astefanoaei <lacramioara.astefanoaei@gmail.com>

* verify elligator_ristretto_flavor Co-Authored-By: Claude Opus 4.6 <noreply@anthropic.com> * fmt Co-Authored-By: Claude Opus 4.6 <noreply@anthropic.com> * Address PR dalek-cryptography#753 review: rename nonneg_field to field_abs, merge elligator axioms, clean up proofs - Rename nonneg_field -> field_abs across specs, lemmas, and ristretto - Merge axiom_elligator_n_t_nonzero + axiom_elligator_t_completed_nonzero into single axiom_elligator_nonzero_intermediates - Simplify axiom_elligator_in_even_subgroup to r_0-only signature (forall in ensures); fix coset4 rlimit with explicit spec_eight_torsion bridges - Extract lemma_bridge_local_pow2 to deduplicate pow2 bridging code - Fix ONE_MINUS_EDWARDS_D_SQUARED doc comment - Remove duplicate code in commented-out ORIGINAL_CODE block - Add math-style algebraic comments to sqrt_ratio lemmas Co-Authored-By: Claude Opus 4.6 <noreply@anthropic.com> --------- Co-authored-by: Claude Opus 4.6 <noreply@anthropic.com>

) * verify ristretto double_and_compress_batch_verus Co-Authored-By: Claude Opus 4.6 <noreply@anthropic.com> * refactor: move ristretto proofs from specs to lemmas/ristretto_lemmas/ Separate proof functions and tests from pure spec definitions following the existing codebase pattern (field_specs + field_lemmas/). - axioms.rs: 8 axiom functions + axiom validation test suite - elligator_lemmas.rs: lemma_elligator_nonzero_denominators - batch_compress_lemmas.rs: 30 batch compression lemmas + test suite - ristretto_specs.rs: now contains only 19 pub open spec fn definitions Added scoped commutativity and bridging asserts to handle solver sensitivity from the module move (no rlimit bumps). Made-with: Cursor Co-Authored-By: Claude Opus 4.6 <noreply@anthropic.com> * refactor: address PR review — move field algebra lemmas, improve docstrings, remove redundant tests - Move 5 pure field algebra lemmas to field_algebra_lemmas.rs: lemma_field_square_nonzero, lemma_mul_one_identity, lemma_sum_sq_minus_diff_sq, lemma_field_abs_neg, lemma_field_abs_mul_sign - Move 3 sqrt(-1) lemmas to sqrt_m1_lemmas.rs: lemma_mul_i_squared_is_neg, lemma_one_minus_x_times_i, lemma_one_plus_x_times_i - Replace "Helper:" prefix with formal math notation in all docstrings - Rename neg_one_minus_d → c_coeff in lemma_z_inv_std_is_one for generality - Expand lemma_curve_eq_batch_identity docstring with full algebraic proof - Remove 5 tests for proven lemmas; keep only 3 axiom validation tests - Add math notation to batch_state_matches_point spec in ristretto.rs Made-with: Cursor Co-Authored-By: Claude Opus 4.6 <noreply@anthropic.com> * refactor: split fused states+invs loop into two separate loops Keep the loop structure faithful to the original two-map pattern (states from points, then invs from states) rather than fusing them into a single loop. Made-with: Cursor Co-Authored-By: Claude Opus 4.6 <noreply@anthropic.com> --------- Co-authored-by: Claude Opus 4.6 <noreply@anthropic.com>

…raphy#756) Remove all assumes from two Ristretto functions: - mul_base: Remove two assumes (is_well_formed_edwards_point and edwards_scalar_mul correctness). The Mul<&RistrettoBasepointTable> postconditions propagate directly — no proof assertions needed. - from_uniform_bytes: Replace three assumes with actual proofs: 1. is_in_even_subgroup: via new axiom_even_subgroup_closed_under_add 2. Functional correctness (== ristretto_from_uniform_bytes): via view equality bridging exec byte arrays to choose-based spec arrays 3. Uniformity implication: replace assume(antecedent) with idiomatic if-branch pattern matching codebase style (montgomery.rs, etc.) New axiom: axiom_even_subgroup_closed_under_add — the even subgroup 2E is closed under addition. The underlying algebra (2A + 2B = 2(A+B)) is fully proven by lemma_edwards_double_of_add; the admit() is only needed because lifting affine coords to EdwardsPoint is not yet formalized. Verification: 1910 verified, 0 errors. cargo test: 21 passed. Made-with: Cursor Co-authored-by: Claude Opus 4.6 <noreply@anthropic.com>

* prove axiom_gcd_symmetric as lemma_gcd_symmetric Replace admit() with a full proof via mutual divisibility: each gcd divides both inputs, hence divides the other gcd, and mutual divisibility of positive naturals implies equality. Also fix pre-existing broken reference to lemma_binomial_factorial_relation (should be axiom_binomial_factorial_relation). Made-with: Cursor Co-Authored-By: Claude Opus 4.6 <noreply@anthropic.com> * prove axiom_gcd_mod_noop as lemma_gcd_mod_noop One-liner proof: spec_gcd(a, m) unfolds to spec_gcd(m, a % m) by definition, then lemma_gcd_symmetric gives the result. Made-with: Cursor Co-Authored-By: Claude Opus 4.6 <noreply@anthropic.com> * prove axiom_neg_distributes_over_add as lemma_neg_distributes_over_add Algebraic proof: edwards_neg flips only the x-coordinate. neg(a)*neg(b)=a*b keeps denominators unchanged, while neg(a)*b=neg(a*b) flips the x-numerator, giving -(P+Q). Made-with: Cursor Co-Authored-By: Claude Opus 4.6 <noreply@anthropic.com> * prove axiom_edwards_to_montgomery_correspondence as lemma Factor out inv(Z) from affine numerator/denominator via distributivity, then cancel the common factor. Degenerate case (Z-Y = 0 in GF(p)) handled separately since both sides are 0. Made-with: Cursor Co-Authored-By: Claude Opus 4.6 <noreply@anthropic.com> * prove axiom_edwards_d2_is_2d as lemma_edwards_d2_is_2d Concrete computation via by(compute_only) with local helper specs, bridged to spec-level pow2/p(). Delete superseded runtime test test_edwards_d2_is_double_d. Made-with: Cursor Co-Authored-By: Claude Opus 4.6 <noreply@anthropic.com> * prove axiom_montgomery_a_neg_is_neg_a as lemma Concrete computation via by(compute_only) with local helper specs. Delete superseded runtime test test_montgomery_a_neg_value. Made-with: Cursor Co-Authored-By: Claude Opus 4.6 <noreply@anthropic.com> * prove axiom_scalar_mul_distributes_over_neg as lemma Structural induction on n mirroring edwards_scalar_mul's recursion. Each case applies lemma_neg_distributes_over_add to the recursive decomposition (double for even n, add for odd n). Made-with: Cursor Co-Authored-By: Claude Opus 4.6 <noreply@anthropic.com> * clean up axiom_references.md and refactor proofs to assert-by style Remove 7 proved axiom entries from docs/axiom_references.md (sections and summary table rows) since they are now lemmas. Refactor all proved lemma functions to wrap floating lemma calls inside assert(...) by { } blocks, aligning proof structure with mathematical reasoning where each lemma justifies a specific assertion. Made-with: Cursor Co-Authored-By: Claude Opus 4.6 <noreply@anthropic.com> * prove axioms as lemmas; refactor proofs to assert-by style Transform axioms to lemmas: gcd_symmetric, gcd_mod_noop, neg_distributes_over_add, edwards_d2_is_2d, montgomery_a_neg_is_neg_a, edwards_to_montgomery_correspondence, scalar_mul_distributes_over_neg. Refactor proofs so lemmas justify asserts (assert(goal) by { lemma; }). Update axiom_references.md to remove proved axioms. Made-with: Cursor Co-Authored-By: Claude Opus 4.6 <noreply@anthropic.com> * verusfmt Co-Authored-By: Claude Opus 4.6 <noreply@anthropic.com> * prove Montgomery identity and inverse axioms as lemmas Transform 3 Montgomery curve axioms into proved lemmas: - axiom_montgomery_add_identity_left -> lemma (trivial: Z3 unfolds open spec) - axiom_montgomery_add_identity -> lemma (trivial: Z3 unfolds open spec) - axiom_montgomery_add_inverse -> lemma (field_sub_self + field_sub_eq_add_neg) Made-with: Cursor Co-Authored-By: Claude Opus 4.6 <noreply@anthropic.com> * prove Edwards→Montgomery basepoint mapping axiom as lemma Transform axiom_edwards_basepoint_maps_to_montgomery_basepoint into lemma_edwards_basepoint_maps_to_montgomery_basepoint, eliminating admit(). Proof strategy: the Ed25519 basepoint y-coordinate satisfies y = 4/5 mod p (verified via compute_only: 5y = 4p + 4). From this, algebraic field identities show (1+y)·inv(1-y) = 9, matching spec_x25519_basepoint_u(). Supporting changes: - Add lemma_ed25519_basepoint_y in edwards_specs.rs to export the closed spec's y-coordinate for cross-module proofs - Add lemma_x25519_basepoint_u_is_9 in montgomery_specs.rs using lemma_u8_32_as_nat_first_byte_only to evaluate the byte-encoded constant - Delete test_edwards_basepoint_maps_to_montgomery_9 (now formally proved) Made-with: Cursor Co-Authored-By: Claude Opus 4.6 <noreply@anthropic.com> * add feasibility comparison docs for Lean, Rocq, and Isabelle Side-by-side comparison of each Verus axiom against existing Lean 4/Mathlib, Rocq/Fiat-Crypto/MathComp, and Isabelle/HOL/AFP theorems, plus a unified merged document with LaTeX formulae and a summary table. Made-with: Cursor Co-Authored-By: Claude Opus 4.6 <noreply@anthropic.com> Made-with: Cursor * address PR comments Co-Authored-By: Claude Opus 4.6 <noreply@anthropic.com> --------- Co-authored-by: Claude Opus 4.6 <noreply@anthropic.com>

…y#759) probe-verus 2.0 wraps specs-data output in an envelope with schema metadata, moving the payload under a .data field. Unwrap the envelope in specs.js so verified_functions and spec_functions are read correctly. Backward-compatible with the old bare format. Made-with: Cursor Co-authored-by: Claude Opus 4.6 <noreply@anthropic.com>

* lizard: specifications for Lizard encoding/decoding functions - Add Verus specs for all Lizard module functions (encode, decode, Elligator, Jacobi quartic, coset operations) - Add lizard_specs.rs with mathematical reference specs, pipeline docs, and collision-conditioned decode model - Add jacobi_to_edwards_affine spec fn and ristretto_coset_affine helper - Add correctness postcondition to elligator_inv (Elligator round-trip) - Prove encode_253_bits, lemma_lizard_decode_sound, lemma_lizard_roundtrip - Track refactorings with ORIGINAL CODE comments throughout - Add ensures comments (Well-formedness, Correctness, etc.) to all functions - Fix verusfmt formatting across all .rs files - Update verus-spec-helper skills with new patterns and proof techniques Made-with: Cursor * website: update specs browser for Lizard module - Add lizard functions to libsignal-used set (encode/decode_verus, from_uniform_bytes_single_elligator, decode_253_bits) - Merge lizard submodules and scalar_helpers into parent modules in charts - Add clickable pill-button jump links for Spec Functions / Axioms - Remove duplicate Elligator axioms from ristretto_specs.rs (now in lemmas/ristretto_lemmas/axioms.rs per main convention) - Add .gitattributes to collapse generated JSON files in PR diffs - Fix verusfmt and ruff formatting Generated files (specs_data.json, stats_history.jsonl) are omitted — CI regenerates them on merge to main. Made-with: Cursor * Address Copilot review - Fix duplicate event listeners on jump links (use onclick assignment instead of addEventListener to avoid accumulation on re-render) - Fix "MSB-first" comment in pow_field_element test (actually LSB-first) - Fix montgomery::hash rlimit by scoping assert-by blocks Made-with: Cursor * Clean up specs: simplify lizard docs, remove duplicate axiom tests - Simplify lizard_specs.rs doc comments (Signal example, decode failure modes) - Remove ~930 lines of duplicate axiom validation tests from ristretto_specs.rs (canonical copy lives in lemmas/ristretto_lemmas/axioms.rs) - Remove .gitattributes (generated files no longer in branch diff) Made-with: Cursor * Fix probe-verus detection for elligator_ristretto_flavor Remove ORIGINAL_CODE comment block that contained assume(false), which caused probe-verus to misdetect the function as unproved. Made-with: Cursor * lizard: fix specs and prove lizard_encode_verus correspondence - Fix write_bytes32_8_to_24 frame condition (bytes outside 8..24 now specified as preserved) - Replace unspecced negate_field with negate_field_element in to_jacobi_quartic_ristretto - Add recommends guards to jacobi_to_edwards_affine for division-by-zero - Prove lizard_encode_verus matches spec_lizard_encode (remove admit) - Prove lizard_decode_verus loop overflow via invariant (remove admit) - Fix elligator_inv postcondition (ret==false ==> out==ZERO seems to be wrong for S!=0, T==1 inputs) - Clean up redundant admits in elligator_ristretto_flavor_inverse Co-Authored-By: Claude Opus 4.6 <noreply@anthropic.com> * lizard_specs: align Ristretto-level doc comments with mathematical style Made-with: Cursor * website: fix specs browser filter interactions - Keep axioms visible when per-function "Focus referenced specs" is active - Clear per-function filter when clicking module/attribute pills Made-with: Cursor * website: add external functions to specs browser via probe-verus branch Made-with: Cursor * homepage: add external/axiom counts, rename to Specified Functions, simplify funnel Made-with: Cursor * homepage: load function browser from specs_data, add external/axiom filters Made-with: Cursor * charts: merge scalar_mul into backend, split u64 from backend in specs browser Made-with: Cursor * fix: ruff format plot_csv_preview.py Made-with: Cursor * specs browser: replace download bar with compact dropdown button Made-with: Cursor * skills: generalize verus-spec-helper for any Verus-verified crate Remove all curve25519-dalek-specific references (function names, file paths, domain concepts) and replace with generic patterns applicable to any Verus verification project. Made-with: Cursor * clean up: untrack specs_data.json, remove unused scripts - specs_data.json is generated by probe-verus in CI, no need to version - Remove 6 unused scripts superseded by probe-verus or never referenced: calculate_r_inverse, extract_specs, find_new_verus_functions, link_skills, update_website, verus_cleaner - Remove test artifacts: test_analysis.log, test_functions.txt Made-with: Cursor * specs browser: rename to Target Functions, add All/Proved/Unproved filter - Rename "Verified Functions" to "Target Functions" in hero and left panel - Add inline dropdown (All / Proved / Unproved) next to the title pill to filter target functions by proof status - Unproved badge now uses amber color (matching external/axiom style) - Page title simplified to "Function Specifications" - plot_csv_preview.py: add fallback when specs_data.json is missing Made-with: Cursor * ci: generate specs_data.json before charts so counts are accurate Move probe-verus specs-data step before plot_csv_preview.py so the chart can read external function and axiom counts from the JSON. Made-with: Cursor --------- Co-authored-by: sbursuc <48085107+sbursuc@users.noreply.github.com> Co-authored-by: astefano <lacramioara.astefanoaei@gmail.com> Co-authored-by: Claude Opus 4.6 <noreply@anthropic.com>

* Prove vartime double-base multiplication * Simplify vartime double-base loop proof * Fix verusfmt formatting * Document proof refactors with original code * Verify non-precomputed basepoint multiplication * Simplify vartime double-base cfg split * Document duplicated cfg control flow

…alek-cryptography#762)

* Revise README

* Add math-style inline comments to spec functions and exec specs Add line-above `// var = formula` comments to spec function bodies and exec function ensures/requires clauses, making it easier to verify correspondence between the Rust spec and the paper/RFC formulas. Changed files: - specs/ristretto_specs.rs: ristretto_compress_extended, ristretto_decode_inner, spec_elligator_ristretto_flavor, elligator_intermediates, batch_compress_body - specs/edwards_specs.rs: edwards_add, completed_to_projective, completed_to_extended, projective_to_extended - specs/montgomery_specs.rs: montgomery_add (doubling and addition branches) - ristretto.rs: from_uniform_bytes ensures - lizard/lizard_ristretto.rs: from_uniform_bytes_single_elligator, encode_253_bits, xcoset4, elligator_ristretto_flavor_inverse ensures - lizard/jacobi_quartic.rs: dual ensures Co-Authored-By: Claude Sonnet 4.6 <noreply@anthropic.com> * Normalize spec comments: remove parentheticals, move trailing comments above Co-Authored-By: Claude Opus 4.6 <noreply@anthropic.com> * Add math comments to ristretto_from_uniform_bytes and is_in_even_subgroup Co-Authored-By: Claude Opus 4.6 <noreply@anthropic.com> * Add inline math comment guidelines to spec and proof helper skills Update both Claude and Codex skill files with rules for spec function inline comments: line-above placement, operational-only style, standard math notation, and showing math meaning for helper function calls. Co-Authored-By: Claude Opus 4.6 <noreply@anthropic.com> --------- Co-authored-by: sbursuc <48085107+sbursuc@users.noreply.github.com> Co-authored-by: Claude Sonnet 4.6 <noreply@anthropic.com>

Co-authored-by: Claude Opus 4.6 <noreply@anthropic.com>

Add domain classification taxonomy for probe-verus extract --taxonomy-config. 17 rules classify functions into domains (field-arithmetic, group-law, curve-equation, scalar-multiplication, ristretto-protocol, etc.) with trust levels (highest/high/moderate/n/a). Validated against probe-verus 5.2.0 extract: 1528/1929 functions labeled, 93% of specified functions classified, all 48 axioms covered. Standardize the justification types in docs/axiom_references.md summary table to 6 canonical values: rfc, paper, tested, construction, crypto-assumption, algebraic-gap. Made-with: Cursor Co-Authored-By: Claude Opus 4.6 <noreply@anthropic.com>

sergiubur and others added 30 commits January 8, 2026 14:07

lemma_decompose proof + proof repair from z3 bump (dalek-cryptograp…

de27648

…hy#658) * lemma_decompose proof + proof repair from z3 bump * fmt

Proof repair after boundary tightening (dalek-cryptography#663)

fac5938

Verify edwards compress create (dalek-cryptography#661)

5c4190a

- Proofs for Edwards compress and create functions - Proofs and axioms for some algrebraic facts on Edwards curve additions and multiplication Co-Authored-By: Claude Opus 4.5 <noreply@anthropic.com>

Zeroize and Identity proofs (dalek-cryptography#666)

a918517

specialized postcondition (dalek-cryptography#667)

e083340

Verify 4 edwards functions (dalek-cryptography#674)

16580d4

Straightforward assert proofs for 4 edwards functions. Co-authored-by: Claude Opus 4.5 <noreply@anthropic.com>

Add Claude and Codex skills (dalek-cryptography#676)

325b844

sergiubur and others added 29 commits February 22, 2026 09:34

Prove EdwardsPoint ct_eq (dalek-cryptography#732)

c624c36

* Prove EdwardsPoint ct_eq * Refactor lemma_cross_mul_iff_div_eq to assert..by style, update skill guidance Co-authored-by: Cursor <cursoragent@cursor.com>

Added Verilib validations (dalek-cryptography#742)

ae4f094

pippenger: replace assume with unreachable-branch proof (dalek-crypto…

b1f18d0

…graphy#744) Remove remaining assume in pippenger scalar mul

verify BatchCompressState::from (dalek-cryptography#750)

9a8437b

Co-authored-by: Claude Opus 4.6 <noreply@anthropic.com>

verify ristretto identity, from_slice, eq, ct_eq (dalek-cryptography#751

9ebf74d

) Co-authored-by: Claude Opus 4.6 <noreply@anthropic.com>

ci: switch probe-verus back to main (include-external-body merged) (d…

b99d7ad

…alek-cryptography#762)

Revise README (dalek-cryptography#763)

8b182c5

* Revise README

verify lizard (dalek-cryptography#771)

d26bf6e

Co-authored-by: Claude Opus 4.6 <noreply@anthropic.com>

astefano closed this Mar 22, 2026

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

Add spec-taxonomy.toml and standardize axiom justification types#1

Add spec-taxonomy.toml and standardize axiom justification types#1
astefano wants to merge 93 commits intomainfrom
add-spec-taxonomy

astefano commented Mar 22, 2026

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

4 participants

Conversation

astefano commented Mar 22, 2026

Summary

Test plan

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

4 participants