ms2k/corago
SHA256
Watch
0
Code Releases 3 Activity

Reconcile goal recovery with human intent and model state transitions

Browse source
This commit is contained in:
ms2k 2026-10-18 19:21:26 +09:00
commit 548eb69211
31 changed files with 1765 additions and 96 deletions
Download patch file Download diff file Expand all files Collapse all files

1
.gitignore vendored
View file

@ -1 +1,2 @@
docs/journal
scratchpad

33
codex-keep/README.md
View file

@ -1,33 +0,0 @@
```mermaid
stateDiagram-v2
[*] --> Running
Running --> [*]: operator stopped / close socket / retain checkpoint
state Running {
state Connection {
[*] --> Connect
Connect --> Reconcile: WebSocket over Unix socket / initialize
Reconcile --> Listen: enumerate loaded threads / subscribe / read goal and latest turn
Listen --> Reconcile: poll interval or retry deadline
Reconcile --> Reconnect: connection failure
Listen --> Reconnect: connection failure
Connect --> Reconnect: connection failure
Reconnect --> Connect: capped exponential backoff with jitter
}
--
state "Per loaded thread; checkpointed across connections" as Recovery {
[*] --> Observe
Observe --> Armed: active goal and in-progress turn observed
Armed --> Backoff: same goal blocked and same turn failed with transient API error
Armed --> Observe: successful turn / reset failure count
Armed --> Observe: human interrupt / pause / clear / replacement / limit / completion / non-transient error
Backoff --> Check: persisted retry deadline reached
Check --> Observe: goal changed / turn changed / thread active or unloaded
Check --> Resume: same blocked goal / failed turn / thread idle or systemError
Resume --> Armed: goal activated and new turn observed
Resume --> Backoff: RPC failure / persist next retry
Resume --> Observe: activation observed before next turn
Backoff --> Observe: human pause / clear / replacement / limit / completion
Observe --> Observe: existing blocked goal or non-transient failure
}
}
```

142
codex-keep/intent.go Normal file
View file

@ -0,0 +1,142 @@
package main
import (
"bufio"
"encoding/json"
"errors"
"io"
"os"
"strings"
)
type intentLog struct {
Path string `json:"path"`
Pos int64 `json:"pos"`
Fence int64 `json:"fence"`
Partial bool `json:"partial,omitempty"`
Sealed bool `json:"sealed,omitempty"`
}
func openIntent(path string) (*intentLog, error) {
f, err := os.Open(path)
if err != nil {
return nil, err
}
defer func() { _ = f.Close() }()
info, err := f.Stat()
if err != nil {
return nil, err
}
log := &intentLog{Path: path, Pos: info.Size(), Fence: info.Size()}
if info.Size() != 0 {
var last [1]byte
if _, err := f.ReadAt(last[:], info.Size()-1); err != nil {
return nil, err
}
log.Partial = last[0] != '\n'
}
return log, nil
}
func (l *intentLog) end() (int64, error) {
info, err := os.Stat(l.Path)
if err != nil {
return 0, err
}
return info.Size(), nil
}
func (l *intentLog) seal() error {
l.Sealed = true
info, err := os.Stat(l.Path)
if err != nil {
return err
}
l.Fence = info.Size()
l.Sealed = false
return nil
}
func (l *intentLog) read(end int64) (goalStatus, error) {
if l.Sealed {
if err := l.seal(); err != nil {
return "", err
}
}
f, err := os.Open(l.Path)
if err != nil {
return "", err
}
defer func() { _ = f.Close() }()
reader := bufio.NewReader(io.NewSectionReader(f, l.Pos, end-l.Pos))
var latest goalStatus
for {
line, err := reader.ReadBytes('\n')
if errors.Is(err, io.EOF) {
return latest, nil
}
if err != nil {
return "", err
}
next := l.Pos + int64(len(line))
if l.Partial {
l.Partial = false
l.Pos = next
continue
}
if l.Pos < l.Fence {
l.Pos = next
continue
}
status, match, err := parseIntent(line)
if err != nil {
return "", err
}
l.Pos = next
if match {
latest = status
}
}
}
func parseIntent(line []byte) (goalStatus, bool, error) {
var record struct {
Type string `json:"type"`
Payload struct {
Type string `json:"type"`
Role string `json:"role"`
Content []struct {
Type string `json:"type"`
Text string `json:"text"`
} `json:"content"`
Meta struct {
Kinds []string `json:"content_item_kinds"`
} `json:"internal_chat_message_metadata_passthrough"`
} `json:"payload"`
}
if err := json.Unmarshal(line, &record); err != nil {
return "", false, err
}
p := record.Payload
if record.Type != "response_item" || p.Type != "message" || p.Role != "user" || len(p.Content) != 1 ||
p.Content[0].Type != "input_text" || len(p.Meta.Kinds) != 1 ||
p.Meta.Kinds[0] != "user.goal" && p.Meta.Kinds[0] != "user.goal.omitted" {
return "", false, nil
}
for _, line := range strings.Split(p.Content[0].Text, "\n") {
if line == "User cleared the goal." {
return "cleared", true, nil
}
if value, ok := strings.CutPrefix(line, "User set goal status: "); ok {
var status goalStatus
if err := json.Unmarshal([]byte(strings.TrimSuffix(value, ".")), &status); err != nil {
return "", false, err
}
switch status {
case active, paused, blocked, "complete", "budgetLimited", "usageLimited":
return status, true, nil
}
}
}
return "", true, nil
}

109
codex-keep/intent_test.go Normal file
View file

@ -0,0 +1,109 @@
package main
import (
"math"
"os"
"path/filepath"
"strings"
"testing"
)
func TestIntentProvenance(t *testing.T) {
for _, status := range []goalStatus{active, paused, "complete", "budgetLimited", "usageLimited", blocked} {
got, ok, err := parseIntent(intentLine(status))
if err != nil || !ok || got != status {
t.Fatalf("status=%s got=%s match=%v error=%v", status, got, ok, err)
}
}
line := string(intentLine(active))
for _, text := range []string{
strings.Replace(line, "user.goal", "user.input", 1),
strings.Replace(line, "\"role\":\"user\"", "\"role\":\"assistant\"", 1),
strings.Replace(line, "input_text", "output_text", 1),
} {
if _, ok, err := parseIntent([]byte(text)); err != nil || ok {
t.Fatalf("accepted untrusted instruction: match=%v error=%v", ok, err)
}
}
}
func TestIntentTail(t *testing.T) {
path := filepath.Join(t.TempDir(), "rollout.jsonl")
if err := os.WriteFile(path, intentLine(active), 0600); err != nil {
t.Fatal(err)
}
log, err := openIntent(path)
if err != nil {
t.Fatal(err)
}
if status, err := log.read(math.MaxInt64); err != nil || status != "" {
t.Fatal("replayed historical authorization")
}
data := intentLine(paused)
appendIntent(t, path, data[:len(data)/2])
if status, err := log.read(math.MaxInt64); err != nil || status != "" {
t.Fatal("accepted partial record")
}
appendIntent(t, path, data[len(data)/2:])
if status, err := log.read(math.MaxInt64); err != nil || status != paused {
t.Fatalf("partial completion: %s %v", status, err)
}
appendIntent(t, path, intentLine(active))
if err := log.seal(); err != nil {
t.Fatal(err)
}
if status, err := log.read(math.MaxInt64); err != nil || status != "" {
t.Fatal("replayed pre-cancellation authorization")
}
appendIntent(t, path, intentLine(active))
if status, err := log.read(math.MaxInt64); err != nil || status != active {
t.Fatalf("new authorization: %s %v", status, err)
}
}
func TestIntentFence(t *testing.T) {
path := filepath.Join(t.TempDir(), "rollout.jsonl")
if err := os.WriteFile(path, nil, 0600); err != nil {
t.Fatal(err)
}
log, err := openIntent(path)
if err != nil {
t.Fatal(err)
}
data := intentLine(active)
appendIntent(t, path, data[:len(data)/2])
if err := log.seal(); err != nil {
t.Fatal(err)
}
appendIntent(t, path, data[len(data)/2:])
if status, err := log.read(math.MaxInt64); err != nil || status != "" {
t.Fatalf("replayed instruction spanning cancellation: %s %v", status, err)
}
appendIntent(t, path, intentLine(active))
if status, err := log.read(math.MaxInt64); err != nil || status != active {
t.Fatalf("new instruction after cancellation: %s %v", status, err)
}
}
func TestIntentCut(t *testing.T) {
path := filepath.Join(t.TempDir(), "rollout.jsonl")
if err := os.WriteFile(path, nil, 0600); err != nil {
t.Fatal(err)
}
log, err := openIntent(path)
if err != nil {
t.Fatal(err)
}
appendIntent(t, path, intentLine(paused))
end, err := log.end()
if err != nil {
t.Fatal(err)
}
appendIntent(t, path, intentLine(active))
if status, err := log.read(end); err != nil || status != paused {
t.Fatalf("read beyond captured input: %s %v", status, err)
}
if status, err := log.read(math.MaxInt64); err != nil || status != active {
t.Fatalf("lost later input: %s %v", status, err)
}
}

1
codex-keep/model/.gitignore vendored Normal file
View file

@ -0,0 +1 @@
/states/

11
codex-keep/model/Delayed.cfg Normal file
View file

@ -0,0 +1,11 @@
SPECIFICATION Spec
CONSTANTS
Mode = "Observe"
GoalBound = 1
EditBound = 1
StampBound = 0
TurnBound = 1
FailBound = 1
INVARIANTS TypeOK ApiEvidence
PROPERTIES StopProgress
CHECK_DEADLOCK FALSE

10
codex-keep/model/GuardOld.cfg Normal file
View file

@ -0,0 +1,10 @@
SPECIFICATION Spec
CONSTANTS
Mode = "BarrierOld"
GoalBound = 1
EditBound = 1
StampBound = 0
TurnBound = 1
FailBound = 1
INVARIANTS TypeOK FreshRepair
CHECK_DEADLOCK FALSE

470
codex-keep/model/Keep.tla Normal file
View file

@ -0,0 +1,470 @@
------------------------------- MODULE Keep -------------------------------
EXTENDS Naturals, Sequences
\* Each connection serializes RPCs; one abandoned write may finish after reconnect. Epochs audit human intent only.
\* Host-authored controls form an append-only input stream; progress assumes eventual connectivity and fair finite work.
CONSTANTS Mode, GoalBound, EditBound, StampBound, TurnBound, FailBound
GoalStates == {"active", "blocked", "paused", "complete", "cleared",
"budgetLimited", "usageLimited"}
TurnStates == {"inProgress", "failed", "completed", "interrupted"}
Reads == {"pollGoal", "pollTurn", "thread", "check", "attach"}
Events == {"goal", "start", "done"}
Episodes == (1..GoalBound) \X (1..TurnBound)
StopType == [id : 0..GoalBound, status : GoalStates, epoch : 0..EditBound]
ASSUME /\ Mode \in {"Baseline", "Local", "Observe", "Unordered", "BarrierOld", "Reconcile"}
/\ GoalBound \in Nat \ {0} /\ EditBound \in Nat \ {0}
/\ StampBound \in Nat /\ TurnBound \in Nat \ {0}
/\ FailBound \in Nat \ {0}
Recon == Mode \in {"Observe", "Unordered", "BarrierOld", "Reconcile"}
Durable == Mode \in {"Unordered", "BarrierOld", "Reconcile"}
Ordered == Mode \in {"BarrierOld", "Reconcile"}
GoalType == [id : 0..GoalBound, stamp : 0..StampBound,
status : GoalStates]
TurnType == [id : 0..(TurnBound + 1), status : TurnStates, api : BOOLEAN]
LiveType == [edits : 0..EditBound, gen : 1..GoalBound, goal : GoalType, turn : TurnType]
WatchType == [cut : 0..EditBound, cursor : 0..EditBound, fence : 0..EditBound, goal : GoalType, turn : TurnType, armed : BOOLEAN,
fails : 0..FailBound, due : {"none", "waiting", "ready"},
hold : GoalStates \cup {"none"}, pending : BOOLEAN, known : BOOLEAN, echo : GoalType, seed : GoalType]
TicketType == [expired : BOOLEAN, status : GoalStates]
MsgType == [kind : Events \cup Reads \cup {"set"}, goal : GoalType,
turn : TurnType, truth : 0..EditBound, busy : BOOLEAN, ok : BOOLEAN]
ActType == [sent : BOOLEAN, view : [goal : 0..GoalBound, turn : 0..(TurnBound + 1)], expected : TicketType,
origin : {"user", "automatic"}, evidence : BOOLEAN, recover : BOOLEAN]
VARIABLES late, inputs, sample, attached, live, w, wire, online, phase, req, invalid,
ticket, lastAct, known, need, resumed, cancelled, stopWant, stopNeed
vars == <<late, inputs, sample, attached, live, w, wire, online, phase, req, invalid,
ticket, lastAct, known, need, resumed, cancelled, stopWant, stopNeed>>
EmptyGoal == [id |-> 0, stamp |-> 0, status |-> "cleared"]
Message(kind, state, ok) ==
[kind |-> kind, goal |-> state.goal, turn |-> state.turn,
truth |-> state.edits, busy |-> state.turn.status = "inProgress", ok |-> ok]
Stop(x) == [x EXCEPT !.armed = FALSE, !.due = "none"]
Increment(x) == [x EXCEPT !.fails = IF @ < FailBound THEN @ + 1 ELSE @]
Eligible(x) == x.armed /\ x.goal.id # 0 /\ x.goal.status = "blocked"
/\ x.turn.status = "failed" /\ x.turn.api
Schedule(x) == IF Eligible(x) /\ x.due = "none"
THEN [Increment(x) EXCEPT !.due = "waiting"] ELSE x
KnownAfter(g) == IF g.id # 0 /\ g.status = "active" THEN known \cup {g.id} ELSE known
BaseGoal(x, g) ==
LET same == g.id # 0 /\ x.goal.id = g.id
cancel == ~same \/ g.status \notin {"active", "blocked"}
\/ (g.status = "active" /\ x.goal.status # "active")
\/ (g.status = "blocked" /\ x.due # "none"
/\ x.goal.stamp # g.stamp)
base == [x EXCEPT !.goal = g, !.fails = IF same THEN @ ELSE 0,
!.armed = @ /\ ~cancel, !.due = IF cancel THEN "none" ELSE @]
IN IF g.status = "active" /\ x.turn.status = "inProgress"
THEN [base EXCEPT !.armed = TRUE] ELSE base
GoalUpdate(x, g, fresh) ==
IF ~Recon THEN BaseGoal(x, g) ELSE
IF ~fresh /\ g.status = "active" /\ x.hold = "none" /\ g.id = x.goal.id THEN x ELSE
LET same == g.id # 0 /\ g.id = x.goal.id
holding == x.hold # "none" /\ same
stopped == g.id # 0 /\ g.status \notin {"active", "blocked"}
base == IF ~same THEN [Stop(x) EXCEPT !.fails = 0, !.hold = "none", !.known = FALSE] ELSE x
active == g.id # 0 /\ g.status = "active"
transition == active /\ (~same \/ x.goal.status # "active")
updated == [base EXCEPT !.goal = g, !.known = @ \/ active,
!.armed = IF active THEN @ \/ transition ELSE IF stopped \/ g.id = 0 THEN FALSE ELSE @,
!.due = IF transition \/ stopped \/ g.id = 0 THEN "none" ELSE @,
!.hold = IF (stopped /\ (Durable \/ x.pending))
\/ (~same /\ g.status = "blocked" /\ x.pending) THEN g.status ELSE @]
IN IF holding
THEN IF ~fresh THEN IF g.status \in {"active", "blocked"} THEN x ELSE [Stop(x) EXCEPT !.goal = g, !.hold = g.status]
ELSE IF g.status = x.hold /\ x.echo.id = 0
THEN [Stop(x) EXCEPT !.goal = g, !.hold = IF Durable /\ g.status # "active" THEN @ ELSE "none",
!.armed = g.status = "active",
!.known = @ \/ g.status = "active"] ELSE x
ELSE updated
TurnUpdate(x, t) ==
LET fresh == t.id # x.turn.id
base == [x EXCEPT !.turn = t,
!.armed = IF fresh /\ ~Recon THEN FALSE ELSE @,
!.due = IF fresh THEN "none" ELSE @]
started == [base EXCEPT !.armed = (Recon /\ x.armed)
\/ (t.status = "inProgress" /\ x.goal.id # 0 /\ x.goal.status = "active")]
terminal == t.status = "interrupted"
\/ (t.status = "failed" /\ ~t.api)
\/ (t.status = "completed" /\ ~Recon)
settled == IF terminal THEN Stop(base) ELSE base
result == IF fresh /\ t.status = "inProgress" THEN started ELSE
IF Recon /\ (fresh \/ x.turn.status = "inProgress") /\ t.status = "failed" /\ t.api
/\ x.known /\ x.hold = "none"
THEN [settled EXCEPT !.armed = TRUE] ELSE settled
held == IF Recon /\ t.status = "interrupted" /\ x.goal.id # 0 /\ x.pending
THEN [Stop(result) EXCEPT !.goal.status = "paused", !.hold = "paused"]
ELSE IF x.hold # "none" THEN Stop(result) ELSE result
IN IF t.status = "completed" /\ (Mode # "Baseline" \/ ~fresh)
THEN [held EXCEPT !.fails = 0, !.due = "none"] ELSE held
ApplyInput(x, status) ==
IF status = "cleared" THEN [Stop(x) EXCEPT !.hold = "none", !.known = FALSE] ELSE
IF x.goal.id = 0 THEN x ELSE
IF status = "active" /\ x.goal.status \in {"active", "blocked"}
THEN [x EXCEPT !.hold = "none", !.known = TRUE, !.armed = TRUE, !.due = "none"]
ELSE [Stop(x) EXCEPT !.goal.status = status, !.hold = status, !.known = status = "active"]
InputEnd(x) == IF Ordered THEN x.cut ELSE Len(inputs)
NewInput(x) == Recon /\ InputEnd(x) > x.cursor /\ InputEnd(x) > x.fence
SyncInput(x) ==
IF ~Recon THEN x ELSE
LET updated == IF NewInput(x) THEN ApplyInput(x, inputs[InputEnd(x)]) ELSE x
IN [updated EXCEPT !.cursor = InputEnd(x)]
Init ==
/\ late = "none"
/\ inputs = <<>>
/\ attached = TRUE
/\ live = [edits |-> 0, gen |-> 1,
goal |-> [id |-> 1, stamp |-> 0,
status |-> "active"],
turn |-> [id |-> 1, status |-> "inProgress", api |-> FALSE]]
/\ sample = live.goal
/\ w = [cut |-> 0, cursor |-> 0, fence |-> 0, goal |-> live.goal, turn |-> live.turn,
armed |-> TRUE, fails |-> 0, due |-> "none", hold |-> "none", pending |-> FALSE, known |-> TRUE, echo |-> EmptyGoal, seed |-> EmptyGoal]
/\ wire = <<>> /\ online = TRUE /\ phase = "idle" /\ req = "none"
/\ invalid = FALSE
/\ ticket = [expired |-> FALSE, status |-> "active"]
/\ lastAct = [sent |-> FALSE, view |-> [goal |-> w.goal.id, turn |-> w.turn.id], expected |-> ticket,
origin |-> "automatic", evidence |-> TRUE, recover |-> TRUE]
/\ known = {1} /\ need = {} /\ resumed = {} /\ cancelled = {}
/\ stopWant = [id |-> 0, status |-> "paused", epoch |-> 0] /\ stopNeed = FALSE
CancelGoal(id) == {e \in Episodes : e[1] = id}
FutureGoal(id) == {e \in Episodes : e[1] = id /\
(e[2] > live.turn.id \/ (e[2] = live.turn.id /\ live.turn.status = "inProgress"))}
IntentChange(status, stamp) ==
/\ live.goal.id # 0 /\ live.edits < EditBound
/\ LET g == [live.goal EXCEPT !.stamp = stamp,
!.id = IF status = "cleared" THEN 0 ELSE @,
!.status = status]
state == [live EXCEPT !.goal = g, !.edits = @ + 1]
IN /\ live' = state
/\ wire' = IF online THEN Append(wire, Message("goal", state, TRUE)) ELSE wire
/\ inputs' = Append(inputs, status)
/\ cancelled' = IF status = "active" THEN cancelled \ FutureGoal(live.goal.id)
ELSE cancelled \cup CancelGoal(live.goal.id)
/\ stopNeed' = FALSE
/\ UNCHANGED <<late, sample, attached, w, online, phase, req, invalid,
ticket, lastAct, known, need, resumed, stopWant>>
ReplaceGoal(stamp) ==
/\ live.gen < GoalBound /\ live.edits < EditBound
/\ LET g == [id |-> live.gen + 1, stamp |-> stamp, status |-> "active"]
state == [live EXCEPT !.goal = g, !.gen = @ + 1, !.edits = @ + 1]
IN /\ live' = state
/\ wire' = IF online THEN Append(wire, Message("goal", state, TRUE)) ELSE wire
/\ inputs' = Append(inputs, "active")
/\ cancelled' = cancelled \cup CancelGoal(live.goal.id)
/\ stopNeed' = FALSE
/\ UNCHANGED <<late, sample, attached, w, online, phase, req, invalid,
ticket, lastAct, known, need, resumed, stopWant>>
StartTurn ==
/\ live.goal.id # 0 /\ live.goal.status = "active"
/\ live.turn.status # "inProgress" /\ live.turn.id <= TurnBound
/\ LET state == [live EXCEPT !.turn = [id |-> @.id + 1,
status |-> "inProgress", api |-> FALSE]]
IN /\ live' = state
/\ wire' = IF online THEN Append(wire, Message("start", state, TRUE)) ELSE wire
/\ resumed' = resumed \cup {e \in need : e[1] = live.goal.id /\ e[2] <= live.turn.id}
/\ UNCHANGED <<late, inputs, sample, attached, w, online, phase, req, invalid,
ticket, lastAct, known, need, cancelled, stopWant, stopNeed>>
FinishTurn(status) ==
/\ live.turn.status = "inProgress"
/\ LET state == [live EXCEPT !.turn.status = status, !.turn.api = FALSE]
IN /\ live' = state
/\ wire' = IF online THEN Append(wire, Message("done", state, TRUE)) ELSE wire
/\ cancelled' = IF status = "interrupted" THEN cancelled \cup CancelGoal(live.goal.id) ELSE cancelled
/\ UNCHANGED <<late, inputs, sample, attached, w, online, phase, req, invalid,
ticket, lastAct, known, need, resumed, stopWant, stopNeed>>
FailTurn(isApi, stamp) ==
/\ live.turn.status = "inProgress" /\ live.turn.id <= TurnBound
/\ LET g == IF live.goal.status = "active"
THEN [live.goal EXCEPT !.status = "blocked",
!.stamp = stamp]
ELSE live.goal
state == [live EXCEPT !.goal = g, !.turn.status = "failed", !.turn.api = isApi]
events == IF live.goal.status = "active"
THEN Append(wire, Message("goal", state, TRUE)) ELSE wire
IN /\ live' = state
/\ wire' = IF online THEN Append(events, Message("done", state, TRUE)) ELSE wire
/\ need' = IF isApi /\ live.goal.status = "active" /\ live.goal.id \in known
THEN need \cup {<<live.goal.id, live.turn.id>>} ELSE need
/\ UNCHANGED <<late, inputs, sample, attached, w, online, phase, req, invalid,
ticket, lastAct, known, resumed, cancelled, stopWant, stopNeed>>
StampUpdate(stamp) ==
/\ live.goal.id # 0 /\ stamp > live.goal.stamp
/\ LET state == [live EXCEPT !.goal.stamp = stamp]
IN /\ live' = state
/\ wire' = IF online THEN Append(wire, Message("goal", state, TRUE)) ELSE wire
/\ UNCHANGED <<late, inputs, sample, attached, w, online, phase, req, invalid, ticket, lastAct,
known, need, resumed, cancelled, stopWant, stopNeed>>
Poll ==
/\ online /\ phase = "idle" /\ req = "none"
/\ phase' = "pollGoal" /\ req' = "pollGoal" /\ invalid' = FALSE
/\ UNCHANGED <<late, inputs, sample, attached, live, w, wire, online, ticket, lastAct,
known, need, resumed, cancelled, stopWant, stopNeed>>
ServeRead ==
/\ req \in Reads
/\ wire' = IF ~online THEN wire ELSE
IF req = "attach" THEN Append(Append(wire, Message(req, live, TRUE)), Message("goal", live, TRUE))
ELSE Append(wire, Message(req, live, TRUE))
/\ req' = "none"
/\ UNCHANGED <<late, inputs, sample, attached, live, w, online, phase, invalid, ticket, lastAct,
known, need, resumed, cancelled, stopWant, stopNeed>>
ReadWatch(m) ==
IF invalid /\ ~(Mode = "BarrierOld" /\ m.kind = "attach")
THEN IF Ordered /\ m.kind = "attach"
THEN [w EXCEPT !.seed = [id |-> 1, stamp |-> 0, status |-> "active"]] ELSE w
ELSE
CASE m.kind = "pollGoal" ->
LET updated == GoalUpdate(w, m.goal, TRUE)
base == IF Recon THEN [updated EXCEPT !.pending = FALSE] ELSE updated
ready == IF Recon /\ base.hold = m.goal.status /\ base.echo.id = 0
/\ (~Durable \/ m.goal.status = "active")
THEN [base EXCEPT !.hold = "none", !.armed = m.goal.status = "active"] ELSE base
IN IF Recon /\ ~attached /\ m.goal.id # 0
THEN [ready EXCEPT !.seed = IF Ordered THEN EmptyGoal ELSE m.goal, !.echo = EmptyGoal] ELSE ready
[] m.kind = "attach" -> IF Ordered THEN [w EXCEPT !.seed = [id |-> 1, stamp |-> 0, status |-> "active"]] ELSE w
[] m.kind = "pollTurn" -> Schedule(TurnUpdate(w, m.turn))
[] m.kind = "thread" -> IF ~m.busy THEN w ELSE
IF Recon THEN [w EXCEPT !.due = "none",
!.turn = [id |-> 0, status |-> "inProgress", api |-> FALSE]] ELSE Stop(w)
[] OTHER -> LET updated == GoalUpdate(w, m.goal, TRUE)
IN IF Eligible(updated)
THEN [updated EXCEPT !.due = "waiting"] ELSE updated
ReadPhase(m, updated) ==
IF invalid /\ ~(Mode = "BarrierOld" /\ m.kind = "attach") THEN "idle" ELSE
CASE m.kind = "pollGoal" -> IF m.goal.id = 0 THEN "idle" ELSE IF ~attached \/ Ordered THEN "attach" ELSE IF Recon THEN "inputs" ELSE "pollTurn"
[] m.kind = "attach" -> IF Recon THEN "inputs" ELSE "pollTurn"
[] m.kind = "pollTurn" -> IF Eligible(updated) /\ updated.due = "ready" /\ updated.echo.id = 0 /\ updated.seed.id = 0
THEN "thread" ELSE "idle"
[] m.kind = "thread" -> IF m.busy THEN "idle" ELSE "check"
[] OTHER -> IF Eligible(updated) THEN "send" ELSE "idle"
ReceiveRead ==
/\ online /\ Len(wire) > 0 /\ Head(wire).kind \in Reads
/\ phase = Head(wire).kind
/\ LET m == Head(wire)
updated == ReadWatch(m)
next == ReadPhase(m, updated)
IN /\ w' = [updated EXCEPT !.cut = IF Ordered /\ m.kind = "pollGoal" /\ next = "attach" THEN Len(inputs) ELSE @]
/\ phase' = next
/\ req' = IF next \in Reads THEN next ELSE "none"
/\ ticket' = IF next = "send"
THEN [expired |-> w.due = "ready", status |-> "active"]
ELSE ticket
/\ known' = IF ~invalid /\ m.kind \in {"pollGoal", "check"}
THEN KnownAfter(m.goal) ELSE known
/\ sample' = IF Head(wire).kind = "pollGoal" /\ ~invalid THEN Head(wire).goal ELSE sample
/\ invalid' = IF Mode = "BarrierOld" /\ Head(wire).kind = "attach" THEN invalid ELSE FALSE
/\ wire' = Tail(wire)
/\ attached' = (attached \/ Head(wire).kind = "attach")
/\ LET m == Head(wire)
stopped == ~invalid /\ m.kind = "pollGoal" /\ m.goal.id # 0
/\ m.goal.status \notin {"active", "blocked"}
/\ (ReadWatch(m)).goal.status = m.goal.status
IN /\ stopWant' = IF stopped THEN [id |-> m.goal.id, status |-> m.goal.status, epoch |-> m.truth] ELSE stopWant
/\ stopNeed' = (stopNeed \/ stopped)
/\ UNCHANGED <<late, inputs, live, online, lastAct, need, resumed, cancelled>>
ReadInput ==
/\ online /\ phase = "inputs" /\ req = "none"
/\ LET updated == SyncInput(w)
blocked == updated.hold = "active" /\ sample.status = "blocked"
ready == IF blocked THEN [updated EXCEPT !.hold = "none", !.goal = sample,
!.known = TRUE, !.armed = TRUE] ELSE updated
repair == ready.hold # "none" /\ ready.hold # sample.status
IN /\ invalid' = (Mode = "BarrierOld" /\ invalid /\ repair)
/\ w' = ready
/\ phase' = IF repair
THEN IF ready.echo.id = 0 /\ (Ordered \/ ready.seed.id = 0) THEN "repair" ELSE "idle"
ELSE "pollTurn"
/\ req' = IF ~repair THEN "pollTurn" ELSE "none"
/\ sample' = IF Ordered THEN EmptyGoal ELSE sample
/\ stopNeed' = IF NewInput(w) THEN FALSE ELSE stopNeed
/\ UNCHANGED <<late, inputs, attached, live, wire, online, ticket, lastAct,
known, need, resumed, cancelled, stopWant>>
ReceiveEvent ==
/\ online /\ phase \notin {"send", "repair", "inputs"} /\ Len(wire) > 0 /\ Head(wire).kind \in Events
/\ LET m == Head(wire)
seed == Recon /\ m.kind = "goal" /\ w.seed.id # 0
snapshot == seed /\ (Ordered \/ (m.goal.id = w.seed.id /\ m.goal.status = w.seed.status /\ m.goal.stamp = w.seed.stamp))
echo == Recon /\ m.kind = "goal" /\ w.echo.id # 0
/\ m.goal.id = w.echo.id /\ m.goal.status = w.echo.status /\ m.goal.stamp = w.echo.stamp
ignore == snapshot \/ echo \/ (m.kind = "done" /\ m.turn.id # w.turn.id)
seal == ~ignore /\ ((~Ordered /\ m.kind = "goal" /\ m.goal.status \notin {"active", "blocked"})
\/ (m.kind = "done" /\ m.turn.status = "interrupted"))
base == IF seal /\ Recon THEN [w EXCEPT !.fence = Len(inputs)]
ELSE IF Ordered \/ (ignore /\ ~echo /\ ~snapshot) THEN w ELSE SyncInput(w)
updated == IF ignore THEN w ELSE
IF m.kind = "goal" THEN GoalUpdate(base, m.goal, FALSE)
ELSE TurnUpdate(base, m.turn)
IN /\ w' = [IF echo THEN [base EXCEPT !.echo = EmptyGoal] ELSE IF snapshot THEN base
ELSE IF ignore THEN w ELSE Schedule(updated)
EXCEPT !.seed = IF seed THEN EmptyGoal ELSE @]
/\ known' = IF m.kind = "goal" THEN KnownAfter(m.goal) ELSE known
/\ stopWant' = IF ~echo /\ ~snapshot /\ m.kind = "goal" /\ m.goal.id # 0 /\ m.goal.status \notin {"active", "blocked"}
THEN [id |-> m.goal.id, status |-> m.goal.status, epoch |-> m.truth]
ELSE IF ~ignore /\ m.kind = "done" /\ m.turn.status = "interrupted" /\ w.goal.id # 0 /\ w.pending
THEN [id |-> w.goal.id, status |-> "paused", epoch |-> m.truth] ELSE stopWant
/\ stopNeed' = ((stopNeed /\ ~(~seal /\ NewInput(w)))
\/ (~echo /\ ~snapshot /\ m.kind = "goal" /\ m.goal.id # 0 /\ m.goal.status \notin {"active", "blocked"})
\/ (~ignore /\ m.kind = "done" /\ m.turn.status = "interrupted" /\ w.goal.id # 0 /\ w.pending))
/\ invalid' = (invalid \/ ((~ignore \/ (~Ordered /\ (echo \/ snapshot) /\ NewInput(w))) /\ phase # "idle"))
/\ wire' = Tail(wire)
/\ UNCHANGED <<late, inputs, sample, attached, live, online, phase, req,
ticket, lastAct, need, resumed, cancelled>>
SendSet ==
/\ online /\ phase \in {"send", "repair"} /\ req = "none" /\ w.echo.id = 0 /\ (Ordered \/ w.seed.id = 0)
/\ IF phase = "send" THEN Eligible(w) ELSE w.hold # "none"
/\ phase' = "set" /\ req' = "set" /\ invalid' = FALSE /\ w' = [w EXCEPT !.pending = TRUE]
/\ ticket' = IF phase = "repair"
THEN [expired |-> FALSE, status |-> w.hold] ELSE ticket
/\ lastAct' = [sent |-> TRUE, view |-> [goal |-> w.goal.id, turn |-> w.turn.id],
expected |-> IF phase = "send" THEN ticket ELSE [ticket EXCEPT !.status = w.hold],
origin |-> IF Mode = "Baseline" THEN "user" ELSE "automatic",
evidence |-> Eligible(w), recover |-> phase = "send"]
/\ UNCHANGED <<late, inputs, sample, attached, live, wire, online, known, need, resumed, cancelled, stopWant, stopNeed>>
ServeSet(stamp) ==
/\ req = "set"
/\ LET allowed == live.goal.id # 0
state == IF allowed THEN [live EXCEPT !.goal.status = ticket.status,
!.goal.stamp = stamp] ELSE live
replies == Append(wire, Message("set", state, allowed))
IN /\ live' = state
/\ wire' = IF online
THEN IF allowed THEN Append(replies, Message("goal", state, TRUE))
ELSE replies
ELSE wire
/\ req' = "none"
/\ UNCHANGED <<late, inputs, sample, attached, w, online, phase, invalid, ticket, lastAct, known, need, resumed, cancelled, stopWant, stopNeed>>
ReceiveSet ==
/\ online /\ phase = "set" /\ Len(wire) > 0 /\ Head(wire).kind = "set"
/\ LET m == Head(wire)
base == [w EXCEPT !.pending = FALSE, !.echo = IF m.ok /\ Recon THEN m.goal ELSE @]
IN /\ w' = IF m.ok
THEN IF invalid THEN base ELSE GoalUpdate(base, m.goal, TRUE)
ELSE IF Mode = "Baseline" \/ (~invalid /\ Eligible(w))
THEN Increment(base) ELSE base
/\ known' = IF m.ok /\ ~invalid THEN KnownAfter(m.goal) ELSE known
/\ phase' = "idle" /\ invalid' = FALSE /\ wire' = Tail(wire)
/\ UNCHANGED <<late, inputs, sample, attached, live, online, req, ticket, lastAct, need, resumed, cancelled, stopWant, stopNeed>>
Receive == ReceiveEvent \/ ReceiveRead \/ ReceiveSet
Clock ==
/\ w.due = "waiting"
/\ w' = [w EXCEPT !.due = "ready"]
/\ UNCHANGED <<late, inputs, sample, attached, live, wire, online, phase, req, invalid,
ticket, lastAct, known, need, resumed, cancelled, stopWant, stopNeed>>
Disconnect ==
/\ online /\ (req # "set" \/ late = "none") /\ online' = FALSE /\ attached' = FALSE /\ wire' = <<>> /\ phase' = "idle"
/\ req' = "none"
/\ late' = IF req = "set" THEN ticket.status ELSE late
/\ invalid' = FALSE
/\ w' = [IF phase = "set" /\ (Mode = "Baseline" \/ (~invalid /\ Eligible(w)))
THEN Increment(w) ELSE w EXCEPT !.echo = EmptyGoal, !.seed = EmptyGoal]
/\ UNCHANGED <<inputs, sample, live, ticket, lastAct, known, need, resumed, cancelled, stopWant, stopNeed>>
ServeLate(stamp) ==
/\ late # "none"
/\ LET state == IF live.goal.id # 0 THEN [live EXCEPT !.goal.status = late,
!.goal.stamp = stamp] ELSE live
IN /\ live' = state
/\ wire' = IF online /\ attached /\ live.goal.id # 0 THEN Append(wire, Message("goal", state, TRUE)) ELSE wire
/\ late' = "none"
/\ UNCHANGED <<inputs, sample, attached, w, online, phase, req, invalid,
ticket, lastAct, known, need, resumed, cancelled, stopWant, stopNeed>>
Reconnect ==
/\ ~online /\ online' = TRUE
/\ UNCHANGED <<late, inputs, sample, attached, live, w, wire, phase, req, invalid,
ticket, lastAct, known, need, resumed, cancelled, stopWant, stopNeed>>
HonourStop ==
/\ stopNeed /\ req # "set"
/\ (live.goal.id # stopWant.id \/ live.edits > stopWant.epoch)
/\ stopNeed' = FALSE
/\ UNCHANGED <<late, inputs, sample, attached, live, w, wire, online, phase, req, invalid,
ticket, lastAct, known, need, resumed, cancelled, stopWant>>
Next ==
\/ \E status \in GoalStates, stamp \in live.goal.stamp..StampBound : IntentChange(status, stamp)
\/ \E stamp \in live.goal.stamp..StampBound : ReplaceGoal(stamp)
\/ StartTurn
\/ \E status \in {"completed", "interrupted"} : FinishTurn(status)
\/ \E isApi \in BOOLEAN, stamp \in live.goal.stamp..StampBound : FailTurn(isApi, stamp)
\/ Poll \/ ServeRead \/ Receive \/ SendSet \/ ReadInput
\/ \E stamp \in live.goal.stamp..StampBound : ServeSet(stamp)
\/ (\E stamp \in live.goal.stamp..StampBound : ServeLate(stamp))
\/ Clock \/ Disconnect \/ Reconnect \/ HonourStop
\/ \E stamp \in (live.goal.stamp + 1)..StampBound : StampUpdate(stamp)
TypeOK ==
/\ late \in GoalStates \cup {"none"}
/\ inputs \in Seq(GoalStates) /\ Len(inputs) <= EditBound /\ sample \in GoalType
/\ attached \in BOOLEAN
/\ live \in LiveType /\ w \in WatchType /\ wire \in Seq(MsgType)
/\ online \in BOOLEAN /\ invalid \in BOOLEAN
/\ phase \in {"idle", "send", "repair", "set", "inputs"} \cup Reads
/\ req \in {"none", "set"} \cup Reads
/\ ticket \in TicketType /\ lastAct \in ActType
/\ known \subseteq 1..GoalBound
/\ need \subseteq Episodes /\ resumed \subseteq Episodes /\ cancelled \subseteq Episodes
/\ stopWant \in StopType /\ stopNeed \in BOOLEAN
FreshRepair == phase # "repair" \/ ~invalid
ApiEvidence == ~lastAct.sent \/ ~lastAct.recover \/ lastAct.evidence
AutoProvenance == ~lastAct.sent \/ lastAct.origin = "automatic"
SuccessReset == w.turn.status # "completed" \/ w.fails = 0
NoEarlyResume == ~lastAct.sent \/ ~lastAct.recover \/ lastAct.expected.expired
StopCancels == w.hold = "none" \/ (~w.armed /\ w.due = "none")
HumanStops == (w.goal.status \notin {"active", "blocked"} \/ w.turn.status = "interrupted")
=> (~Eligible(w) /\ w.due = "none")
StopWins == <>[](~stopNeed \/ live.goal.id # stopWant.id
\/ live.edits > stopWant.epoch \/ live.goal.status = stopWant.status)
EventuallyResume == \A e \in Episodes :
(e \in need) ~> (e \in resumed \cup cancelled)
RecoveryProgress == (<>[]online) => EventuallyResume
StopProgress == (<>[]online) => StopWins
HoldProgress == (<>[]online) => (w.hold # "none" ~> (w.hold = "none" \/ live.goal.id # w.goal.id \/ live.goal.status = w.hold))
FairLate == \E stamp \in live.goal.stamp..StampBound : ServeLate(stamp)
FairSet == \E stamp \in live.goal.stamp..StampBound : ServeSet(stamp)
Fairness == WF_vars(Poll) /\ WF_vars(ServeRead) /\ WF_vars(Receive)
/\ WF_vars(SendSet) /\ WF_vars(FairSet) /\ WF_vars(Clock) /\ WF_vars(StartTurn)
/\ WF_vars(FairLate) /\ WF_vars(HonourStop) /\ WF_vars(ReadInput)
Spec == Init /\ [][Next]_vars /\ Fairness
=============================================================================

11
codex-keep/model/LocalProgress.cfg Normal file
View file

@ -0,0 +1,11 @@
SPECIFICATION Spec
CONSTANTS
Mode = "Local"
GoalBound = 1
EditBound = 1
StampBound = 0
TurnBound = 2
FailBound = 1
INVARIANTS TypeOK AutoProvenance SuccessReset ApiEvidence NoEarlyResume
PROPERTIES RecoveryProgress
CHECK_DEADLOCK FALSE

11
codex-keep/model/LocalStamp.cfg Normal file
View file

@ -0,0 +1,11 @@
SPECIFICATION Spec
CONSTANTS
Mode = "Local"
GoalBound = 1
EditBound = 1
StampBound = 1
TurnBound = 1
FailBound = 1
INVARIANTS TypeOK AutoProvenance SuccessReset ApiEvidence NoEarlyResume
PROPERTIES RecoveryProgress
CHECK_DEADLOCK FALSE

11
codex-keep/model/LocalStop.cfg Normal file
View file

@ -0,0 +1,11 @@
SPECIFICATION Spec
CONSTANTS
Mode = "Local"
GoalBound = 1
EditBound = 1
StampBound = 0
TurnBound = 1
FailBound = 1
INVARIANTS TypeOK AutoProvenance SuccessReset ApiEvidence NoEarlyResume
PROPERTIES StopProgress
CHECK_DEADLOCK FALSE

10
codex-keep/model/Origin.cfg Normal file
View file

@ -0,0 +1,10 @@
SPECIFICATION Spec
CONSTANTS
Mode = "Baseline"
GoalBound = 1
EditBound = 1
StampBound = 0
TurnBound = 1
FailBound = 1
INVARIANTS TypeOK AutoProvenance
CHECK_DEADLOCK FALSE

11
codex-keep/model/Overlap.cfg Normal file
View file

@ -0,0 +1,11 @@
SPECIFICATION Spec
CONSTANTS
Mode = "Reconcile"
GoalBound = 1
EditBound = 2
StampBound = 0
TurnBound = 1
FailBound = 1
INVARIANTS TypeOK FreshRepair AutoProvenance SuccessReset ApiEvidence NoEarlyResume StopCancels HumanStops
PROPERTIES RecoveryProgress StopProgress HoldProgress
CHECK_DEADLOCK FALSE

11
codex-keep/model/Progress.cfg Normal file
View file

@ -0,0 +1,11 @@
SPECIFICATION Spec
CONSTANTS
Mode = "Baseline"
GoalBound = 1
EditBound = 1
StampBound = 0
TurnBound = 2
FailBound = 1
INVARIANTS TypeOK ApiEvidence
PROPERTIES RecoveryProgress
CHECK_DEADLOCK FALSE

11
codex-keep/model/Queue.cfg Normal file
View file

@ -0,0 +1,11 @@
SPECIFICATION QueueSpec
CONSTANTS
Mode = "Reconcile"
GoalBound = 1
EditBound = 2
StampBound = 0
TurnBound = 1
FailBound = 1
INVARIANTS TypeOK FreshRepair AutoProvenance SuccessReset ApiEvidence NoEarlyResume StopCancels HumanStops
PROPERTIES QueueProgress
CHECK_DEADLOCK FALSE

26
codex-keep/model/Queue.tla Normal file
View file

@ -0,0 +1,26 @@
------------------------------- MODULE Queue -------------------------------
EXTENDS Keep
QueueInit ==
/\ late = "none"
/\ inputs = <<"paused", "active">>
/\ attached = TRUE
/\ live = [edits |-> 2, gen |-> 1,
goal |-> [id |-> 1, stamp |-> 0,
status |-> "active"],
turn |-> [id |-> 1, status |-> "inProgress", api |-> FALSE]]
/\ sample = live.goal
/\ w = [cut |-> 0, cursor |-> 0, fence |-> 0, goal |-> live.goal, turn |-> live.turn,
armed |-> TRUE, fails |-> 0, due |-> "none", hold |-> "none", pending |-> FALSE, known |-> TRUE, echo |-> EmptyGoal, seed |-> EmptyGoal]
/\ wire = <<Message("goal", [live EXCEPT !.goal.status = "paused", !.edits = 1], TRUE), Message("goal", live, TRUE)>> /\ online = TRUE /\ phase = "idle" /\ req = "none"
/\ invalid = FALSE
/\ ticket = [expired |-> FALSE, status |-> "active"]
/\ lastAct = [sent |-> FALSE, view |-> [goal |-> w.goal.id, turn |-> w.turn.id], expected |-> ticket,
origin |-> "automatic", evidence |-> TRUE, recover |-> TRUE]
/\ known = {1} /\ need = {} /\ resumed = {} /\ cancelled = {}
/\ stopWant = [id |-> 0, status |-> "paused", epoch |-> 0] /\ stopNeed = FALSE
QueueNext == Next /\ ~FinishTurn("interrupted")
QueueSpec == QueueInit /\ [][QueueNext]_vars /\ Fairness
QueueProgress == (<>[]online) => (<>[](live.goal.status # "paused"))
=============================================================================

11
codex-keep/model/QueueOld.cfg Normal file
View file

@ -0,0 +1,11 @@
SPECIFICATION QueueSpec
CONSTANTS
Mode = "Unordered"
GoalBound = 1
EditBound = 2
StampBound = 0
TurnBound = 1
FailBound = 1
INVARIANTS TypeOK AutoProvenance SuccessReset ApiEvidence NoEarlyResume StopCancels HumanStops
PROPERTIES QueueProgress
CHECK_DEADLOCK FALSE

7
codex-keep/model/Reach.tla Normal file
View file

@ -0,0 +1,7 @@
------------------------------- MODULE Reach -------------------------------
EXTENDS Keep
NoRecovery == ~(lastAct.sent /\ lastAct.recover /\
<<lastAct.view.goal, lastAct.view.turn>> \in (resumed \ cancelled))
NoRestore == ~(lastAct.sent /\ ~lastAct.recover /\ lastAct.expected.status = "paused"
/\ live.goal.status = "paused" /\ w.hold = "paused" /\ ~w.pending /\ w.echo.id = 0)
=============================================================================

10
codex-keep/model/ReachStop.cfg Normal file
View file

@ -0,0 +1,10 @@
SPECIFICATION Spec
CONSTANTS
Mode = "Reconcile"
GoalBound = 1
EditBound = 1
StampBound = 0
TurnBound = 1
FailBound = 1
INVARIANTS TypeOK FreshRepair NoRestore
CHECK_DEADLOCK FALSE

10
codex-keep/model/ReachWork.cfg Normal file
View file

@ -0,0 +1,10 @@
SPECIFICATION Spec
CONSTANTS
Mode = "Reconcile"
GoalBound = 1
EditBound = 1
StampBound = 0
TurnBound = 1
FailBound = 1
INVARIANTS TypeOK FreshRepair NoRecovery
CHECK_DEADLOCK FALSE

Some files were not shown because too many files have changed in this diff Show more