Improve formalization UX on the lean side - #9

Draft

mitschabaude wants to merge 230 commits into

zksec/clean-integrationfrom

Commits on Mar 19, 2026

fv: setup documentation mdbook
gio54321
committed
8beb29f
fv: add documentation about the clean framework
gio54321
committed
bfd7190

Commits on Mar 21, 2026

fv: add docs about clean/ragu integration
gio54321
committed
5904057
fv: address docs comments
gio54321
committed
cea49ca

Commits on Mar 23, 2026

fv: add assumption points
gio54321
committed
7546ec4

Commits on Mar 30, 2026

chore: remove consequence language from API contract doc
LucidSamuel
committed
ccb9923

Commits on Apr 12, 2026

chore: feedback update
LucidSamuel
committed
002b10d

Commits on Apr 13, 2026

doc: improve wording for promote() contract
LucidSamuel
committed
db5a5cf

Commits on Apr 17, 2026

Apply suggestion from @pirapira
pirapira
authored
3366e93
Update fv/docs/src/clean/core/provable.md
pirapira
authored
d0c7a2d
Update fv/docs/src/ragu/assumptions.md
pirapira
authored
e5cd6f9
doc: add allocation page to book
LucidSamuel
committed
485a8aa
address feedback and restructure primitives section
LucidSamuel
committed
52dc9e9
re: address feedback
LucidSamuel
committed
d76ecea
fv: add a sentence about elaborater of Lean
pirapira
committed
3f35b9c
fv: Update soundness proof explanation
pirapira
committed
8b94e8b
fv: update doc after GeneralFormalCircuit
pirapira
committed
74fe964
fv: reflect weaker assumption
pirapira
committed
eac17c1
fv: remove an almost empty file
pirapira
committed
9bf82e1
fv: update doc for weaker assumption
pirapira
committed
63970c8
fv: fix remaining inconsistencies in example.md for weaker assumption

pirapira
and
claude
committed
f1aaa73
Merge branch 'zksec/clean-integration' into fv-docs
pirapira
committed
7cb84b7
fv: explain GeneralFormalCircuit too
pirapira
committed
d104aaf
fv: more about ProverData
pirapira
committed
731f021
fv: remove 'only' that might not be true
pirapira
committed
736e333
fv: clarify Assumptions is shared for soundness and completeness
pirapira
committed
3eae970

Commits on Apr 18, 2026

circuits: txz prediction computed using geosum
ebfull
committed
d842f01
fv: clarify ProverData usage for witness generation is hacky
pirapira
committed
4917763
book: expand local protocol overview with footnotes and combined-check derivation
ebfull
committed
eccba76
book: more changes
ebfull
committed
c888548
Merge pull request #664 from ebfull/misc
ebfull
authored
b32cd84
Apply suggestions from code review
ebfull
authored
c6c9d66
Apply suggestions from code review
ebfull
authored
2147153
Merge pull request #652 from LucidSamuel/docs/allocation-page
ebfull
authored
4a96149

Commits on Apr 20, 2026

automatically infer Input, Output, inputLen, outputLen
mitschabaude
committed
cd60ca2
use reimpliementation spec by default
mitschabaude
committed
1a77883
Merge branch 'zksec/clean-integration' into fv-clean-ux
mitschabaude
committed
f8b9e1c
fv: refresh docs for Environment / VerifierEnvironment split

pirapira
and
claude
committed
2c26899
fv: document the axiom footprint in assumptions.md

pirapira
and
claude
committed
2fec3a8
fv: merge axiom note into the "axioms we use" bullet

pirapira
and
claude
committed
25ff48f
fv: note that falsehood provability of propext/choice/Quot.sound is open

pirapira
and
claude
committed
7d15bf6
Apply suggestion from @pirapira
pirapira
authored
4ae16ec
fv: a sentence about Expression
pirapira
committed
e76ff94
Merge remote-tracking branch 'origin/fv-docs' into fv-docs
pirapira
committed
4ae02be
fv: clarify what Circuit does
pirapira
committed
da03bab
fv: clarify what `Var` is.
pirapira
committed
73bbd27
fv: mention possible nondeterminism
pirapira
committed
e59f645
fv: elaborate on Prop corresponding to the reality
pirapira
committed
1c462aa

Commits on Apr 21, 2026

fv: add deterministic assumption
pirapira
committed
f1bfa56
fv: unsure about contradiction
pirapira
committed
94c6326
fv: mention triviality explosion
pirapira
committed
6590221
fv: mention approximation does not work
pirapira
committed
49630c5
fv: rename Environment -> ProverEnvironment, VerifierEnvironment -> Environment

pirapira
and
claude
committed
87fac8a
fv: mention serialization order of elements
pirapira
committed
5c74fe5
fv: clarify Lean-impl correspondence of field elements
pirapira
committed
369fb0f
fv: clarify a bit about requirements
pirapira
committed
7f9760e
fv: clarify out of scope of formal verification
pirapira
committed
4540136
fv: split backend reliance to soundness and completeness
pirapira
committed
5111dca
fv: typo Fromal
pirapira
committed
0f5fb3a
fv: compress
pirapira
committed
31fd4d5
fv: elaborate on completeness status
pirapira
committed
b65e93e
fv: clarify the situation about copied values
pirapira
committed
8598fc0
fv: drop examples of theory and implementation
pirapira
committed
5084d36
fv: clarify
pirapira
committed
709028b
pcd: make Side public

ebfull
and
claude
committed
b1b5930
pcd: add stashed_preamble to s_prime bridge stage

ebfull
and
claude
committed
4072115
pcd: make preamble::Stage parent PointsStage

ebfull
and
claude
committed
948e5a4
pcd: expand preamble ChildWitness with 9 stashed fields

ebfull
and
claude
committed
2e28bed
pcd: plumb ChildStageRx through Proof for future copying claims

ebfull
and
claude
committed
03f287d
pcd: introduce empty Loading circuit

ebfull
and
claude
committed
062ad79
pcd: loading enforces points.initial = BridgeF.native_f

ebfull
and
claude
committed
f1d550c
pcd: loading enforces s_prime.stashed_preamble relay

ebfull
and
claude
committed
23c6096
pcd: loading walks 30 per-child PointsStage inputs

ebfull
and
claude
committed
87fd05c
pcd: loading walks current-step stages and asserts exhaustion

ebfull
and
claude
committed
900e423
pcd: introduce empty Copying(Side) circuits

ebfull
and
claude
committed
da1cffb
pcd: copying enforces stashed_preamble via s_prime relay

ebfull
and
claude
committed
c4d46e9
pcd: copying enforces stashed inner_error/outer_error/ab/query/eval

ebfull
and
claude
committed
2f9e109
pcd: copying enforces stashed_p against PointsStage last interstitial

ebfull
and
claude
committed
7a926fd
pcd: adopt final-form doc comments from origin/loading-and-copying

ebfull
and
claude
committed
f2de234
Merge branch 'zksec/clean-integration' into fv-clean-ux
mitschabaude
committed
b4886cf

Commits on Apr 22, 2026

Merge pull request #642 from zksecurity/zksec/clean-integration
TalDerei
authored
672917f
fv: add element mul extraction instance and FormalInstance
TalDerei
committed
bb85b31
fv: add Element.Square extraction instance and FormalInstance
TalDerei
committed
e7306e7
fv: add Element.AllocSquare extraction instance and FormalInstance
TalDerei
committed
4c06961
fv: add Element.DivNonzero extraction instance and FormalInstance
TalDerei
committed
0c55be4
fv: add Core.AllocMul extraction instance and FormalInstance
TalDerei
committed
b009aa1
fv: add Point.Endo extraction instance and FormalInstance
TalDerei
committed
7713d50
fv: fix lake build failures
TalDerei
committed
932492c
fv: fmt imports
TalDerei
committed
5b07b72
fv: clarify spec notation while auditing spec correctness
TalDerei
committed
b2510eb

Commits on Apr 24, 2026

pcd: extract child p-accumulation order into helpers
TalDerei
committed
2a241b6
pcd: Arc-cloning todo to avoid cloning
TalDerei
committed
db61501
pcd: extract endoscaling logic into shared helper
TalDerei
committed
578a35f
pcd: ChildBridgeKind enum for child bridge rxs
TalDerei
committed
0fac749
pcd: rust fmt and docs
TalDerei
committed
85bd374
pcd: fix doc link
TalDerei
committed
1e1be0a
pcd: address feedback; revert p-accumulation helpers
TalDerei
committed
80bdd24
Merge pull request #656 from ebfull/loading-and-copying
ebfull
authored
f93e2f1
staging: route rx_configured through the Allocator

ebfull
and
claude
committed
13e6555
allocator: place values on A-wire instead of B-wire

ebfull
and
claude
committed
b33601b
wiring: move ONE wire from b[0] to d[0]

ebfull
and
claude
committed
2d046b1
wiring: swap a and b monomial positions

ebfull
and
claude
committed
12b9fc3
wiring: drop WireEval sentinel, use F/DirectSum

ebfull
and
claude
committed
3280ddc
book: rename local/overview to local/arithmetization
ebfull
committed
9bc87cc
book: rewritten local/arithmetization
ebfull
committed
9223674
book: rewritten local/wiring
ebfull
committed
fd27d8c
book: fix nits
ebfull
committed
2c80d06

Commits on Apr 25, 2026

fv: "requirements"->"expectations"
pirapira
committed
ad06af6
fv: re-add examples
pirapira
committed
8babf08
fv: add assumption law of physics
pirapira
committed
d83086e
fv: clarify warning
pirapira
committed
d8a94f1
fv: opsec is assumed too
pirapira
committed
0a9f785
fv: formatting
pirapira
committed
64a718f
trace: place SYSTEM-gate alpha at a[0] to match book

ebfull
and
claude
committed
d02c0cc
raw: drop GateWires from RawCircuit::witness

ebfull
and
claude
committed
b8802a0
circuits: address swap-ab review nits

ebfull
and
claude
committed
d4bef72
fv: simplify whoever's expectations matter
pirapira
committed
b1cbd0e
fv: remove redundancy
pirapira
committed
95e1164
fv: grammar
pirapira
committed
c40db08
Merge pull request #683 from ebfull/swap-ab
ebfull
authored
80d6ef8
Merge pull request #670 from TalDerei/fv-more-gadgets
TalDerei
authored
e7602ee
fv: add Element.Negate extraction instance and FormalInstance
TalDerei
committed
11b0993
fv: add Element.Add extraction instance and FormalInstance
TalDerei
committed
2690f36
fv: add Element.Sub extraction instance and FormalInstance
TalDerei
committed
41b718f
fv: add Element.Double extraction instance and FormalInstance
TalDerei
committed
cb74d0e
fv: add Element.Scale extraction instance and FormalInstance
TalDerei
committed
83fe81d
fv: add Element.AddCoeff extraction instance and FormalInstance
TalDerei
committed
04d4a8e
fv: add Element.EnforceZero extraction instance and FormalInstance
TalDerei
committed
0275bfd
fv: add Element.InvertWith extraction instance and FormalInstance
TalDerei
committed
95629e7
fv: add Element.Invert extraction instance and FormalInstance
TalDerei
committed
7f76ab8
fv: add Element.Alloc extraction instance and FormalInstance
TalDerei
committed
419f67e
fv: add Element.Sum extraction instance and FormalInstance
TalDerei
committed
7d70c6a
fv: add Element.Multiadd extraction instance and FormalInstance
TalDerei
committed
f56fa81
fv: add Element.Fold extraction instance and FormalInstance
TalDerei
committed
1f1438f
fv: add Element.EnforceRootOfUnity extraction instance and FormalInstance
TalDerei
committed
c7d76df
fv: add Point.Constant extraction instance and FormalInstance
TalDerei
committed
9c3daaf
fv: register EnforceRootOfUnity + Point.Constant in extractor; clippy
TalDerei
committed
08bd892
fv: post-rebase fixes to pass lake build
TalDerei
committed
b491345
fv: drop zero-operation gadgets from FV surface
TalDerei
committed
efb3431
fv: remove Rust extractor instances for dropped zero-op gadgets
TalDerei
committed
06988fd
fv: drop unused hintReader
TalDerei
committed
84d2a67
fv: drop general prefix from GeneralFormalCircuit definitions
TalDerei
committed
a3dd83e
fv: refactor clean reimpl to FormalAssertion (from the general case)
TalDerei
committed
e76202f
fv: drop redundant subcircuit keyword in reimpls
TalDerei
committed
14c515a
fv: delegate Element.Invert reimpl to Element.InvertWith
TalDerei
committed
caf48b7

Commits on Apr 26, 2026

fv: todo comment for polymorphic work
TalDerei
committed
8b858e4
Merge pull request #672 from TalDerei/fv-more-gadgets-supplemental
TalDerei
authored
492eff5
fv: add Boolean.Alloc extraction instance and FormalInstance
TalDerei
committed
6d468f1
primitives: primitives: add Boolean::promote unchecked constructor
TalDerei
committed
4bea341
fv: type-annotate Coeff::One and Coeff::Two in autogen
TalDerei
committed
e576ba4
fv: regenerate autogen after regenerating codegen
TalDerei
committed
956438a
fv: add Boolean.Not extraction instance and FormalInstance
TalDerei
committed
cba81c7
fv: add Boolean.And extraction instance and FormalInstance
TalDerei
committed
0948013
fv: add Boolean.ConditionalSelect extraction instance and FormalInstance
TalDerei
committed
6719180
fv: add Boolean.ConditionalEnforceEqual extraction instance and FormalInstance
TalDerei
committed
9a74cb3
fv: add Boolean.IsZero extraction instance and FormalInstance
TalDerei
committed
118af78
fv: add Element.IsEqual extraction instance and FormalInstance
TalDerei
committed
e6343a7
fv: rename Boolean:IsZero to Element::IsZero
TalDerei
committed
46e5b6c
fv: add Point.ConditionalEndo extraction instance and FormalInstance
TalDerei
committed
7711988
fv: add Point.ConditionalNegate extraction instance and FormalInstance
TalDerei
committed
b99691b
fv: add Boolean.Multipack extraction instance and FormalInstance
TalDerei
committed
be6c58e
fv: tighten Boolean spec statements
TalDerei
committed
5b5b831
fv: scaffold Point.DoubleAndAddIncomplete (soundness/completeness deferred)
TalDerei
committed
7c7980c
fv: soundness proof for Point.DoubleAndAddIncomplete
TalDerei
committed
a13fb9c
fv: drop general prefix from GeneralFormalCircuit definitions
TalDerei
committed
f7c9746
fv: apply review feedback from #672
TalDerei
committed
098ac12
fv: delegate Boolean.Alloc gate to Core.AllocMul subcircuit
TalDerei
committed
031bde7
fv: switch Boolean.Alloc hint to Bool, delegate gate to AllocMul
TalDerei
committed
a7ce8b5
fv: lift Boolean.And spec to high-level boolean form
TalDerei
committed
6b62ff4
fv: lift Boolean gadget specs to high-level operations
TalDerei
committed
2dedcab
v: lift Point.Conditional{Endo,Negate} specs to high-level form
TalDerei
committed
a1691a1
fv: delegate Boolean.And gate to Element.Mul subcircuit
TalDerei
committed
aa3b028
fv: delegate Element.AllocSquare gate to Core.AllocMul subcircuit
TalDerei
committed
091b622
fv: drop Boolean::promote, inline gadget bodies in extraction
TalDerei
committed
db3eb0f
fv: nigthly fmt
TalDerei
committed
80c3bdb
fv: minor nits
TalDerei
committed
ba45d19
fv: add advances in cryptoanalysis
pirapira
committed
81bf4d2
fv: mention quantum computers
pirapira
committed
6ce9a84
Merge pull request #674 from TalDerei/fv-boolean-gadget
ebfull
authored
9762bf2
bump pasta_curves to add deferred reduction support
ebfull
committed
17c7473
Merge pull request #687 from ebfull/bump-pasta
ebfull
authored
d37fb99
fv: mention bugs in operating system
pirapira
committed
39da98f
fv: mention semantics by real world
pirapira
committed
1b8b7f6
fv: moving the semantics to the beginning
pirapira
committed
1f8065b
fv: clarification
pirapira
committed
293f358
perf: lazy Montgomery reduction in revdot via DeferredField

alxiong
and
claude
committed
325ff87
Merge pull request #580 from alxiong/lazy-mont-reduction
ebfull
authored
d5b58d3
Merge pull request #626 from LucidSamuel/chore/api-contract-docs
TalDerei
authored
b17f21f

Commits on Apr 27, 2026

fv: edits
pirapira
committed
98d6d73

Commits on Apr 28, 2026

minor
mitschabaude
committed
d3e015a
Merge remote-tracking branch 'upstream/main' into fv-clean-ux
mitschabaude
committed
fa81f95
Bump clean dependency
mitschabaude
committed
04b5782
Port circuits to GFC prover specs
mitschabaude
committed
3326f33
Update formal instances for latest Clean
mitschabaude
committed
90d43b6
Merge pull request #689 from zksecurity/fv-docs
TalDerei
authored
ac389b5
fv: migrate docs under qa/lean subdirectory
TalDerei
committed
02bd0d4
fv: dedicated formal verification skills
TalDerei
committed
fb77d70
start porting to new hints
mitschabaude
committed
9ce1a57
Merge pull request #691 from TalDerei/fv-organization
ebfull
authored
9b7128e

Commits on Apr 29, 2026

Use verifier value size for hinted instances
mitschabaude
committed
9f43a5d
Port allocator and invert circuits to prover hints
mitschabaude
committed
647aa04
Infer instance input and output types
mitschabaude
committed
b493986
adapt div non zero
mitschabaude
committed
d86c679
Refactor div nonzero to derive hints internally
mitschabaude
committed
8b42582
Refactor point allocation to use prover point hints
mitschabaude
committed
3f0aca4
Use clean prover proof expansion
mitschabaude
committed
31c70dc
Refactor element prover hint circuits
mitschabaude
committed
3053c08
Clean up point circuit assumptions
mitschabaude
committed
b04b6f0
Simplify point circuit specs
mitschabaude
committed
fd3dd43
Correct double-and-add spec cleanup
mitschabaude
committed
6e29e46
Drop redundant formal instance specs
mitschabaude
committed
7eeb73e
Align element alloc hint interface
mitschabaude
committed
3491a13
minor simpliciation
mitschabaude
committed
d3d012d
clear up misunderstanding of FormalAssertion
mitschabaude
committed
2565e83
Use shared mul gate circuits internally
mitschabaude
committed
77db92a
Make conditional enforce equal an assertion
mitschabaude
committed
feda309
Rename core alloc mul to core mul
mitschabaude
committed
b1b1dcc
Merge remote-tracking branch 'upstream/main' into fv-clean-ux
mitschabaude
committed
e87d5da
Refresh Lean FV docs after upstream merge
mitschabaude
committed
886cb22
Collapse formal instance definitions
mitschabaude
committed
0db8012
Rename formal instance wrapper
mitschabaude
committed
0ef1f63
Update Clean dependency to main
mitschabaude
committed
bb41827
fv: update skills for Clean prover/verifier precondition split
TalDerei
committed
70dac4c
fv-review: preconditions go in Assumptions, not Spec
TalDerei
committed
6a97728
fv: more skill nits
TalDerei
committed
6ea5ad3
fv: even more skill nits
TalDerei
committed
782f381

Commits on Apr 30, 2026