|
| 1 | +/- |
| 2 | +Copyright (c) 2025 ArkLib Contributors. All rights reserved. |
| 3 | +Released under Apache 2.0 license as described in the file LICENSE. |
| 4 | +Authors: XC0R |
| 5 | +-/ |
| 6 | +import ArkLib.ProofSystem.ConstraintSystem.Basic |
| 7 | +import Clean.Circuit.Foundations |
| 8 | + |
| 9 | +/-! |
| 10 | +# Clean ↔ ArkLib Bridge via ConstraintSystem |
| 11 | +
|
| 12 | +This module bridges Clean's `FormalCircuit` to ArkLib's `ConstraintSystem` and |
| 13 | +`BehavioralContract` abstractions, transferring circuit-level security guarantees |
| 14 | +(soundness and completeness) to ArkLib's universal constraint system interface. |
| 15 | +
|
| 16 | +A Clean `FormalCircuit F Input Output` maps to: |
| 17 | +- A `ConstraintSystem` where `satisfies` checks input consistency (`eval env inputVar = inp`) |
| 18 | + and circuit constraint satisfaction (`ConstraintsHold`). |
| 19 | +- A `BehavioralContract` where `Assumptions` and `Spec` are transferred directly from the |
| 20 | + circuit, with soundness proved via `original_soundness` and completeness via |
| 21 | + `original_completeness`. |
| 22 | +
|
| 23 | +## Main definitions |
| 24 | +
|
| 25 | +- `Clean.toConstraintSystem`: wraps a `FormalCircuit` as a `ConstraintSystem` |
| 26 | +- `Clean.toBehavioralContract`: wraps a `FormalCircuit` as a `BehavioralContract`, |
| 27 | + transferring both Clean security properties |
| 28 | +
|
| 29 | +## Dependencies |
| 30 | +
|
| 31 | +Targets upstream [Verified-zkEVM/clean](https://github.com/Verified-zkEVM/clean) at pinned |
| 32 | +commit `4a013fed` (post toolchain-bump-v4.28 merge via clean#357). |
| 33 | +-/ |
| 34 | + |
| 35 | +open Circuit |
| 36 | + |
| 37 | +namespace Clean.Bridge |
| 38 | + |
| 39 | +variable {F : Type} [Field F] |
| 40 | + {Input Output : TypeMap} [ProvableType Input] [ProvableType Output] |
| 41 | + |
| 42 | +/-- The canonical variable encoding for the input type, starting at offset 0. -/ |
| 43 | +abbrev canonicalInputVar (Input : TypeMap) (F : Type) [Field F] [ProvableType Input] : |
| 44 | + Var Input F := |
| 45 | + varFromOffset Input 0 |
| 46 | + |
| 47 | +/-- A Clean `FormalCircuit` viewed as an ArkLib `ConstraintSystem`. |
| 48 | +
|
| 49 | +The single index `Unit` reflects that one circuit is one constraint system (no size family). |
| 50 | +`satisfies` checks that the environment encodes the claimed input and that all circuit |
| 51 | +constraints hold. -/ |
| 52 | +def toConstraintSystem (circuit : FormalCircuit F Input Output) : |
| 53 | + ConstraintSystem where |
| 54 | + Index := Unit |
| 55 | + Stmt := fun _ => Input F |
| 56 | + OStmt := fun _ => PUnit |
| 57 | + Wit := fun _ => Environment F |
| 58 | + satisfies := fun _ inp _ env => |
| 59 | + eval env (canonicalInputVar Input F) = inp ∧ |
| 60 | + ConstraintsHold env |
| 61 | + (circuit.main (canonicalInputVar Input F) |>.operations 0) |
| 62 | + |
| 63 | +/-- A Clean `FormalCircuit` viewed as an ArkLib `BehavioralContract`. |
| 64 | +
|
| 65 | +- **Soundness**: Clean's `original_soundness` guarantees that if assumptions hold and |
| 66 | + constraints are satisfied, the circuit output satisfies `Spec`. |
| 67 | +- **Completeness**: Clean's `original_completeness` guarantees that if assumptions hold |
| 68 | + and a witness environment exists (encoding the input with valid local witnesses), |
| 69 | + constraints are satisfied and the output meets the spec. |
| 70 | +
|
| 71 | +The `hWitGen` parameter asserts that for every input satisfying `Assumptions`, there exists |
| 72 | +an environment encoding that input and using the circuit's local witness generators. This |
| 73 | +is guaranteed by Clean's circuit construction (witness generators are deterministic functions |
| 74 | +over the input), but is not directly exported as an existence theorem in Clean's API. -/ |
| 75 | +noncomputable def toBehavioralContract (circuit : FormalCircuit F Input Output) |
| 76 | + (hWitGen : ∀ inp, circuit.Assumptions inp → ∃ env : Environment F, |
| 77 | + eval env (canonicalInputVar Input F) = inp ∧ |
| 78 | + env.UsesLocalWitnesses 0 |
| 79 | + (circuit.main (canonicalInputVar Input F) |>.operations 0)) : |
| 80 | + ConstraintSystem.BehavioralContract (toConstraintSystem circuit) () where |
| 81 | + Assumptions := fun inp => circuit.Assumptions inp |
| 82 | + Spec := fun inp env => |
| 83 | + circuit.Spec inp (eval env (circuit.output (canonicalInputVar Input F) 0)) |
| 84 | + soundness := fun inp _ env hAssume ⟨hEval, hConstr⟩ => |
| 85 | + circuit.original_soundness 0 env (canonicalInputVar Input F) inp hEval hAssume hConstr |
| 86 | + completeness := fun inp hAssume => by |
| 87 | + obtain ⟨env, hEval, hLocalWit⟩ := hWitGen inp hAssume |
| 88 | + have hConstr := circuit.original_completeness 0 env |
| 89 | + (canonicalInputVar Input F) inp hEval hAssume hLocalWit |
| 90 | + have hSpec := circuit.original_soundness 0 env |
| 91 | + (canonicalInputVar Input F) inp hEval hAssume hConstr |
| 92 | + exact ⟨PUnit.unit, env, ⟨hEval, hConstr⟩, hSpec⟩ |
| 93 | + |
| 94 | +end Clean.Bridge |
0 commit comments