warda_grant.sil · v4 · fingerprint b3e5eeefacf2021f

Covenant audit

Every verdict below comes from TxScriptEngine, the same script engine a Kaspa node validates a transaction with. Nothing here is inferred from reading the source.

Where this audit is strong, and where it is thin

One bar per entrypoint, on one scale: a longer bar is more published claims. Boundary means a numeric pair was measured on the claim's own axis, one unit apart. Flip means only the refusal was executed, attributable because the case is a single field from an accepted baseline — a Merkle root has no number line, so its claims can only ever be flip grade. Neither is better; they are different evidence.

Why a rejection here means something

The engine collapses every failed require into one opaque VerifyError. It never says which rule rejected, so asserting that something was refused proves nothing on its own — a malformed signature script looks exactly like a working spending cap.

Every case is a single field changed from a baseline this run proved the engine accepts. A rejection can therefore only be caused by the field that moved. Numeric rules are exercised one unit either side of their boundary, so a rule that is present but in the wrong place shows up as a disagreement rather than as a pass.

Where each boundary actually is

The filled mark is the tightest value the engine accepted. The barred mark is the loosest it refused. Both were executed; neither is inferred.

Findings

No violations — nothing the guarantees forbid was accepted. No over-refusals — nothing they permit was refused.

Every claim the guarantees make

This is the report's denominator: each enforcement claim GUARANTEES.md makes, and each require in the two exits, against what this run executed. A claim nothing covers is listed here as uncovered rather than left out of the count.

Boundary — a numeric pair was measured on the claim's own axis, one unit apart. Flip — only the refusal was executed, and it is attributable because the case is a single field away from an accepted baseline. A Merkle root has no number line, so its claims can only ever be flip grade.

Every case

The check that reads no specification

Everything above compares the bytecode to a written claim, which is why it cannot notice a rule that should exist and does not. A second pass asks a question nobody had to write down first: it generates spend attempts structurally, discards everything the engine refused, and asserts one property of what is left — an accepted spend must not leave the agent able to do more than it could before, minus what it just paid.

The second row is the self-check, and it is not decoration. An oracle that has never fired is indistinguishable from one that cannot, so the run ends by deleting require(currentEpoch >= prevState.epochIndex) from the covenant — and requiring the same oracle to catch it. It does: an agent whose epoch allowance is exhausted claims an earlier epoch, and the whole allowance comes back.

That is the one line in this report that says a clean run above is worth something. The oracle can fire, it fires on a covenant this one used to be, and it is silent on the covenant as written.

What this run did not test

• One claim on settle: that output 0 is the co-input grant's single authorised continuation. The baseline builds exactly that shape, so there is no transaction in this run where it is the only thing wrong — the refusals that would prove it are indistinguishable from the co-input check firing first.
• The subset witness: a child narrowing its allowlist to a subtree.
• Any grant shape but one. Every case runs against a single parameterisation — 100 KAS, a 2 KAS per-spend cap, delegation depth 2, a four-member allowlist, maxProofDepth 4. Whether the same boundaries hold at depth 16, or with a 65,536-member tree, or a one-sompi budget, is untested.
• Anything above the script engine — a node's mempool policy, relay rules, or what a wallet does with a transaction before it is broadcast.
• The residual described in GUARANTEES.md: allowance from unused epochs stays spendable after the chain passes expiresAt. That is a property of the design, correctly implemented, not a defect the engine can report.

What a clean run does not mean

This instrument checks the bytecode against a written claim. It cannot notice a rule that should exist and does not, because the document it takes its claims from is the same document that would have omitted it.

That is not a hypothetical. Of the five vulnerabilities this covenant has had, none would have been caught by the claims suite. The epoch cap that limited nothing and the missing expiry check were both absent from the guarantees at the time. The template-id defect is not engine-visible. The fifth was in settle, The fifth is now covered — but only because it has already been found: the claim it violates was written as part of its fix, and a suite whose oracle is the documentation learns about a hole the day somebody else closes it. Every one of the five was found the same way, and it was not this way: a person asked what an adversary supplies at each input, built it, and watched the engine accept it.

The section above it is the answer to that, and the only one this tool has: an oracle that consults no document, and a covenant with a known hole in it to prove the oracle can fire.