control.t27: journal hand-off so a restarted agent does not repeat a paid call or a PR open #7006

Activity

1. gHashTag commented on Oct 6, 2026

   

   gHashTag

   on Oct 6, 2026

   OwnerAuthor

   More actions

   Answer to the open question, and the design that follows from it (local commits on the landing branch for epic #6971; the PR opens after #7043 merges, Closes #7006).

   Can Restate's ctx.run run twice? Yes. Its TypeScript SDK reference for run says: "There is a small window where an action may be re-run, if a failure occurred between a successful run and persisting the result." (https://restatedev.github.io/sdk-typescript/interfaces/_restatedev_restate-sdk.Context). Temporal says the same of activities and recommends an idempotency key of Workflow Run ID + Activity ID, without the attempt (https://docs.temporal.io/develop/python/best-practices/error-handling). So "journal before, skip if done" cannot be exactly-once by itself: the window between the effect and the "done" write stays open.

   What control.t27 section 7 does instead:

   • one entry per effect: intent before it, done after it, at the holder's fence;
   • the key is (task, kind, target):
     • not the position: a model turn is not deterministic, so replay by position (Temporal, Restate) does not apply;
     • not the fence, as the proposal said: every retry must see the same key, as Temporal leaves the attempt out of its key;
   • effect_action(entry, kind, fence, my_fence):
     • a stale fence does nothing;
     • with no entry, the effect runs;
     • a done entry is skipped;
     • an open intent is looked up at GitHub where it can be (push, pull request, comment) and runs again where it cannot (a model call);
   • look_wait_seconds: after a DOWN, the look waits out GitHub's 10 s request limit (https://docs.github.com/en/rest/using-the-rest-api/troubleshooting-the-rest-api), and an invariant keeps that wait under the first heartbeat;
   • effect_may_repeat: the receiver refuses a copy of a push (leased) and of a pull request. A second PR for the same head is a 422, "A pull request already exists" (Errors.Code == "custom" when from Client.PullRequests.Create when PR already exists google/go-github#1441).

   Limits, stated in the spec:

   • A comment can still repeat behind a partition, because the old holder may be alive and send again. The journal's marker only makes the copy detectable.
   • A model call runs again after every crash that leaves its intent open. This is the same at-least-once window Restate and Temporal have.
   • GitHub documents that it terminates a request after 10 s. It does not document that a terminated write is never applied later, so the spec names this as an assumption. If it fails, a comment can repeat even after a DOWN.

   Evidence, printed by commands in this tick:

   • control.t27 has 42 pub functions, 8 invariants and 15 tests. All 15 pass with 0 vacuous passes, and parse, typecheck, gen-rust, gen-verilog and gen-c exit 0.
   • tri mutate spec --fn (feat(tri): tri mutate spec -- guard, operator and arithmetic mutants of a .t27 spec (Closes #6993 #7022) #7043 build) on the 7 new functions killed 36 of 36 mutants after one gap. Dropping seconds_since_down > LIMIT survived, because at 11 s both paths return 0. Asserts at 12 s and 3600 s now kill it, since the u32 subtraction underflows.
   • 16 hand constant mutants were all killed. With the_effect_codes_are_distinct removed, the four DO_* mutants survive, so that invariant is what pins them.
   • actors.t27 reclaim_wait_seconds points at the journal. This is doc only: actors.t27 does not import control.t27.
2. gHashTag

   closed this as completedin 96cf7c8on Oct 6, 2026
3. gHashTag

   added 2 commits that reference this issue on Oct 6, 2026

   feat(t27b): std.mem.eql/indexOf on byte slices and byte-array pointers (

   ...

   7743aff

   fix(codegen): gen-rust enum order and gen-zig float-call cast (#6941) (…

   ...

   5913764