Curve 3Crv.

Safety, after any history

Exactly the committed calls, and conservation.

After any configured history from a checkpoint where the bytes are installed and the storage abstracts a model state, the code is intact and the final storage abstracts the state reached by running the model over exactly the settlement-committed calls to the token’s writers, in order — and that state conserves supply: totalSupply equals the sum of balances. The statement is short enough to read whole:

theorem c3crv_history_committed_derived {ca : Adr} {cfg : ChainConfig}
    {checkpoint future : BlockChain} {initial : Blanc.Curve3Crv.State}
    {initialKeys : Key → Prop}
    (trace : ConfiguredHistoryTrace cfg checkpoint future)
    (installed : some (checkpoint.state.getCode ca).toList = c3crvSem.image)
    (invariant : VyInv (checkpoint.state.getStor ca) initial initialKeys)
    (fresh : FreshKeys initialKeys (historyTouchedKeys ca trace)) :
    some (future.state.getCode ca).toList = c3crvSem.image ∧
      ∃ s, InvRun initial (committedInvocations ca trace) s ∧
        runInvocations initial (committedInvocations ca trace) = some s ∧
        VyInv (future.state.getStor ca) s
          (Key.extend initialKeys (invocationKeys (committedInvocations ca trace))) ∧
        Blanc.Curve3Crv.Conserved s

Besides the history itself, two hypotheses about the start and one about the hashes. fresh is trace-local: the mapping rows the history touches — rolled-back frames included — are tracked already or land on unused slots, and distinct rows land on distinct slots. No filter on static frames is needed, because no writer can succeed in one: every writer reaches an SSTORE or a LOG3, which a static frame forbids, and Blanc proves it from the frame’s own run (c3crv_writer_nonstatic).

Refinement

Every successful call is a step of the model.

From a fresh entry, a successful frame of the deployed runtime is exactly the model’s step for the decoded call. For a writer, the storage abstraction moves to the model’s next state, the logs are the model’s events, every other account’s storage is untouched, and the return bytes are the model’s: the ABI word true for transfer, transferFrom, approve, mint and burnFrom, empty for set_minter and set_name; the step for set_name also consumes the minter’s answer to owner(). For a view, storage and logs are unchanged and the return bytes equal the model’s output. Unknown selectors and short calldata have no successful run (c3crv_frame_refines).

Documentation that cannot drift

A token’s real policy.

Each of the following is a theorem about the model, carried to the bytes by the refinement theorems above.

• Every call conserves supply, and the initial state is conserving.Blanc.Curve3Crv.step_conserved
• Only the minter changes the supply, and only through mint or burnFrom; only the minter replaces the minter.supply_change_by_minter · minter_change_by_minter
• There is no infinite approval. A non-minter’s transferFrom of a nonzero amount spends allowance even when the allowance is the maximum value.transferFrom_spends_max_allowance
• The minter may move anything. The minter’s own transferFrom leaves every allowance untouched, as the deployed source’s comment “minter is allowed to transfer anything” says.transferFrom_minter_keeps_allowances
• Approvals start from zero. approve can set a nonzero allowance only when the current one is zero.approve_zero_first

theorem transferFrom_spends_max_allowance {ctx : Ctx} {f d v : B256} {s : State}
    {out : Out} (h : step ctx (.transferFrom f d v) s = .ok out)
    (hm : ctx.sender ≠ s.minter) (hv : v ≠ 0) :
    out.1.allowances f.toAdr ctx.sender ≠ s.allowances f.toAdr ctx.sender

Constructed executions

Live, at an exact cost.

A call the model accepts — any function but set_name — is a real execution ending in the model’s step, with exact logs and return bytes, at an exact cost: there is a constant c such that for every residual G above the 2,300-gas call stipend, the call succeeds when given G + c and leaves exactly G (c3crv_step_exec). The proofs construct each c; the exported theorem names no formula. The same holds at the state any configured history reaches (c3crv_history_live). set_name asks the minter’s owner() and is live given the callee premise OwnerCallOk, that the answer names the caller.

Where a history can start

Deployment.

Under every covered fork, the recorded creation input, run as a CREATE from the recorded deployer at nonce 42, installs the runtime at the token’s mainnet address and leaves storage that abstracts the model’s initial state — name, symbol, 18 decimals, zero supply, and the deployer as minter — with no hash premise: the constructor’s write of 0 at keccak(3 ‖ caller) is discharged by kernel evaluation (curve_deploy_covered). The recorded deployment therefore satisfies the history theorem’s checkpoint predicate. It is a modeled deployment: the 2020 transaction’s inclusion is not proved.

Stated, so it is not inferred

Not claimed.

• A closed cost formula; the cost is exact but existential.
• Logs and return bytes at the history level; they are stated frame by frame.
• set_name without the owner-call premise; transaction-level liveness.
• That today’s 3Crv storage abstracts a model state: that needs the holders and allowance pairs recovered from its Transfer and Approval logs, and a complete enumeration of its storage showing nothing else is stored.

We found no earlier machine-checked verification of this contract. The claim map’s 3Crv section lists every theorem with its premises, file and line.