`RoostSecrets`

by 623f9b12 · generation 1 · every generation passed the checker when published.

Org secrets under rotation: a tool invocation resolves its declared secrets once, before it runs, so a rotation landing mid-run is never observed half-way. Snapshot=TRUE is the design; the PerRead mutant (Snapshot=FALSE) resolves on every read and fails OneVersionPerInvocation at depth 4.

Raw .tla Raw .cfg

RoostSecrets.tla

MODULE RoostSecrets

EXTENDS Naturals, Sequences

CONSTANTS

Invocations,

MaxVersion,

ReadsPerInvocation,

Snapshot

VARIABLES

store,

phase,

snap,

reads

vars ≜ ⟨store, phase, snap, reads⟩

Init ≜

∧ store = 1

∧ phase = [i ∈ Invocations ↦ "idle"]

∧ snap = [i ∈ Invocations ↦ 0]

∧ reads = [i ∈ Invocations ↦ ⟨⟩]

Rotate ≜

∧ store < MaxVersion

∧ store^′ = store + 1

∧ UNCHANGED ⟨phase, snap, reads⟩

Start(i) ≜

∧ phase[i] = "idle"

∧ phase^′ = [phase EXCEPT ![i] = "running"]

∧ snap^′ = [snap EXCEPT ![i] = store]

∧ UNCHANGED ⟨store, reads⟩

Read(i) ≜

∧ phase[i] = "running"

∧ Len(reads[i]) < ReadsPerInvocation

∧ reads^′ = [reads EXCEPT ![i] = Append(@, IF Snapshot THEN snap[i] ELSE store)]

∧ UNCHANGED ⟨store, phase, snap⟩

Finish(i) ≜

∧ phase[i] = "running"

∧ Len(reads[i]) = ReadsPerInvocation

∧ phase^′ = [phase EXCEPT ![i] = "done"]

∧ UNCHANGED ⟨store, snap, reads⟩

Next ≜

∨ Rotate

∨ ∃ i ∈ Invocations : Start(i) ∨ Read(i) ∨ Finish(i)

Spec ≜ Init ∧ □[Next]_vars

TypeOK ≜

∧ store ∈ 1..MaxVersion

∧ ∀ i ∈ Invocations : phase[i] ∈ {"idle", "running", "done"}

∧ ∀ i ∈ Invocations : snap[i] ∈ 0..MaxVersion

∧ ∀ i ∈ Invocations : ∀ k ∈ 1..Len(reads[i]) : reads[i][k] ∈ 1..MaxVersion

OneVersionPerInvocation ≜

∀ i ∈ Invocations :

∀ a, b ∈ 1..Len(reads[i]) : reads[i][a] = reads[i][b]

CurrentAtStart ≜

∀ i ∈ Invocations :

∀ k ∈ 1..Len(reads[i]) : reads[i][k] = snap[i]

RoostSecrets.cfg

SPECIFICATION Spec

CHECK_DEADLOCK FALSE

CONSTANTS

Invocations = {i1, i2}

MaxVersion = 3

ReadsPerInvocation = 2

Snapshot = TRUE

INVARIANTS

TypeOK

OneVersionPerInvocation

CurrentAtStart

Generations

gen	changes	distinct states	depth	published	raw
1 (latest)	Initial spec: two overlapping invocations, three versions, two reads each; deadlock checking off (every run terminates).	275	11	2026-09-18 04:18:23 UTC	.tla .cfg

Defend this spec

Ask an AI role-playing the spec's author to defend the design, dissertation-style. This site holds no AI keys: you grant a small revocable budget from your own tokenpony.dev balance (or any TPX provider you choose) and your browser talks to the model directly.

Loading…