Skip to content

feat: add proofs for the TaskProcessing and ObjectProcessing specifications #13

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Merged
qdelamea-aneo merged 2 commits into from
Jan 19, 2026
Merged

feat: add proofs for the TaskProcessing and ObjectProcessing specifications #13

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
2 commits
Select commit Hold shift + click to select a range
42741c0
feat: add proofs for the ObjectProcessing specification
qdelamea-aneo Jan 19, 2026
3d7e99a
feat: add proofs for the TaskProcessing specification
qdelamea-aneo Jan 19, 2026
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
6 changes: 4 additions & 2 deletions specs/ObjectProcessing.cfg
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -7,8 +7,10 @@ SPECIFICATION

INVARIANTS
TypeInv
TargetStateConsistent
DistinctObjectStates
TargetValidity

PROPERTIES
EventualTargetFinalization
PermanentFinalization
EventualTargetFinalization
EventualTargetResolution
37 changes: 18 additions & 19 deletions specs/ObjectProcessing.tla
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -128,7 +128,9 @@ Next ==
* eventually finalized.
*)
Fairness ==
/\ \A o \in ObjectId: WF_vars(o \in objectTargets /\ FinalizeObjects({o}))
\A o \in ObjectId:
EventuallyFinalized(o) ::
WF_vars(o \in objectTargets /\ FinalizeObjects({o}))

(**
* Full system specification.
Expand All @@ -148,35 +150,32 @@ Spec ==
* SAFETY
* An object can only be targeted if it is known to the system.
*)
TargetStateConsistent ==
TargetValidity ==
objectTargets \intersect UnknownObject = {}

(**
* SAFETY
* Once an object reaches the FINALIZED state, it remains there permanently.
*)
PermanentFinalization ==
\A o \in ObjectId:
[](o \in FinalizedObject => [](o \in FinalizedObject))

(**
* LIVENESS
* Every targeted object is eventually either finalized or untargeted.
*)
EventualTargetFinalization ==
\A o \in ObjectId:
o \in objectTargets ~> (o \in FinalizedObject \/ o \notin objectTargets)
<>[](o \in objectTargets) => <>(o \in FinalizedObject)

(**
* LIVENESS
* Once an object reaches the FINALIZED state, it remains there permanently.
* Any object added to the target set must eventually be resolved,
* meaning it is either finalized or removed from the target set.
*)
PermanentFinalization ==
\A o \in ObjectId:
[](o \in FinalizedObject => [](o \in FinalizedObject))

-------------------------------------------------------------------------------

(*****************************************************************************)
(* THEOREMS *)
(*****************************************************************************)

THEOREM Spec => []TypeInv
THEOREM Spec => []DistinctObjectStates
THEOREM Spec => []TargetStateConsistent
THEOREM Spec => EventualTargetFinalization
THEOREM Spec => PermanentFinalization
EventualTargetResolution ==
\A o \in ObjectId :
o \in objectTargets ~> (o \in FinalizedObject \/ o \notin objectTargets)

===============================================================================
108 changes: 108 additions & 0 deletions specs/ObjectProcessing_proof.tla
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -0,0 +1,108 @@
------------------------ MODULE ObjectProcessing_proof ------------------------
EXTENDS ObjectProcessing, TLAPS

THEOREM TypeCorrect == Spec => []TypeInv
<1>. USE DEF OBJECT_UNKNOWN, OBJECT_REGISTERED, OBJECT_FINALIZED, UnknownObject,
RegisteredObject, FinalizedObject
<1>1. Init => TypeInv
BY DEF Init, TypeInv
<1>2. TypeInv /\ [Next]_vars => TypeInv'
BY DEF TypeInv, Next, vars, RegisterObjects, TargetObjects,
UntargetObjects, FinalizeObjects, Terminating
<1>. QED
BY <1>1, <1>2, PTL DEF Spec

THEOREM DistinctObjectStatesCorrect == Spec => []DistinctObjectStates
<1>. USE DEF IsPairwiseDisjoint, OBJECT_UNKNOWN, OBJECT_REGISTERED,
OBJECT_FINALIZED, OBJECT_COMPLETED, OBJECT_ABORTED, OBJECT_DELETED,
UnknownObject, RegisteredObject, FinalizedObject, CompletedObject,
AbortedObject, DeletedObject
<1>1. Init => DistinctObjectStates
BY DEF Init, DistinctObjectStates
<1>2. TypeInv /\ DistinctObjectStates /\ [Next]_vars => DistinctObjectStates'
BY DEF TypeInv, DistinctObjectStates, Next, vars, RegisterObjects,
TargetObjects, UntargetObjects, FinalizeObjects, Terminating
<1>. QED
BY <1>1, <1>2, TypeCorrect, PTL DEF Spec

THEOREM TargetValidityCorrect == Spec => []TargetValidity
<1>. USE DEF OBJECT_UNKNOWN, OBJECT_REGISTERED, OBJECT_FINALIZED, UnknownObject,
RegisteredObject, FinalizedObject
<1>1. Init => TargetValidity
BY DEF Init, TargetValidity
<1>2. TypeInv /\ TargetValidity /\ [Next]_vars => TargetValidity'
BY DEF TargetValidity, TypeInv, Next, vars, RegisterObjects,
TargetObjects, UntargetObjects, FinalizeObjects, Terminating
<1>. QED
BY <1>1, <1>2, TypeCorrect, PTL DEF Spec

ObjectSafetyInv ==
/\ TypeInv
/\ DistinctObjectStates
/\ TargetValidity

THEOREM ObjectSafetyInvCorrect == Spec => []ObjectSafetyInv
BY TypeCorrect, DistinctObjectStatesCorrect, TargetValidityCorrect, PTL
DEF ObjectSafetyInv

THEOREM PermanentFinalizationCorrect == Spec => PermanentFinalization
<1>. SUFFICES ASSUME NEW o \in ObjectId
PROVE Spec => [](o \in FinalizedObject => [](o \in FinalizedObject))
BY DEF PermanentFinalization
<1>. USE DEF OBJECT_UNKNOWN, OBJECT_REGISTERED, OBJECT_FINALIZED, UnknownObject,
RegisteredObject, FinalizedObject
<1>1. TypeInv /\ o \in FinalizedObject /\ [Next]_vars
=> (o \in FinalizedObject)'
BY DEF TypeInv, Next, vars, RegisterObjects, TargetObjects,
UntargetObjects, FinalizeObjects, Terminating
<1>. QED
BY <1>1, TypeCorrect, PTL DEF Spec

LEMMA TargetsAreKnown == ASSUME NEW o \in objectTargets
PROVE ObjectSafetyInv => \/ o \in RegisteredObject
\/ o \in FinalizedObject
BY DEF ObjectSafetyInv, TypeInv, DistinctObjectStates, TargetValidity,
OBJECT_UNKNOWN, OBJECT_REGISTERED, OBJECT_FINALIZED, UnknownObject,
RegisteredObject, FinalizedObject

THEOREM EventualTargetFinalizationCorrect == Spec => EventualTargetFinalization
<1>. SUFFICES ASSUME NEW o \in ObjectId
PROVE Spec => (<>[](o \in objectTargets) => <>(o \in FinalizedObject))
BY DEF EventualTargetFinalization
<1>1. Fairness => Fairness!EventuallyFinalized(o)
BY DEF Fairness
<1>2. []ObjectSafetyInv /\ [][Next]_vars /\ Fairness!EventuallyFinalize(o) /\ [](o \in objectTargets)
=> <>(o \in FinalizedObject)
<2>. USE DEF OBJECT_FINALIZED, FinalizedObject
<2>1. ObjectSafetyInv /\ (o \in objectTargets) /\ ~(o \in FinalizedObject)
=> ENABLED <<o \in objectTargets /\ FinalizeObjects({o})>>_vars
BY ExpandENABLED, TargetsAreKnown DEF FinalizeObjects, vars
<2>2. <<o \in objectTargets /\ FinalizeObjects({o})>>_vars => (o \in FinalizedObject)'
BY DEF FinalizeObjects, vars
<2>3. QED
BY <2>1, <2>2, PTL
<1> QED
BY <1>1, <1>2, PTL, ObjectSafetyInvCorrect DEF Spec

THEOREM EventualTargetResolutionCorrect == Spec => EventualTargetResolution
<1>. SUFFICES ASSUME NEW o \in ObjectId
PROVE Spec => (o \in objectTargets ~> (o \in FinalizedObject \/ o \notin objectTargets))
BY DEF EventualTargetResolution
<1>1. o \in objectTargets /\ [Next]_vars => \/ (o \in objectTargets)'
\/ (o \in FinalizedObject)'
\/ (o \notin objectTargets)'
BY DEF Next, vars, RegisterObjects, TargetObjects, UntargetObjects,
FinalizeObjects, Terminating
<1>2. <<o \in objectTargets /\ FinalizeObjects({o})>>_vars
=> (o \in FinalizedObject)'
BY DEF FinalizeObjects, OBJECT_REGISTERED, OBJECT_FINALIZED,
RegisteredObject, FinalizedObject
<1>3. ObjectSafetyInv /\ o \in objectTargets => ENABLED <<o \in objectTargets /\ FinalizeObjects({o})>>_vars \/ o \in FinalizedObject
BY ExpandENABLED, TargetsAreKnown DEF FinalizeObjects, vars,
OBJECT_REGISTERED, OBJECT_FINALIZED, RegisteredObject, FinalizedObject
<1>4. Fairness => Fairness!EventuallyFinalize(o)
BY DEF Fairness
<1>. QED
BY <1>1, <1>2, <1>3, <1>4, ObjectSafetyInvCorrect, PTL DEF Spec, ObjectSafetyInv

===============================================================================
2 changes: 1 addition & 1 deletion specs/ObjectStates.tla
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -8,9 +8,9 @@
(* allowing other specifications to reason about groups of objects sharing *)
(* the same lifecycle phase. *)
(*****************************************************************************)
EXTENDS Utils

LOCAL INSTANCE FiniteSets
LOCAL INSTANCE Utils

(**
* Abstract operator returning the set of objects in a given state.
Expand Down
6 changes: 5 additions & 1 deletion specs/TaskProcessing.cfg
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -10,10 +10,14 @@ SPECIFICATION

INVARIANTS
TypeInv
AllocConsistent
DistinctTaskStates
AllocStateConsistent
ExclusiveAssignment

PROPERTY
PermanentFinalization
EventualStaging
EventualDeallocation
EventualProcessing
EventualFinalization
EventualQuiescence
66 changes: 41 additions & 25 deletions specs/TaskProcessing.tla
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -8,6 +8,8 @@
(* properties of the system. *)
(*****************************************************************************)

EXTENDS Utils

CONSTANTS
AgentId, \* Set of agent identifiers (theoretically infinite)
TaskId \* Set of task identifiers (theoretically infinite)
Expand Down Expand Up @@ -165,9 +167,9 @@ Next ==
*)
Fairness ==
\A t \in TaskId:
/\ WF_vars(StageTasks({t}))
/\ SF_vars(\E a \in AgentId : ProcessTasks(a, {t}))
/\ WF_vars(FinalizeTasks({t}))
/\ EventuallyStaged(t) :: WF_vars(StageTasks({t}))
/\ EventuallyProcessed(t) :: SF_vars(\E a \in AgentId : ProcessTasks(a, {t}))
/\ EventuallyFinalized(t) :: WF_vars(FinalizeTasks({t}))

(**
* Full system specification.
Expand All @@ -183,18 +185,11 @@ Spec ==
(* SAFETY AND LIVENESS PROPERTIES *)
(*****************************************************************************)

(**
* SAFETY
* The set of all allocated tasks always belongs to the universe of tasks.
*)
AllocConsistent ==
UNION {agentTaskAlloc[a] : a \in AgentId} \subseteq TaskId

(**
* SAFETY
* A task is assigned to an agent if and only if it is in the ASISGNED state.
*)
AllocStateConsistent ==
AssignedStateIntegrity ==
\A t \in TaskId:
t \in AssignedTask <=> \E a \in AgentId: t \in agentTaskAlloc[a]

Expand All @@ -213,6 +208,40 @@ ExclusiveAssignment ==
PermanentFinalization ==
\A t \in TaskId: [](t \in FinalizedTask => [](t \in FinalizedTask))

(**
* LIVENESS
* Every registered task is eventually staged for processing.
*)
EventualStaging ==
\A t \in TaskId :
t \in RegisteredTask ~> t \in StagedTask

(**
* LIVENESS
* Any task assigned to an agent will eventually be either released back
* to the staged pool or successfully processed.
*)
EventualDeallocation ==
\A t \in TaskId :
t \in AssignedTask ~> t \in StagedTask \/ t \in ProcessedTask

(**
* LIVENESS
* If a task is repeatedly assigned to agents, it must eventually reach
* the processed state.
*)
EventualProcessing ==
\A t \in TaskId :
[]<>(t \in AssignedTask) => <>(t \in ProcessedTask)

(**
* LIVENESS
* Every processed task will eventually reach the finalized state.
*)
EventualFinalization ==
\A t \in TaskId :
t \in ProcessedTask ~> t \in FinalizedTask

(**
* LIVENESS
* Any staged task ultimately remains in the STAGED or FINALIZED state.
Expand All @@ -223,17 +252,4 @@ EventualQuiescence ==
\/ [](t \in StagedTask)
\/ [](t \in FinalizedTask)

-------------------------------------------------------------------------------

(*****************************************************************************)
(* THEOREMS *)
(*****************************************************************************)

THEOREM Spec => []TypeInv
THEOREM Spec => []AllocConsistent
THEOREM Spec => []AllocStateConsistent
THEOREM Spec => []ExclusiveAssignment
THEOREM Spec => PermanentFinalization
THEOREM Spec => EventualQuiescence

=============================================================================
===============================================================================
Loading