Why a retried refund runs once Diagram

The short answer

• The check refuses an irreversible effect with two or more attempts that names no guarantee, and the runtime puts the same key on every attempt

Not shown here

• The certificate and the vendored engines, which carry the finding and the outbox but do not decide it
• Connected but out of scope: poly CLI, poly-lang, poly-embed, poly-core, poly-lower, Certified build

What it guarantees

• An irreversible effect that may be attempted twice is not admitted unless it names how its target is kept from running it twice: poly-ref reports PL4003 with a witness (a delivery in which the target may execute twice) unless the effect is keyed (an idempotency header and a window that holds the retry horizon) or idempotent by nature in the pinned standard library. The runtime sets the key on every write in a capability the handler cannot bypass. What poly does not verify are the assumptions K17 (the target honours the key) and K18 (an effect declared idempotent by nature is), which a certificate names when an effect declares them
• A check that did not run or hit a bound is never CLEAN: the verdict fold ranks INCONCLUSIVE and UNDERPOWERED apart from CLEAN, vacuous properties are INCONCLUSIVE, and admission refuses a build with any check not run

Why a retried refund runs once

How does poly keep an effect that cannot be undone from running twice when a delivery is retried?

A worker retries an effect when an answer is lost. For a read that costs nothing. For a refund the target may have done the work already, and a second request moves the money twice. The question is where in poly that is decided, and what is left to trust.

The long read

Retry safety is decided in poly-ref, from the semantics, with no code shared with the compiler. For every effect of class irreversible, poly-ref reads the number of attempts the effect declares (or the default of five). One attempt is at most once and needs no finding. Two or more need a guarantee: a keyed one, which names the header and a window longer than the retry horizon, or idempotent by nature, which only a pinned standard-library file may declare. Otherwise the check reports PL4003 with a path to the step that emits the effect and the delivery in which the target may execute twice. An effect that reaches outside without a class is PL6304.

The pipeline tells poly-ref whether the module is a pinned library file, by comparing its digest with std/PINS.json. Admission then refuses a build with such a finding unless a person has signed an acceptance.

At run time the worker retries the effect and the capabilities wrapper gives the handler an egress call that sets the key header, the intent id, on every write. A handler that supplies the header has it replaced, and the replacement is audited. A second write in one attempt is refused. This is why the rule is a rule about what runs: the manifest entry the runtime reads is compared with the same declarations by the read-back of artefacts.

Two things stay outside the check. The target must honour the key (K17) and an effect declared idempotent by nature must be (K18). And the key belongs to an intent, not to an order: a second request is a second intent. That is the lesson of the v1.3.0 concierge, and the reason v1.3.1 adds a ledger to the program itself.

Terms used here

artefact: A file produced by lowering a machine, such as the contract, the SAM v2 module or the effects manifest. The engines read artefacts and never the source.
certificate: A signed record that binds a program's source and artefact digests to the checks that ran and their results. The runtime loads only what one names.
poly-ref: poly's own model checker. It is written from the semantics and shares no code with the compiler.
gate: The two-phase mediation of an effect: propose before the call, settle after it. The Polyaxion engine decides allow, deny or escalate.
outbox: The table in which a step leaves its effect intents. The effect worker takes them out one at a time, at least once.
ledger: The record of every step, advice, decision, outcome, gate verdict and effect of a run, hash-chained per run with signed heads and a periodic anchor.
witness: The path of states and actions that shows a finding, exported as a test and kept so that a person can accept the finding.
vacuous: A property whose antecedent is never true where it is judged. It holds for no reason the program gives, so it is INCONCLUSIVE and never CLEAN.
vendored engine: An engine file copied unchanged into vendor/ and pinned by hash and commit, so poly relies on the Poly stack conceptually and not physically.
idempotency key: A value sent with a write so that the receiver can recognise a retry of the same request and do the work once. In poly it is the intent id, and the runtime sets it.
irreversible effect: An effect whose result cannot be taken back once it has happened, such as a refund or a message sent. poly requires such an effect that may be attempted twice to say how it is kept from running twice.