feat(ConstraintSystem): universal CS abstraction with Hom and BehavioralContract - #465
Open
quangvdao wants to merge 3 commits into
Open
feat(ConstraintSystem): universal CS abstraction with Hom and BehavioralContract#465quangvdao wants to merge 3 commits into
quangvdao wants to merge 3 commits into
Conversation
…ralContract Introduces a small theory of constraint systems that unifies the indexed relations used across ArkLib (R1CS, Plonkish, lookups, memory checking, AIR, CCS, and DSL-level systems such as Clean's FormalCircuit). ArkLib/ProofSystem/ConstraintSystem/Basic.lean (new): - `ConstraintSystem` bundling Index, Stmt, OStmt, Wit, satisfies. - Smart constructors `ofRelation` (no oracle slot) and `ofWitnessFree`. - `ConstraintSystem.Hom` — completeness-preserving morphism with `index`, `stmt`, `oStmt`, `wit`, and `preserves`. Name follows Mathlib convention (RelHom, RingHom, LinearMap). - `Hom.id`, `Hom.comp`, and the category laws `id_comp`, `comp_id`, `comp_assoc` (all rfl). - `Hom.isSatisfiable_map` lifting satisfiability along a morphism. - `BehavioralContract` — per-index contract with `Assumptions`, `Spec`, soundness, and completeness, mirroring Clean's `FormalCircuit` pattern. ArkLib/ProofSystem/ConstraintSystem/Examples.lean (new): - `R1CS.toConstraintSystem` and `Plonk.toConstraintSystem` (+ `Plonk.Shape`) wiring the existing concrete relations into the universal abstraction, with `Iff.rfl` sanity lemmas. ArkLib/ProofSystem/ConstraintSystem/Plonk.lean: - `Plonk.ConstraintSystem` marked `protected` so bare `ConstraintSystem` inside namespace `Plonk` resolves to the universal one. Internal uses qualified to `Plonk.ConstraintSystem`. ArkLib.lean regenerated via scripts/update-lib.sh. Made-with: Cursor
Contributor
🤖 PR SummaryUniversal Constraint System Theory
Refactoring and Integration
Proof Status
Statistics
Lean Declarations ✏️ **Added:** 15 declaration(s)
✏️ **Affected:** 4 declaration(s) (line number changed)
✏️ **Affected:** 1 `sorry`(s) (line number changed)
🎨 **Style Guide Adherence**There are 35 style guide violations in the provided changes. They are grouped by rule below. Functions and Terms: lowerCamelCase
Functions: Prefer
|
Contributor
Build Timing Report
Incremental Rebuild Signal
This compares a clean project build against an incremental rebuild in the same CI job; it is a lightweight variability signal, not a full cross-run benchmark. Slowest Current Clean-Build FilesShowing 20 slowest current targets, with comparison against the selected baseline when available.
|
Contributor
🤖 AI ReviewOverall Summary: Errors during review:
🔍 **Mechanical Pre-Check Results**Escape hatches introduced in this PR (triggers hard verdict rule):
Pre-existing escape hatches in touched files (context only, does not affect verdict):
🔗 **Cross-File Analysis**Cross-file analysis failed: Error code: 400 - {'type': 'error', 'error': {'type': 'invalid_request_error', 'message': 'You have reached your specified workspace API usage limits. You will regain access on 2026-05-01 at 00:00 UTC.'}, 'request_id': 'req_011CaAUgu6rn97a6ozDFgBVb'} 📄 **Review for `ArkLib.lean`**An error occurred while analyzing 📄 **Review for `ArkLib/ProofSystem/ConstraintSystem/Basic.lean`**An error occurred while analyzing 📄 **Review for `ArkLib/ProofSystem/ConstraintSystem/Examples.lean`**An error occurred while analyzing 📄 **Review for `ArkLib/ProofSystem/ConstraintSystem/Plonk.lean`**An error occurred while analyzing |
Contributor
Collaborator
Author
|
@mitschabaude what do you think about this PR? Just a generic layer for embedding constraint systems into ArkLib protocols |
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
3 participants
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
Introduce a small theory of constraint systems that unifies the indexed relations used across ArkLib (R1CS, Plonkish, lookups, memory checking, AIR, CCS, and DSL-level systems such as Clean's
FormalCircuit), so protocols and compilers can target a single universal interface.Three goals:
(index, statement, oracle statement, witness, satisfies)so that one abstract CS value covers an entire family (e.g. R1CS of every size) rather than one value per parameter choice.ConstraintSystem.Homtransports satisfiability along index/statement/witness maps, modelling reductions between constraint systems (e.g. Clean gadget → R1CS row block, Plonkish → CCS, plain R1CS → padded R1CS). Name chosen per Mathlib convention (RelHom,RingHom,LinearMap).BehavioralContractpairs a CS with user-facingAssumptions+Specplus soundness and completeness proofs, mirroring theFormalCircuitpattern from Clean. This gives us a native ArkLib target for DSL-level systems without a language-specificReductionbridge.Files
New
ArkLib/ProofSystem/ConstraintSystem/Basic.leanstructure ConstraintSystembundlingIndex,Stmt,OStmt,Wit,satisfies.relation,IsSatisfiable.ofRelation(no oracle slot) andofWitnessFree.structure Homwithindex,stmt,oStmt,wit,preserves.Hom.id,Hom.comp,id_comp,comp_id,comp_assoc(all byrfl),Hom.isSatisfiable_map.structure BehavioralContractwithAssumptions,Spec,soundness,completeness, plusisSatisfiable_of_assumptions.ArkLib/ProofSystem/ConstraintSystem/Examples.leanR1CS.toConstraintSystem (R : Type*) [CommSemiring R] : ConstraintSystem.Plonk.Shape+Plonk.toConstraintSystem (𝓡 : Type) [CommRing 𝓡] : ConstraintSystem.Iff.rflsanity lemmas confirming agreement with the existing concrete relations.Modified
ArkLib/ProofSystem/ConstraintSystem/Plonk.lean—Plonk.ConstraintSystemmarkedprotectedso bareConstraintSysteminsidenamespace Plonkresolves to the universal one. Internal uses qualified toPlonk.ConstraintSystem(accepts,partition,perm,isPreparedFor,relation).ArkLib.lean— umbrella imports regenerated viascripts/update-lib.sh.Notes
OStmtis a singleType*; bundle multiple oracle slots via a dependent function type inside (e.g.MatrixIdx → Matrix _ _ Rfor R1CS).Reductionbridge in feat(Bridge): Clean to ArkLib bridge with completeness and structural soundness #451: a CleanFormalCircuitis naturally aBehavioralContractover an appropriate constraint system, without introducing a protocol-level wrapper.Test plan
./scripts/validate.shpasses (3630 jobs, no new warnings beyond pre-existing sorries).R1CS.toConstraintSystem_satisfiesandPlonk.toConstraintSystem_satisfiesconfirm definitional agreement with existing relations.Opened by Cursor assistant (model: Opus 4.7) on behalf of the user (Quang Dao) with approval.
Made with Cursor