How it works

Write the rule. Prove the transition.

A transaction proposes a change to state, names the predicates that govern it, and carries a proof that they hold over that change. The validator checks the proof, and admits the change only if it holds. Your contract itself never executes anywhere on the chain.

The predicate

A statement in logic about a proposed change to state.

Written with the ordinary connectives and quantifiers, with equality and arithmetic comparison over the values involved. It evaluates to true or false over a transition, and that is the whole of it. No method table, no storage layout, no entry point, no execution order.

A payment predicatesays value is conserved and the spender's authorisation is present.

An escrow predicatesays when funds may move, and to whom.

A compliance predicatesays what every transfer of the asset it governs must satisfy.

What you do not write

Circuit performance, without authoring circuits.

Circuit languages get the same natural fit, because they have no machine in the middle either. The cost is where they put the author: you express the rule as a constraint system yourself, by hand, once per application. That is expert work, and a mistake in it is close to invisible, because an under-constrained circuit accepts what it should refuse and produces no behaviour to observe while doing so.

Modulus keeps the fit and moves the authoring up. You write the rule; the compiler produces the constraints. The trust moves off every application's hand-built circuit and onto one compiler with published semantics, reviewed once for all of them.

Every transaction

Three things travel together.

The statement

Which state is consumed, which state is produced, and under which predicates.

The witness

The private inputs that make those predicates true. Signatures, amounts, the contents of a position.

The proof

Evidence that such a witness exists and satisfies every governing predicate over exactly this transition, revealing none of it.

Whoever proposes a transition produces its proof, on their own machine, before anything is submitted. Verification is the network's side of the bargain and it is the cheapest thing here: milliseconds, identical for everyone, light enough to run in a wallet or on a phone.

Failure

A flawed transaction fails on your machine, not on the chain.

Elsewhere it runs anyway. It executes, burns the fee, and leaves whatever state its flaw produced for somebody else to unwind. Here the proof does not complete, on the author's own hardware, before the network has seen anything.

ReentrancyNothing executes, so nothing can call out mid-execution and re-enter against a half-updated balance.

Compiler and opcode mismatchesThere is no bytecode. Compilation is a proved translation into constraints, not a reinterpretation into instructions for a machine.

Proxy upgradesState is governed by the predicate attached to it. Moving to different rules is explicit and visible, never swapped in behind a constant address.

Out-of-gas half-statesNothing meters execution, so nothing stops partway and leaves the books in an intermediate state.

Spam inverts as well. Whoever writes an expensive rule pays to prove it themselves, so flooding the network mostly costs the flooder.

One relation, both directions

The rule that checks an answer can also find one.

A predicate is a relation rather than a procedure, so it runs either way round. The predicate that validates a finished sudoku grid also finds one: from seventeen clues, in roughly 160 milliseconds. Proving that a solution exists without disclosing any of it takes 16.

On an exchange that makes the quote a query. The sentence that validates a trade also answers what the trade returns, and there is only ever one sentence to maintain.