TITLE:
Independent Alloy review request — ChronoRealm Assurance Protocol v1.2 state-transition model
BODY:
Daniel Jackson recommended that I post this here. I’m seeking adversarial review of this bounded relational/state-transition model. Counterexamples, modeling errors, vacuous assertions, omitted/spurious transitions, and abstraction objections are all useful outcomes. I am not seeking endorsement.
module ChronoRealmAssuranceV12_AlloyReview
/*
CHRONOREALM ASSURANCE PROTOCOL v1.2
PUBLIC-ONLY ALLOY REVIEW MODEL
Prepared 2026-08-11 for independent adversarial review.
PURPOSE
-------
This is a candidate relational/trace translation of the public finite TLA+
semantic abstraction ChronoRealmAssuranceV12.tla. It is NOT a proof that the
TLA+ abstraction faithfully represents the whole v1.2 protocol.
Please try to find:
- source/model mismatches;
- impossible or spurious state combinations;
- omitted transitions;
- branch-isolation failures;
- replay failures;
- dispute/freeze/recovery inconsistencies;
- canonical/supersession defects;
- vacuous or too-weak assertions;
- two distinct source states that collapse to one abstract state but permit
different future behavior relevant to a safety property.
A counterexample is a useful result.
BOUNDARY
--------
This code models the bounded semantic slice only. It does not model
cryptographic identity, external truth of evidence, denial-of-service
resistance, legal authorization, or any physical/metaphysical claim.
TRANSLATION NOTE
----------------
The source TLA+ model reduces richer source concepts to small finite domains.
This Alloy model preserves that same finite-review posture and adds only a
`step` field as trace instrumentation so an Alloy assertion can distinguish an
actual transition from a later AdvanceTime step that preserves the source
model's last-audit fields.
IMPORTANT: AddResidualNeverWas below is translated LITERALLY from the supplied
TLA+ source, including its use of residualActual. Reviewers are specifically
invited to challenge whether that source behavior is intended or a defect.
*/
open util/ordering[State]
abstract sig Bool {}
one sig BTrue, BFalse extends Bool {}
abstract sig Val {}
one sig Val0, Val1, Val2 extends Val {}
abstract sig Authority {}
one sig AuthA, AuthB extends Authority {}
abstract sig Version {}
one sig Ver0, Ver1, Ver2, Ver3 extends Version {}
abstract sig DStatus {}
one sig DNone, DOpen, DFrozen, DReview, DResolved, DDismissed extends DStatus {}
abstract sig Hash {}
one sig H1, H2 extends Hash {}
abstract sig Code {}
one sig CodeNone,
Accepted,
ReplayCode,
CounterfactualMutation,
TargetFrozen,
ResidualIdConflict,
LowProvenance,
InvalidDispute,
UnknownDispute,
DisputeExpired,
BadDisputeTransition,
UnsupportedOperation extends Code {}
abstract sig Action {}
one sig ANone,
AUpdateActual,
AUpdateNeverWas,
AAddResidualActual,
AAddResidualNeverWas,
ARecordCounterfactual,
ACanonicalHigh,
ACanonicalLow,
AOpenDispute,
AFreeze,
AUnderReview,
AResolveRelease,
ADismiss,
ARecover,
AUnsupported,
AAdvanceTime extends Action {}
sig Proposal {}
sig State {
value: one Val,
authority: one Authority,
authorityVersion: one Version,
disputeStatus: one DStatus,
disputeActive: one Bool,
canonical: lone Hash,
supersession: Hash -> Hash,
residualActual: one Bool,
residualCF: one Bool,
applied: set Proposal,
lastPid: lone Proposal,
lastAction: one Action,
lastAccepted: one Bool,
lastCode: one Code,
lastSemanticChanged: one Bool,
lastActualChanged: one Bool,
lastDisputeChanged: one Bool,
lastCanonicalChanged: one Bool,
lastPreFrozen: one Bool,
lastExpiredRestriction: one Bool,
lastOldCanonical: lone Hash,
// Alloy-only trace instrumentation; not part of the source semantic state.
step: one Action
}
pred sameSemantic[s, s2: State] {
s2.value = s.value
s2.authority = s.authority
s2.authorityVersion = s.authorityVersion
s2.disputeStatus = s.disputeStatus
s2.disputeActive = s.disputeActive
s2.canonical = s.canonical
s2.supersession = s.supersession
s2.residualActual = s.residualActual
s2.residualCF = s.residualCF
}
pred audit[
s, s2: State,
p: Proposal,
a: Action,
accepted: Bool,
code: Code,
semChanged, actualChanged, disputeChanged, canonicalChanged: Bool,
preFrozen, expiredRestriction: Bool,
oldCanonical: set Hash
] {
lone oldCanonical
(accepted = BTrue => s2.applied = s.applied + p)
(accepted = BFalse => s2.applied = s.applied)
s2.lastPid = p
s2.lastAction = a
s2.lastAccepted = accepted
s2.lastCode = code
s2.lastSemanticChanged = semChanged
s2.lastActualChanged = actualChanged
s2.lastDisputeChanged = disputeChanged
s2.lastCanonicalChanged = canonicalChanged
s2.lastPreFrozen = preFrozen
s2.lastExpiredRestriction = expiredRestriction
s2.lastOldCanonical = oldCanonical
s2.step = a
}
pred init[s: State] {
s.value = Val0
s.authority = AuthA
s.authorityVersion = Ver0
s.disputeStatus = DNone
s.disputeActive = BFalse
no s.canonical
no s.supersession
s.residualActual = BFalse
s.residualCF = BFalse
no s.applied
no s.lastPid
s.lastAction = ANone
s.lastAccepted = BFalse
s.lastCode = CodeNone
s.lastSemanticChanged = BFalse
s.lastActualChanged = BFalse
s.lastDisputeChanged = BFalse
s.lastCanonicalChanged = BFalse
s.lastPreFrozen = BFalse
s.lastExpiredRestriction = BFalse
no s.lastOldCanonical
s.step = ANone
}
pred replay[s, s2: State, p: Proposal, a: Action] {
p in s.applied
sameSemantic[s, s2]
audit[s, s2, p, a, BFalse, ReplayCode,
BFalse, BFalse, BFalse, BFalse, BFalse, BFalse, s.canonical]
}
pred updateNeverWas[s, s2: State, p: Proposal] {
p not in s.applied
sameSemantic[s, s2]
audit[s, s2, p, AUpdateNeverWas, BFalse, CounterfactualMutation,
BFalse, BFalse, BFalse, BFalse, BFalse, BFalse, s.canonical]
}
pred nextVal[v, v2: Val] {
(v = Val0 and v2 = Val1) or
(v = Val1 and v2 = Val2) or
(v = Val2 and v2 = Val0)
}
pred updateActual[s, s2: State, p: Proposal] {
p not in s.applied
(
s.disputeActive = BTrue and
s.disputeStatus in DStatus & (DFrozen + DReview)
and sameSemantic[s, s2]
and audit[s, s2, p, AUpdateActual, BFalse, TargetFrozen,
BFalse, BFalse, BFalse, BFalse, BTrue, BFalse, s.canonical]
)
or
(
not (s.disputeActive = BTrue and s.disputeStatus in DFrozen + DReview)
and nextVal[s.value, s2.value]
and s2.authority = s.authority
and s2.authorityVersion = s.authorityVersion
and s2.disputeStatus = s.disputeStatus
and s2.disputeActive = s.disputeActive
and s2.canonical = s.canonical
and s2.supersession = s.supersession
and s2.residualActual = s.residualActual
and s2.residualCF = s.residualCF
and audit[s, s2, p, AUpdateActual, BTrue, Accepted,
BTrue, BTrue, BFalse, BFalse, BFalse, BFalse, s.canonical]
)
}
pred addResidualActual[s, s2: State, p: Proposal] {
p not in s.applied
(
s.residualActual = BTrue
and sameSemantic[s, s2]
and audit[s, s2, p, AAddResidualActual, BFalse, ResidualIdConflict,
BFalse, BFalse, BFalse, BFalse, BFalse, BFalse, s.canonical]
)
or
(
s.residualActual = BFalse
and s2.residualActual = BTrue
and s2.value = s.value
and s2.authority = s.authority
and s2.authorityVersion = s.authorityVersion
and s2.disputeStatus = s.disputeStatus
and s2.disputeActive = s.disputeActive
and s2.canonical = s.canonical
and s2.supersession = s.supersession
and s2.residualCF = s.residualCF
and audit[s, s2, p, AAddResidualActual, BTrue, Accepted,
BTrue, BFalse, BFalse, BFalse, BFalse, BFalse, s.canonical]
)
}
/*
Literal translation of the supplied TLA+ AddResidualNeverWas:
it checks residualActual and sets residualActual rather than residualCF.
Do not silently "repair" this during review; report it if it is semantically wrong.
*/
pred addResidualNeverWas[s, s2: State, p: Proposal] {
p not in s.applied
(
s.residualActual = BTrue
and sameSemantic[s, s2]
and audit[s, s2, p, AAddResidualNeverWas, BFalse, ResidualIdConflict,
BFalse, BFalse, BFalse, BFalse, BFalse, BFalse, s.canonical]
)
or
(
s.residualActual = BFalse
and s2.residualActual = BTrue
and s2.value = s.value
and s2.authority = s.authority
and s2.authorityVersion = s.authorityVersion
and s2.disputeStatus = s.disputeStatus
and s2.disputeActive = s.disputeActive
and s2.canonical = s.canonical
and s2.supersession = s.supersession
and s2.residualCF = s.residualCF
and audit[s, s2, p, AAddResidualNeverWas, BTrue, Accepted,
BTrue, BFalse, BFalse, BFalse, BFalse, BFalse, s.canonical]
)
}
pred recordCounterfactual[s, s2: State, p: Proposal] {
p not in s.applied
(
s.residualCF = BTrue
and sameSemantic[s, s2]
and audit[s, s2, p, ARecordCounterfactual, BFalse, ResidualIdConflict,
BFalse, BFalse, BFalse, BFalse, BFalse, BFalse, s.canonical]
)
or
(
s.residualCF = BFalse
and s2.residualCF = BTrue
and s2.value = s.value
and s2.authority = s.authority
and s2.authorityVersion = s.authorityVersion
and s2.disputeStatus = s.disputeStatus
and s2.disputeActive = s.disputeActive
and s2.canonical = s.canonical
and s2.supersession = s.supersession
and s2.residualActual = s.residualActual
and audit[s, s2, p, ARecordCounterfactual, BTrue, Accepted,
BTrue, BFalse, BFalse, BFalse, BFalse, BFalse, s.canonical]
)
}
pred canonicalLow[s, s2: State, p: Proposal] {
p not in s.applied
sameSemantic[s, s2]
audit[s, s2, p, ACanonicalLow, BFalse, LowProvenance,
BFalse, BFalse, BFalse, BFalse, BFalse, BFalse, s.canonical]
}
pred canonicalHigh[s, s2: State, p: Proposal] {
p not in s.applied
(
s.canonical = H1
and s2.canonical = H2
and s2.supersession = s.supersession + (H1 -> H2)
and s2.value = s.value
and s2.authority = s.authority
and s2.authorityVersion = s.authorityVersion
and s2.disputeStatus = s.disputeStatus
and s2.disputeActive = s.disputeActive
and s2.residualActual = s.residualActual
and s2.residualCF = s.residualCF
and audit[s, s2, p, ACanonicalHigh, BTrue, Accepted,
BTrue, BTrue, BFalse, BTrue, BFalse, BFalse, H1]
)
or
(
s.canonical = H2
and s2.canonical = H1
and s2.supersession = s.supersession + (H2 -> H1)
and s2.value = s.value
and s2.authority = s.authority
and s2.authorityVersion = s.authorityVersion
and s2.disputeStatus = s.disputeStatus
and s2.disputeActive = s.disputeActive
and s2.residualActual = s.residualActual
and s2.residualCF = s.residualCF
and audit[s, s2, p, ACanonicalHigh, BTrue, Accepted,
BTrue, BTrue, BFalse, BTrue, BFalse, BFalse, H2]
)
or
(
no s.canonical
and s2.canonical = H1
and s2.supersession = s.supersession
and s2.value = s.value
and s2.authority = s.authority
and s2.authorityVersion = s.authorityVersion
and s2.disputeStatus = s.disputeStatus
and s2.disputeActive = s.disputeActive
and s2.residualActual = s.residualActual
and s2.residualCF = s.residualCF
and audit[s, s2, p, ACanonicalHigh, BTrue, Accepted,
BTrue, BTrue, BFalse, BTrue, BFalse, BFalse, none]
)
}
pred openDispute[s, s2: State, p: Proposal] {
p not in s.applied
(
s.disputeStatus != DNone
and sameSemantic[s, s2]
and audit[s, s2, p, AOpenDispute, BFalse, InvalidDispute,
BFalse, BFalse, BFalse, BFalse, BFalse, BFalse, s.canonical]
)
or
(
s.disputeStatus = DNone
and s2.disputeStatus = DOpen
and s2.disputeActive = BTrue
and s2.value = s.value
and s2.authority = s.authority
and s2.authorityVersion = s.authorityVersion
and s2.canonical = s.canonical
and s2.supersession = s.supersession
and s2.residualActual = s.residualActual
and s2.residualCF = s.residualCF
and audit[s, s2, p, AOpenDispute, BTrue, Accepted,
BTrue, BTrue, BTrue, BFalse, BFalse, BFalse, s.canonical]
)
}
pred freeze[s, s2: State, p: Proposal] {
p not in s.applied
(
s.disputeStatus = DNone
and sameSemantic[s, s2]
and audit[s, s2, p, AFreeze, BFalse, UnknownDispute,
BFalse, BFalse, BFalse, BFalse, BFalse, BFalse, s.canonical]
)
or
(
s.disputeStatus != DNone
and s.disputeActive = BFalse
and sameSemantic[s, s2]
and audit[s, s2, p, AFreeze, BFalse, DisputeExpired,
BFalse, BFalse, BFalse, BFalse, BFalse, BTrue, s.canonical]
)
or
(
s.disputeStatus != DNone
and s.disputeActive = BTrue
and s.disputeStatus not in DOpen + DReview
and sameSemantic[s, s2]
and audit[s, s2, p, AFreeze, BFalse, BadDisputeTransition,
BFalse, BFalse, BFalse, BFalse, BFalse, BFalse, s.canonical]
)
or
(
s.disputeActive = BTrue
and s.disputeStatus in DOpen + DReview
and s2.disputeStatus = DFrozen
and s2.disputeActive = s.disputeActive
and s2.value = s.value
and s2.authority = s.authority
and s2.authorityVersion = s.authorityVersion
and s2.canonical = s.canonical
and s2.supersession = s.supersession
and s2.residualActual = s.residualActual
and s2.residualCF = s.residualCF
and audit[s, s2, p, AFreeze, BTrue, Accepted,
BTrue, BTrue, BTrue, BFalse, BFalse, BFalse, s.canonical]
)
}
pred underReview[s, s2: State, p: Proposal] {
p not in s.applied
(
s.disputeStatus = DNone
and sameSemantic[s, s2]
and audit[s, s2, p, AUnderReview, BFalse, UnknownDispute,
BFalse, BFalse, BFalse, BFalse, BFalse, BFalse, s.canonical]
)
or
(
s.disputeStatus != DNone
and s.disputeActive = BFalse
and sameSemantic[s, s2]
and audit[s, s2, p, AUnderReview, BFalse, DisputeExpired,
BFalse, BFalse, BFalse, BFalse, BFalse, BTrue, s.canonical]
)
or
(
s.disputeStatus != DNone
and s.disputeActive = BTrue
and s.disputeStatus not in DOpen + DFrozen
and sameSemantic[s, s2]
and audit[s, s2, p, AUnderReview, BFalse, BadDisputeTransition,
BFalse, BFalse, BFalse, BFalse, BFalse, BFalse, s.canonical]
)
or
(
s.disputeActive = BTrue
and s.disputeStatus in DOpen + DFrozen
and s2.disputeStatus = DReview
and s2.disputeActive = s.disputeActive
and s2.value = s.value
and s2.authority = s.authority
and s2.authorityVersion = s.authorityVersion
and s2.canonical = s.canonical
and s2.supersession = s.supersession
and s2.residualActual = s.residualActual
and s2.residualCF = s.residualCF
and audit[s, s2, p, AUnderReview, BTrue, Accepted,
BTrue, BTrue, BTrue, BFalse, BFalse, BFalse, s.canonical]
)
}
pred resolveRelease[s, s2: State, p: Proposal] {
p not in s.applied
(
s.disputeStatus = DNone
and sameSemantic[s, s2]
and audit[s, s2, p, AResolveRelease, BFalse, UnknownDispute,
BFalse, BFalse, BFalse, BFalse, BFalse, BFalse, s.canonical]
)
or
(
s.disputeStatus != DNone
and s.disputeStatus not in DFrozen + DReview
and sameSemantic[s, s2]
and audit[s, s2, p, AResolveRelease, BFalse, BadDisputeTransition,
BFalse, BFalse, BFalse, BFalse, BFalse, BFalse, s.canonical]
)
or
(
s.disputeStatus in DFrozen + DReview
and s2.disputeStatus = DResolved
and s2.disputeActive = s.disputeActive
and s2.value = s.value
and s2.authority = s.authority
and s2.authorityVersion = s.authorityVersion
and s2.canonical = s.canonical
and s2.supersession = s.supersession
and s2.residualActual = s.residualActual
and s2.residualCF = s.residualCF
and audit[s, s2, p, AResolveRelease, BTrue, Accepted,
BTrue, BTrue, BTrue, BFalse, BFalse, BFalse, s.canonical]
)
}
pred dismiss[s, s2: State, p: Proposal] {
p not in s.applied
(
s.disputeStatus = DNone
and sameSemantic[s, s2]
and audit[s, s2, p, ADismiss, BFalse, UnknownDispute,
BFalse, BFalse, BFalse, BFalse, BFalse, BFalse, s.canonical]
)
or
(
s.disputeStatus != DNone
and s.disputeStatus not in DOpen + DFrozen + DReview
and sameSemantic[s, s2]
and audit[s, s2, p, ADismiss, BFalse, BadDisputeTransition,
BFalse, BFalse, BFalse, BFalse, BFalse, BFalse, s.canonical]
)
or
(
s.disputeStatus in DOpen + DFrozen + DReview
and s2.disputeStatus = DDismissed
and s2.disputeActive = s.disputeActive
and s2.value = s.value
and s2.authority = s.authority
and s2.authorityVersion = s.authorityVersion
and s2.canonical = s.canonical
and s2.supersession = s.supersession
and s2.residualActual = s.residualActual
and s2.residualCF = s.residualCF
and audit[s, s2, p, ADismiss, BTrue, Accepted,
BTrue, BTrue, BTrue, BFalse, BFalse, BFalse, s.canonical]
)
}
pred nextAuthority[a, a2: Authority] {
(a = AuthA and a2 = AuthB) or
(a = AuthB and a2 = AuthA)
}
pred nextVersion[v, v2: Version] {
(v = Ver0 and v2 = Ver1) or
(v = Ver1 and v2 = Ver2) or
(v = Ver2 and v2 = Ver3) or
(v = Ver3 and v2 = Ver3)
}
pred recover[s, s2: State, p: Proposal] {
p not in s.applied
nextAuthority[s.authority, s2.authority]
nextVersion[s.authorityVersion, s2.authorityVersion]
s2.value = s.value
s2.disputeStatus = s.disputeStatus
s2.disputeActive = s.disputeActive
s2.canonical = s.canonical
s2.supersession = s.supersession
s2.residualActual = s.residualActual
s2.residualCF = s.residualCF
audit[s, s2, p, ARecover, BTrue, Accepted,
BTrue, BTrue, BFalse, BFalse, BFalse, BFalse, s.canonical]
}
pred unsupported[s, s2: State, p: Proposal] {
p not in s.applied
sameSemantic[s, s2]
audit[s, s2, p, AUnsupported, BFalse, UnsupportedOperation,
BFalse, BFalse, BFalse, BFalse, BFalse, BFalse, s.canonical]
}
pred advanceTime[s, s2: State] {
s.disputeStatus != DNone
s.disputeActive = BTrue
s2.disputeActive = BFalse
s2.value = s.value
s2.authority = s.authority
s2.authorityVersion = s.authorityVersion
s2.disputeStatus = s.disputeStatus
s2.canonical = s.canonical
s2.supersession = s.supersession
s2.residualActual = s.residualActual
s2.residualCF = s.residualCF
s2.applied = s.applied
// Source TLA+ keeps the audit fields unchanged on AdvanceTime.
s2.lastPid = s.lastPid
s2.lastAction = s.lastAction
s2.lastAccepted = s.lastAccepted
s2.lastCode = s.lastCode
s2.lastSemanticChanged = s.lastSemanticChanged
s2.lastActualChanged = s.lastActualChanged
s2.lastDisputeChanged = s.lastDisputeChanged
s2.lastCanonicalChanged = s.lastCanonicalChanged
s2.lastPreFrozen = s.lastPreFrozen
s2.lastExpiredRestriction = s.lastExpiredRestriction
s2.lastOldCanonical = s.lastOldCanonical
s2.step = AAdvanceTime
}
pred attemptUpdateActual[s, s2: State, p: Proposal] {
replay[s, s2, p, AUpdateActual] or updateActual[s, s2, p]
}
pred attemptUpdateNeverWas[s, s2: State, p: Proposal] {
replay[s, s2, p, AUpdateNeverWas] or updateNeverWas[s, s2, p]
}
pred attemptAddResidualActual[s, s2: State, p: Proposal] {
replay[s, s2, p, AAddResidualActual] or addResidualActual[s, s2, p]
}
pred attemptAddResidualNeverWas[s, s2: State, p: Proposal] {
replay[s, s2, p, AAddResidualNeverWas] or addResidualNeverWas[s, s2, p]
}
pred attemptRecordCounterfactual[s, s2: State, p: Proposal] {
replay[s, s2, p, ARecordCounterfactual] or recordCounterfactual[s, s2, p]
}
pred attemptCanonicalHigh[s, s2: State, p: Proposal] {
replay[s, s2, p, ACanonicalHigh] or canonicalHigh[s, s2, p]
}
pred attemptCanonicalLow[s, s2: State, p: Proposal] {
replay[s, s2, p, ACanonicalLow] or canonicalLow[s, s2, p]
}
pred attemptOpenDispute[s, s2: State, p: Proposal] {
replay[s, s2, p, AOpenDispute] or openDispute[s, s2, p]
}
pred attemptFreeze[s, s2: State, p: Proposal] {
replay[s, s2, p, AFreeze] or freeze[s, s2, p]
}
pred attemptUnderReview[s, s2: State, p: Proposal] {
replay[s, s2, p, AUnderReview] or underReview[s, s2, p]
}
pred attemptResolveRelease[s, s2: State, p: Proposal] {
replay[s, s2, p, AResolveRelease] or resolveRelease[s, s2, p]
}
pred attemptDismiss[s, s2: State, p: Proposal] {
replay[s, s2, p, ADismiss] or dismiss[s, s2, p]
}
pred attemptRecover[s, s2: State, p: Proposal] {
replay[s, s2, p, ARecover] or recover[s, s2, p]
}
pred attemptUnsupported[s, s2: State, p: Proposal] {
replay[s, s2, p, AUnsupported] or unsupported[s, s2, p]
}
fact Trace {
init[first]
all s: State - last |
let s2 = next[s] |
(
some p: Proposal |
attemptUpdateActual[s, s2, p]
or attemptUpdateNeverWas[s, s2, p]
or attemptAddResidualActual[s, s2, p]
or attemptAddResidualNeverWas[s, s2, p]
or attemptRecordCounterfactual[s, s2, p]
or attemptCanonicalHigh[s, s2, p]
or attemptCanonicalLow[s, s2, p]
or attemptOpenDispute[s, s2, p]
or attemptFreeze[s, s2, p]
or attemptUnderReview[s, s2, p]
or attemptResolveRelease[s, s2, p]
or attemptDismiss[s, s2, p]
or attemptRecover[s, s2, p]
or attemptUnsupported[s, s2, p]
)
or advanceTime[s, s2]
}
/* -------------------------------------------------------------------------
SOURCE-NAMED ASSERTIONS
------------------------------------------------------------------------- */
assert NeverWasNoActualMutation {
all s: State - first |
s.step = AUpdateNeverWas =>
(
s.lastAccepted = BFalse
and s.lastCode = CounterfactualMutation
and s.lastActualChanged = BFalse
)
}
assert FrozenUpdateBlocked {
all s: State - first |
s.step = AUpdateActual and s.lastPreFrozen = BTrue =>
(
s.lastAccepted = BFalse
and s.lastCode = TargetFrozen
)
}
assert RecoveryPreservesDispute {
all s: State - last |
let s2 = next[s] |
s2.step = ARecover and s2.lastAccepted = BTrue =>
(
s2.disputeStatus = s.disputeStatus
and s2.disputeActive = s.disputeActive
)
}
assert CounterfactualNoActualAuthority {
all s: State - first |
s.step = ARecordCounterfactual and s.lastAccepted = BTrue =>
s.lastActualChanged = BFalse
}
assert LowProvenanceNoCanonical {
all s: State - first |
s.step = ACanonicalLow =>
(
s.lastAccepted = BFalse
and s.lastCode = LowProvenance
and s.lastCanonicalChanged = BFalse
)
}
assert ExpiredDisputeActionRestricted {
all s: State - first |
s.lastExpiredRestriction = BTrue =>
(
s.lastAccepted = BFalse
and s.lastCode = DisputeExpired
)
}
assert ReplayNoSemanticMutation {
all s: State - first |
s.step != AAdvanceTime and s.lastCode = ReplayCode =>
(
s.lastAccepted = BFalse
and s.lastSemanticChanged = BFalse
)
}
assert AcceptedPidApplied {
all s: State - first |
s.step != AAdvanceTime and s.lastAccepted = BTrue =>
s.lastPid in s.applied
}
assert RejectedNonReplayNotApplied {
all s: State - first |
s.step != AAdvanceTime
and s.lastAccepted = BFalse
and s.lastCode != ReplayCode
and some s.lastPid =>
s.lastPid not in s.applied
}
assert CanonicalReplacementPreservesSupersession {
all s: State - last |
let s2 = next[s] |
s2.step = ACanonicalHigh
and s2.lastAccepted = BTrue
and some s.canonical =>
(s.canonical -> s2.canonical) in s2.supersession
}
/* -------------------------------------------------------------------------
ALLOY-SPECIFIC RELATIONAL CHALLENGES
These go beyond merely restating the audit-flag invariants.
------------------------------------------------------------------------- */
assert ReplayPreservesAllSemanticRelations {
all s: State - last |
let s2 = next[s] |
s2.step != AAdvanceTime and s2.lastCode = ReplayCode =>
sameSemantic[s, s2]
}
assert RecoveryDoesNotChangeCanonicalOrSupersession {
all s: State - last |
let s2 = next[s] |
s2.step = ARecover and s2.lastAccepted = BTrue =>
(
s2.canonical = s.canonical
and s2.supersession = s.supersession
)
}
assert AdvanceTimeDoesNotEraseDispute {
all s: State - last |
let s2 = next[s] |
s2.step = AAdvanceTime =>
(
s2.disputeStatus = s.disputeStatus
and s2.disputeStatus != DNone
and s2.disputeActive = BFalse
)
}
assert NoSilentCanonicalReplacement {
all s: State - last |
let s2 = next[s] |
some s.canonical and s2.canonical != s.canonical =>
(
s2.step = ACanonicalHigh
and (s.canonical -> s2.canonical) in s2.supersession
)
}
/*
Potential source-model issue probe:
The literal TLA+ AddResidualNeverWas transition writes residualActual.
If a reviewer believes NEVER_WAS residuals should affect residualCF instead,
the following assertion is EXPECTED to expose that mismatch once a reachable
AAddResidualNeverWas acceptance exists.
*/
assert NeverWasResidualShouldNotChangeActualResidual {
all s: State - last |
let s2 = next[s] |
s2.step = AAddResidualNeverWas and s2.lastAccepted = BTrue =>
s2.residualActual = s.residualActual
}
/* -------------------------------------------------------------------------
NON-VACUITY / REACHABILITY PROBES
Run these before trusting "no counterexample" results.
------------------------------------------------------------------------- */
pred ReachAcceptedUpdate {
some s: State | s.step = AUpdateActual and s.lastAccepted = BTrue
}
pred ReachFrozenRejection {
some s: State | s.step = AUpdateActual and s.lastCode = TargetFrozen
}
pred ReachReplay {
some s: State | s.lastCode = ReplayCode
}
pred ReachRecovery {
some s: State | s.step = ARecover and s.lastAccepted = BTrue
}
pred ReachCanonicalReplacement {
some s: State - first |
s.step = ACanonicalHigh and s.lastAccepted = BTrue and some s.lastOldCanonical
}
pred ReachExpiredDisputeRestriction {
some s: State | s.lastExpiredRestriction = BTrue
}
pred ReachNeverWasResidualAcceptance {
some s: State | s.step = AAddResidualNeverWas and s.lastAccepted = BTrue
}
/*
Suggested commands.
Alloy analysis is bounded by the chosen scope. "No counterexample" means only
"no counterexample within this model and scope."
*/
run ReachAcceptedUpdate for 8 but exactly 8 State, exactly 3 Proposal
run ReachFrozenRejection for 8 but exactly 8 State, exactly 4 Proposal
run ReachReplay for 8 but exactly 8 State, exactly 3 Proposal
run ReachRecovery for 8 but exactly 8 State, exactly 3 Proposal
run ReachCanonicalReplacement for 8 but exactly 8 State, exactly 4 Proposal
run ReachExpiredDisputeRestriction for 8 but exactly 8 State, exactly 4 Proposal
run ReachNeverWasResidualAcceptance for 8 but exactly 8 State, exactly 3 Proposal
check NeverWasNoActualMutation for 8 but exactly 8 State, exactly 4 Proposal
check FrozenUpdateBlocked for 8 but exactly 8 State, exactly 4 Proposal
check RecoveryPreservesDispute for 8 but exactly 8 State, exactly 4 Proposal
check CounterfactualNoActualAuthority for 8 but exactly 8 State, exactly 4 Proposal
check LowProvenanceNoCanonical for 8 but exactly 8 State, exactly 4 Proposal
check ExpiredDisputeActionRestricted for 8 but exactly 8 State, exactly 4 Proposal
check ReplayNoSemanticMutation for 8 but exactly 8 State, exactly 4 Proposal
check AcceptedPidApplied for 8 but exactly 8 State, exactly 4 Proposal
check RejectedNonReplayNotApplied for 8 but exactly 8 State, exactly 4 Proposal
check CanonicalReplacementPreservesSupersession for 8 but exactly 8 State, exactly 4 Proposal
check ReplayPreservesAllSemanticRelations for 8 but exactly 8 State, exactly 4 Proposal
check RecoveryDoesNotChangeCanonicalOrSupersession for 8 but exactly 8 State, exactly 4 Proposal
check AdvanceTimeDoesNotEraseDispute for 8 but exactly 8 State, exactly 4 Proposal
check NoSilentCanonicalReplacement for 8 but exactly 8 State, exactly 4 Proposal
// Deliberate review probe: this may produce a counterexample because the
// supplied TLA+ AddResidualNeverWas writes residualActual literally.
check NeverWasResidualShouldNotChangeActualResidual for 8 but exactly 8 State, exactly 4 Proposal