feat(Bridge): Clean to ArkLib bridge with completeness and structural soundness

[XC0R]

Summary

Bridge module that wraps Clean's FormalCircuit as an ArkLib NonInteractiveReduction,
transferring circuit-level security guarantees to protocol-level probabilistic security definitions.

Both Clean security properties (original_completeness and original_soundness) are transferred
through reduction_perfectCompleteness, which composes them to show the output satisfies Spec
with probability 1. reduction_soundness is a structural property of the bridge construction
(inputs outside Assumptions are rejected, error = 0).

Architecture

A Clean FormalCircuit F Input Output is wrapped as a 1-round ProverOnly protocol:

• Prover: sends the witness Environment F as its single message
• Verifier: noncomputably checks circuit.Assumptions on the input; if satisfied, computes
  and returns the circuit output
• Completeness: original_completeness (constraints hold) + original_soundness (spec holds) compose to give ArkLib perfect completeness
• Soundness: verifier rejects inputs outside the Assumptions language (error = 0)

Clean dependency

Now targets upstream Verified-zkEVM/clean at pinned
commit 4a013fed (post toolchain-bump-v4.28 merge via clean#357).

lake-manifest.json changes are a lake update artifact from retargeting the dep.

New file

• ArkLib/Bridge/Clean.lean (230 lines, 0 sorrys)

[chatgpt-codex-connector]

Codex usage limits have been reached for code reviews. Please check with the admins of this repo to increase the limits by adding credits.
Credits must be used to enable repository wide code reviews.

[github-actions]

🤖 Gemini PR Summary

Implements a formal bridge between the Clean circuit library and ArkLib's protocol framework, allowing FormalCircuit constructions to be treated as NonInteractiveReduction objects.

Mathematical Formalization

• Circuit-to-Protocol Mapping: Wraps a FormalCircuit as a 1-round ProverOnly protocol. The prover provides the Environment (witness), and the verifier noncomputably validates circuit.Assumptions to determine the output.
• Security Transfer: Enables the lifting of deterministic circuit-level correctness to probabilistic protocol-level security definitions.

Proofs

• Completeness: reduction_perfectCompleteness proves that Clean completeness implies ArkLib perfect completeness.
• Soundness: reduction_soundness proves that Clean soundness translates to zero-error soundness (rejecting all inputs outside the assumption language).
• Status: The implementation contains zero sorry or admit placeholders.

Infrastructure & Dependencies

• Lake Dependency: Adds XC0R/clean (branch toolchain-bump-v4.28) as a dependency.
• Compatibility: The dependency fork aligns the Lean toolchain to v4.28.0 and renames Vector.cons to Vector.listCons to prevent namespace collisions with CompPoly.
• New File: ArkLib/Bridge/Clean.lean contains the bridge implementation and transfer theorems.

---

Statistics

Metric	Count
📝 Files Changed	4
✅ Lines Added	258
❌ Lines Removed	12

---

Lean Declarations

✏️ **Added:** 7 declaration(s)

• def relOut (circuit : FormalCircuit F Input Output) : in ArkLib/Bridge/Clean.lean
• def mkProver (circuit : FormalCircuit F Input Output) : in ArkLib/Bridge/Clean.lean
• abbrev canonicalInputVar (Input : TypeMap) (F : Type) [Field F] [ProvableType Input] : in ArkLib/Bridge/Clean.lean
• theorem reduction_soundness (circuit : FormalCircuit F Input Output) : in ArkLib/Bridge/Clean.lean
• theorem reduction_perfectCompleteness (circuit : FormalCircuit F Input Output) : in ArkLib/Bridge/Clean.lean
• def pSpec : ProtocolSpec 1 in ArkLib/Bridge/Clean.lean
• def relIn (circuit : FormalCircuit F Input Output) : in ArkLib/Bridge/Clean.lean

---

sorry Tracking

• No sorrys were added, removed, or affected.

---

🎨 **Style Guide Adherence**

There are 26 violations of the style guide. They are grouped by rule below:

• Variable Conventions (Elements) (11 violations): x, y, z, ... : Elements of a generic type

  • Line 78 & 81: _inp should be a standard element variable like x.
  • Line 104, 106, & 115: p and input used as elements should be x, y, or z.
  • Line 133 & 179: stmtIn, witIn, and prover should be replaced with x, y, z.

• Variable Conventions (Assumptions/Hypotheses) (5 violations): h, h₁, ... : Assumptions/Hypotheses

  • Line 133: hIn violates the naming convention.
  • Line 135: hAssume, hEval, and hWit violate the convention.
  • Line 179: hNotIn violates the convention.

• Syntax and Formatting (Parentheses/Nesting) (2 violations): Avoid parentheses where possible. Use <| (pipe left) and |> (pipe right) to reduce nesting.

  • Line 106: eval p.2 (canonicalInputVar Input F) uses unnecessary parentheses; use <|.
  • Line 108: (circuit.main (canonicalInputVar Input F) |>.operations 0) contains multiple levels of nested parentheses.

• Documentation Standards (2 violations): Every definition and major theorem should have a docstring.

  • Line 101: def relIn is missing a /-- ... -/ docstring.
  • Line 114: def relOut is missing a /-- ... -/ docstring.

• Variable Conventions (Types) (2 violations): α, β, γ, ... : Generic types

  • Line 179: WitIn and WitOut should use Greek letters like α and β.

• Individual Violations:

  • Line 2: Copyright (c) 2025 ArkLib Contributors. All rights reserved. violates the header rule: "Use standard file headers including copyright... Copyright (c) 2024 Author Name. All rights reserved."
  • Line 98: The definition of toReduction uses { ... } instead of the where syntax, violating: "Use the where syntax for defining instances and structures."
  • Line 142: This line exceeds the 100-character limit (107 characters), violating: "Keep lines under 100 characters."
  • Line 155: The use of ge_iff_le indicates the presence of a ≥ operator, violating: "Avoid ≥ (ge) and > (gt) in theorem statements unless necessary for argument ordering."

---

📄 **Per-File Summaries**

• ArkLib.lean: This change updates the main ArkLib entry point to import the ArkLib.Bridge.Clean module. This integrates new definitions and theorems related to the bridge functionality into the top-level library structure.
• ArkLib/Bridge/Clean.lean: This file introduces a bridge between Clean's circuit foundations and ArkLib's protocol security framework by wrapping a FormalCircuit as a NonInteractiveReduction. It defines the associated protocol specifications, prover, and verifier, and proves theorems reduction_perfectCompleteness and reduction_soundness to transfer security properties between the two systems. The module contains no sorry or admit placeholders.
• lakefile.toml: This change adds the Clean library as a new project dependency, pinned to a specific toolchain-compatible revision.

---

Last updated: 2026-04-12 22:39 UTC.

[mitschabaude]

wow! will look at this next week, amazing

I definitely want the toolchain bump on main in clean so the libs can stay synced, can you create a PR from https://github.com/XC0R/clean/tree/toolchain-bump-v4.28 ?

Vector.cons → Vector.listCons rename to avoid namespace collision with CompPoly

I will try to align the definitions in clean so we don't have to change the name!

[XC0R]

PR for the toolchain bump: Verified-zkEVM/clean#357

Re the Vector.cons rename: if you align the definitions on the Clean side, I can drop that commit from the PR. Let me know how you'd like to handle it.

[quangvdao]

@XC0R Thanks for putting this together! Two substantive items before this can land:

1. Lake dependency should target upstream Verified-zkEVM/clean. lakefile.toml currently points at https://github.com/XC0R/clean at branch toolchain-bump-v4.28. Once bump: Lean v4.25.2 → v4.28.0 with Mathlib v4.28.0 clean#357 lands the toolchain bump on upstream main, please retarget the dep there with a pinned commit. Depending on a personal fork long-term creates a bus factor.

2. Soundness narrative is weaker than the title implies. ArkLib Verifier.soundness (ArkLib/OracleReduction/Security/Basic.lean:226-248) only quantifies over stmtIn ∉ langIn. With langIn = { inp | circuit.Assumptions inp }, your reduction_soundness proof goes through the if_neg hNotIn branch and never invokes Clean's Soundness property at all. That's formally correct, but a reader who sees "completeness and soundness transfer" in the title will assume Clean's full constraint soundness is being lifted to ArkLib for in-language statements, which isn't what's happening. Please:

   • Update the module docstring on Bridge/Clean.lean to say explicitly that this transfers ArkLib's out-of-language soundness only, not Clean's constraint soundness on in-language inputs, and
   • Maybe rephrase the PR title to something like "Clean ↔ ArkLib bridge: completeness transfer + ArkLib-style soundness" so it matches what the proofs actually do.

The completeness side genuinely uses Clean's original_completeness + original_soundness on the canonical input variable, which is fine. The diff has no sorrys, which is great.

Minor: the unrelated lake-manifest.json churn (mathlib "scope" change, ExtTreeMapLemmas reordering) deserves a one-line note in the PR body so reviewers know it's a lake update artifact and not deliberate.

[Posted by Cursor assistant (model: Opus 4.7) on behalf of @quangvdao with approval.]

[github-actions]

🤖 PR Summary

Mathematical Formalization

• toReduction: A new constructor that transforms a Clean FormalCircuit into an ArkLib NonInteractiveReduction modeled as a one-round ProverOnly protocol.
• reduction_perfectCompleteness: A theorem lifting Clean’s original_completeness and original_soundness to prove that the reduction satisfies its specification with probability 1 when circuit assumptions are met.
• reduction_soundness: A theorem establishing structural soundness; the protocol verifier is defined to reject any inputs outside the circuit’s Assumptions language with zero error.
• Protocol Modeling: The bridge models the prover’s message as the circuit’s witness (Environment) and the verifier as a noncomputable check that validates constraints to produce the circuit output.

Proof Status

• No sorry or admit placeholders are present. All theorems regarding the bridge's completeness and soundness in ArkLib/Bridge/Clean.lean are fully proved.

Infrastructure & Dependencies

• Clean Integration: Adds Verified-zkEVM/clean as a formal dependency in lakefile.toml, pinned to commit 4a013fed.
• Library Exports: Integrates the bridging functionality into the top-level namespace by exporting ArkLib.Bridge.Clean in ArkLib.lean.
• Manifest: Updates lake-manifest.json to reflect the new dependency and toolchain compatibility requirements.

---

Statistics

Metric	Count
📝 Files Changed	4
✅ Lines Added	267
❌ Lines Removed	12

---

Lean Declarations

✏️ **Added:** 9 declaration(s)

• abbrev canonicalInputVar (Input : TypeMap) (F : Type) [Field F] [ProvableType Input] : in ArkLib/Bridge/Clean.lean
• theorem reduction_perfectCompleteness (circuit : FormalCircuit F Input Output) : in ArkLib/Bridge/Clean.lean
• def relIn (circuit : FormalCircuit F Input Output) : in ArkLib/Bridge/Clean.lean
• noncomputable def toReduction (circuit : FormalCircuit F Input Output) : in ArkLib/Bridge/Clean.lean
• def relOut (circuit : FormalCircuit F Input Output) : in ArkLib/Bridge/Clean.lean
• noncomputable def mkVerifier (circuit : FormalCircuit F Input Output) : in ArkLib/Bridge/Clean.lean
• def mkProver (circuit : FormalCircuit F Input Output) : in ArkLib/Bridge/Clean.lean
• def pSpec : ProtocolSpec 1 in ArkLib/Bridge/Clean.lean
• theorem reduction_soundness (circuit : FormalCircuit F Input Output) : in ArkLib/Bridge/Clean.lean

---

sorry Tracking

• No sorrys were added, removed, or affected.

---

🎨 **Style Guide Adherence**

The following violations of the style guide were identified:

• Syntax and Formatting: Prefer fun x ↦ ... over λ x, .... (The community standard ↦ is preferred over => for functions).

  • Line 90: sendMessage | ⟨0, _⟩ => fun ⟨_inp, env⟩ => pure (env, ⟨_inp, env⟩)
  • Line 93: output := fun ⟨_inp, env⟩ =>
  • Line 110: verify := fun inp transcript =>
  • Line 233: ... >>= fun _ => pure none

• Syntax and Formatting: Put spaces on both sides of :, :=, and infix operators.

  • Line 68: (F := F) (Missing spaces around :=)
  • Line 70: (pSpec (F := F)) (Missing spaces around :=)
  • Line 72: (pSpec (F := F)) (Missing spaces around :=)
  • Line 81: (pSpec (F := F)) (Missing spaces around :=)
  • Line 108: (pSpec (F := F)) (Missing spaces around :=)

• Naming Conventions: Acronyms: Treat as words (e.g., HtmlParser not HTMLParser).

  • Line 68: VCVCompatible (Should be VcvCompatible)

• Naming Conventions: Use manual dot notation for logical connectives and equality (e.g., And.intro, Eq.refl, Iff.mp).

  • Line 207: refine ⟨?_, ?_⟩ (Use And.intro ?_ ?_ for the logical And connective)
  • Line 215: exact ⟨⟨stmtIn, hSpec⟩, rfl⟩ (The inner ⟨stmtIn, hSpec⟩ should use Exists.intro stmtIn hSpec for the existential connective)
  • Line 215: exact ⟨⟨stmtIn, hSpec⟩, rfl⟩ (The outer constructor should use And.intro for the logical And connective)
  • Line 215: exact ⟨⟨stmtIn, hSpec⟩, rfl⟩ (Use Eq.refl instead of rfl for equality)

• Variable Conventions: u, v, w, ... : Universes; α, β, γ, ... : Generic types.

  • Line 229: intro WitIn WitOut ... (Generic types WitIn and WitOut should follow the naming convention for generic types, e.g., α and β).

---

📄 **Per-File Summaries**

• ArkLib.lean: This change updates the top-level ArkLib.lean file to export the ArkLib.Bridge.Clean module, effectively integrating its definitions and theorems into the main library. The modification expands the library's scope without introducing any new proofs or sorry placeholders in this file.
• ArkLib/Bridge/Clean.lean: This file establishes a bridge between Clean's circuit model and ArkLib's protocol reduction framework by defining toReduction, which wraps a FormalCircuit as a NonInteractiveReduction. It introduces theorems reduction_perfectCompleteness and reduction_soundness to transfer Clean's internal security properties into ArkLib's probabilistic security definitions. The implementation is complete and contains no sorry or admit placeholders.
• lakefile.toml: Adds the Clean library as a new project dependency, sourcing it from the Verified-zkEVM GitHub repository at a specific revision.

---

Last updated: 2026-04-17 20:25 UTC.