# Capsulang ZK / Noir add-on

Capsulang can now model selected privacy-preserving proof obligations as `zk-proof` declarations and emit a Noir project for the restricted supported subset.

The purpose is narrow and deliberate:

```text
Capsulang governs the workflow.
Noir proves a selected private predicate.
Lean/SMT remain the path for public program invariants.
```

A Noir proof does **not** prove the whole Capsulang workflow. It proves that a private witness satisfies the generated circuit relation for a declared proof.

## Example

```lisp
(zk-proof DeploymentRiskProof
  (backend noir)
  (public
    (change_id U64)
    (threshold U32)
    (risk_model_hash Bytes32))
  (private
    (risk_score U32)
    (findings_commitment Bytes32))
  (proves (<= risk_score threshold))
  (summary "Proves that a private risk score is below a public threshold."))
```

In a machine transition, the proof verification appears as a typed effect intent:

```lisp
(effects
  (zk.verify DeploymentRiskProof)
  (db.write operational.proof_events)
  (a2ui.emit private_change_approval))
```

## Commands

```bash
caps check examples/24_private_deployment_risk_proof.caps --json
caps zk-plan examples/24_private_deployment_risk_proof.caps --json
caps emit-noir examples/24_private_deployment_risk_proof.caps \
  --proof DeploymentRiskProof \
  --out build/DeploymentRiskProof.nr \
  --json
caps emit-noir examples/24_private_deployment_risk_proof.caps \
  --proof DeploymentRiskProof \
  --out-dir build/DeploymentRiskProof \
  --json
```

If `nargo` is installed:

```bash
caps noir-compile build/DeploymentRiskProof --json
caps noir-execute build/DeploymentRiskProof --json
```

If `nargo` is not installed, these commands report `status: unavailable` rather than pretending to prove anything.

## Generated project

`caps emit-noir --out-dir` writes:

```text
Nargo.toml
Prover.toml
src/main.nr
capsulang_zk_manifest.json
```

`Prover.toml` contains example witness values only. Replace private witness values before generating a proof.

## Supported subset

The v0 ZK emitter supports:

```text
Bool, Field, Bytes32, Address, U32, U64, I32, I64
pure comparisons and arithmetic predicates
and / or / not
simple if expressions
```

It does not support arbitrary Capsulang machines, adapters, stores, A2UI, MCP, A2A, SurrealDB, TypeDB, or dynamic LLM authoring.

## Correctness boundary

Noir helps prove private statements such as:

```text
I know a private risk score below this public threshold.
I know a private credential/member witness.
I know private evidence satisfying a public policy relation.
```

It does not prove:

```text
The generated circuit is the right circuit.
The whole workflow is safe.
The runtime policy is complete.
The host adapter behaved correctly.
```

For those, use Capsulang checking, scenario tests, semantic trace/replay, Lean/SMT obligations, and human review.