feat(ConstraintSystem): universal CS abstraction with Hom and BehavioralContract

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

Author: quangvdao

ArkLib.lean

@@ -145,6 +145,8 @@ import ArkLib.ProofSystem.Component.RandomQuery
 import ArkLib.ProofSystem.Component.ReduceClaim
 import ArkLib.ProofSystem.Component.SendClaim
 import ArkLib.ProofSystem.Component.SendWitness
+import ArkLib.ProofSystem.ConstraintSystem.Basic
+import ArkLib.ProofSystem.ConstraintSystem.Examples
 import ArkLib.ProofSystem.ConstraintSystem.Lookup
 import ArkLib.ProofSystem.ConstraintSystem.MemoryChecking
 import ArkLib.ProofSystem.ConstraintSystem.Plonk

ArkLib/ProofSystem/ConstraintSystem/Basic.lean

@@ -0,0 +1,222 @@
+/-
+Copyright (c) 2025 ArkLib Contributors. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Quang Dao
+-/
+
+import Mathlib.Data.Set.Defs
+
+/-!
+# Universal constraint system abstraction
+
+This file introduces a small theory of constraint systems that provides a uniform interface
+for the various concrete systems used across ArkLib (R1CS, Plonkish, lookups, memory
+checking, AIR, CCS, and DSL-level systems such as Clean's `FormalCircuit`).
+
+The goals are:
+
+1. **Unify**: capture the common shape `(index, statement, oracle statement, witness,
+   satisfies)` so that protocols and compilers can be written once and instantiated for any
+   concrete CS.
+2. **Compose**: introduce morphisms `ConstraintSystem.Hom` that transport satisfiability
+   along index/statement/witness maps, modelling reductions between constraint systems
+   (e.g. Clean gadget → R1CS row block, Plonkish → CCS, Plain R1CS → padded R1CS).
+3. **Extend with behaviour**: add a `BehavioralContract` layer that pairs a CS with
+   user-facing I/O contracts (assumptions + spec), in the style of Clean's `FormalCircuit`.
+
+## Design notes
+
+- The structure is **indexed**: a single `ConstraintSystem` value packages an entire family
+  of concrete relations (one per `Index`), so that, e.g., R1CS of every size is a single
+  constraint system rather than one per `(m, n, n_w)`.
+- The statement is split into an **in-the-clear** part (`Stmt`) and a **committed/oracle**
+  part (`OStmt`). Use `fun _ => PUnit` for `OStmt` if the system is purely non-oracle. If
+  multiple oracle slots are needed (as in R1CS with three matrices), bundle them via a
+  dependent function type inside `OStmt`.
+- `satisfies` is a `Prop`, not a `Set`, for ergonomic use inside proofs and reductions.
+- Morphisms are one-way (completeness-preserving). Soundness-reflecting variants
+  (extractors, embeddings, isos) are future work.
+-/
+
+universe u v w
+
+/-- A **constraint system** packages a family of indexed relations into a single bundle.
+
+For each `i : Index` there is a `Stmt i` (the in-the-clear statement), an `OStmt i` (the
+committed/oracle-accessible statement data; use `PUnit` if absent), and a `Wit i` (the
+private witness). The predicate `satisfies i s o w` asserts that the triple `(s, o, w)` is
+a valid instance at index `i`. -/
+structure ConstraintSystem : Type (max (u + 1) (v + 1) (w + 1)) where
+  /-- Index type parametrising the family of relations (sizes, shape parameters, etc.). -/
+  Index : Type u
+  /-- In-the-clear part of the statement at each index. -/
+  Stmt : Index → Type v
+  /-- Committed/oracle-accessible part of the statement. Use `fun _ => PUnit` for a
+    purely non-oracle constraint system. Multiple oracle slots can be bundled via a
+    dependent function type (e.g. `MatrixIdx → Matrix _ _ R` for R1CS). -/
+  OStmt : Index → Type v
+  /-- Private witness. -/
+  Wit : Index → Type w
+  /-- The satisfiability predicate at each index. -/
+  satisfies : (i : Index) → Stmt i → OStmt i → Wit i → Prop
+
+namespace ConstraintSystem
+
+variable (C : ConstraintSystem.{u, v, w})
+
+/-- The underlying set-theoretic relation at a given index. -/
+def relation (i : C.Index) : Set (C.Stmt i × C.OStmt i × C.Wit i) :=
+  { t | C.satisfies i t.1 t.2.1 t.2.2 }
+
+/-- Existence of valid oracle data and witness for a given in-the-clear statement. -/
+def IsSatisfiable (i : C.Index) (s : C.Stmt i) : Prop :=
+  ∃ o w, C.satisfies i s o w
+
+/-- Build a constraint system from a plain indexed relation (no oracle statement slot). -/
+def ofRelation
+    {Idx : Type u} {S : Idx → Type v} {W : Idx → Type w}
+    (rel : (i : Idx) → S i → W i → Prop) : ConstraintSystem.{u, v, w} where
+  Index := Idx
+  Stmt := S
+  OStmt := fun _ => PUnit
+  Wit := W
+  satisfies := fun i s _ w => rel i s w
+
+/-- Build a witness-free constraint system (assertions purely over the public and oracle
+parts of the statement). -/
+def ofWitnessFree
+    {Idx : Type u} {S O : Idx → Type v}
+    (rel : (i : Idx) → S i → O i → Prop) : ConstraintSystem.{u, v, 0} where
+  Index := Idx
+  Stmt := S
+  OStmt := O
+  Wit := fun _ => PUnit
+  satisfies := fun i s o _ => rel i s o
+
+end ConstraintSystem
+
+/-!
+## Morphisms between constraint systems
+
+A `ConstraintSystem.Hom` transports valid instances of one constraint system to valid
+instances of another. It consists of:
+
+- `index` — a map of shape indices (e.g. scale the size of an R1CS instance);
+- `stmt`, `oStmt`, `wit` — compatible maps of statement, oracle-statement, and witness
+  data that in general may depend on the input in-the-clear statement;
+- `preserves` — the core axiom that maps satisfying triples to satisfying triples.
+
+Intuitively, `Hom C D` is a *completeness-preserving* reduction from `C` to `D`: if you can
+satisfy `C` at some index, you can satisfy `D` at the image index, with an explicit
+construction of the needed data. Soundness-reflecting morphisms (with extractors) are a
+strict strengthening and are future work.
+
+The name `Hom` follows Mathlib convention (`RelHom`, `RingHom`, `LinearMap`). A future
+extension can add `ConstraintSystem.Hom.Embedding` or `ConstraintSystem.Iso` without
+renaming anything.
+-/
+
+namespace ConstraintSystem
+
+/-- A completeness-preserving morphism between constraint systems. -/
+@[ext]
+structure Hom (C D : ConstraintSystem.{u, v, w}) where
+  /-- Map on index types. -/
+  index : C.Index → D.Index
+  /-- Map on in-the-clear statements. -/
+  stmt : (i : C.Index) → C.Stmt i → D.Stmt (index i)
+  /-- Map on oracle/committed statement data. It may depend on the in-the-clear statement
+    as well, which is needed e.g. when the index encodes a global shape and the statement
+    fixes public inputs before committed data is computed. -/
+  oStmt : (i : C.Index) → (s : C.Stmt i) → C.OStmt i → D.OStmt (index i)
+  /-- Map on witnesses, likewise allowed to depend on the input statement. -/
+  wit : (i : C.Index) → (s : C.Stmt i) → C.Wit i → D.Wit (index i)
+  /-- Preservation property: valid instances map to valid instances. -/
+  preserves : ∀ i s o w,
+    C.satisfies i s o w → D.satisfies (index i) (stmt i s) (oStmt i s o) (wit i s w)
+
+namespace Hom
+
+/-- The identity morphism on a constraint system. -/
+def id (C : ConstraintSystem.{u, v, w}) : Hom C C where
+  index := _root_.id
+  stmt := fun _ => _root_.id
+  oStmt := fun _ _ => _root_.id
+  wit := fun _ _ => _root_.id
+  preserves := fun _ _ _ _ h => h
+
+/-- Composition of two morphisms. Reads right-to-left as usual. -/
+def comp {C D E : ConstraintSystem.{u, v, w}} (g : Hom D E) (f : Hom C D) : Hom C E where
+  index := g.index ∘ f.index
+  stmt := fun i s => g.stmt (f.index i) (f.stmt i s)
+  oStmt := fun i s o => g.oStmt (f.index i) (f.stmt i s) (f.oStmt i s o)
+  wit := fun i s w => g.wit (f.index i) (f.stmt i s) (f.wit i s w)
+  preserves := fun i s o w h =>
+    g.preserves (f.index i) (f.stmt i s) (f.oStmt i s o) (f.wit i s w) (f.preserves i s o w h)
+
+variable {C D E F : ConstraintSystem.{u, v, w}}
+
+@[simp] theorem id_comp (f : Hom C D) : (id D).comp f = f := rfl
+
+@[simp] theorem comp_id (f : Hom C D) : f.comp (id C) = f := rfl
+
+theorem comp_assoc (h : Hom E F) (g : Hom D E) (f : Hom C D) :
+    (h.comp g).comp f = h.comp (g.comp f) := rfl
+
+end Hom
+
+/-- Morphisms preserve satisfiability. -/
+theorem Hom.isSatisfiable_map {C D : ConstraintSystem.{u, v, w}} (f : Hom C D)
+    {i : C.Index} {s : C.Stmt i} (hs : C.IsSatisfiable i s) :
+    D.IsSatisfiable (f.index i) (f.stmt i s) := by
+  obtain ⟨o, w, h⟩ := hs
+  exact ⟨f.oStmt i s o, f.wit i s w, f.preserves i s o w h⟩
+
+end ConstraintSystem
+
+/-!
+## Behavioural contracts
+
+In DSL-level systems like Clean, a circuit is bundled with a user-facing contract:
+preconditions (`Assumptions`) on the statement and a high-level specification (`Spec`)
+relating statement and witness. A `BehavioralContract` lifts this pattern onto an
+arbitrary constraint system: at a fixed index, one provides such a contract together with
+proofs that the underlying constraints *imply* the spec under the assumptions (soundness
+of the gadget) and that a satisfying witness *exists* under the assumptions (completeness).
+
+This gives us a clean target for migrating Clean's `FormalCircuit` into ArkLib without a
+Clean-specific protocol bridge.
+-/
+
+namespace ConstraintSystem
+
+/-- A behavioural contract for a constraint system at a fixed index, consisting of an
+`Assumptions` precondition on the in-the-clear statement and a `Spec` postcondition
+relating statement and witness, together with soundness and completeness proofs tying the
+contract to the underlying satisfiability relation. -/
+structure BehavioralContract (C : ConstraintSystem.{u, v, w}) (i : C.Index) where
+  /-- Precondition on the in-the-clear statement under which the contract applies. -/
+  Assumptions : C.Stmt i → Prop
+  /-- High-level specification relating the in-the-clear statement and the witness. -/
+  Spec : C.Stmt i → C.Wit i → Prop
+  /-- Soundness: if the assumptions hold and the underlying constraints are satisfied,
+    the spec holds for the recovered witness. -/
+  soundness : ∀ s o w, Assumptions s → C.satisfies i s o w → Spec s w
+  /-- Completeness: if the assumptions hold, there exist oracle and witness data making
+    the underlying constraints satisfied *and* the spec true. -/
+  completeness : ∀ s, Assumptions s → ∃ o w, C.satisfies i s o w ∧ Spec s w
+
+namespace BehavioralContract
+
+variable {C : ConstraintSystem.{u, v, w}} {i : C.Index} (B : BehavioralContract C i)
+
+/-- Under the assumptions, the constraint system is satisfiable at `i` for every statement.
+This is the most immediately useful corollary of `completeness`. -/
+theorem isSatisfiable_of_assumptions {s : C.Stmt i} (hs : B.Assumptions s) :
+    C.IsSatisfiable i s := by
+  obtain ⟨o, w, hsat, _⟩ := B.completeness s hs
+  exact ⟨o, w, hsat⟩
+
+end BehavioralContract
+
+end ConstraintSystem

ArkLib/ProofSystem/ConstraintSystem/Examples.lean

@@ -0,0 +1,81 @@
+/-
+Copyright (c) 2025 ArkLib Contributors. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Quang Dao
+-/
+
+import ArkLib.ProofSystem.ConstraintSystem.Basic
+import ArkLib.ProofSystem.ConstraintSystem.R1CS
+import ArkLib.ProofSystem.ConstraintSystem.Plonk
+
+/-!
+# Concrete instances of the universal `ConstraintSystem`
+
+This file wires the existing R1CS and Plonkish relations into the universal
+`ConstraintSystem` abstraction as a smoke test that the interface captures their shapes.
+
+- `R1CS.toConstraintSystem R` packages R1CS of every size `(m, n, n_w)` over a commutative
+  semiring `R` as a single constraint system. The three matrices `A, B, C` live in the
+  oracle-statement slot.
+- `Plonk.toConstraintSystem R` packages the gate-based Plonkish relation of every shape
+  `(numWires, numGates, ℓ)` over a commutative ring `R`. The gate layout itself lives in
+  the oracle-statement slot.
+
+Each instance is accompanied by a trivial verification lemma showing the `satisfies`
+predicate agrees with the original relation by definitional equality.
+-/
+
+/-- R1CS of every size over a fixed commutative semiring, packaged as a universal
+`ConstraintSystem`. The in-the-clear statement holds the public inputs, the oracle
+statement holds the three constraint matrices `A, B, C`, and the witness holds the
+private witness variables. -/
+def R1CS.toConstraintSystem (R : Type*) [CommSemiring R] : ConstraintSystem where
+  Index := R1CS.Size
+  Stmt := fun sz => Fin sz.n_x → R
+  OStmt := fun sz => R1CS.MatrixIdx → Matrix (Fin sz.m) (Fin sz.n) R
+  Wit := fun sz => Fin sz.n_w → R
+  satisfies := R1CS.relation R
+
+@[simp] theorem R1CS.toConstraintSystem_satisfies
+    (R : Type*) [CommSemiring R] (sz : R1CS.Size)
+    (stmt : Fin sz.n_x → R)
+    (mats : R1CS.MatrixIdx → Matrix (Fin sz.m) (Fin sz.n) R)
+    (wit : Fin sz.n_w → R) :
+    (R1CS.toConstraintSystem R).satisfies sz stmt mats wit ↔
+      R1CS.relation R sz stmt mats wit :=
+  Iff.rfl
+
+/-- The index data for the Plonkish constraint system: the number of wires, the number
+of gates, and the number of public inputs `ℓ ≤ numWires`. -/
+structure Plonk.Shape where
+  /-- Number of wires in the circuit. -/
+  numWires : ℕ
+  /-- Number of gates in the circuit. -/
+  numGates : ℕ
+  /-- Number of public inputs, bounded by `numWires`. -/
+  ℓ : ℕ
+  /-- Proof that `ℓ ≤ numWires`. -/
+  hℓ : ℓ ≤ numWires
+
+instance : Inhabited Plonk.Shape where
+  default := ⟨0, 0, 0, Nat.le_refl _⟩
+
+/-- The Plonkish relation of every shape over a fixed commutative ring, packaged as a
+universal `ConstraintSystem`. The in-the-clear statement holds the public inputs, the
+oracle statement holds the full gate layout (a `Plonk.ConstraintSystem` value), and the
+witness holds the private wire values. -/
+def Plonk.toConstraintSystem (𝓡 : Type) [CommRing 𝓡] : ConstraintSystem where
+  Index := Plonk.Shape
+  Stmt := fun s => Fin s.ℓ → 𝓡
+  OStmt := fun s => Plonk.ConstraintSystem 𝓡 s.numWires s.numGates
+  Wit := fun s => Fin (s.numWires - s.ℓ) → 𝓡
+  satisfies := fun s stmt cs wit => Plonk.relation cs s.ℓ s.hℓ stmt wit
+
+@[simp] theorem Plonk.toConstraintSystem_satisfies
+    (𝓡 : Type) [CommRing 𝓡] (s : Plonk.Shape)
+    (stmt : Fin s.ℓ → 𝓡)
+    (cs : Plonk.ConstraintSystem 𝓡 s.numWires s.numGates)
+    (wit : Fin (s.numWires - s.ℓ) → 𝓡) :
+    (Plonk.toConstraintSystem 𝓡).satisfies s stmt cs wit ↔
+      Plonk.relation cs s.ℓ s.hℓ stmt wit :=
+  Iff.rfl

ArkLib/ProofSystem/ConstraintSystem/Plonk.lean

@@ -107,8 +107,12 @@ end Gate
 
 /-- A Plonk constraint system is a vector of `numGates` gates, each parametrized by the underlying
   ring `𝓡` and `numWires`, the number of wires.
+
+  Marked `protected` so that bare `ConstraintSystem` inside `namespace Plonk` refers to the
+  universal `ConstraintSystem` in `ArkLib.ProofSystem.ConstraintSystem.Basic`. Users access
+  this definition as `Plonk.ConstraintSystem`.
 -/
-def ConstraintSystem (𝓡 : Type) (numWires numGates : ℕ) := Fin numGates → Gate 𝓡 numWires
+protected def ConstraintSystem (𝓡 : Type) (numWires numGates : ℕ) := Fin numGates → Gate 𝓡 numWires
 
 variable {𝓡 : Type} [CommRing 𝓡] {numWires numGates : ℕ}
 
@@ -122,15 +126,15 @@ namespace ConstraintSystem
 
 /-- A constraint system accepts an input vector `x` if all of its gates accept `x`. -/
 def accepts (x : Fin numWires → 𝓡)
-    (cs : ConstraintSystem 𝓡 numWires numGates) : Prop :=
+    (cs : Plonk.ConstraintSystem 𝓡 numWires numGates) : Prop :=
   ∀ i : Fin numGates, (cs i).accepts x
 
 /-- The partition induced by a constraint system as defined in the Plonk paper.
 
 For `i ∈ [numWires]`, let `T_i ⊆ [3*numGates]` be the set of indices `j` such that `V_j = i`,
 where `V` is the flattened vector of all wire indices `(a,b,c)` from all gates.
 This creates a partition of `[3 * numGates]` based on which gates use each wire index. -/
-def partition (cs : ConstraintSystem 𝓡 numWires numGates) :
+def partition (cs : Plonk.ConstraintSystem 𝓡 numWires numGates) :
     Fin numWires → Finset (Fin (3 * numGates)) :=
   -- We first cast via the equivalence `Fin (3 * numGates) ≃ Fin 3 × Fin numGates`,
   -- then filter by matching on the first coordinate `j.1`, which determines which wire we are
@@ -142,12 +146,13 @@ def partition (cs : ConstraintSystem 𝓡 numWires numGates) :
     (Finset.univ : Finset (Fin 3 × Fin numGates)))
 
 /-- The permutation corresponding to the partition induced by a constraint system. -/
-def perm (cs : ConstraintSystem 𝓡 numWires numGates) : Equiv.Perm (Fin (3 * numGates)) := sorry
+def perm (cs : Plonk.ConstraintSystem 𝓡 numWires numGates) : Equiv.Perm (Fin (3 * numGates)) :=
+  sorry
 
 /-- A constraint system is prepared for `ℓ` public inputs, for some `ℓ ≤ numGates, numWires`,
   if for all `i ∈ [ℓ]`, the `i`-th gate constrains the `i`-th wire to be some public value. -/
 def isPreparedFor (ℓ : ℕ) (hℓ : ℓ ≤ numGates) (hℓ' : ℓ ≤ numWires)
-    (cs : ConstraintSystem 𝓡 numWires numGates) : Prop :=
+    (cs : Plonk.ConstraintSystem 𝓡 numWires numGates) : Prop :=
   ∀ i : Fin ℓ, ∃ c, cs (Fin.castLE hℓ i) = Gate.eq (Fin.castLE hℓ' i) c
 
 end ConstraintSystem
@@ -158,7 +163,7 @@ end ConstraintSystem
 - A natural number `ℓ ≤ m` representing the number of public inputs
 - A subset `ℐ ⊂ [m]` of "public inputs" (assumed to be `{1,...,ℓ}` without loss of generality)
 -/
-def relation (cs : ConstraintSystem 𝓡 numWires numGates) (ℓ : ℕ) (hℓ : ℓ ≤ numWires) :
+def relation (cs : Plonk.ConstraintSystem 𝓡 numWires numGates) (ℓ : ℕ) (hℓ : ℓ ≤ numWires) :
     (publicInputs : Fin ℓ → 𝓡) → (privateWitness : Fin (numWires - ℓ) → 𝓡) → Prop :=
   fun (x : Fin ℓ → 𝓡) (ω : Fin (numWires - ℓ) → 𝓡) =>
     let combined := Fin.append x ω ∘ Fin.cast (by omega)