feat: self-sign release binaries, Lean4 proofs, verification guide#72
Merged
feat: self-sign release binaries, Lean4 proofs, verification guide#72
Conversation
…ion guide Self-signing (dogfooding): - Release workflow uses freshly-built wsc binary to sign its own ELF binaries with --format elf --keyless - Detached .sig files uploaded as release assets Lean4 proofs: - Added scalarMul_zero_point axiom - Completed scalarMul_mul_order proof (no sorry) - 3 sorry stubs remain with detailed Mathlib strategies Verification guide: - Added PulseEngine Verification Guide link to AGENTS.md and CLAUDE.md - Key rules: spec first, simple first, multi-candidate, all-track compat Co-Authored-By: Claude Opus 4.6 (1M context) <noreply@anthropic.com>
Down from 4 sorry to 2: - scalarMul_mul_order: proven (scalarMul_zero_point axiom) - verification_equation_sound: FULLY PROVEN (Int.modEq witness extraction → scalarMul_add distribution → scalarMul_mul_order elimination → hypothesis substitution) - verification_equation_complete: sorry (needs basepoint_prime_order) - basepoint_prime_order: sorry (needs Mathlib addOrderOf) Co-Authored-By: Claude Opus 4.6 (1M context) <noreply@anthropic.com>
Codecov Report✅ All modified and coverable lines are covered by tests. 📢 Thoughts on this report? Let us know! |
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
1 participant
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
Summary
Self-signing (dogfooding)
Release workflow uses the freshly-built
wscbinary to sign its own ELF release binaries withsigil sign --format elf --keyless. Detached.sigfiles uploaded as release assets.Lean4 proofs
scalarMul_zero_pointaxiomscalarMul_mul_orderproof (nosorry)sorrystubs remain with detailed Mathlib proof strategiesVerification guide
Added PulseEngine Verification Guide link to AGENTS.md and CLAUDE.md for all proof work.
🤖 Generated with Claude Code