Proof of computation
Mudra
Prove that a committed calculation trace is unchanged — and, when the witness is shared for replay, that it was executed correctly — without revealing the model.
- What
- A proof-of-trace system: it binds a program digest, input/output hashes, the return value, and the step count in a constant-size proof. It does not constrain each instruction; per-instruction correctness comes from deterministic replay with the witness, or from trusting the prover.
- Why
- A hash on Arweave proves a file existed. It does not prove the math inside it was right. Regulated work still moves as spreadsheets and sealed models, and the counterparty has to trust the vendor’s black box. Mudra replaces that trust with a receipt the other side can verify. What a regulator or counterparty needs is not “here is our file hash”, but “here is proof this calculation produced this number, and you can check it without seeing our model.” The case studies are insurance brokering and fiscal metering.
- The combination
- A BigInt-native ZK VM + a constant-size Halo2 hash-chain seal (~6 KB; one verifying key for every program) + an Arweave receipt with an entropy beacon.
The difference
Table 1. What a hash proves, and what a proof of computation adds.The difference is the calculation, not the file.
| Measure | Hash + timestamp | Mudra |
|---|---|---|
| What is proved | A file existed at a time. | A specific program, its inputs, its output, and the step count are bound in one proof. |
| What stays private | Usually nothing; the file is revealed to check it. | The formulas, inputs, and business logic; the proof carries fingerprints. Replay requires the witness, optionally shared encrypted. |
| What the verifier needs | The file and its hash. | The proof (~6 KB), the verifying key, and the program digest; replay requires the witness. |
| What it does not prove | That the math inside the file is right. | That the spreadsheet is a good model, that every instruction is constrained, or that a proof-only verifier can check execution. |
The circuit seals a hash chain, not every instruction; per-instruction correctness relies on deterministic replay.
Design
- Prove the trace, not just the file. The proof binds a program digest, input and output hashes, the return value, the step count, and the specification digest into one seal; a file hash cannot. It does not constrain each instruction; replay does that.
- Keep the formulas private. The proof contains fingerprints, not the spreadsheet; the program, inputs, and business logic stay on the prover’s machine. Encrypted witness sharing is optional for a counterparty that must replay.
- Use one circuit for every program. The Halo2 circuit seals a Poseidon hash chain across 21 field elements; it is constant-size regardless of the program, so every program uses the same verifying key. Halo2 is the seal, not the execution engine.
- Make the seed independently chosen. The entropy beacon derives the seed from Arweave block hashes that did not exist when the intent was posted, so a prover cannot rerun with favourable seeds and publish only the best result.
- Verify anywhere. A lightweight WASM verifier checks the hash chain in a browser, on a phone, or from the CLI.
Provenance
Mudra is extracted from DarkFi; the ZK VM lineage is inherited. The spreadsheet transpiler, the constant-circuit hash-chain seal, the verifier WASM, the Arweave receipt pipeline, the entropy beacon, and the Lean 4 specification are the project’s work. The code is AGPL-3.0-only.
Evidence
| Measure | Value | Source |
|---|---|---|
| Proof size | ~6 KB, constant | README |
| Circuit | 21 field elements; one verifying key for every program | Architecture |
| VM | 32 BigInt registers; 64 KB memory; 21 instructions | README |
| Demos | 4 spreadsheets, 100–632 instructions | Demos |
| Verifier | WASM; browser, phone, CLI | README |
| Audit trail | Arweave receipt (TXID) | Arweave verification |
| Formal specification | Lean 4 | Lean specification |
Sources: repository README and docs, as of October 2026. Proof size and circuit properties are implementation claims; the Lean specification and demos are in the repository.
Spreadsheet or programBigInt VM execution~6 KB Halo2 proofArweave receipt (TXID)Browser / CLI verifier
Limits
- Research build; not a production audit system; no third-party audit is claimed.
- The circuit seals a hash chain, not every instruction. Per-instruction correctness relies on deterministic replay; a verifier with only the proof and public inputs cannot check it without the witness. The encrypted-witness path is how that can be shared without publishing the model. If you need per-opcode constraints, use RISC Zero, SP1, or zkWASM.
- Proving runs on a single machine and needs the ~2 MB Halo2 parameters for k=15; distributed proving is future work.
- The entropy beacon adds roughly six minutes of latency and requires Arweave gateways; the instant path uses a user-supplied seed.
- The spreadsheet transpiler supports a subset of spreadsheet functions — 33 in the insurance case study — and roughly 1,024 dense cells; it is not a full Excel engine.
- The browser-side verifier is a lightweight check; full Halo2 verification uses the CLI with the parameters.