From a398fe30dd586a10f738ec04a72c11a73ef8b6e3 Mon Sep 17 00:00:00 2001 From: Andrew Helwer <2n8rn1w1f@mozmail.com> Date: Fri, 24 Mar 2023 12:59:11 -0400 Subject: [PATCH] Publishing three sets of specs: * Checkpoint Coordination * Least-Circular Substring * Introduction to TLA+ proofs Signed-off-by: Andrew Helwer <2n8rn1w1f@mozmail.com> --- README.md | 5 +- manifest.json | 158 ++++++ .../CheckpointCoordination.tla | 533 ++++++++++++++++++ .../MCCheckpointCoordination.cfg | 29 + .../MCCheckpointCoordination.tla | 21 + .../MCCheckpointCoordinationFailure.cfg | 28 + .../CheckpointCoordination/README.md | 154 +++++ specifications/LearnProofs/AddTwo.tla | 85 +++ specifications/LearnProofs/FindHighest.tla | 243 ++++++++ specifications/LearnProofs/MCFindHighest.cfg | 16 + specifications/LearnProofs/MCFindHighest.tla | 13 + .../LeastCircularSubstring.pdf | Bin 0 -> 52270 bytes .../LeastCircularSubstring.tla | 165 ++++++ .../MCLeastCircularSubstring.tla | 11 + .../MCLeastCircularSubstringMedium.cfg | 12 + .../MCLeastCircularSubstringSmall.cfg | 12 + .../LeastCircularSubstring/README.md | 10 + .../LeastCircularSubstring/ZSequences.tla | 78 +++ specifications/LeastCircularSubstring/lcs.py | 41 ++ .../LeastCircularSubstring/requirements.txt | 3 + 20 files changed, 1616 insertions(+), 1 deletion(-) create mode 100644 specifications/CheckpointCoordination/CheckpointCoordination.tla create mode 100644 specifications/CheckpointCoordination/MCCheckpointCoordination.cfg create mode 100644 specifications/CheckpointCoordination/MCCheckpointCoordination.tla create mode 100644 specifications/CheckpointCoordination/MCCheckpointCoordinationFailure.cfg create mode 100644 specifications/CheckpointCoordination/README.md create mode 100644 specifications/LearnProofs/AddTwo.tla create mode 100644 specifications/LearnProofs/FindHighest.tla create mode 100644 specifications/LearnProofs/MCFindHighest.cfg create mode 100644 specifications/LearnProofs/MCFindHighest.tla create mode 100644 specifications/LeastCircularSubstring/LeastCircularSubstring.pdf create mode 100644 specifications/LeastCircularSubstring/LeastCircularSubstring.tla create mode 100644 specifications/LeastCircularSubstring/MCLeastCircularSubstring.tla create mode 100644 specifications/LeastCircularSubstring/MCLeastCircularSubstringMedium.cfg create mode 100644 specifications/LeastCircularSubstring/MCLeastCircularSubstringSmall.cfg create mode 100644 specifications/LeastCircularSubstring/README.md create mode 100644 specifications/LeastCircularSubstring/ZSequences.tla create mode 100644 specifications/LeastCircularSubstring/lcs.py create mode 100644 specifications/LeastCircularSubstring/requirements.txt diff --git a/README.md b/README.md index b698f053..767f436c 100644 --- a/README.md +++ b/README.md @@ -113,8 +113,11 @@ A central manifest of specs with descriptions and accounts of their various mode | 96 | Nano Blockchain Protocol | Directory | Andrew Helwer | | ✔ | Naturals, Bags | | | | 97 | Coffee Can White/Black Bean Problem | Directory | Andrew Helwer | | ✔ | Naturals | | | | 98 | The Slush Protocol | Directory | Andrew Helwer | | ✔ | Naturals, FiniteSets, Sequences | ✔ | | -| 99 | SDP (Software Defined Perimeter) | Specifying and Verifying SDP Protocol based Zero Trust Architecture | Luming Dong, Zhi Niu | | ✔| FiniteSets, Sequences, Naturals | | +| 99 | SDP (Software Defined Perimeter) | Specifying and Verifying SDP Protocol based Zero Trust Architecture | Luming Dong, Zhi Niu | | ✔| FiniteSets, Sequences, Naturals | | | | 100 | Simplified Fast Paxos | Simplified version of Fast Paxos (Lamport, 2006) | Lim Ngian Xin Terry, Gaurav Gandhi | |✔| TLC, Naturals, FiniteSets, Integers | | | +| 101 | Learn TLA⁺ Proofs | Basic PlusCal algorithms and formal proofs of their correctness | Andrew Helwer | ✔ | ✔ | Sequences, Naturals, Integers, TLAPS | ✔ | | +| 102 | Lexicographically-Least Circular Substring | Booth's 1980 algorithm to find the lexicographically-least circular substring | Andrew Helwer | | ✔ | FiniteSets, Integers, Naturals, Sequences | ✔ | | +| 103 | Distributed Checkpoint Coordination | Algorithm for coordinating checkpoint/snapshot leases in a Paxos ring | Andrew Helwer | | ✔ | FiniteSets, Naturals, Sequences, TLC | | | ## License diff --git a/manifest.json b/manifest.json index 612cfb13..873890d6 100644 --- a/manifest.json +++ b/manifest.json @@ -145,6 +145,57 @@ } ] }, + { + "path": "specifications/CheckpointCoordination", + "title": "Distributed Checkpoint/Snapshot Coordination", + "description": "An algorithm for controlling checkpoint leases in a Paxos ring", + "source": "https://github.com/Azure/RingMaster", + "authors": [ + "Andrew Helwer" + ], + "tags": [], + "modules": [ + { + "path": "specifications/CheckpointCoordination/CheckpointCoordination.tla", + "communityDependencies": [], + "tlaLanguageVersion": 2, + "features": [], + "models": [] + }, + { + "path": "specifications/CheckpointCoordination/MCCheckpointCoordination.tla", + "communityDependencies": [], + "tlaLanguageVersion": 2, + "features": [], + "models": [ + { + "path": "specifications/CheckpointCoordination/MCCheckpointCoordination.cfg", + "runtime": "00:01:00", + "size": "medium", + "mode": "exhaustive search", + "config": [], + "features": [ + "state constraint", + "symmetry" + ], + "result": "success" + }, + { + "path": "specifications/CheckpointCoordination/MCCheckpointCoordinationFailure.cfg", + "runtime": "00:00:10", + "size": "small", + "mode": "exhaustive search", + "config": [], + "features": [ + "state constraint", + "symmetry" + ], + "result": "safety failure" + } + ] + } + ] + }, { "path": "specifications/CigaretteSmokers", "title": "The Cigarette Smokers Problem", @@ -507,6 +558,113 @@ } ] }, + { + "path": "specifications/LearnProofs", + "title": "Learn TLA⁺ Proofs", + "description": "Some specs of very simple algorithms & formal proofs of their correctness", + "source": "", + "authors": [ + "Andrew Helwer" + ], + "tags": [ + "beginner" + ], + "modules": [ + { + "path": "specifications/LearnProofs/AddTwo.tla", + "communityDependencies": [], + "tlaLanguageVersion": 2, + "features": [ + "pluscal", + "proof" + ], + "models": [] + }, + { + "path": "specifications/LearnProofs/FindHighest.tla", + "communityDependencies": [], + "tlaLanguageVersion": 2, + "features": [ + "pluscal", + "proof" + ], + "models": [] + }, + { + "path": "specifications/LearnProofs/MCFindHighest.tla", + "communityDependencies": [], + "tlaLanguageVersion": 2, + "features": [], + "models": [ + { + "path": "specifications/LearnProofs/MCFindHighest.cfg", + "runtime": "00:00:01", + "size": "small", + "mode": "exhaustive search", + "config": [], + "features": [ + "state constraint" + ], + "result": "success" + } + ] + } + ] + }, + { + "path": "specifications/LeastCircularSubstring", + "title": "Lexicographically-Least Circular Substring", + "description": "Booth's 1980 algorithm to find the lexicographically-least circular substring", + "source": "", + "authors": [ + "Andrew Helwer" + ], + "tags": [], + "modules": [ + { + "path": "specifications/LeastCircularSubstring/LeastCircularSubstring.tla", + "communityDependencies": [], + "tlaLanguageVersion": 2, + "features": [ + "pluscal" + ], + "models": [] + }, + { + "path": "specifications/LeastCircularSubstring/MCLeastCircularSubstring.tla", + "communityDependencies": [], + "tlaLanguageVersion": 2, + "features": [], + "models": [ + { + "path": "specifications/LeastCircularSubstring/MCLeastCircularSubstringMedium.cfg", + "runtime": "00:01:00", + "size": "medium", + "mode": "exhaustive search", + "config": [], + "features": [], + "result": "success" + }, + { + "path": "specifications/LeastCircularSubstring/MCLeastCircularSubstringSmall.cfg", + "runtime": "00:00:05", + "size": "small", + "mode": "exhaustive search", + "config": [], + "features": [], + "result": "success" + } + ] + }, + { + "path": "specifications/LeastCircularSubstring/ZSequences.tla", + "communityDependencies": [], + "tlaLanguageVersion": 2, + "features": [], + "models": [] + } + ] + }, { "path": "specifications/LevelChecking", "title": "TLA⁺ Level Checking", diff --git a/specifications/CheckpointCoordination/CheckpointCoordination.tla b/specifications/CheckpointCoordination/CheckpointCoordination.tla new file mode 100644 index 00000000..0d41777a --- /dev/null +++ b/specifications/CheckpointCoordination/CheckpointCoordination.tla @@ -0,0 +1,533 @@ +----------------------- MODULE CheckpointCoordination ----------------------- +EXTENDS + Naturals, + FiniteSets, + Sequences + +CONSTANTS + Node, \* The set of all nodes available for use in the cluster + Majority \* The number of nodes constituting a majority + +VARIABLES + IsNodeUp, \* Whether each node is up + NetworkPath, \* Whether a network path exists between nodes + Leader, \* Which node is currently elected leader + ReplicatedLog, \* The replicated log of commands on each node + ExecutionCounter, \* The index in the log each node will next execute + LastVotePayload, \* Data field which piggybacks on vote responses + CurrentLease, \* The current checkpoint lease recorded at each nodes + CanTakeCheckpoint, \* Whether node believes it can take a checkpoint + IsTakingCheckpoint, \* Whether node is currently taking a checkpoint + TimeoutCounter, \* Counter of oldest lease which has not yet timed out + LatestCheckpoint \* The latest recorded log checkpoint + +(***************************************************************************) +(* Variables relating to the environment in which the cluster is running. *) +(***************************************************************************) +EnvironmentVars == << + IsNodeUp, + NetworkPath +>> + +(***************************************************************************) +(* Variables relating to the function of the Paxos (RSL) system itself. *) +(***************************************************************************) +PaxosVars == << + Leader, + ReplicatedLog, + ExecutionCounter, + LastVotePayload +>> + +(***************************************************************************) +(* Variables relating to the checkpoint coordination system logic. *) +(***************************************************************************) +CheckpointVars == << + CurrentLease, + CanTakeCheckpoint, + IsTakingCheckpoint, + TimeoutCounter, + LatestCheckpoint +>> + +(***************************************************************************) +(* All variables. *) +(***************************************************************************) +AllVars == << + IsNodeUp, + NetworkPath, + Leader, + ReplicatedLog, + ExecutionCounter, + LastVotePayload, + CurrentLease, + CanTakeCheckpoint, + IsTakingCheckpoint, + TimeoutCounter, + LatestCheckpoint +>> + +(***************************************************************************) +(* An arbitrary value not in the set of all nodes. *) +(***************************************************************************) +NoNode == CHOOSE n : n \notin Node + +(***************************************************************************) +(* The set of all logs, the values of which are decided by Paxos. *) +(***************************************************************************) +Log == Seq(Node \cup {NoNode}) + +(***************************************************************************) +(* The set of all log indices. *) +(***************************************************************************) +LogIndex == Nat \ {0} + +(***************************************************************************) +(* The very first log index. *) +(***************************************************************************) +MinLogIndex == 1 + +(***************************************************************************) +(* A blank log. *) +(***************************************************************************) +BlankLog == [i \in LogIndex |-> NoNode] + +(***************************************************************************) +(* The set of all log checkpoints. *) +(***************************************************************************) +LogCheckpoint == [ + log : Log, \* The saved log entries + counter : LogIndex \* Highest log index in checkpoint, exclusive +] + +(***************************************************************************) +(* The set of all log checkpoint leases. *) +(***************************************************************************) +CheckpointLease == [ + node : Node, \* The node to which the checkpoint lease applies + counter : LogIndex \* The log index at which the lease was issued +] + +(***************************************************************************) +(* Value indicating no checkpoint lease. *) +(***************************************************************************) +NoCheckpointLease == CHOOSE lease : lease \notin CheckpointLease + +(***************************************************************************) +(* Reads the value from the index of the node's log. *) +(***************************************************************************) +ReadLog(node, index) == + IF index \in DOMAIN ReplicatedLog[node] + THEN ReplicatedLog[node][index] + ELSE NoNode + +(***************************************************************************) +(* Writes the value to the index of the node's log. *) +(***************************************************************************) +WriteLog(node, index, value) == [ + [i \in LogIndex |-> ReadLog(node, i)] EXCEPT ![index] = value +] + +(***************************************************************************) +(* Merges the logs of two replicas. Replica logs can differ if one was *) +(* unable to receive messages from the leader. While replica logs can be *) +(* missing values, they will never have conflicting values for any index. *) +(***************************************************************************) +MergeLogs(srcNode, dstNode) == [ + i \in LogIndex |-> + IF ReadLog(dstNode, i) /= NoNode + THEN ReadLog(dstNode, i) + ELSE ReadLog(srcNode, i) +] + +(***************************************************************************) +(* The set of all unused log indices. *) +(***************************************************************************) +OpenIndices == { + i \in LogIndex : + \A n \in Node : + ReadLog(n, i) = NoNode +} + +(***************************************************************************) +(* Finds the first unused replicated log index. *) +(***************************************************************************) +FirstOpenIndex == + CHOOSE index \in OpenIndices : + \A other \in OpenIndices : + index <= other + +(***************************************************************************) +(* The type invariant of all variables. *) +(***************************************************************************) +TypeInvariant == + /\ IsNodeUp \in [Node -> BOOLEAN] + /\ NetworkPath \in [Node \X Node -> BOOLEAN] + /\ Leader \in Node \cup {NoNode} + /\ ReplicatedLog \in [Node -> Log] + /\ ExecutionCounter \in [Node -> LogIndex] + /\ LastVotePayload \in [Node -> LogIndex] + /\ CurrentLease \in [Node -> (CheckpointLease \cup {NoCheckpointLease})] + /\ CanTakeCheckpoint \in [Node -> BOOLEAN] + /\ IsTakingCheckpoint \in [Node -> BOOLEAN] + /\ TimeoutCounter \in LogIndex + /\ LatestCheckpoint \in LogCheckpoint + +(***************************************************************************) +(* Safety checks which must hold in all states for the system to be *) +(* considered functional. *) +(***************************************************************************) +SafetyInvariant == + /\ Leader /= NoNode => + \* The leader cannot take a checkpoint + /\ ~CanTakeCheckpoint[Leader] + /\ ~IsTakingCheckpoint[Leader] + \* If the leader doesn't know about a lease, neither does any node + /\ CurrentLease[Leader] = NoCheckpointLease => + /\ \A n \in Node : + /\ ~CanTakeCheckpoint[n] + /\ ~IsTakingCheckpoint[n] + \* If the leader knows about a lease, only that node can checkpoint + /\ CurrentLease[Leader] /= NoCheckpointLease => + /\ \A n \in Node : + /\ (CanTakeCheckpoint[n] \/ IsTakingCheckpoint[n]) => + /\ CurrentLease[Leader].node = n + \* Two nodes can't take a checkpoint simultaneously + /\ \A n1, n2 \in Node : + /\ (CanTakeCheckpoint[n1] /\ CanTakeCheckpoint[n2]) => + /\ n1 = n2 + /\ (IsTakingCheckpoint[n1] /\ IsTakingCheckpoint[n2]) => + /\ n1 = n2 + \* Prerequisites for taking a checkpoint must be satisfied + /\ \A n \in Node : + /\ IsTakingCheckpoint[n] => CanTakeCheckpoint[n] + /\ CanTakeCheckpoint[n] => (CurrentLease[n] /= NoCheckpointLease) + /\ CanTakeCheckpoint[n] => CurrentLease[n].node = n + /\ CanTakeCheckpoint[n] => CurrentLease[n].counter >= TimeoutCounter + \* Replicated logs can never conflict + /\ \A i \in LogIndex : + /\ \A n1, n2 \in Node : + \/ ReadLog(n1, i) = NoNode + \/ ReadLog(n2, i) = NoNode + \/ ReadLog(n1, i) = ReadLog(n2, i) + +(***************************************************************************) +(* Expectations about system capabilities. *) +(***************************************************************************) +TemporalInvariant == + \* Eventually, a checkpoint can be taken + /\ <>(\E n \in Node : CanTakeCheckpoint[n]) + \* If a node can take a checkpoint, eventually it will take a checkpoint + /\ \A n \in Node : + /\ CanTakeCheckpoint[n] ~> + \/ IsTakingCheckpoint[n] + \/ ~IsNodeUp[n] + \/ CurrentLease[n].counter < TimeoutCounter + \* If a node takes a checkpoint, eventually it will complete or timeout + /\ \A n \in Node : + /\ IsTakingCheckpoint[n] ~> + \/ LastVotePayload[n] = ExecutionCounter[n] + \/ ~IsNodeUp[n] + \/ CurrentLease[n].counter < TimeoutCounter + \* Eventually, a checkpoint will be completed + /\ <>(LatestCheckpoint /= BlankLog) + +(***************************************************************************) +(* Whether the dst node will receive a message from the src node. *) +(***************************************************************************) +ConnectedOneWay(src, dst) == + /\ IsNodeUp[src] + /\ IsNodeUp[dst] + /\ NetworkPath[src, dst] + +(***************************************************************************) +(* Whether the two nodes can talk to one another. *) +(***************************************************************************) +Connected(src, dst) == + /\ ConnectedOneWay(src, dst) + /\ ConnectedOneWay(dst, src) + +(***************************************************************************) +(* Whether we have quorum from the given prospective leader node. *) +(***************************************************************************) +HaveQuorumFrom[leader \in Node] == + LET available == {n \in Node : Connected(leader, n)} IN + /\ IsNodeUp[leader] + /\ Cardinality(available) >= Majority + +(***************************************************************************) +(* Whether we have a leader and that leader has quorum. *) +(***************************************************************************) +HaveQuorum == + /\ Leader /= NoNode + /\ HaveQuorumFrom[Leader] + +(***************************************************************************) +(* A node fails, losing all volatile local state. *) +(***************************************************************************) +NodeFailure(n) == + /\ IsNodeUp' = [IsNodeUp EXCEPT ![n] = FALSE] + /\ Leader' = IF n = Leader THEN NoNode ELSE Leader + /\ ExecutionCounter' = [ExecutionCounter EXCEPT ![n] = MinLogIndex] + /\ LastVotePayload' = [LastVotePayload EXCEPT ![n] = MinLogIndex] + /\ CurrentLease' = [CurrentLease EXCEPT ![n] = NoCheckpointLease] + /\ CanTakeCheckpoint' = [CanTakeCheckpoint EXCEPT ![n] = FALSE] + /\ IsTakingCheckpoint' = [IsTakingCheckpoint EXCEPT ![n] = FALSE] + /\ UNCHANGED <> + /\ UNCHANGED <> + /\ UNCHANGED <> + +(***************************************************************************) +(* A node recovers. State is first rehydrated from the last checkpoint, *) +(* with the node's locally-persisted log filling in any gaps after that. *) +(***************************************************************************) +NodeRecovery(n) == + /\ ~IsNodeUp[n] + /\ IsNodeUp' = [IsNodeUp EXCEPT ![n] = TRUE] + /\ ReplicatedLog' = + [ReplicatedLog EXCEPT ![n] = + SubSeq(LatestCheckpoint.log, MinLogIndex, LatestCheckpoint.counter - 1) + \o SubSeq(@, LatestCheckpoint.counter, Len(@))] + /\ ExecutionCounter' = [ExecutionCounter EXCEPT ![n] = LatestCheckpoint.counter] + /\ LastVotePayload' = [LastVotePayload EXCEPT ![n] = MinLogIndex] + /\ CurrentLease' = [CurrentLease EXCEPT ![n] = NoCheckpointLease] + /\ CanTakeCheckpoint' = [CanTakeCheckpoint EXCEPT ![n] = FALSE] + /\ IsTakingCheckpoint' = [IsTakingCheckpoint EXCEPT ![n] = FALSE] + /\ UNCHANGED <> + /\ UNCHANGED <> + /\ UNCHANGED <> + +(***************************************************************************) +(* A network link between two nodes fails in one direction. *) +(***************************************************************************) +NetworkFailure(src, dst) == + /\ src /= dst + /\ NetworkPath' = [NetworkPath EXCEPT ![src, dst] = FALSE] + /\ UNCHANGED <> + /\ UNCHANGED PaxosVars + /\ UNCHANGED CheckpointVars + +(***************************************************************************) +(* A network link between two nodes recovers. *) +(***************************************************************************) +NetworkRecovery(src, dst) == + /\ NetworkPath' = [NetworkPath EXCEPT ![src, dst] = TRUE] + /\ UNCHANGED <> + /\ UNCHANGED PaxosVars + /\ UNCHANGED CheckpointVars + +(***************************************************************************) +(* Elects a new leader if one is not currently elected. *) +(* We can safely assume nodes currently taking a backup are excluded from *) +(* the leader election process, because their state is too far behind. *) +(* The leader is required to be completely caught up, and thus cannot have *) +(* any unprocessed replicated requests. *) +(***************************************************************************) +ElectLeader(n) == + /\ Leader = NoNode + /\ IsNodeUp[n] + /\ ~IsTakingCheckpoint[n] + /\ HaveQuorumFrom[n] + /\ ExecutionCounter[n] = FirstOpenIndex + /\ Leader' = n + /\ CanTakeCheckpoint' = [CanTakeCheckpoint EXCEPT ![n] = FALSE] + /\ UNCHANGED EnvironmentVars + /\ UNCHANGED <> + /\ UNCHANGED <> + + +(***************************************************************************) +(* Critical logic determining whether we should replace the current lease. *) +(***************************************************************************) +ShouldReplaceLease(currentLease) == + \* Current lease has timed out + \/ currentLease.counter < TimeoutCounter + \* Snapshot has been completed & reported to leader by node + \/ /\ Connected(Leader, currentLease.node) + /\ currentLease.counter < LastVotePayload[currentLease.node] + +(***************************************************************************) +(* The leader designates an arbitrary node to take a checkpoint. This is *) +(* done by sending a replicated request to all nodes in the quorum. The *) +(* request contains the node selected to perform a checkpoint. *) +(***************************************************************************) +SendReplicatedRequest(prospect) == + LET currentLease == CurrentLease[Leader] IN + LET index == FirstOpenIndex IN + /\ HaveQuorum + /\ Leader /= prospect + /\ Connected(Leader, prospect) + /\ currentLease /= NoCheckpointLease => ShouldReplaceLease(currentLease) + /\ ReplicatedLog' = + [n \in Node |-> + IF ConnectedOneWay(Leader, n) + THEN WriteLog(n, index, prospect) + ELSE ReplicatedLog[n]] + /\ CurrentLease' = [ + CurrentLease EXCEPT ![Leader] = [ + node |-> prospect, + counter |-> index + ] + ] + /\ UNCHANGED EnvironmentVars + /\ UNCHANGED <> + /\ UNCHANGED <> + +(***************************************************************************) +(* Propagates chosen values to a node which might have missed them. *) +(***************************************************************************) +PropagateReplicatedRequest(src, dst) == + /\ ConnectedOneWay(src, dst) + /\ ReplicatedLog' = [ReplicatedLog EXCEPT ![dst] = MergeLogs(src, dst)] + /\ UNCHANGED EnvironmentVars + /\ UNCHANGED <> + /\ UNCHANGED CheckpointVars + +(***************************************************************************) +(* The node processes a replicated request. If the request specifies the *) +(* node processing the request, and the node is not currently leader, then *) +(* the node marks itself as able to take a checkpoint. *) +(***************************************************************************) +ProcessReplicatedRequest(n) == + LET request == ReadLog(n, ExecutionCounter[n]) IN + LET isTimedOut == ExecutionCounter[n] < TimeoutCounter IN + /\ IsNodeUp[n] + /\ ~IsTakingCheckpoint[n] + /\ request /= NoNode + /\ CanTakeCheckpoint' = [ + CanTakeCheckpoint EXCEPT ![n] = + /\ Leader /= n + /\ n = request + /\ ~isTimedOut + ] + /\ CurrentLease' = + IF n = Leader + THEN CurrentLease + ELSE [ + CurrentLease EXCEPT ![n] = + IF isTimedOut + THEN NoCheckpointLease + ELSE [node |-> request, counter |-> ExecutionCounter[n]] + ] + /\ ExecutionCounter' = [ExecutionCounter EXCEPT ![n] = @ + 1] + /\ UNCHANGED EnvironmentVars + /\ UNCHANGED <> + /\ UNCHANGED <> + +(***************************************************************************) +(* A node begins a checkpoint if it believes it is able. *) +(***************************************************************************) +StartCheckpoint(n) == + /\ CanTakeCheckpoint[n] + /\ IsTakingCheckpoint' = [IsTakingCheckpoint EXCEPT ![n] = TRUE] + /\ UNCHANGED EnvironmentVars + /\ UNCHANGED PaxosVars + /\ UNCHANGED <> + +(***************************************************************************) +(* Completes a checkpoint successfully. *) +(***************************************************************************) +FinishCheckpoint(n) == + /\ IsTakingCheckpoint[n] + /\ LastVotePayload' = [LastVotePayload EXCEPT ![n] = ExecutionCounter[n]] + /\ CurrentLease' = [CurrentLease EXCEPT ![n] = NoCheckpointLease] + /\ CanTakeCheckpoint' = [CanTakeCheckpoint EXCEPT ![n] = FALSE] + /\ IsTakingCheckpoint' = [IsTakingCheckpoint EXCEPT ![n] = FALSE] + /\ LatestCheckpoint' = [ + log |-> SubSeq( + ReplicatedLog[n], + MinLogIndex, + ExecutionCounter[n] - 1 + ), + counter |-> ExecutionCounter[n] + ] + /\ UNCHANGED EnvironmentVars + /\ UNCHANGED <> + /\ UNCHANGED <> + +(***************************************************************************) +(* Increments the timeout counter; while in a real-world system we can't *) +(* expect every node to have its local time flow at the same rate, the *) +(* specific system being modeled will drop a node from the replica set if *) +(* its time dilation is beyond a small margin relative to the primary. *) +(***************************************************************************) +TriggerTimeout == + /\ \E n \in Node : ReadLog(n, TimeoutCounter) /= NoNode + /\ TimeoutCounter' = TimeoutCounter + 1 + /\ CanTakeCheckpoint' = [ + n \in Node |-> + /\ CanTakeCheckpoint[n] + /\ CurrentLease[n].counter > TimeoutCounter + ] + /\ IsTakingCheckpoint' = [ + n \in Node |-> + /\ IsTakingCheckpoint[n] + /\ CurrentLease[n].counter > TimeoutCounter + ] + /\ UNCHANGED EnvironmentVars + /\ UNCHANGED PaxosVars + /\ UNCHANGED <> + +(***************************************************************************) +(* The initial system state. All nodes healthy, log is blank. *) +(***************************************************************************) +Init == + /\ IsNodeUp = [n \in Node |-> TRUE] + /\ NetworkPath = [src, dst \in Node |-> TRUE] + /\ Leader = NoNode + /\ ReplicatedLog = [n \in Node |-> BlankLog] + /\ ExecutionCounter = [n \in Node |-> MinLogIndex] + /\ LastVotePayload = [n \in Node |-> MinLogIndex] + /\ CurrentLease = [n \in Node |-> NoCheckpointLease] + /\ CanTakeCheckpoint = [n \in Node |-> FALSE] + /\ IsTakingCheckpoint = [n \in Node |-> FALSE] + /\ TimeoutCounter = MinLogIndex + /\ LatestCheckpoint = [log |-> BlankLog, counter |-> MinLogIndex] + +(***************************************************************************) +(* The next-state relation. *) +(***************************************************************************) +Next == + \/ \E n \in Node : NodeFailure(n) + \/ \E n \in Node : NodeRecovery(n) + \/ \E src, dst \in Node : NetworkFailure(src, dst) + \/ \E src, dst \in Node : NetworkRecovery(src, dst) + \/ \E n \in Node : ElectLeader(n) + \/ \E n \in Node : SendReplicatedRequest(n) + \/ \E src, dst \in Node : PropagateReplicatedRequest(src, dst) + \/ \E n \in Node : ProcessReplicatedRequest(n) + \/ \E n \in Node : StartCheckpoint(n) + \/ \E n \in Node : FinishCheckpoint(n) + \/ TriggerTimeout + +(***************************************************************************) +(* Assumptions that good things eventually happen. *) +(***************************************************************************) +TemporalAssumptions == + /\ \A n \in Node : WF_AllVars(NodeRecovery(n)) + /\ \A src, dst \in Node : WF_AllVars(NetworkRecovery(src, dst)) + /\ \A n \in Node : SF_AllVars(ElectLeader(n)) + /\ \A n \in Node : SF_AllVars(SendReplicatedRequest(n)) + /\ \A src, dst \in Node : SF_AllVars(PropagateReplicatedRequest(src, dst)) + /\ \A n \in Node : SF_AllVars(ProcessReplicatedRequest(n)) + /\ \A n \in Node : SF_AllVars(StartCheckpoint(n)) + /\ \A n \in Node : SF_AllVars(FinishCheckpoint(n)) + +(***************************************************************************) +(* The spec, defining the set of all system behaviours. *) +(***************************************************************************) +Spec == + /\ Init + /\ [][Next]_AllVars + /\ TemporalAssumptions + +(***************************************************************************) +(* Want to show: the set of all behaviours satisfies our requirements. *) +(***************************************************************************) +THEOREM Spec => + /\ []TypeInvariant + /\ []SafetyInvariant + /\ []TemporalInvariant + +============================================================================= + diff --git a/specifications/CheckpointCoordination/MCCheckpointCoordination.cfg b/specifications/CheckpointCoordination/MCCheckpointCoordination.cfg new file mode 100644 index 00000000..853964ae --- /dev/null +++ b/specifications/CheckpointCoordination/MCCheckpointCoordination.cfg @@ -0,0 +1,29 @@ +\* Finishes in around one minute + +SPECIFICATION + Spec + +CONSTANTS + Node = {n1,n2,n3} + Majority = 2 + +CONSTANTS + MaxLog = 3 + MaxNat = 5 + +CONSTANTS + Nat <- MCNat + LogIndex <- MCLogIndex + NoNode = NoNode + NoCheckpointLease = NoCheckpointLease + +INVARIANTS + TypeInvariant + SafetyInvariant + +CONSTRAINT + StateConstraint + +SYMMETRY + NodeSymmetry + diff --git a/specifications/CheckpointCoordination/MCCheckpointCoordination.tla b/specifications/CheckpointCoordination/MCCheckpointCoordination.tla new file mode 100644 index 00000000..44679af1 --- /dev/null +++ b/specifications/CheckpointCoordination/MCCheckpointCoordination.tla @@ -0,0 +1,21 @@ +---------------------- MODULE MCCheckpointCoordination ---------------------- +EXTENDS CheckpointCoordination, FiniteSets, Naturals, TLC + +CONSTANTS MaxLog, MaxNat + +MCNat == 0..MaxNat + +MCLogIndex == 1..MaxLog + +StateConstraint == OpenIndices /= {} + +NodeSymmetry == Permutations(Node) + +IncorrectlyOptimizedShouldReplaceLease(currentLease) == + LET CC == INSTANCE CheckpointCoordination IN + \/ CC!ShouldReplaceLease(currentLease) + \* (Bad optimization) lease is held by the current leader + \/ currentLease.node = Leader + +============================================================================= + diff --git a/specifications/CheckpointCoordination/MCCheckpointCoordinationFailure.cfg b/specifications/CheckpointCoordination/MCCheckpointCoordinationFailure.cfg new file mode 100644 index 00000000..e65cd897 --- /dev/null +++ b/specifications/CheckpointCoordination/MCCheckpointCoordinationFailure.cfg @@ -0,0 +1,28 @@ +SPECIFICATION + Spec + +CONSTANTS + Node = {n1,n2,n3} + Majority = 2 + +CONSTANTS + MaxLog = 3 + MaxNat = 5 + +CONSTANTS + Nat <- MCNat + LogIndex <- MCLogIndex + ShouldReplaceLease <- IncorrectlyOptimizedShouldReplaceLease + NoNode = NoNode + NoCheckpointLease = NoCheckpointLease + +INVARIANTS + TypeInvariant + SafetyInvariant + +CONSTRAINT + StateConstraint + +SYMMETRY + NodeSymmetry + diff --git a/specifications/CheckpointCoordination/README.md b/specifications/CheckpointCoordination/README.md new file mode 100644 index 00000000..ada4fa02 --- /dev/null +++ b/specifications/CheckpointCoordination/README.md @@ -0,0 +1,154 @@ +# Ringmaster Checkpoint Coordination + +This spec was written in June 2017 while the author worked in Microsoft Azure Networking, on the Azure DNS team. +At the time the Azure DNS backend used an in-memory tree database called [RingMaster](https://github.com/Azure/RingMaster) built on top of a Paxos implementation called the [Replicated State Library (RSL)](https://github.com/Azure/RSL). +Both of those systems were long ago released as open source, and now this spec has followed. +This spec was written while designing a checkpoint/backup coordination feature described below. +It is notable for two reasons: + 1. The TLC model checker found a 12-step error trace for a very subtle bug introduced by an attempted optimization + 2. The actual feature was implemented directly after the spec was written, providing an account of the experience of writing a program following a TLA⁺ spec + +Both of these points are covered in detail in [this](https://ahelwer.ca/post/2023-04-05-checkpoint-coordination) blog post. +What follows is the informal-language feature spec distributed alongside the TLA⁺ spec. + +## The Problem + +### Summary & Motivation + +There are five replicas in a Ring Master cluster, one of which is elected primary at any given time. +The other four replicas are secondaries. +These secondaries must occasionally take a checkpoint of their local state and upload the resulting codex to cloud storage as a backup. +Currently, the secondaries take checkpoints at random. +This means that occasionally multiple secondary replicas take checkpoints simultaneously. +We want to begin performing read operations on secondaries, which is not possible while they are taking a checkpoint. +Thus, we want only one secondary replica to take a checkpoint at any given time. +We furthermore wish for the replicas to rotate evenly through taking a checkpoint. +This is a distributed coordination problem. + +### Invariants + +The system has the following invariants, which must hold true in every state: + + * Safety invariant: the primary never takes a checkpoint + * Safety invariant: multiple secondary replicas never take a checkpoint concurrently + * Temporal invariant: all secondary replicas eventually take a checkpoint + * Temporal invariant: a checkpoint always eventually completes or is aborted + +### Failure Model + +We want our system to gracefully handle the following failure modes: + + * Replicas crashing, then later recovering + * Network links failing between any two replicas in the cluster, then recovering + * The rate of passage of time differing between replicas + +### Discarded Approaches + +We considered a simple time slice approach, where each replica is allocated a slice of time in an uncoordinated round-robin fashion. +For example, each replica calculates the number of hours passed since some shared fixed date in the past modulo the number of replicas in the cluster; the result maps uniquely onto a replica in the cluster, which has that hour to take a checkpoint. +This approach was discarded with the following objections: + + * Requires coordination mechanism to adaptively vary time slice size, removing advantage + * Local time passage rate can vary between replicas, causing them to drift out of coordination + * Inefficient: primary does not take backup, so hour is wasted; similar if replica is down + +We considered an approach like the above based on RSL decree numbers instead of real time, but this was considered unreliable as the rate of new decrees can vary widely; this gives inconsistent slices of real time to take a checkpoint. + +## Solution + +### Outline + +We developed a randomized turn-based solution: the primary selects a secondary replica to take a checkpoint, weighted so healthier replicas are selected more often. +The primary then uses the RSL consensus mechanism (via the `ManagedRSLStateMachine.ReplicateRequest` method) to issue a checkpoint lease to the selected secondary. + +Secondary replicas receive & process the checkpoint lease message via their implementation of the abstract `ManagedRSLStateMachine.ExecuteReplicatedRequest` method. +If the checkpoint lease applies to the secondary replica processing the message, it schedules a checkpoint. + +### Sub-Problem: Checkpoint Lease Revocation + +A problem arises with checkpoint timeouts & aborts: once a secondary replica begins taking a checkpoint, it stops processing further replicated requests (although it continues to participate in the RSL Paxos rounds); the requests are stored in a log to be executed after checkpoint completion. +Thus, we lack a mechanism for the primary to directly revoke a secondary's checkpoint lease. + +The “best” solution to the checkpoint lease revocation problem is a modification to the RSL library itself exposing a separate checkpoint coordination-specific API which executes regardless of whether the secondary is taking a checkpoint, but in the interest of simplicity and expediency we are instead using coordinated timeouts between primary and secondary. +This means the primary will decide on a local timeout after which it will issue a new checkpoint lease; the same timeout is also given to the secondary, which is assumed to be running in a similar reference frame. +When the timeout expires on the secondary, it is expected to abort its checkpoint if not yet complete. + +The timeout coordination solution to the checkpoint lease revocation problem runs afoul of our failure model: we cannot assume time passes at the same rate on each replica. +However, RSL's heartbeat system ensures a difference of at most 30% (configurable) in time passed between primary and secondary – so one second on the primary synchronizes with at least 0.7 seconds on the secondary. +Thus, if the secondary sets its checkpoint timeout as 70% of the timeout given by the primary, it is guaranteed to either finish its checkpoint before the timeout, timeout before the primary, or be kicked out of the replica set. + +### Sub-Problem: Adaptive Checkpoint Timeouts + +To avoid manual intervention, the timeout decided by the primary must adapt to reality. +If a replica times out before completing a checkpoint, the primary should allocate a larger length of time. +Inversely, if a replica completes a checkpoint before timeout this may mean the timeout is too long and should be adjusted downward. +The adaptive timeout calculation has one requirement: secondaries communicate their checkpoint completion (or lack thereof) back to the primary. +Replica health reports contain a 64-bit field (`ManagedReplicaHealth.LastVotePayload`) for piggybacking status updates to the primary. +Upon completion of a checkpoint, a secondary will persistently fill this payload with the RSL sequence number up to which the checkpoint applied (it is zero by default). +The primary will either see this value and register completion of the checkpoint, or fail to see the value within its local timeout period and register a timeout. + +A global absolute maximum timeout is pre-defined to cap runaway checkpoint time budgets. + +### Sub-Problem: Lease Handover on Primary Failover + +The case of primary failover during an active checkpoint lease requires special scrutiny. +First, note that the new primary will have seen and executed the replicated request containing the currently-active checkpoint lease, as a secondary. +We know this because we require replicas to be fully caught up before being elected primary. +The new primary maintained this lease data in-memory, and upon primary election appears situated to properly calculate the timeout of the current lease. +There is, however, a possible problem – what if the new primary is in a reference frame where time runs faster than the reference frame of the old secondary? +For example: + +| Role | Time Dilation | Lease Start Time | Elapsed Local Time | Local Time | +| ----------- | ------------- | ---------------- | ------------------ | ----------- | +| Old Primary | 1.0x | T = 0 | 10s | T = 10s | +| Secondary | 1.25x | T' = 0 | 8s | T' = 8s | +| New Primary | 0.8x | T'' = 0 | 12.5s | T'' = 12.5s | + +If the checkpoint lease was issued by the old primary to the secondary at T = 0 with a local timeout of 10 seconds, then the secondary uses a local timeout of 0.7\*10 = 7 seconds. +Consider a primary failover at T = 8s, so T' = 6.4s and T'' = 10s. +We might be concerned that the new primary believes the lease has timed out, so issues a new lease to a different replica – thus violating our safety invariant of never having multiple replicas taking a checkpoint concurrently. +However, if we can rely on the RSL heartbeat system to instantly boot the secondary from the replica set (since its time dilation relative to the primary is 1.6, below the 70% threshold) once the new primary comes online, this problem is taken care of. + +### Sub-Problem: Primary Lacks Knowledge of Lease + +Will there ever be a case where a replica becomes primary with no knowledge of an active checkpoint lease, despite such a lease existing? +Let us consider cases where a replica becomes leader without knowledge of an active checkpoint lease, regardless of whether such a lease exists: + + * The cluster was just created and no checkpoint lease has yet been issued in its history + * A somewhat complicated execution trace: + 1. Checkpoint lease given to secondary A + 2. Secondary A finishes checkpoint before timeout + 3. Secondary B dies + 4. Secondary B recovers + 5. Secondary B is rehydrated from checkpoint created by secondary A + 6. Leader dies + 7. Secondary B becomes leader + +In both cases, even though no knowledge of an existing lease is present, it is safe for the primary to issue a new lease immediately. +In the second case, we are saved by the requirement that all replicas elected leader must have executed (not merely possessed) all chosen transactions before acting as leader. +If our requirement were weaker – a replica can be elected by possessing all transactions but not executing them – then we could possibly issue a new checkpoint lease while an existing checkpoint lease sits in our log of unprocessed transactions. + +### Pitfall: Attempted Optimization of Lease Pre-emption + +The original system design optimized the case of a node being elected leader while in possession of the most-current checkpoint lease. +Since the leader cannot take a checkpoint, the node would immediately issue a new checkpoint lease to one of the secondaries. +However, this resulted in the following twelve-step error trace for a three-node system: +1. Initial state with nodes `n1`, `n2`, and `n3` +2. `n1` elected leader +3. `n1` sends replicated request `1` assigning checkpoint lease to `n2` +4. `n1` dies +5. `n2` executes replicated request `1` and marks self as able to take checkpoint +6. `n2` elected leader +7. `n2` sees self in possession of checkpoint lease, so (using optimization rule) pre-empts it and issues replicated request `2` assigning checkpoint lease to `n3` +8. `n2` dies +9. `n2` recovers +10. `n2` executes replicated request `1` again, marks self able to take checkpoint +11. `n3` executes replicated request `1`, knows `n2` can take checkpoint +12. `n3` executes replicated request `2`, marks self able to take checkpoint + +So between steps 10 and 12, both `n2` and `n3` end up believing they can take a checkpoint: a violation of our invariant that it is never the case that multiple nodes believe they can take a checkpoint simultaneously. +This is all due to the use of the lease pre-emption optimization in step 7. +Removing this attempted optimization rule solves the problem; instead of issuing a new lease immediately, the leader node simply waits for the lease (extended to itself) to time out before issuing another. + +The `MCCheckpointCoordinationFailure.cfg` model reproduces the above error trace. + diff --git a/specifications/LearnProofs/AddTwo.tla b/specifications/LearnProofs/AddTwo.tla new file mode 100644 index 00000000..ed51bedb --- /dev/null +++ b/specifications/LearnProofs/AddTwo.tla @@ -0,0 +1,85 @@ +------------------------------ MODULE AddTwo -------------------------------- +(***************************************************************************) +(* Defines a very simple algorithm that continually increments a variable *) +(* by 2. We try to prove that this variable is always divisible by 2. *) +(* This was created as an exercise in learning the absolute basics of the *) +(* proof language. *) +(***************************************************************************) + +EXTENDS Naturals, TLAPS + +(**************************************************************************** +--algorithm Increase { + variable x = 0; { + while (TRUE) { + x := x + 2 + } + } +} +****************************************************************************) +\* BEGIN TRANSLATION (chksum(pcal) = "b4b07666" /\ chksum(tla) = "8adfa002") +VARIABLE x + +vars == << x >> + +Init == (* Global variables *) + /\ x = 0 + +Next == x' = x + 2 + +Spec == Init /\ [][Next]_vars + +\* END TRANSLATION + +TypeOK == x \in Nat + +THEOREM TypeInvariant == Spec => []TypeOK + <1>a. Init => TypeOK + BY DEF Init, TypeOK + <1>b. TypeOK /\ UNCHANGED vars => TypeOK' + BY DEF TypeOK, vars + <1>c. TypeOK /\ Next => TypeOK' + <2> SUFFICES + ASSUME TypeOK, Next + PROVE TypeOK' + <2> USE DEF TypeOK, Next + <2>1. x \in Nat + <2>2. x + 2 \in Nat + <3>1. \A n \in Nat : n + 2 \in Nat + OBVIOUS + <3> QED BY <3>1, <2>1 + <2>3. x' \in Nat BY <2>1, <2>2 + <2>4. TypeOK' BY <2>3 + <2> QED BY <2>4 + <1> QED BY PTL, <1>a, <1>b, <1>c DEF Spec + +a|b == \E c \in Nat : a*c = b + +AlwaysEven == 2|x + +THEOREM Spec => []AlwaysEven + <1>a. Init => AlwaysEven + BY DEF Init, AlwaysEven, | + <1>b. AlwaysEven /\ UNCHANGED vars => AlwaysEven' + BY DEF AlwaysEven, vars + <1>c. AlwaysEven /\ Next => AlwaysEven' + <2> SUFFICES + ASSUME AlwaysEven, Next + PROVE AlwaysEven' + <2> USE DEF AlwaysEven, Next + <2>a. PICK c \in Nat : 2 * c = x BY DEF | + <2>b. 2*(c + 1) = x + 2 BY <2>a + <2>c. \E n \in Nat : 2*n = x + 2 + \* We specify the Isabelle prover here to save some time + <3> SUFFICES ASSUME (c + 1) \in Nat + PROVE 2*(c + 1) = x + 2 + BY Isa + <3>b. (c + 1) \in Nat BY <2>a + <3>c. 2*(c + 1) = x + 2 BY <2>b + <3> QED BY <3>c + <2>d. x' = x + 2 BY DEF Next + <2> QED BY <2>c, <2>d DEF | + <1> QED BY PTL, <1>a, <1>b, <1>c DEF Spec + +============================================================================= + diff --git a/specifications/LearnProofs/FindHighest.tla b/specifications/LearnProofs/FindHighest.tla new file mode 100644 index 00000000..71ddd62f --- /dev/null +++ b/specifications/LearnProofs/FindHighest.tla @@ -0,0 +1,243 @@ +---------------------------- MODULE FindHighest ----------------------------- +(***************************************************************************) +(* Defines a very simple algorithm that finds the largest value in a *) +(* sequence of Natural numbers. This was created as an exercise in finding *) +(* & proving type invariants, inductive invariants, and correctness. *) +(***************************************************************************) + +EXTENDS Sequences, Naturals, Integers, TLAPS + +(**************************************************************************** +--algorithm Highest { + variables + f \in Seq(Nat); + h = -1; + i = 1; + define { + max(a, b) == IF a >= b THEN a ELSE b + } { +lb: while (i <= Len(f)) { + h := max(h, f[i]); + i := i + 1; + } + } +} +****************************************************************************) +\* BEGIN TRANSLATION (chksum(pcal) = "31f24270" /\ chksum(tla) = "819802c6") +VARIABLES f, h, i, pc + +(* define statement *) +max(a, b) == IF a >= b THEN a ELSE b + + +vars == << f, h, i, pc >> + +Init == (* Global variables *) + /\ f \in Seq(Nat) + /\ h = -1 + /\ i = 1 + /\ pc = "lb" + +lb == /\ pc = "lb" + /\ IF i <= Len(f) + THEN /\ h' = max(h, f[i]) + /\ i' = i + 1 + /\ pc' = "lb" + ELSE /\ pc' = "Done" + /\ UNCHANGED << h, i >> + /\ f' = f + +(* Allow infinite stuttering to prevent deadlock on termination. *) +Terminating == pc = "Done" /\ UNCHANGED vars + +Next == lb + \/ Terminating + +Spec == Init /\ [][Next]_vars + +Termination == <>(pc = "Done") + +\* END TRANSLATION + +\* The type invariant; the proof system likes knowing variables are in Nat. +\* It's a good idea to check these invariants with the model checker before +\* trying to prove them. To quote Leslie Lamport, it's very difficult to +\* prove something that isn't true! +TypeOK == + /\ f \in Seq(Nat) + /\ i \in 1..(Len(f) + 1) + /\ i \in Nat + /\ h \in Nat \cup {-1} + +\* It's useful to prove the type invariant first, so it can be used as an +\* assumption in further proofs to restrict variable values. +THEOREM TypeInvariantHolds == Spec => []TypeOK +\* To prove theorems like Spec => []Invariant, you have to: +\* 1. Prove Invariant holds in the initial state (usually trivial) +\* 2. Prove Invariant holds when variables are unchanged (usually trivial) +\* 3. Prove that assuming Invariant is true, a Next step implies Invariant' +\* The last one (inductive case) is usually quite difficult. It helps to +\* never forget you have an extremely powerful assumption: that Invariant is +\* true! +PROOF + \* The base case + <1>a. Init => TypeOK + BY DEFS Init, TypeOK + \* The stuttering case + <1>b. TypeOK /\ UNCHANGED vars => TypeOK' + BY DEFS TypeOK, vars + \* The inductive case; usually requires breaking down Next into disjuncts + <1>c. TypeOK /\ Next => TypeOK' + <2>a. TypeOK /\ lb => TypeOK' + \* SUFFICES steps transform P => Q goals into Q goals, while assuming P + <3> SUFFICES ASSUME TypeOK, lb + PROVE TypeOK' + OBVIOUS + \* Making this a non-named step expands TypeOK and lb definitions for + \* all subsequent & recursive steps in this sub-proof, without requiring + \* the step to explicitly use BY DEFS TypeOK, lb + <3> USE DEFS TypeOK, lb + <3>a. CASE i <= Len(f) BY DEF max + <3>b. CASE ~(i <= Len(f)) + <4>a. UNCHANGED <> BY <3>b + <4> QED BY <3>b, <4>a DEF lb + <3> QED BY <3>a, <3>b + <2>b. TypeOK /\ Terminating => TypeOK' + BY DEFS TypeOK, Terminating, vars + <2> QED BY <2>a, <2>b DEF Next + <1> QED BY PTL, <1>a, <1>b, <1>c DEF Spec + +\* The inductive invariant; writing these is an art. You want an invariant +\* that can be shown to be true in every state, and if it's true in all +\* states, it can be shown to imply algorithm correctness as a whole. +InductiveInvariant == + \A idx \in 1..(i - 1) : f[idx] <= h + +THEOREM InductiveInvariantHolds == Spec => []InductiveInvariant +PROOF + <1>a. Init => InductiveInvariant + BY DEFS Init, InductiveInvariant + <1>b. InductiveInvariant /\ UNCHANGED vars => InductiveInvariant' + BY DEFS InductiveInvariant, vars + \* Here we introduce TypeOK and TypeOK' as powerful assumptions, since we + \* have already proved that Spec => []TypeOK. Note that TypeOK is a + \* separate assumption from TypeOK' - including both can be the difference + \* between a proof being impossible or trivial! + <1>c. InductiveInvariant /\ TypeOK /\ TypeOK' /\ Next => InductiveInvariant' + <2>a. InductiveInvariant /\ Terminating => InductiveInvariant' + BY DEFS InductiveInvariant, Terminating, vars + <2>b. InductiveInvariant /\ TypeOK /\ TypeOK' /\ lb => InductiveInvariant' + <3> SUFFICES ASSUME InductiveInvariant, TypeOK, TypeOK', lb + PROVE InductiveInvariant' + OBVIOUS + <3> USE DEF TypeOK + <3>a. CASE i <= Len(f) + <4>a. f[i] <= h' BY <3>a DEFS lb, max + <4>b. h <= h' BY <3>a DEFS lb, max + <4>c. \A idx \in 1..i : f[idx] <= h' + BY <4>a, <4>b DEF InductiveInvariant + <4>d. i = i' - 1 BY <3>a DEF lb + <4>e. UNCHANGED f + BY DEF lb + \* These steps are annotated to use the Zenon prover, which succeeds + \* immediately; otherwise we have to wait for other solvers to have + \* their turn and fail. + <4>f. \A idx \in 1..(i' - 1) : f'[idx] <= h' + BY Zenon, <4>c, <4>d, <4>e + <4> QED + BY Zenon, <4>f DEF InductiveInvariant + <3>b. CASE ~(i <= Len(f)) + <4> UNCHANGED <> BY <3>b DEF lb + <4> QED BY DEF InductiveInvariant + <3> QED BY <3>a, <3>b DEF lb + <2> QED BY <2>a, <2>b DEF Next + \* We need to note we made use of the type invariant theorem here + <1> QED BY PTL, <1>a, <1>b, <1>c, TypeInvariantHolds DEF Spec + +\* A small sub-theorem that relates our inductive invariant to correctness +DoneIndexValue == pc = "Done" => i = Len(f) + 1 + +THEOREM DoneIndexValueThm == Spec => []DoneIndexValue +PROOF + <1>a. Init => DoneIndexValue + BY DEF Init, DoneIndexValue + <1>b. DoneIndexValue /\ UNCHANGED vars => DoneIndexValue' + BY DEFS DoneIndexValue, vars + <1>c. DoneIndexValue /\ TypeOK /\ Next => DoneIndexValue' + <2>a. DoneIndexValue /\ Terminating => DoneIndexValue' + BY DEFS DoneIndexValue, Terminating, vars + <2>b. DoneIndexValue /\ TypeOK /\ lb => DoneIndexValue' + <3> SUFFICES ASSUME DoneIndexValue, TypeOK, lb + PROVE DoneIndexValue' + OBVIOUS + <3> USE DEFS DoneIndexValue, TypeOK, lb + <3>a. CASE i <= Len(f) + <4>a. pc' /= "Done" BY <3>a + <4> QED BY <3>a, <4>a DEF lb + <3>b. CASE ~(i <= Len(f)) + <4>b. i \in 1..(Len(f) + 1) BY DEF TypeOK + <4>c. i = Len(f) + 1 BY <3>b, <4>b + <4>d. UNCHANGED <> BY <3>b + <4>e. i' = Len(f') + 1 BY <4>c, <4>d + <4>f. pc' = "Done" BY <3>b + <4> QED BY <4>e, <4>f DEF DoneIndexValue + <3> QED BY <3>a, <3>b DEF lb + <2> QED BY <2>a, <2>b DEF Next + <1> QED BY PTL, <1>a, <1>b, <1>c, TypeInvariantHolds DEF Spec + +\* The main event! After the algorithm has terminated, the variable h must +\* have value greater than or equal to any element of the sequence. +Correctness == + pc = "Done" => + \A idx \in DOMAIN f : f[idx] <= h + +THEOREM IsCorrect == Spec => []Correctness +PROOF + <1>a. Init => Correctness + BY DEF Init, Correctness + <1>b. Correctness /\ UNCHANGED vars => Correctness' + BY DEF Correctness, vars + <1>c. /\ Correctness + /\ InductiveInvariant' + /\ DoneIndexValue' + /\ Next + => Correctness' + <2>a. Correctness /\ Terminating => Correctness' + BY DEF Correctness, Terminating, vars + <2>b. + /\ Correctness + /\ InductiveInvariant' + /\ DoneIndexValue' + /\ lb + => Correctness' + <3> SUFFICES ASSUME + Correctness, + InductiveInvariant', + DoneIndexValue', + lb + PROVE + Correctness' + OBVIOUS + <3>a. CASE i <= Len(f) + <4>a. pc' /= "Done" BY <3>a DEF lb + <4> QED BY <3>a, <4>a DEFS Correctness, lb + <3>b. CASE ~(i <= Len(f)) + <4>a. pc' = "Done" BY <3>b DEF lb + <4>b. i' = Len(f') + 1 BY <4>a DEF DoneIndexValue + <4>c. DOMAIN f' = 1..Len(f') BY lb + <4>d. DOMAIN f' = 1..(i' - 1) BY <4>b, <4>c + <4>e. \A idx \in 1..(i' - 1) : f'[idx] <= h' + BY DEF InductiveInvariant + <4>f. \A idx \in DOMAIN f' : f'[idx] <= h' + BY <4>d, <4>e + <4> QED BY <4>f DEF Correctness + <3> QED BY <3>a, <3>b, lb + <2> QED BY <2>a, <2>b DEF Next + <1> QED + BY + <1>a, <1>b, <1>c, + InductiveInvariantHolds, DoneIndexValueThm, PTL + DEF Spec + +============================================================================= + diff --git a/specifications/LearnProofs/MCFindHighest.cfg b/specifications/LearnProofs/MCFindHighest.cfg new file mode 100644 index 00000000..76bb9ddc --- /dev/null +++ b/specifications/LearnProofs/MCFindHighest.cfg @@ -0,0 +1,16 @@ +SPECIFICATION Spec +\* Add statements after this line. +CONSTANT + MaxLength = 3 + MaxNat = 4 + Nat <- MCNat + Seq <- MCSeq + +INVARIANTS + TypeOK + InductiveInvariant + DoneIndexValue + Correctness + +CONSTRAINT MCConstraint + diff --git a/specifications/LearnProofs/MCFindHighest.tla b/specifications/LearnProofs/MCFindHighest.tla new file mode 100644 index 00000000..60bb7f01 --- /dev/null +++ b/specifications/LearnProofs/MCFindHighest.tla @@ -0,0 +1,13 @@ +--------------------------- MODULE MCFindHighest ---------------------------- +EXTENDS FindHighest + +CONSTANTS MaxLength, MaxNat +ASSUME MaxLength \in Nat +ASSUME MaxNat \in Nat + +MCConstraint == Len(f) <= MaxLength +MCNat == 0..MaxNat +MCSeq(S) == UNION {[1..n -> S] : n \in Nat} + +============================================================================= + diff --git a/specifications/LeastCircularSubstring/LeastCircularSubstring.pdf b/specifications/LeastCircularSubstring/LeastCircularSubstring.pdf new file mode 100644 index 0000000000000000000000000000000000000000..4de777f32ddaf6020beaae75524f8b478d0fe1e3 GIT binary patch literal 52270 zcmce;1z1#T*Eg;LA_LMP(jW*DLkuk)(%oG{cZUd)(jwj6Ez%_dA}Jt^w9=r0G|GR^ zC?3x7oacYu=l#C#nrqnm&b`*X*1Fekt$PpD3ZmkSEKHmr>h7(mY!EfIq^+x+v7xht zoh=W!nG-pq139AtBRQjqvXHo#5^$B1R}fNF76a~tg;Yc&$QhkP#ndE4#Q5w@Ox+wU zoS{ICle3APi!+}9a4YZPZ13VMZeb0D6+!Ie%;a`PmZ1Ch!7@-=GiP&h4xmN}40LdY zI+BCMtqq-_qEKTy6DU7F$jR9eYG?y;PufHK`aUC7T*y-}p=aLGYSOl3R=N2}U4MxEo#ulHQ3703 zx(N9xykzQec{Q*aD~b+=z#w>nEJMg#qnnB6WBiQfB zDQd17V;pZe%GR>G$===1t{S;_W41ZJ3VnEe@}ayjU5j#S!&(JB-m3{SpJ0Wxm$|ox zHEpQwWbpZ=o)Xbl`LEfNiAUz%m!N;L&|<9@O)7;-m`t|zoMl>T?BTQ5dKy^C1(I~e zfi44m5qN1a6p&RSbKFX@F{_OLRl}iC%^XxZuthl52Z;Vqgz&A3Fe0**{dgWpx?Zt* zIdzZryYDDXlH1bD__fy;j0*UiibDqX=s&3Fbd<7i<TkqAYSYdoZp=;>N8&7k4 zv`w2Syr%m-VeX^Qv);1M=cp`3cPF24j(CQmJWs^1f9Z64##h&4(mC0YrQbn|oj{!k zkNkS8tf}x<(5j&uS{j>1ivG?=+5*}o^Xpw2BOR_<>x)K>+bp_cX<@Aziz#~4)R;H~ z->$zPik05fJBuZL;8S1kRQomNzRV5;6f>IX^ul)9{n;z(U8E`eBzKN8Zu*gY_WRA5 zAl;-l>H=Dr~ zJ?@c+-H8Bk5=2Y12z?PJLB(#kB4GYJh@%l%dm;1M%9ZKT?fYVq!rUY|^7vH}j#M$# z%u`4jS4E6f?&e;dyGeJjE)yWAGsi>wpOSZ1T{UXu+^?ii3 ziOg*S9~X7guh-0|$WCY4FMy~7ksh+#J5&6mrXs36qxW(!C$(06f=w;%wAgSMr&!9T z#!z{Q-zkw>uu@RVdN?trHnB_{vsMjBg%4|@?3y|E8;L{aS7T?RcU!SzpDx^1v>*s0 zRQGuOaz&v|5#7A7uxsmgSoJgT0iX9;$H%)pF z`?&SM+IY{|w+Ly5ePlMQ!c@xWHUte6I9^Yk52iq0*cv3;Z-ntkns`3nPAiz91mT@N zEcaTkG-!Ns@5*GiYOZd@n8!iCV0oEZkQa>?g18H!EP}3VhMsC#^NfGdb>H=yL4-$a z#9WoP7>y7=$L1#1zW{wyeOvcld7r`!?A3@x zlBvgp-!wp(r<9}lxz9WvvK*0!6y2eFi%yA#;5$dz-PB~?yh*|*L2;ITSw086du(=0 zqVa2pjlxgfHC=mLdfK&PqS4Ieu#dyk8XY&uoOSTnslsDM8}kd3MZDHk6b_!@l$57p zSEF{X`L)z<3B|k47v{vbI_BWa#d!`v$%7Q^7Ir5Y(NJuAPs$b4glM%Tx4>vGCu-@8 zsT&=*i4Bg-<31O?xE*F`j*UYWgknBqtO0?_Pi@6+j!2`5P}?Jvq)vPKJ3kwH^|&h1 z&{fYrZ@z6WIk1gkABq@>Z8NX%{=CVd5ocj?V4-Fqo7DT-ZH@W>d5X<)REzT7d6)VN>gP@HW9f!xgN?@o+uikvm z+aiq{uFqB~KJ1YF;UPayPRWdI+4ZoD1`1vW%!S@GiI2H&`IhFCigQb!_VN?GAn9{A zYPfToSM7ChvbDY2+v(O;MWGL3inD1um?X!7(8U2Go0%+@2xZP;H?D`Y`uZ3V~F%3%E^;10%N81O!-XkYjYh!AMF0VPy6t5F)q)QhsTVkabW!~Y$1v$xl5Zp_}Bd+Z{n zHwrLRWhrWh8{&(->u|Dat!m$tQbDY0)|;64}La`(36`w9sWiimLb86)nbmD(=Z(`&c6Qlc<11Xzm3IhHh&7)Ui| z?#;Rxd9@8?b(X%k<^tvS*N-1Z!li>;am9~DekF#5!s;CT>SeDv#!UoSJ@c>>d_#p- z0?F(#e22qEyUjXTVTpqFoQ0UO;}kd$K2mKtl%5z&?h*t8{i)@51ZZ6@!bRNo!wJ27 zTwH@`RZ!>6*RScv?JK2bv0YW=oZvq6&i4H#(vo~kd^YHwF!zE+Y3U6}mR1q-I4&yQ zM+WPT;E~Soki)mlG*Na!B))e^`1)#zgf$A2hXKnz(P?1rd0+)^l6*OZ)HzYNkE z?^J5H+D_Ug(`)chA>#Mt`_^vm^|ASAj@0w@!Hrxz<8KxQ#`)3r5AEG&Bn9Jw*2koLi4OL0w>GoX*nR=>pAi$ zcior``d_WDV08r3l|)&}R^W+@>W+@fy_KrY@sWSMg)zS&D%VB6r8b$UspljXpQS)L z?1qnKGp!B9~6Uiv?a2MC9IMv!q(-wy0 zOy$?Q1?D4)wSi*ti(=mm5)m@0Iog`r7a8I>JXLffu%AZ{*qPMAP0!2>caj97MC<=+3A=9D(rS(Zn^Q*-f?3hR?XNN6M zzT3^Ygq#ml50@TcX-<4B-WR+P4gDIPQHy@Yex&JD-Nv0^Sh^oHh?9Y%dxUrBE(==`$&@#dc7Bq> zO##YuHkk;U(=V}WjEAImJIeVdS=c7M>oRJsAAI|6=rqXVS=}M-qGJCT^u}GQh9k|S zpgPQzQz0z3Rv>)kt-vH|f>(OrkQGn#+`Xo(1y*F_gzO5;hR=_#C)}r~x6KT);by}a zw?h?(TDmhjaBc2Dy}S4uE1z#H4dh&^eLL-4{_#U)wyQ0XgSY4T9^Yzu>FK^BSptkOm1)}ZDCYrH$KJ%ExryR?tt34oz7zYPHit)_)lpU| z%E-=S{g(Pf`A1Uh&=QeO9j$pEO-Fu8%$NMs$r-V`dS0Qw+Q3LTw?+^#J;mwj>eFQ2 z_i^ShFX#3>Y&`U7;=;u7b)J!U26SHT4J7EoK0pST^kgJFFb!iQa1xw)A^ zKkL}oehUQHApb5Bu!$mO$G-l>rYq_eW!h-YJBaHPQ^Kc6jPA#nv`fyF8IiuR34zvg zkxvo7?9nyNTh}#td72(fK2_wmu2?>hJ}xRqzxQ^lFQV|H_>s@{+u*n0&Xt0&1Oiq7 zUy@;D*zvbC9~}{)5NY$$=f2nZ?mpa1$*I(EyL3v!(5mR`%ICH z>Uk+9al?l6xy&na!To*Lg7ESPwK1r<_{g(jyR+(e^oWx04YNI3T+i0LP9Fr9pNt$)r4r1);c zI1XF9nn?t|kHy6!J{K>Wom9vpbSVp`*y8EfdeeBF8qp=K0$-fNchEUaOu!Ku^Z+d? z(m}DuD46%ykG6{6>*kB6g^won_z4-O#>KDp%tRzlwDZP3lY4z5BwAS%6^ub45>^!W z0_g=Jk+QprR?_(UEWBVf&KDcst8O3_GA5y!sA=UL2qxV&RqS~07Nph|H~Q#>L;pSB zX^c8$rE$5Qfx&agQ25Da{1e^0>J&$EoqcI?BC5EqjcEZkB&~ubCTk~Uz8f3~Bb1ZZ zM?2!RSd@!nMjoagc#9xzCRBwKJ zg~6C;scK>VwOMYbGRp@oXgsK>q1ifw*5JHKvLT(Ue6@Q#T#vWZWVSJbA)+izr+UYI zt6=dCcck#to&K8$6=g)p%l@T#)zA27((bt2y3XN*$o$fS;U)fJRCc1*zTqA!GX{mJ)D>KWEPbQ>C6+uXe0fi^} zY~{vPLtGS^rs^iBXxnyvBA|{n8;gW*MIBr=5T{}l%o{P5+XHW2V+eFOf3o`~@eC?; z3ZjuV5eaT>`j97oo7yi^#=>}RYqV+I2buD?_E4ynnT%5F`B>lk)fhZ`@}M^)$(b*o zx(LVRt1-lo<_pXC2NeW@4}wWww7T&^Rfw)dQ(K^*JhSZn=Z4C?XT9$~jkK_ImJWO+_kMH@AzVRS>EYo)_9XQ>Gd=QRg7jZ54S|yag+`zJv1)laR{Zt!10xohY8It*k{QW zXZait2KenvUKdw+EH6FM9zqs!NSHBjv1o$WM~ns6q1T<5@dx8bHPCoiYa`HdpI?13 z%a>7kEnzZ%n9M*AU$2YC?)qI1mizn+p2Odo?d-ER3i78`>sc`UModqAhx2NPcGsPK zf`V~t^ZO|38Y^9%_hkq`4e602wI;PnxwG1a-c~q_(@{9733K8~qALk+?!Jiq#5IM7=Yw{azMjlO}csPaurE^5m;b-Cg|Nnv*2;o_nip&+vR3Wgv)x zJ}R`|J+i-BbOmo~w|k6MTwUHN0S_5zuqZRNp;!MtgfM|T^I`ddM55%uOTq(}hHdq}D&Whe*Io#R1!@5*a^0kMnr{~y@t0waG zb%pRp;rkCBcGNic8XT)^JBM>E#U?eRk}|EMkF>nIJ@kOX`yOIhYqNy3IKu<0_Pgnz z#=3I3!*11ZO7uG9v2`AhK*BmYtEVWb(WhIU<^5^YCk?D_BfY7!>gV&Hky+=Jz6s#) zu6#XrMp;R{lFD%P%_NP~6%av{S%i-j`=k7aNM3<~b!UDjYUa$I-2tDPw3#jlm57Ep^>C$$l4kDy;vV1kts8ncuPbyPx|x24*KgXUVnQU8FDHuX4AN^E3GKb}u{K z*CUIn=8e2V3f9M>KktS_7GpIy4K>qsWytNcO;SzX1AW_=0jm~dTsuG8T@pC^bpl|sj z2nB76F+IcP+O@QqdUh7No$)DZi{O-nZ-%X!-ePRBT{ae&->PI)O}Exs@%i|)*d*#U}3nU z?4(Q=`S8|O5?)hLLkizSP6pcQ&Zd#s%{%u}(#D|%#pdzr3&D(=O33J4?-;k*ad?xI z#AyTlH1koJ2y-wtUVRQ{A{DrE_#PHF-ocwU zZ=bB4OQJkhq1AJZlGJ$|j@rdJJ5v#4>}^kjJ27U}S6g4KhvT9DFfF{Dxhicb&D$b% z|0bCQp@y7-sZ*Ew0Z6#78GMSmu=`78Q{s z4x)YkJo=c&--p8ygMHbvZ{-ocKpi6^+R~ebHX^B}3W-GWhouAv2lS2wgd8P?&)o^X z-NoX22?`BtDWKDLn$(1R@EkL{1cPlVU%#XXZ$MYEH#=c^1uu5LTKh z9J?zgZwmI~+5H^`Z*$%_c99HPYI&kC)bj( zK7{tI=Aew}Q4xyx_e+Q??gzbMBqfM@w=B;~BA-f8arioBj>k`79<*b(M45Y~PUY$&ZugwV;lA+P8Ix9-FWyE^ z%aZKBr`0Nk*J6BpBza53%E~HSF)M^v*o4+tN*ot6dp4T2xTAcHXUlbk>va&8hsQ_qjM8S^ENAHFH}t-7`q;gpY& zd2k}gQhjaz6l1iz%HztY7yB-2bZWzmp?e+stBltWU4?a2uYQm#yY_YH_(1h)NOzv9 z-~;FL65pg)R&^v|yy0<51FZYR0hy&Y+*QtuyN>N{4w4BPBUL=H=_G|{SA8iO3XgpC zT9#Nl>r2rtCp|kBACpBIv!BD`E9^yr~DH|X};o#Updyy2|s(Cp)zJ!!jGZi5bLkQePW(V>I{P zCGEcRD|GUFbbFTaHceqK0X{V?-A#&nQ8>6EVD=P|GGZI44IU7c9ZA5jL2isK>CvNk zY@sltP3Gj{&z8Q3c8DiC*WCg=Yo4$Z$!w>7q1(!Ofuf6blyK)t_v@3M!N+t-nl;xQ zEmuQNNNG(P^+q%B_qA7uxDk9$bCqr(^W0#T9mfqTAlpz#nZ!@st-?C1mOVvLjVle#@m!UYswHzs!@b$3S^cgMZzUA*+t&mV3E z+zrM^+r>;oPs^lz-he~=`Ytn*-eM0(Ud?@1t{ul7S!aP>pwjP#%_4G4A_D)`Lhm7x zQ>BtLbGMDyvv(}rdmjD6lM9sni_&>taaXvC%mm(OVx=OB(ja>d-Tqy7upgC zH*9P^XC!8sQ+}9rim^5eLK2U zO~ze+6O0zgFM9hjPtIBnr#|aHtH0(XQJ0RUP423GrqlM|<+EP)4U65w3wA{c|$1bIL6hNzCIkNsII=+lL_TzC~*&hGyKBo8A%vg~fLoa#-OPv!hUI|Z}x+dEqiam$Xcvc#T5wmX` z>&j@XEh--E!l=m6*r3s;j80liCA-Sw-EY9W>4^g;x1UU*8DuYhm{9v1A?ERz-_j~T z!P#Xj>T@hdkU8xQi!Ago9jdBeLY=mal{3DP+c;UmrnxcZdQy?mXOXh@ngY(w;xpAZ z=w@P%=EWB52yq^!$hfch+r13%!byCJAhXsy-Xbf0mO>u!nTDC=Fv9tEr!%8tH^Tsd zV?|)za82jL+mVN{VGJJVZrw5YL&V9Q-8~!FRiqj%$26@R-CsD?_(I%tH!bW{n`pKd z8=-wS6%Be5Jm$(2$wwN$mR~g~WRjn9c{FxA*DFZ>P+=Us5bSQU_=x8GIg$P{+fDQ@ z3%T5uQ(;uqcOLD469=fj$m94{SE8ra^G0WWzUBQjf`|0FqLn)pvzdo@Oza8xDw6-M zvUY5}z4{0fFO%owlo9lv6^{GU~2@{PQRbzEVFTHU# zh$ zc1&-Yh+u%X#=f0j*u(tqh*<5o%cg0;J0*JDvD;i9X4Atz_m!&dk-Lny;MXrb&?fVi zoHFHKU98Pe^D_x{;g^o3{o?nQCUrDO6qz$64awn5-3$lm&D{iojOA5~+l3Z`zu_V{ z-htyHRyOtvT*Ur6E@J;zxM)lZz(wqs_)8pSoehhlP8!Au`cO>aB??@`-~jGuL^|u| z9@{HD^ylesZRP7`qmuduX-r}|c;p(kicgAlGQ9LTlnTXPw;ivpcS&(zsDst-4R9QH zuZ!(%o9=fpp0Pbyc#~x6RJ##hC~m>nycdz6M;me8s4;8HY4s_9MtVDCA7zvtnrEqB zT87=LJ;twL{H%v(e(uS&Ia*MyH-14LM6b^0E(&e#fnMwoYrw*^x5cBQ(t!}>Q!)QoOnmdMoxR#WXgk|$AfP$yo* z#pc=25!)_{H-_}zba$hJ&l|j37d8mG&h#alUMLK=>UB_v&TVQ|hXkU0wqu>?u_tT_ zHXrPwy5gj^|0;$noS8mQHMe%8jk@Go&(L?`EQ^{kYRK|2^%{lUu%NH`ibIGLJtdVBv_A4y>B#c{lC3 zTNbb=Ze=H|S5Gghf6ZVJWmA>d)`elau!w8kJfZg%_=M}>ee6>2faL2$7FgjgZoEFI z-e2kY5DQAAnAn`zMvZFJxKetEq>G@>Jh<-1ct!9{0y!bqOihSzGVTMgr3cfYn$|@6 z-LIN#P3#Y4ay_^Bh_&?_Ky^YMgH1Ty;~x16J^oq7yIWs)`>XpF*NdG>{CdWWLbnxg z1#ZctA;wxooYpn1#Y12a2yXD(FlgKyc@^h6u)CNa6u`8h?4a6V1*F^(~8LHw*$d`6`AMI2J-*Mf;p zYA5r^P{Jiwn)#Rw7};M2B}ln&21C}8sT4B(7~H~aoo|-7#5RXr$91N5ZVvQ|UK1wk zs)9b_`ewW(bR&B|?FH8O^nnY$kf1l6WBjYUA@>J?iph1U=HiF`&3w4&7(AqBGc`v? zF{(M(g*Bf@)YZ*EkzP{qSb1U0weO??F`5hG~uE)Ik}_1uAR>v5Q=X}lD?rJ zMbB5#7$57wJ5aieDjL8IGVORSiP5t)WD&A#;baeqjz>0-s} z3H`F^#aPQX-}~eFV!@-}3ect9{Wf?Q?7G&QJMjrVxR>XAs*bl?M1>QJ{4XrutI&r*J;&n*6U7kQ2VfD zIZ(JzbLE?n){al_{Yoa8o1`pWxJy~g51-E;=JMOmCp0C99hcrB2=uBwy=i`&r`0O{ zAV4_Kck}6k)IA&iBeVvNp|E$0#q=>HM^Z|2K}c5#gPhWco~U1WoOpVpAUrv5-R>06 z_5*sytDtnfkG6HEw1h7WuAiEE%U2CAcUfj`ql?Zpyc0lwG5^5vhO?Ppl9{qG!i{Hr zvYZQ_@~i~rj}afcBHLo*+$W(%CNHwda8Ht#T9>vrJ**((n#Yb7#XO)_>oww)jKa3!io?gj_vwnn# zdyS$bWsS|t`z@H!{Ck0Y+RAMxia>8ou58<&`23FJy9BS%^rI3H3cyT z^TYg|p?iv2d_+UU)UwVGFDdco9p* z!yXD&Ff@aLWuYb(hQfC4m80rK}qTpy}tPFM51_SStk%LvB?#{qCF?Z(&%J89VunB=7;&!m%FpsJP0$%U} zivVR{MkjLEi(&ApivuEtT%k)5C4E(>L2l6-cz>_nV>0$qW zLeC!pWdA91_=>T^kLvy+z+XbWkl?Qc1M~q<($Igx{ebG}P3?8kH>hR%l8c4imz{v=Qq>TGBNv;eAmA=aN0aQ-6b zhsytA4g^*fA~!X(b^_ixydeJ4@+xtHU_+JuAO)_#Kb1j=l?%km1#1T@v2uV|f4tAA z#0mki!U+IsSwXBn0HYEsGl&B4_E)dJlVJsYgY5tgj1p;FEIgEuB#PV|(3p0r2 z=P)i1e9$FYVA^s)3mYeh4Nfaq2>`HcaH9eU_O5`-ND`N=GV4FrL!!XHZn*WC-UeiJ5KnJ-%Z+g1BpN`I3T=OrEf@y6@r7hW&k zh-Kkm;phML>Z`7N6M6?Z+WTYB`Be`z-E4;SXIZLa2gpxYutd-(P1fc)F-NjGG#aLlT3*}jav9Dh7}GaF?Z1x^b0ZV%eEEN4iEeo61FRh&iQekOumxn4e?ny{%NbuxCe zuy?j|Bxn0!1}b){wid7#f63v?r1Zl`VWR=JVd3cHEMjixNDkow%NYJ~uWn)DZ0@8D zVq@io`5RkcyoIe9Ip+_DM?gjNXe$!0HyZLbgs8 zzsjN(rlwH9{{apU*uA*G_Kp@dP~AVKg`3-78JAL$kOtl~1sGRmVg8NtA65^i;jfIc zLH=Nrg@py62F@utJ2Px2_=gX$fdYQ}Uwki(2VLBA!gr~Q670$jcRRoxyblN5#9;Lt z95BK!KEEjXH4`&A1OnT|{`_GFHaVd0pX3C$RPaB^3D)|*loPOw4lZ`iP!l6-M+-A^ zXAn2*uL^6Zsq-cI!FTb$%1=b>fw-JFAU`Gczer6jf1BgE9HLjY>S{L4(v$qAbU{`uD`%KCH6&#{-3>(6R+G4J2jlK+?m_{0P6os4q<$=aluUGpJrfVfoUrI z^S^k;#dvmhZt@>A!~U`Z`oRXI$k;jA;k6gff?c`Ux!`p`8~nKtPBwA~;EW+~|INY7 zLC(eY=k4If^8JH2fG7M?-T!vm283X0amgGwFPXzXdt_ENuFD=dTFAD898>I&ABmGW z9A_pvdnz}DK}*#J>}&X>`G$C>=GTKX!n>+tT_T<@36kZ#c-m6;nv)M&m=IR{c5#K>Yes8b%Vp*p^ zlQ%T7uu^OMTL9>ayP|NQ>fG#I6%Fc{!$J*SnQVl6rHa81<*4?g9NwnO)K5rxjJekE zS=bDIJ-rI0d&VlWhfosevGKcmhdYVC8ik~qn3UuLn3vQ18>9HK$zSsC|H17sUosMA z_6s8cU2Gt~e9eVI|8a$@*pGgf|Nd0`i+(^a7Uthv=wGYgbN$83vBT8w(g)t>Qu%Tl z?EW9xFJ^^Zf$yJsU3l)F8|S4h3)n${IhFp=Q^H#Rm%f4-Y-3^T;sjy?1NaK+XyIgK zW9V!S1Sw!gsHrv7-O0ts3F-{QFJNn^lM~dz#n2jvYXB4kHHMl%e^#&oqa7XXfFFXv zd@Y3KN9mXIWoHIMt)VtR#1CSJfNh~>@E@8vSsOZ;gKZ4$ot*8!F18k~P)8?Va&8t_ z!Oj-M4FLmjo`tcYwV|!a#jTwq5EHS2jT{Y)fhkR$f84>J3pTVhgVkF>o#8Ei6yeR6 z%pV?%{Z*M&(#`~IY-eM083n*2&%g4mCL^IJBMUcTuD@a(xCi+MNPfv=0ZCmTaxQoz z{6DvkUnBlx8NX^_mi6QFf3=;Hnd?uo`T_O+NmiFa@c-5^U0C0rbp4X1!V?64m6(jQ zs*Ex$xR90nU1I+MxBW>`{|GHufrKAyaoO2eE;G*stNX{T2j2RBN>M=^EMWL;dF!q1y6$kUL8u+68)ViNN z*dZ|cgmAL~F%lR2`bP_9Zc$#H3+0b>3f zaQ=h3!LvetRfPxQ>LN0Vz=A0Kt_eT=FD%miYn1sXP|Es;DzJ0^>}*UEC3yxKrJUcna#z*0)+Um82?A8 z!Nvu@A$BhU{{5zq?)WCmcpVOKT){a@7o zpoN`-8BP@!7r+b93up!XSSJXOvx5LzB%Etl3(ynxMA#MhUXn36K+k_Nrb`K;|8^&V zLtN1RAnt{y7XPYG@>&m+wZz~C_PY}VmLJB%-&z>QrI?WAl16c|T*gmqz#76O280h> z+#KYbu$Hb&cO;KfnYu0^*?$78ue2r;XT;_A|Sx}!oC;xY(PkHQHI@Llvx4n z#>E1Y2OwV-Kx!9bS%Ep20b2yJ(ClnK#=>R<^p}hMlGOgKWy0f{zpkX1rktV{3{I#> z{+9ZJ?+E{}kldFS5OKvZr4lbg z5-Rzw){JlJeTSDR)O~)Ra!L-Dnm6`@us?xyL{iWYpwE(aJu9SZJ@uW(}jUkTlk?Z@FP3GjJS1S2MfTz?|^{7 zLQcl8Gh3h%IBqqxmw>`TvmZs+)UY;Y5Lgm8OS3Q*vNf{?&Ut|YF=wca8jz>~fn_b6 zoPd-%oH1DX7MKLc!vjaXv_BHyba1Kwn}Gth4BK%oos+@KKl%CHs(`0l&d-ZnoPPk` z_L7wun-~}x8JL)uI33)KgdkU`Jd$Ah{?zbKOP}{(`C+Xxz zeDUXAu~!gKsf_g;l$)F$2|*Q2J;g)(#GmK;W##2HMEXTPew^oLY-_1#>S&biXJ;fS zZfR?T@-!v~Gc_YMNlU3H(=bL+Ny#9uLSIj>JRwoLG(kVswxB3SAzkxX7G|tgs+LN8 za`r-ehI;lwLSjns71tEfMCZY`jI@lBj7pye1liWWuXQJ1`q>-Eh7UX6O*dr z;r7FCJMl;YpjEb=?{ja@yl0|_hkKknY24(OG~(L0?$+=ZG|KMOb&^e#4<0n`F!h|M zM#S9R|2mj_r(3=GsNfrR?fmY$sYCni#W}W&VB{wrgtx9lkXrcuZsUMA`?K-+>i@xVqs%p=H&RLQb5aPm4X*9R0DzbO1j1vo)np|)Tr z3wN-yxg!(`c6PG^dqN%U{-n0>-R+Nq8~~aBTDyO*wt#cE>>XrPtW;Dc2wM_(qv)eh zWSX(CdD%qYWk$QX(`D|)PH+jL#!KD4{y-4Hf0-P$>j?bZ0L7X;$w#dXEfT__=d)$`=d&$2YJlSkH+f`zaN~KOBsj_Lm1H`q-DN- z)%e!>SU=~BC;b`y^^cl5jKjhvedO9geV)V5aKCR|nF6D=2M1Eg8EM zD-@1Ld3vKAv-R?x7uGaCloC8v78~W;Kp_z%c&Dq@sz#{R5zZUa^RT@ibq)t|Bkz@b zfOox$Ux^~0o^j@YxC9F;7xs=lRiJ!GCmZ#ybBHyAGk4Do=u&jhdQV_zr9Z3V3~l_v zNH&EA>(GFB{osU&5EF7m>v8Jj(*zD2`sa~c-}{ipeYZyh7V!vssAuY*4DnYYH1+H( z1~2z?CTlz>cI~B(|5k{Ral?|*(AW+d zdp!T82SyKGNqoLeNdsy?tjnf2YmQ9M0RBry#i3Tn>lATOy^m)?)}a!9s$$n~G$Jb@ zc-vf45b$pi?8}PZ4e>r4!-!pF#gx7!Z}tkSJ8+`iwesB2IHlQyi-UVZgwJt0$mq3{ zkAXmIcUngCDO6xX$Xj!4r?hh^U?Xeh%2>(!b`#S|vc!5HP9OH5{w>O^b8(J05uLm!zI z|FZ*?V&#T4=hG$wmkrjb5TE5W8o#${*?~^Y-78{k2@s1Pc&NDZ@=t9$e0*@YGst! z{XDLZpeXixUK`kWxl5hC@m^c0S%TFQk^3??F@wkIGg;pAiyE7TKE_mV=uDqPHU1pL zg3ZYPSS~hWAy_c193m%omREG}DlMgkfQQ%XQ}!nfOgml5NYU6^ADlGQT)r+p>mBKR zUi~S9Pw#L-d|A13aDEEwL(0?4X~y#&O!IFb&~Xn}E+y(}yW1hbC_VsGORW4Ui{3cLw(6>v=Bor+8q-2FiIHa$q-Noj(-tIp}| zo6p(4Q!%wutS?$TS0&l6obuIm|Hv10tN)d&?eKyh0-xxIe#cA&6oNOdF^QwX6ccO+ zgZ9|_)qMv`1n)_S$PJ!wM2YZZsH)%ZYd@ygHPPgvEVgJH=J1^adyaL+TT^2@TP8d& z<9zUlyo$XzTY(l4x{~W;@0PhoL(6gXc?X|GLcP$vL+{ZSPulU2$-A*{98C0V9IBgU zyD8vH@s;uy^To#brYcf2YkIn{vy1J!KMW6IoM%;dQc!nz7Ay9bDCv!agNcOhh%W~?YQi&{wwf!F6htu>KBbRhv!_s@ zj)`?=*BvttG(5g#ZA$Qc5Awcp^BF^P66)LxAJ6pcenb%)H;=QtWnn4o1-M^1y}PaH_*L4F`OkDHN@`FqSwv(Ufysp96u6eix3m?ErK_ga6ArKzWV zeA5|qwtUUJS$AS|a?<~iAiIe-6m;uin&8us++nw-LO1f^|T*55G$Ja6@H;OAct z#ebns;2Z@2`79h4fZ-4L2~=Lj3h?3uR`@6Q$-)j`f#0FRFZ>BV+y0Xyhvz&mIdWL} ze~drbSTDbS^9z5v9Nc6@V)+yNEIBs2X2pr&#EH>2{i!6dwHx#(YU!Mm>E+8;ZxXd9 zhc;666*Oa$(iO8aqf3hn%q=X+a|}!j42l*KQ?z1}QWFanQZ$}LC#Ps!`|yDlarLfQ ze!R*(^GTD~SX_N}Yp-M?Bh2cKjQ&tMw)lqVi!X~`sTWvq2L+xXLCf188Y9SiSSKE`(+&PUJOX-~eL zWFVFL*VeZAXCva7nHxz zvP(kwl`Z(YAm_KY5`FM^ta&- z3rt7C!Rpukevj4Wy}72<+4Gh*w|P8;c>GvFa!fDJQyy;gin-PN8}&u_?;#YJvzd>W zwGq{XE1%zo#MxH1KSR02hb}-WkAmdq4y`p4HnLPw5zUpdC1X|I`LNMwQ2Tyrcvy7@ ziy$5s51SZ#h^{6U)P+=XBwP9(OmXL)Ox(RXec~b|>c)Yz615T%zvWnT6iF;;v%&b1 z9F=Itd1k1_NO`5gac_Wo+*!^-J@c`IJvvpjnXr!0^Lq@EJ877=<8kE`V?`)Ygpp4Cu_-QDoWGQWpG0! zEeiYmpnj+LVGQXYwtz!MW6@ai*0p&fj4Hh|EmlSBJ3Sv>jHhx;adGv~9-T48&*C}G zeBnW;+p~Kxr*Pk)?B;bcjaH{%k^bH@>dG7Oaa=C-WG+qR{8w8(+jvhbuasmQbO@MZ z3zf5FRnEnph&o|iU$~|dL=SCo;aV|mK+#%|vP|<1B&+Y>(YUUcTtisxy?pKQN=g(;iajA7qepq&|_RuF|7QoQTZa+LhOePWVJ zXZ7zhOT*u%jy=7P?X&yXN@BU`CfCV?G);=!i_~*sf}8bim2udhs3qx@L9^Ai6_i;A z?$h?u9sZr+*ReF!?USR`H(53ILg-b?1l>|4U8i;H4b7f1Fp*28sKhGgGV}+gX1}L= zlbt7Wdw_JPT6c-pMvtv$H13PgOu{-?v=@CfCBi(EjnsIB;u%|1FRv98!ZIAvuxvg}e?7xCcpXb-ombHi zQD|TvzR4zxWGx>RZr~8p`E=sh3>qZz^h8m$=-}P^Y~i7mzR@Y|u@Z7bT(8=()isdE zh%^3&+`cy`lJ`ESe4-nVi?58Uv1yrar(>q;RkG>`6EQ?(^hStY$U##J3i_n-((yB2 znyZj{E`2d#qnMqgwG5k>nfS`R72UMJc-D2R+zbJsBI`Q_J83~pQPan6o=>t6tVpM& zg6**%bwi{oal7l%t+)EaSf3M8VBVTZG%V%Q_tvw z7f-mz#9B9Ownv@3>k!RkqmTo1C=WyF=25#86)3dS+A$`?cz^vx}MsZM~6;@ zt4=$LE{orpRHMqi(lIUIhA$bkQw+V+|LUUG^vENoz|P!P{*G0@L8}F?1E_omVQ`h$ ztlonw7a!Tx)|lR{jyh??d_C;um%X#CyXVKp#R;^Y4-Z{RRx~v3rYL3TRn?}YWA!i8 zQzI)iE-z5=MnO|_Rz36@y;_fV4`;U|?vx=M-mZ5G{!&5sawxcCjIz^8COqIFt8NvA zjq#T((b|$yNjtUiI|bd);PQ>xFMO=#5y~t<1ySOZ$GuZNR+bB{t`9Qr-HIPJc_m<$ zO-=9p4awP=BekICC{Kommi(Y^lw=U_IrK~%D@W23NK{iX9f-G z3G3rD-hBH?D5~8?#=@ftU245|%TZSCk*zIhQ`jk z5r6HRk&z|2g+}+3j>wa8Q08h)Bf6!@d*fXe-Nu*{XJz^*gP<0=1`3EbBcCNWW+64GT$8Guxo z`z)MKM3kVX{?zK8FB9YN_OZW}%&NCrcI4wnHzW5SL}NszOe7#V>j?>^Znlge9RYu@1=O-(ER&YNcp#cE!V4&wgg6m z!z|m?bN!E|eaJhh;Z_etTSM=S^_i-|}rAYG=Hjxc&|T+w;| zWaF0Wi;vg*$7qck;>J|{$23AuFivj>`2P)9gJpF8O-S(jYmvXu8Z!$yH*l!K3B3CI zTUHvV{1Z}x75_kLz_IT?AT zRYBPdzm?*t7m#V0V8}k8X{~8hm~!z}70W8e6GKEo750_Dd_@&d5L|N?*?~{lBYLpNwmC}zNJmIJf5DmaC0?tWtH4%*&E=VKmP7C z=q47MgFuZPvR3nGt{s(cJAv&eg!0idg!7s}#>Njmcul4{3dUeJ?IK_BdoZvCj0ZYHs%i@E_S!L#0ykL)DIGXx4C3 zVsFP81CSF^yO4ZWT4v`}_9FOQxoN43dlwCYRp$MQW|OSX^l zHhI^I$p1g$&M7+3HS5+DCzXorq+;8)ZJQO_6{BL?so1t{+qTVC+{LO~&@u{%I*}sU-OCqBxw%TEg6h?n!PV+>h>ukr)dXk36BXP=sB?fP`n} z5!Ri<14!#KO_Mj3jaY0ORaukHV-7{5D2fa}&hE7>YI94sL{6>vh7Qkt*o?*&kzrFu zDxIRT2ah!JWs*-Dj%r`v&TRq#mTO}LQr2>YK~>T^w{jzB%uSfsL~|F80zTLZ~;_w zT0#H}VUe#R9S4-aLYy7q&M)4u-s1%_5U?9WI@%)9VKCr=y)QV*J)&^QZ_@mJ&l%uh zFuOi@nNi^ikSitCw))DI;6wnk21EpM!^R3XiB|FM9E=vO#)2?|NlA0x=kaN_gJIjf z18w!t;z)?qjk$@m%-PVt!@jr;;oY!XaW%M+V9@NK0|agNW`RqmFsa zT%^v753*zOw1kgOmc639XW66)OM|u)svM7sxpk9H%n1_(13I3pmmqX^*<{1r&u@)& zfMgvx@M4f+l%e(qdm`~qcp=UtiUV>Avd#xpoFQYGw0S)6e#!E}RhVbYXQSiu7}vY< z1G-;3<)u(8qFJ^beL-V08P3s!H1jC&bUxu@*5E5gc3jF=j6jDn2%zKRVRwyIas%3| zi6=ytba~uv$in#lB#fi3aDRc6dkZo4iAT9r3WH+K=y6f1N4EEb?9Wc{P@8g2Xs&Vw ze~v$nQAps|w1D0jU{3NoGD8c^!6|+A8-d21@(t-;rjuf*S80+mQrJsr?At-sp?lOyyXxlX#)B@3Zj_72kQMT3cOeC z%<{6v^v>e&T(7ag&@UPwU!nlRn1grD5yiSS#`f>!~=>j89!-V)oYtao@cyk&PN&?Q;}~O zMMFO3;X3`JiQbY@`!N%BJ_{B5X~oI7eLW^bpehc={f#9)B_1dKDMbi~}GprojH)C_VMdQ>^kE@@Y67(Hvv z)SKMnYcamMy{%)An8LABzNFVl7gm}L>*JbfMHB?KN?6u`-T75mOr!FAy{$S1b2p|) z0L=isf5M4H;I@pKbIk*+oj>s4gz8kN)CLLymVl?UhSSZRr#n*kKwzsuF0(-Sh(IWO ziiFI``(@Myr7RnCyJu@ouJgBrI_#|cWzHJ{Dv`!&X_Hc4#v;#DS=!E?Ne$oZ*$*^UcY6Wl)gF zc%uNHgf0(MXuq5^zLwv7U8ZON<+N$RT|_xRb6ZOD2!D14Q>|~J+=_!;wXj&ld?tu@ zryjoj0sdot2b%`fuWw1Y?tCIDKf-2;cxf0w_wp#H0HNr*wjUY=(FWfN*0*j#d_Jy`5Lft5iuALXPI92Dlx%3zP1;QM>c>oAeHmK0^e zPw62a5~3#3Mc1anw-K<-`5+)P{yaehW6QmWoQLB`77}OVkhO6Eq=zU}tL*v{w8sNU zwWj*ed+tzn%Abbt@Jf8k8ZuYxW4$(_wZ(SE!Nufa=$gVw8b1+lt+q@LsQyCU{VQVe zKe@#J4*35e?>?4stRF99d`_IhzFFg96!1li;$Nx^J z{}XYi{wwnQAFTTC!2G{p?0@3n|Afx}jb{HR;Qp(`{D9d0wATCm`TtsC(z4Rh{UR|H z6~0*`%p^CrVo*FIzc`L&9E7n>9P% zPCfTre}o>MnWLc?9#VHYeZ7p4jBD5K9#(D12IVFKfNz~vvlY#f0(7XQF5lo%3BBhC zou}%8(l$b#_6Uta)8PmmFi6@SVckm@VcY|~M%iP!wlWHjtB$CEIvG;ZUk@r&FRm_7 zb}EtOZZw?^s6E=t%ac5!Z1pK@=GT`wpHi{sEAQjuzBy{`3%Bf~%hp=Wu2y+U*Q&QP zF)5Ip{$|OLTr*yxT8w>EcQCV#GU8(@bD&^Fk4|xPZsrQ&fb?DecGm3V6r%#1=$1-9 zUxyAAm@>?gA@LTyx=eZ6xDJ&O)S_8*dJfDU>T z=GzE^L49K&-|T3FW8LvSF>vbyIVy!~PMs}qjwp3vv0FRpBr2OEUxF4Y6HHAC$gr2U zUKY2n&tS(n@nLs6-;cLahz%z1@ry4ZpRW(lfF&~R0b}TSLsi2u4fQRskXJ!4 z4dyK{r07uzZ{PV4yIoZ*A|VLMVXPaovi~XD+lGzw16EEJ3lWT%@6MMaAkKl$fYFxdPSVPFhl7A1_BY=HE7Hxx#*(~e)~!a@ zz^{Y&*dX&m%G*56h-?`&{J&feI`-UU*o=YF&1xV{xv;c;&)bf(IJDf*kg^^FQhr_H zUXF3&Ix6~_9|=uVn(vkeCXK~)xMnbk?Z>I%VG6Gra)Lt}9jk;_tfvS6*&nW=Xo#Nf z82k&AWS3u2`a%9VMK(oIg|?iU%2KY#-iNJ{aIt3|?lr%+In14!Vz+FP?KPEVy;CJi zo3U|Bo>h)a_&vwFH;3Wkle6N1>?2$vI=auMYu|6urcm3gbH2qZSgiI zwphnM2W#x^jvdBq$$H|rY22p=TB>&PsnApJA!W1c_(`_~H~FkOeXhW6T#xBy=7S%6 zW!cO5b{Tq-PIc?lx2M`#EhG07boB%zsolK1RyW#;z?X^-IT&nhK-bs)5aIOhmy1$W zX#xx%c_HMx$&av;B@So?VZbj-Zfyz1;!~KmUtj#WHQ%25baPM05Pvo_hD@!nTyon` zA>>UQ-X7jc$?w{_1V^aTGGd9fnL~Omim+beQl|$qd9a6(pyiqE%|JtX-%c zZ7Y^&i9VfFjQV}^blfi~&T`K+HMaJIKidc5wRmvI$G%bDx3lG8tMHqQxmL!ahh=rinZLGwd-0$4WH3L;9XwmCJ zL4 z1Mt0QpeM#=UR;-x%q`y0{%U zPB7b8>0Hoh*y5(dp{>!Pv#->8+`CO8>WFO)8Q*LbgwhFz2Xk_h+<`6yyxV^A3FBne z;O5Z7*L-5kL=q7?cOZ*ST)y#b4-ZC(JqE-C<2k-gHev>~R z0rhv_ll(gggoiZT3-<6kC!d#hQWR}_O)qPEW)%rNXN~|bzN&oZ#MG3AaOXfrhg>Hu zb1exyE3I@Vb0q;jBXcG2z@RMnnDm$gWud}E#UKeOX~on$H8u6T_z30PFtu3y^o%UY zIK|+HLq#b?NhU5SYdt(pE_)$9BB|)bA_c?8y1$Pc8=s3z`mmRui@f_=f>eD`g`Vbu zet_{lj$kFuYgp3)D_(55$Dklx<<5E^lC=wz9eWffRyL9=ZL@%52yf zQG1Pc{`xTXGW{Z)a&QwILu4<#ojAwvGb^XM`KQ#`c-uNX#!~Wf(=lQ5F>$@*w`Tyv z$i&I1<<I*j*@`huE_lSeVY)MkpUBO3? zYsh(tj7e_8A`NXTX=!O@VQFdQQvHDMO7ZUe{7%MBV8X+GcM#K->knh3{mM-jf!8&r z^lkf82G40MVID~HhL)^U$k&e?sp3Re7c?}VJ`JFju>JeM|DG27Z??w&7CHRKynh5U zm_Ld{nEq;K{PD?ONB#H5KSrJIe_R=Vl<54$%J`2h@h>|6cUk|ZLH{is@QdmG5hM9u zEP&~m82)O|f8&~KKK;ryYu;7g^kd9fV((dE$NR5mfP0L?zNC-5b82~c`$y51Hx%~& zKbiAS&5|$@Y=55f-JN`238@ir-4C=`FGycUrEj6PV`N|;TlFr-_k6$ce3u<9<0aPU z?eM)-!~U-8OfW>Oxp?}oN{dGT6;G2h&vJ<)R>P#QnG_hnlt?ZfGe8l5=^V>+e#_BplwYqKJOd&my z<9&@(!aljy%d{uJvQ^{Z345cX?Rn~OH&9Q@moJ}gGQ-jTVm|*{1m)iXmVeCW$E}y) zqo?MVTkoIGj8z=hvgvPDIeD;Vyc)=cg=T!LpATDnh{Qowfza7M?i*z67uvc17HvIF)R6d`b zosWc$x6{*qkKiU~V*0Mj>u95^wRbgTSd2ogiPwLx|9IX8((beWF_F3*FZj2{eg{2C ztF5aZnDprRbBguz%yq-BZ?EHdwRO$a&HPoCX4|2QuhaQ=!pkPDu~ z5{BBN4l(NCA-(QgF#A`Y*w~<;pFRn=k^jXI{G4(f=g`^@p|g+iK>ILsOhuo?4e$|95-sH)qY1`rGfO zniaM6@1~kPwZosr^tUMQujlA5(cb@lOz9YCeg*VOl}xSW_mMoRDqOs_QRQe!2+m0% z7jY>>F{b943TkI@dqWS#g++WPQp(IGVcX=!!_A}Wd{7a5cy}E(|Q6!0T1cx?R zlmd6NQJ4gg`e=EHDkXe^xwAczv=R~N?kW5Xc#mAC?wXNooL@qBIpT#;M``-w3PDjx zSsZvz%V~BupbZi)thm7J7P=_qclAkKUQyFUOI<-i-W_=M;8g+a%D@3)CivnYlwb-y z`b+pINpnI^u@(t)V%wnRi_u`09?v8v_$6ACWc!B^tAZI@r-wn#cH0) zjlM3Jn7z=Q0;c#}eF}zmvLBj;#9*>0`&OzbbF`Ry*hZ|^G%>b}_iS5RDE`>FiLl$7 z;Lwimx(rwOZPPax3FD48K&)H}(S!<|jwX>`u_Wwcc-%$BGH3eC+!S^-GOnU<_ggG%da(32^WS4A%s zdRkRx9m^a&gNaC&^wZ*;N!3GaO^v# z%i_UQZ;Vo{F;D?4tR@h}Mn+~;nK~;VX~o<@Zm=7rO-DMV(VrNLe%l4hGT>ONtwtGt z>6F2B!>X3R1KI!nU{J8akHiq?g3H_2M8tJ+Y*la}i$)UM8i^*1(M?ga^A*E^=zQNj z3i(D?_lQ@tTpEK1hHbe6n#wY84PR4pAK>QgfH?!WiwlKiLcUwnlBvK~%()ntk*+tD0x-VC3%3 z^8Cmgzvt{YXD7J*%zh|IwXvWPj%*zT5LPawS&V>2dRSQmjw51(X9so-e%&!dzg(8i zNjrs>mGWa7X}jKIDtsH$!}QLskq29$mGNcon~Cl`DyO?4K`4}4*)A!ig;KteL|UNp zRfdgH6?&|un^i?PP_LIx!mdU`DH6Tlxd3jGwY9Wfe^dVE|y6xRQAqACf zT;O*-Jcgej9ck?DM?E!@coTqDmOvwqR|AOVgI4!`u1h`x>lvX$TE2(c9FdvfZrBQA zdAfqvU#P`;(?#itXN)BpJhUztSQ7S z(q~brSwdxdn(Q#wQT*N~_3^jsB%R@w9^rkQ(m7-47CZ}qwqfkFbRU<~wF$S%F@l8R|XdQexP#B#aqQl^&re%8SWrV@ zCZ}$p-1#NrB8RC-K7kZ$fGfDMzuZ~6KUOShlOu}{-)qrGWH(c3Ho|5i76j#xFE#Q)Oi1F}Y_F)wyZ&sJhd2!y18 zz5@P$Yn`&9F8+LXywes8sGnB z+||KpQozy<@9s=Gk>O;W;iDq^GBf;a_V(!chIpp(^MYuZ$I+#tv=!=8-st4vjl52^ zi#1dRXsB7WqGj$K{qqQVG01ogXnF5xEqgM@%tF%kV~iLkg$deMI50zO<#x{<#wNBr zYtBjCDx8bM)0eqq093qkkC(%Q^_Dsp{>Ph(Oa`tC;0|nC*=iwfhgIg{$KHEl?$^oW zKtM`P>?7c%3>qyt9x4=R(ik)=@OW1fTqhXhHu|YmoGV!@UvCKOar=TPJ%uEaTPjs4 zfJiZiX`PPAGxMA@0PAi4jj6q{(Khd~o}m8gvBu4C023hToM~KU(IXy)YJB^pV}(vb|8nP(fGDZA}G}4sHM`TPaUM zp{9DO=AAi;!G~~0_O?7v+G)yZ$S|liAqFu3+W~5>-2O#P(e@FR(g)1cf$3+FjApxn z;46DZVhvqo;1kMzAe4C4WLF|#EtuNg?%;Rf5Q9^s6C|0ZVRnA7O=D}F1Pwh@^0W1K zeC7gmxEQo45nFls=mnoBhP(_XqN-F;%!un@A?YAiF-wLzre~Gj@{Kl+NJ5#&- zTe$Tj!TV>;{mZrEzt`N1%*?+oFG^LxKEka{T-yVw_~?kEvLY?U6PZ4|f(Xq~1+ub} z0!2BARRMP(!9{ceV6Z$#_W3+1y^Bwu%{UX7J|^7 zxtI&Kx(nL{*%M(zXN}161LU=K9{Mp+(E$Fw>IqMdL9JfA2#GRQU!AOP)jnaSS|RP% zo?sj_>na_bAzhL0_X20Ii+QwrjvriIrMg8NiM2{>4{?{7M?t-`0JxwmWP(2h4AirZ zp}>xr=uGkf>iB}Dl#SLJhCA2I>S_Jpx{IBT%*BZ6UG+yc;%sH`8ks_)=7EzL18n&) z$4F+z;E4Z-@(AAypV2>Aj8#5`6vGU1mrpXkPHwqicgE2SgwfabCs(GDTy=qBEN5-9 zZSI`Rxy-jhr^3cqgxd5ap0K<=nY|emGt67IUb*c;)Q`M^Xe)24sAMk7PzE}$s%+kj z2w5Us4l*S%;KHMRO5Z4I!rN2Lyq)Sd zC2r5V2d~S1B5)#LDHfy3f$WZ{zAJ>`<(3h1YwCkZCeC->I4^CEg8?I?;j3*tXoEvl zQI@M-kC2&)gEUBQh)i{b{wzSXOo;FSSK-#5`A#I=#hGwdxWe)?VI!0>tp@~klOlK+ zJMo?Bc(IU~=Y_T#z^Md~(lC@i^3!k`wU@d!pxc53b1o?nzI>&B12}l3WdlIBfdbJ+ zxVk(bc#e}^H^7KMijtGMOaqq|rG?0(J{z<~+NN9L|9m{K7pM@J<-L*#1dV1@BlS5= zuO`6L@pvGK{wI4H3+8?KelnC1?DhD8OtF@i`FU1(I=CAs)`A!MldIH^@&`eXQ*vq5 zAwiG}$FDt{uh;eU32Qxjgn9%8ocCxN2G~-~{_7hRkZm2=Uz!++%R~6}CVBR!B9y*2 zAcpj)e7uF}?5ahHwuq1YfH;3my=uT_7qJqpT-;)h_z+kUMs}YckDC9Dg05Z&v91Go zF0pHG;iZw%6|1tHLvRl>erxmu`C>+>RuD55%Uf#!EQ0}Os?I^dp_`TkQTBL#qi_XK zYlCVX^9XHk7p@)%bxZLiTiELOA$Sy!pd}y~=d&zY`Y`%xP2|~{BSR|)Dg!i>o7fm# z#uKOKsGI)LoW)i(LmeZ_3#4RT{)7KGw@o&XcK;mqfdx0%$nEuYQ0dJNkdT)ZaW|me zDO(vnLVYIZP~bb|trb(4M^unIus1<*RF;TOl!>vVnztQ$fbj-SGkZXhN@_&duKnDzp_=8+_r(h*ue zu)I6#zUt!+rB476cAo!8kyVU5Sk2YJuw)a1LyJhH;0wuo>i+x!I!*DJmzIbc8+axt zbe{6{w23>?FOB~s8ycZrioe_&bLPk?gQPV+HUp>>Ze+jE> zY%+B#30(Tkmtn1(4ZvXnhSl1Wgi-%s_o}OvKzJ|z=)v^Xr;aOjl30MF-HX!KXNLlf zfWX>TP%ZfjB5t6B1D~!)7Fgv3*}&%Z=_wvr(gTmR#T|&L)6y-0%BXW-^LR44?Y1*r zf@TTs?jQk=YYA#Z76NW9i*jK}$p%AmmtI(&opQa#w}HTJWv*k0N6d&4xcq$<6a#*l zbah5don$k%HoNaZp{vY z1pw(l$CH_ zmwTIsqe|y1cSzivZMP;|Gp5=`fiEH_9vsddx(N3ipjq@qc&MVuV?)T2ad(`_BdzQl z-DLODv6c|J^S}@(cL_yZSZri4~32`WuPv*F(Z8ACI0n`NG*3 z;8w49*j1xrsXF9(ax~6U;k#uJ(+yBw{^v=Hs~3`>Km`{iM|5xWFc2m|hos&}NY?mU zx2#lPi~JENJv?--0G{n+`piL!TjA+TFF`FmOCg9@o;7SqIMNo*K6)^V2~DQxE)RC_Z4Yk$@WstQZp#5eMg2}GrUwzJU^ z7f%@?gF<2`}gA4=C11tBN zI>aeLIRx*@qL;O{MaW>(hN(yZj7|l#QePMi~zBYyMU~LqofBW-WQl_ z;k0hKo08QlH$&Ou!P9hCoXX|d3aR`39=1t*U92bPl1;}5y)&&mXE}3+c0L=$WgtE# z)`&wG&>M{u-_OPqe#RWz_|y@a4p z{LE)#RUObcqgeQiBFf|BI7R|WP6KvP!1pqfaNgjS6|m9H@3j|+h%L5+G;k1txMRbG zlzu`&D4OU<_@dBDHUstNy5rY?jG|$gGe$M%$3sTE%ltd{Dg!Y4#Fbg5i|~xQCtTew?$o`pg0%5Tx4s9y2ucP+r zo0>m~+eEq~sVs^9fN2PjefH-CAVu3!i9#=xfD7}FH+aQe=;aq-)EL`%T7p#VKjVX6YC#Pjp|C!XilPF#1(fUn@Deqp|#3D^L8V9|K#@@8t96AwZDVp`S` z!sp49b&{-6;BoK-neNvwQQxOe6H;K>le6ubF<)c|GDvzAD$(eCf74jSA{T!)+o{>9 zc|poRD@K_TQF1n03xp0}#vw|Ir=%4$2eZV4K|=Fvys3lj+Vj=v1zMK~r3Gue4-!KC zRN%UjbIDI*qS*xcYU6_X0a@H{I@c-^{bx>Ly(b@HGDpTiD~I{(m_a346BjVDh*VAG zVcdBe@>gRZx3H=0$pL|z4UzrLsuy$rf|@nAmMJ zAFAof>SqA78`IbRYi4v=v7F38oS*CFrzqKm2@AN20zfDJO)D=gFX2J2stz4rG#c&o zwcW*Yl{DmX%ek^g;tdUX0TGl_HDu+aNN^h+gkSm>)6X;n{GA#xXqbkTTle#Bi^JiB z1#`jp2u_MV7X_~;*9>EqAbA4jCstQe6H)*;WRexa$-D1w=j)s zXi-w0`81-vaZ0jYav@M9Yoa5BNwfOkQ3oLD)vF%gv@BtFa8yin+>Y-#EBR$}dYuvR zyn!98&*t-u%8gqM+1vXGiCMM-n(Iss|LRkvz+E;y_xE)MT@5-MpSP~Hf~PaY6=Tqg zhUJC$ZszX@3GG?Y0~54q*q@<4gh#iP3aY!JUJw%H=MiZjm?)=JTUJ^v*uAiC z@%HM^e@p`A7pO&FF=m88=Bu*rM@5c zXLI@ZWLusRg%an=k#grSWg}z>yYv?{6l~!=NvS?3F*jmomRQlvZn3N&E~#wFY30W( z`|ga72w$B>+tHohbf&vW9SEG=f=##?0OJ={g z?Zhn(DFo?g#ZG%h-XQNI;F>ApeTI(W^{jzeJmYT%A+*qIOASyXDN@?sXNaCP2w4h( zf5ASa4i(#&$Ad@8=2946YkpX)gqCcbl9Lu5iVi}y^(WX3$IOA3DTu*C$kyMQrmti) zqIjTrg0XXMFN!$GAOk9VqoU53KzUZkyd@8*r3j-6Aq^o7E`$ygAmUOY+6~pvmTDR* zQue;~W4S%E>`R0SU`MCxd^}fad$_k@PF=ijA7gkv4r;Hx#S5U`)PW-HS@z7Y(1~xB z7Xd_Za*>}^ON2fvj_yu;Zy9fQ*;#q)vPgNiP<$h{gCdHV`R?b(SF;VgjIM-mgoA{9 zv=008TdC=U4QPde;`?l)*u?lUq|18eX-OXVOk_7=J~9EZf%s3=j|*@u%kTqiv__tl9GyLQlKgz49 zm%f}M*gt?9iKpcdmy3O-X#qJ9AyK;t6vZHDB^5vc9bE)%qzhf%-Gw(bc3v~Z?POo= zXd%h;FqC5-qvo-falm04bp8YuxUwz0JosY?$^gJ=;(k2+2&6v)Z?K+kCcv@E@F&(& zRdjX!lXM637j)KBwn@00_=Rzs)eKp=RgI?e1;F9V5Z$7=Kk9~XVrshOWDRSs|_A`J5NCAflGto&gQf;XG% zK7|0q3M)Brjoss$(2jVuvXNqrbP_D3L=r8>>i+1TAo|Hnou@_ET0^hrQr@7Y%LbxV zLCE^$jQUCR=D7vpxeIuIl0TjkgQwU&s8v~k&{--my~bC`om)NC1Gl!@OKSd2LoG3D zD0&!=T=FFCfNGWR>#-WTLTpi#FJPj9NHD@SRkHoZ8w?eWIMK@r?AIsVtl`mDuJwnV z_8WYeAIR$b&Vr!sKHGZNR-9$-w1`ECD=_917n)eYkcJ0CO02Rz2YkG@`;l6D0<~x4 z9U{fjN&MoTwkM_jL}>bpy-p#2u>+sMAh&L(WBoIzLm#!5JXqT|}b}6hYP^-e`*8?vl>jwxqZsf1f9=%v&fz)| z2_=taTjV@>i?D+s0 zTsO|B_g~oIhZ-N~{B139e2qDc_=oT@vcg!M4m(hoxg1m*C%bQRV8?Vhi{tSphpu9) zYV^G?@T%=6`yuyPQX8*#2j9dgh2|N!8*{daqnkN|lF$8K1ZKMR(2O{kg{%}A18o9l z$v6>dB%`ke8X^%hW{I6R`M&dQPYNJ<{h;+2MNg4R_9xc48~kE$)tfbzLQK`20iZe(z{-h?Q8!Za%@g*SqW#GG?u)E;{ zHy_baC)KRU;&3m)>ighU5DFjioRHN@B`3XRnO8}cIcb|KM%aw8_8KNE61Ltz{FO!= zQ3SpZM(dnEvIE2uSp8=({z;Fzn$Kq6@bP3{j=^R12t)`JWyrAIp`I&$I_$)tb`$Sq z_n=;hV#T7vN=k{-JBjjZ+bS6tXz&2K`7fhqt`Ur*asNAFQ~=HbjXIv#&JN=eSH z_0%;bO-kZVdX>&+nx8$YwF%?uD>Qof5bc-KE_h85iYMt`N#w|52YdBihsCwMcr*EaCYoV!Xr|VcO46VF6SIjAV z(M!;8njmg2p_jcdM&(9iuH$2BIECFEBTTxZ6b!TB!ms-|($61sR+xc#cAoKl43hx= zE>(~WxlNKM`*vXFHtN+PdqiH8UTmRUgiJ_jp~}DJz?oo zn-6ldrBP5r5f|TUIDmL42OW{2`D1O2G+{Qt#}Jc%uqZlFp$TzW_wIP-MS^c2-e$_L zXJKo^$DFpxv1{&Ft~!PuZ;pJoI+AGQBv^_0 zW(!WLX5#*Zj7cyG#1;gN$AAbs0yx{dy(YuLY$&L7e`oEm8L$?Dk+Ad;EW+wE$vC9H z8T}2P=Hwi`iW^?);InJS*+7iz51ZZg^g&1y`Wwtrc4`tn3%;4KxypT;Wwj-Wretl| zAAFE^3LzE7c%{s(OwsgMTX#Fv_5*Q0N&f1!~epd_=Q9Lj|RoRmt6mD zQBZ!Q)hRzJa(;VL$VU-14dXv@>wltaev6p@QK$OxO~2X{zdijmUGtl}@gIWg48PhG z{J+~1k{<@e-|Pt`YPAoG;x}jFZ*lg&5jSRkXKsEAvRhNz{DZssFa$pAfIrbU|59`L z`%Aq3uQNsrA042-P-3MjF3$1}OYDv>XRNioj%MR3 zaBL(dUwVm)m3968ZSCBn{oXq0a2gysklxO2pv~gjyu?eBpK6aTc1qt17;{wElhhGp z3V>Y$jj`*se#FigzwzGJL4J}KU7z92T*E@9{NSq|AHSZF4MW;t-}y4_c1yzx`fqb3 zFl({s#K=7Y5Wf7`bO_sWIdqpeq@8ZldcZbGE}g?#QX?aXtv5H*tgNiXIdb$$`N0TU zs%>;E!jVa+EyPs#QmI%d7%#5LH1y8K3T7G?3J%5jYfSk+e^k+J_jKZ!R@&&{@xn@j zPcwx;{|uq0tFAK?-W6(3LP3CUrl;b;mRjCw-_QHwdvKvlk*vh`G{qd4u`~gEeGMcyAN_zFO7*?+Ouzv{ zM9LQHVDnxax}gKmtX*8V!C5~6E#M4dgwYYCJSGF;)iK3nM0u4}BuE9bcbmOO<`SBZ zFmLbFnv8P6Bm-ryVm#9MkJmqs#>o`{@Y)d&@JJc)npuY0qa29%15p@)`u6iFYL;SO z0II_9xp*_xH+Xr*VNDj^qEB4y-gPBUiK*9yeKt68B1?BfiqqPqQ`*^GU31uFz0-~F z=jxvfzB~=6f5oY@2+B$v*4;Wx%@+zxiu5GI8Kkmj@U= zGyvKGd-U#Y>6Puo4|R?8NGtqt9VV4d3G`b>e<`4=uScVjQOb_Wen1&vMlp*NN_}k) z^}RuSV6b3>X|^OhIZEDg;y4D(Rd!A-;5$vmf$BUb5m;?87E5o}9 z{j-AUO`}A5>uHy;vDb;+iD)={B@DRJ1f9)Jyf4q0(n?Lr7owarXao0&zL(YE#WL$VG?OXDJ70xU$w> z>$~sGLSa!cmm%gdytE-e96F!A&9aDTo6sZ=ckpZp&Dyqd@r(9W(}NT*&U+aofCAG+ z-Rto8uq2S`rSD75fC^O!n9d9#z)ycBQI&UnR(}AbVo%W=q;kpnJ`Bd0b_*3|PtmM| zT}Zu_wJ*LKscta4bbxHaT+2spZ=&uAUNve$t73{pw;i+CsEZRB7`LAc)@q_OYtv*| z^1TA=#9Bc+ZjZzo91o@DNiQw=i^1IR>cNok?t@0c`o>q{qfU@JyfvH-z%Utn(b#V> zy!>L~w#UUSW%}LAX`Q4Djn`^ZimFZ4 z*aO$KVQ;Vi5y#lG4&-@IlPH!dSiaR87I>job=ZWe*Va(5(^GQm?VEI2P5z)lT=@P? zU(p@{>Bb_Nv2*R&q}1)jl|TRMoG2j*xnL&l?%d1L(9_h~+kyV_g6gC+R;EvzuQHW5 zy3PFoQMy7KibYvxD95;<;fUVasFxVAP%Zf911NwrlcYrup^A&uM`VAMs4zi-cn`-u zNPx!&5d%UQUTv6#5y#_@5J;Xb7^^U}xAQFaXnY`#^yncs^1WHk4?L<2u)2RP$aK+F z7&{%C|66}UsIO`dy&4oUO_Y?Oi&T+V!HjHqrAIQy1d`}uqiNR+K93M$nhDmo*AmOr zx@JnM0wS=OmZ)NcMZ+V~g)l05!+WL`Y>=tLnLJ|>foK&r5Ai1=79K8UG7iqExfKm@ zMgQBP;w*#}huyWJvMJdw2L^?%9`VW1C!-$npA6U-8qVT}fXXAbcU!tow&);Hd#dYI z#LGS%I!auXC5C&GSTG3i=aRbmL^SMk6hfITCF5!r#~jr%JSVmbCn@B*13fGXMiSQ_ zn%gsDGT-vR+?X{JQ&mYusz9*f>DX;G(j{y^3$1yZj3ypasIhk#B935cHII;wAQ~Hq zS&$X~D3W9*)Q^*9A4y(J(!J`On~Yb7I+u<=P8LR))vvHI=xg2?uFV!54Qy5JLaN&&9hRPED zc9toVnI$+L*e?W-ginT5=5V*PY_flO1$n15Z{3{~qvOL?5ETtbe=35FTDNiVeWp?o&mCy zN1RxLKq@kgBD3a=C!J;RwKF*SjtG%w*{oAVYkFpNcJ5YQ3hp3A5=7&#}A9|2aJmE*W^EVyIR@$@ZI;j0dLSrzkEYeaegaYFKT zap=PPGB@;%#03v^WDFuO(pxESey^xt$M~yiv?kDwH~^_mm8v8(#j>{qHijaXZR>hB zMOl>F-s^3ib;-+#Po`B=c{)me*}6Re=0H7xCbDm*4*i6dxG9iAMw>B=#{Y-=Lyj<^geI$1wSBGYY(&);V7zKH%ckVQ`p33Ze`bJ(h(eD zhRqGJcl?WK)!3>!RIO{W=B6287aObSEXGv1UN1rHUFk8eK{)|$@J_dfCj z1V0N2qqh}u3p#0Fo1X&_-y9C*40fFFNn=e|wYeoduWAHzUg_6s_gu*XDjJFnx>$hKMt288_&AQkpwz$XR(72$la~D0n$qlZtsQQJM#~xo3z1E;DNocjy)U2zj ziDeZj7)DOIg*Lg8^taR|lf!11YM6kdUVk?n0aIkX81B%kW=m4#f_`IuZg}5%1-AAH zKJ(MhqdM@xw%E_@*tDXQ=N+@GNI>miBDKDA^Q9qW(Ac}7M)g}QshJ=*3+hT+%O}Pn zUIALY8J{n*{YKeZe1}pB+2+HJzkO}%ku=iZ@ zUk321ix80<92ieqCxvqoLKcOA$;eXDnDm!{g;*0ocW?Z?=3lA}@P3#$Flm!UVvBqN z*-75n9Yt2AoQX{55cXC{jX|AES$%YX`Ei~YL=e?bGzHUsL*tEYZi&wouUNPwl`@sH&upmY(o6IP7qw`Es;&U86V;HgM6Bs(;NW z{f0?3PfkSwWYsb{2pu1#a(Xf8gzoMVMar^w?QRtI<}NlqIw2|qrPETG=zJxpl~TfK z)TIb*)HWmcSSsV7TXf%jkZt!KY-?|^s8ZYL%L&~(Wvi4nFk4$oZpD(O(jkNF-WBpq zP^k?WdAvPps3IjJWh+Yg8++9jMsRQ;sX`_-<1mmG!xnG17IaJ?i$#VcOK^tqw>k`q zhgrZ`9<3+H5;>G|XviFS|IH+IZw+`aK0=l^htPGO`@slL2mdtj$~bO9Rc`A92%AG6 zOA4y~iU!Q*tcJu+6UWH}+1@V#z?e8x3lx*cqIXkQ-M#Pwgv?=t+AWhWrK@?>Vn1EO zB*b^mB_*W*=oFVH1vXlTBW0W@pajjR2i-o88@s_*~5-bE!# z*&@nF)|i<)n;8b#mr&V-$})Cl%#0;li%RySlBKdQSwggskdh=35ha8u*_G_yJKC7( z{rU9!KE99N<&S$`^E%t>yk6&=d+vF?o;rtyDy|gsg25pzv+B|fk6aXcIu-^C*;6wm zX6up~T;Zy|r{1XXI!agUCiDsPDQ|yTh|9(N_?k~*^?ej9^G&C|q&qcD(H{B4uhTIF z8aJP4V{M3^%PKH^N1cwH>+ilEw*fz=sa|Y6bTD=shZZmUwvLiZ$Mi#xn>lOI0h{FP%s9xafJ-N=mSX z-(%LLk&zVLo|=TOVDhcquQ=cQ942tbU8gN4^p-@qT}{AK zUjwL4KC(gk3Kucy(PXfa)s{X@(?-85iyv4>(c*@F)6h3BpvIk@UAab`;AsD?)w3q| ze)frymrACkN?x`b$0qmMwDEUb&EOUE9MvcJJA4gsX@hl94V8~1YX%G*i!e8d!-|Ng zeyYvR%bRSmh6=5PReO>BC-kAn6W$A(*x#^u*{(DCXXeX6?Tz}gp;pEE>~f#SUWObB z&yeDJ6@GhrJr){2!<8H|A^#7#Ks;yCtI%Sb&BFC>V`>GMgetp~aE+jW-hBDPohw3Tv}|-=)M%wW`*@48Nz&Ln>&&>mBwCFi7;GyhHAZc zZ5m(6dHa`Fs?L-M87@WEZ5GH6w8V&tio>p!&A_y^Z{-y}(qc;%xf;K(y&!=@N}^S# zU~3ks_^rRe+hY%#4-Kc`t@44yt`YvcsiPw%i5+UCsc22N2Vb6J)jDbkN1v zXKPFyCDiz{$MJ@TLE(NHljo{>;yZFnjPQ>fd-tvh$w(^;JH=|M=qSx8@NqJ*0%%Lh zUZa?CqAH}MR@Qe^vbzB&UYg_hXG5jgC-?22cRX${7GmcOHBzzKT7Fe#uBrN-`_$VO z^t_PO)C>8C5uNDZJEw(k7jz_V3T8!~IDoyl+h?w8Y&Y<%+SMzC)%J||i3oDTRKw2W zC*lhf*@-c8rm2N@pCf?1XBTM zURXcewZLCiZYV83{&Lr%`L6zPKZ)kp{kPjm*2`N%UaPi*XpWF89kNz9M*jWbP%M1q z*-)AD7P?%=_#Q8*<}AK)_iRJe4C+7073O100fe*0i*}c}Ul$w6zrkfp7{Wkac>&B44WUYRd#;m=m*S;afVqE7BDwgZ#AC5BOCQvZ3 z6fYPNh-1pAy?eFY%EY8JrrprMphmE;=>B8J0)U6Ps{Rn0iXsXwj!iwob6>YEVw4ai35&69?c)0=s+HQy=M5aoILkrAO^u;<~U2l}6ihr6=1UbnP|OlNkdi3$UHETW+#AtSO*e#;qTH1%-m z!YxWz_Gce^_Sqh1ht>h!g!0C7_jFzScgtcaIlGS42Nv}@@(f$t2%(VHS|(oiZkv-z z=GpLmi=LOKb~*KZdo7in#I75=$e!p74B?p0%T9cUB*X`lMJFoc~PeZQ@3)29%pX zf3^5rZuI2AD^*V)#q4iy$27z9M3E_KQ^&quf6<>mCsm|&ek7t$evpLymf;A0tCNWb zHoPt`<;lE9K7mVbE)<+wcUK75{s(|ecn;lZ$mlgBD;nP{& z6FhlE%I!C}5&Lrv!@A=3XHJbHC$CA?R$WT2ZyEej72FunyVh~s%WEu;YN*#+C|7AY zr?zWttcdx7P;cpF=2%0L6$)KEv-UcdJ+X@~W^-EE?9&aK+cMTFMU3*OULD?{T;3Y9 zt3ROV)}FXS*_MMA=#me^hkPSSQR(I~>gesK7dK4bx3^>*UsePZ{f`^ge?Z{-HNc=~ z5msrSl>aio(BLXp>{u^9{vKfd)g6?!mHqD{%=b)JMp|9HIsG%j>MwUt+P3tn5r{6H zJ?4KG&mMtZiM3CG#SR7rdSelDE#loJ#&B7!gAe6u@FI%&;cy|7VN}!C^wT#m*ll91& z8&69LOWz$TX*{l{rpI;Q9k$pOpKc^U-aK4b`gT`qI$wsBD=jD>>EFN{kJP_j=-TS) zX?7=|%zHRWd1>?+fN#(IYPByybkn;{6&AiNa8Sk^# zhl*$?os!)ArO+n(eL|8xq2OiOyk-GlXRZZ%-rPTBTJQD2rS-WYKbOLXvz9!<94B{Y z?qhjGP1-Mi(J|+9x72n)(i$_tjLaz24L*6F$JW=Zd0Hr?KrtHJR^GVY;p&B6|JOsD zT$^Jf#|N*6XR>zkN9LeSg9I`#50gdi&$Ccip=>vH*9^YxmpIM&T5?dmNc#n=O3}$D z199h)J<{EZvh_TABxk1$)93kb^fyZ5c_W@6$E5{BpTu-Ya7U^(CG@dqCQIm?DZhKc zA|fb1g}ZoD)4<4Ebzw>D*39lCnVgx8Gpgs$f8di6POEvVO4xsCP#EEHd};nebyfc~ zyt=p7cQ*3b?O>sdI0Y{YLF-qNmOKI7L3<*h0~>R&Wpk(~UbwMD%n-$RI%}lKahLS| zeZd5uT~R#L)APpJZDPrIp}H8c*^{>w-_A@un5s*&xdz876{HM_~O??-BiIVpTq@~>v*uE;f4|r)3C4c13o&S zc+EtQmDZ`0nD#vN0MUiYch03fo+qE!d6^hZw4P?oARYK!F5~`YPmNUD$)P6s1mK}cJKK|X^DgF!~LR{FwbG$JKwEyt)KPW7o$HSZ&~B* zRDS6=CeU#L8_92VY53k4G~vPnPq%li@z*+USSc6}Bn~$m3Om4*yD3*4A9xA3kvGa> zi@%;!?6YR0-jVt;$GdEwyWH`!efGXW8|U9mbC|%!wp+!OV1UPd1=~tr-wGHQNz%^q zsbAcF$&txIp@6MhPDN^VLrRmCICqxy0m%wj+1(yQDL0HQdQcA4^d|IT<>BnJo%8U= zX~yxf+2OvWcV^|LqKD+BOlFXdc9)G?r^gYG6SL3mIXA)6tL-Tja?#^ln(AoV66DjR zixLO*yYuvx{aRY zJ(W11OBFnUe=X9-{PhU)oe~cr9lm#bA2A`V%#Q1uhTYY2`i?~p%g#L(JDIe7$31kpht==QpX3Y>E5ljb>U2A6KzjXI41e6m zJq>rqr%hu+j)T8VW_J)Tc4&;*?uwL&r|OQDQ?C~^dDEL7q;)(zD_x-Xim(@Gaw{WU zy`m~RB^S8?vs?MhvzF@jo6hx;b}fh&ow-jE#5teHDKvdk^^b{PbOXn0VM`G=AHmr~ z@qa#CSjUWQwCp%BkZehrM51Jh229Ik79MIv-n#1h&@0xAFH8ScYLkkTp{wMrLzi`< z5+m-0R(GF@&u)Ab>@zm4YTHe<5xnSx9%&@7frOd zN?YYVP?>rFC3|AqA?Kll0C9cq08&vD>ZQnqXF-Y=m38=L(XW`&dPsj|=gBt$P+0DO2g@O@vDk{2M^G})U({NBk&6m)nlf2CofdHH zQ+~jZ%{OyuMtNzJW&+>KO=@}eA+OW%BXCoHN(7W{-M&3+U0CN3!V6 z^bK{jRSC!NyY}n9lM4uZuX5CoWF-GmSRqvL-SMTT82rbLutQ7<4#mxl24dYzk>oHb z8wnpOY73=o)-0rkm7FSA%8yzQc$DI#g z=?TwttM*5rt0H<_;`GNnk0ZOU6}*W4P#?tlnl0zIt*LIj}V+pEHTB3f8EP*e*pVMHP-`+Q!_r6!R;S&w+Z+){GX*ay*2Dy@hY>ktv zHkVu5?)El&eRQ80R()YZRD!GtcGH9hGTltPqm)wNv|c7xlc{TAPx6P@t|B0Iyx-5Q(vAvd-jEs682>x?By`Z zle-SN55axPAj~kV&cKlS?Zl)G_dF-XkOz|A9CSc2L^ykENCtCA##vTYR$Yx6)^Mxv zPS*PHaOuc|K%U&hZd%6y?-Y4SnW*5T2itBneUekuc}zb=;J z>nd*gS3K-^*VX!_wX?OeqrHipvut*b#YNLk+$`%(-pzFqUl%@&=HvzpbIFTS*I5&l z%ti}Gqtq)#*Hm>Kt*tY?-JQ9ha{IYu!oB{xX7vM;B=-+J?f$2OV^6MK6SgT=@((Jz zBHGJ;e9NJSV*aJD01YYrH@X}h=-2-OVGi*}EZSc>OYpIEwRT&nva)n>dY7O7pU==B z0pyA!G`~XLfe3R&>sKSpDZF2SFt_jYgW%1996d`rB`U#~TOh(*_x~S&IZH->IX>{> z;pe*o{_&gRL3Iu2dcAP9r{R>4@g%>{afhSKrH3`CRwIe;-@m=VdQb0oim$WZA$#h+ zhQX1z7G#WVGjUzhrN?0u%E^g)VPU5EmiK+q1&@4uDAYiCFrb%k_x!N;OX^o+OVgkF z1&yn%rg&mFVC&YcsrGaiV^lCKy@KfxsMdDYRO{bJ(`I_QKVhZ;1p0RvA-s|g$=cS1 zK!w;49Gu)0#7E02#34?03gV_{J-8l8mEh>4#0vja@VbA2}a4k{ehJh>x4AJ4Mb%L3}xh9C%M7!^9!W zEL0Z-aWlOG5Gs-A>f%I&AfPxXAOj$!A@*bt@Y|b6c7Xs;j5wGj+0I_hKuzOEhTxNe zxFeNHl7qp#y}hB{NGOr)00Y3|N-#JAhCs-G95R$+?o?|Z8Fz{ZSl)6)oXmbDbEiO; z>jVXZJ;I#KU;q>j`&kfe)F(TUXfEmyTEW&fL{F;1u3bNJA+0EVRW{%cU_MB&dElMg z0W#6f)0RM15Z64Q3(<5WQmEgv1y9&P;Q$m6hy7^Se<=?X=AWw#_P~#N<3S!dJ))hH z{V_FbDnSteM<8Y3DDdA1K*^y2ITQ}OmxIIcFgi}Kx4@*TWCED%Z<4OyT#=MWHUj%l z(ay_>M3HcjgwV=|0uTu!f*C{?gs)yENJ1d0MAETk48Uaq#K79l$=2ExqJE43F(lek zy+O3V?=@U5=0~o07_Adl2XNu39{iE&M0F)7E}Md~EA{)0s}oHr`;ZCtEVS?=EHoAVenG&61bF1v9`c!vR@PT(s*K4S*w&^n7rfEP{as2LSLy@~X6OBmhQ_TulSZl?8)ytl|SOC^)zy zx{8KE;gH}=w~7X!u?%U!aJL9XJ_HsF-?Az#5`m=!Y+XeIzy{N|0||orGUSJnr9l;} zN{hguXh_1VXaEX{0FNK9q9MR4gWsE0(Et=&mcG3REF27UNXG}ps-%}60*%Jerv)c@ zhJFL}mQnTy1S20D4Mtq1D;EI=u`cLnI2@K<1^^t*C{s8ZMK2dP4$F`h)D0Yc+u&&0 z*F(B;0W^+5Ut}5c0{|rLZIO2U)?HZy7*U#z2FGCO>qk2QPcH+oE+~3ifXm_-+6HPk zie4@#ECRGNx^gjC+RBY~{i+{m2`G9RfT5kqr{hCn0R}!emQnxU0PV}dsxrVj)0Xe6 zX*djyQ3ikLUx3j*05F~rLmz>rMK5~<9AJ<$0**t_*AIb2(!M*dsviQ3c1&+G2vDXB zWnghw`nn)+7&N`Ckl+|buLnrbRO#i6#Gx4U83m61^yQ+^2(TAd*BK=%i)P@%qEPhh z07prHk%nd%{{S$YIlcY?2mni81_1iS(8~Zo!qN0?1CX*bSBO<|22cpbGEf+Xu@0R2 z0DAcWXjwFUzX2EwV|ziT5&HU}KvP)JM^v)4lPiJDg2zK(hEBc&aNdHz42VQ31WX7q zfWWlf?THZDJZ=CU5Kx0y;MK9}8XC%~NDUPE%1BvNBt}I=7K_0s{&x;5 b7BG-7g=$TvE>D(da5}`Wh>EK3*I@Y{T*n`& literal 0 HcmV?d00001 diff --git a/specifications/LeastCircularSubstring/LeastCircularSubstring.tla b/specifications/LeastCircularSubstring/LeastCircularSubstring.tla new file mode 100644 index 00000000..f7e63397 --- /dev/null +++ b/specifications/LeastCircularSubstring/LeastCircularSubstring.tla @@ -0,0 +1,165 @@ +---------------------- MODULE LeastCircularSubstring ------------------------ +(***************************************************************************) +(* An implementation of the lexicographically-least circular substring *) +(* algorithm from the 1980 paper by Kellogg S. Booth. See: *) +(* https://doi.org/10.1016/0020-0190(80)90149-0 *) +(***************************************************************************) + +EXTENDS Integers, ZSequences + +CONSTANTS CharacterSet + +ASSUME CharacterSet \subseteq Nat + +(**************************************************************************** +--algorithm LeastCircularSubstring + variables + b \in Corpus; + n = ZLen(b); + f = [index \in 0..2*n |-> nil]; + i = nil; + j = 1; + k = 0; + define + Corpus == ZSeq(CharacterSet) + nil == -1 + end define; + begin +L3: while j < 2 * n do +L5: i := f[j - k - 1]; +L6: while b[j % n] /= b[(k + i + 1) % n] /\ i /= nil do +L7: if b[j % n] < b[(k + i + 1) % n] then +L8: k := j - i - 1; + end if; +L9: i := f[i]; + end while; +L10: if b[j % n] /= b[(k + i + 1) % n] /\ i = nil then +L11: if b[j % n] < b[(k + i + 1) % n] then +L12: k := j; + end if; +L13: f[j - k] := nil; + else +L14: f[j - k] := i + 1; + end if; +LVR: j := j + 1; + end while; +end algorithm; + +****************************************************************************) +\* BEGIN TRANSLATION (chksum(pcal) = "c2e05615" /\ chksum(tla) = "81694c33") +VARIABLES b, n, f, i, j, k, pc + +(* define statement *) +Corpus == ZSeq(CharacterSet) +nil == -1 + + +vars == << b, n, f, i, j, k, pc >> + +Init == (* Global variables *) + /\ b \in Corpus + /\ n = ZLen(b) + /\ f = [index \in 0..2*n |-> nil] + /\ i = nil + /\ j = 1 + /\ k = 0 + /\ pc = "L3" + +L3 == /\ pc = "L3" + /\ IF j < 2 * n + THEN /\ pc' = "L5" + ELSE /\ pc' = "Done" + /\ UNCHANGED << b, n, f, i, j, k >> + +L5 == /\ pc = "L5" + /\ i' = f[j - k - 1] + /\ pc' = "L6" + /\ UNCHANGED << b, n, f, j, k >> + +L6 == /\ pc = "L6" + /\ IF b[j % n] /= b[(k + i + 1) % n] /\ i /= nil + THEN /\ pc' = "L7" + ELSE /\ pc' = "L10" + /\ UNCHANGED << b, n, f, i, j, k >> + +L7 == /\ pc = "L7" + /\ IF b[j % n] < b[(k + i + 1) % n] + THEN /\ pc' = "L8" + ELSE /\ pc' = "L9" + /\ UNCHANGED << b, n, f, i, j, k >> + +L8 == /\ pc = "L8" + /\ k' = j - i - 1 + /\ pc' = "L9" + /\ UNCHANGED << b, n, f, i, j >> + +L9 == /\ pc = "L9" + /\ i' = f[i] + /\ pc' = "L6" + /\ UNCHANGED << b, n, f, j, k >> + +L10 == /\ pc = "L10" + /\ IF b[j % n] /= b[(k + i + 1) % n] /\ i = nil + THEN /\ pc' = "L11" + ELSE /\ pc' = "L14" + /\ UNCHANGED << b, n, f, i, j, k >> + +L11 == /\ pc = "L11" + /\ IF b[j % n] < b[(k + i + 1) % n] + THEN /\ pc' = "L12" + ELSE /\ pc' = "L13" + /\ UNCHANGED << b, n, f, i, j, k >> + +L12 == /\ pc = "L12" + /\ k' = j + /\ pc' = "L13" + /\ UNCHANGED << b, n, f, i, j >> + +L13 == /\ pc = "L13" + /\ f' = [f EXCEPT ![j - k] = nil] + /\ pc' = "LVR" + /\ UNCHANGED << b, n, i, j, k >> + +L14 == /\ pc = "L14" + /\ f' = [f EXCEPT ![j - k] = i + 1] + /\ pc' = "LVR" + /\ UNCHANGED << b, n, i, j, k >> + +LVR == /\ pc = "LVR" + /\ j' = j + 1 + /\ pc' = "L3" + /\ UNCHANGED << b, n, f, i, k >> + +(* Allow infinite stuttering to prevent deadlock on termination. *) +Terminating == pc = "Done" /\ UNCHANGED vars + +Next == L3 \/ L5 \/ L6 \/ L7 \/ L8 \/ L9 \/ L10 \/ L11 \/ L12 \/ L13 \/ L14 + \/ LVR + \/ Terminating + +Spec == Init /\ [][Next]_vars + +Termination == <>(pc = "Done") + +\* END TRANSLATION + +TypeInvariant == + /\ b \in Corpus + /\ n = ZLen(b) + /\ f \in [0..2*n -> 0..2*n \cup {nil}] + /\ i \in 0..2*n \cup {nil} + /\ j \in 0..2*n \cup {1} + /\ k \in ZIndices(b) \cup {0} + +\* Is this shift the lexicographically-minimal rotation? +IsLeastMinimalRotation(s, r) == + LET rotation == Rotation(s, r) IN + /\ \A other \in Rotations(s) : + /\ rotation \preceq other.seq + /\ rotation = other.seq => (r <= other.shift) + +Correctness == + pc = "Done" => IsLeastMinimalRotation(b, k) + +============================================================================= + diff --git a/specifications/LeastCircularSubstring/MCLeastCircularSubstring.tla b/specifications/LeastCircularSubstring/MCLeastCircularSubstring.tla new file mode 100644 index 00000000..a9b1ffee --- /dev/null +++ b/specifications/LeastCircularSubstring/MCLeastCircularSubstring.tla @@ -0,0 +1,11 @@ +--------------------- MODULE MCLeastCircularSubstring ----------------------- +EXTENDS Naturals, LeastCircularSubstring + +CONSTANTS CharSetSize, MaxStringLength + +ZSeqNat == 0 .. MaxStringLength + +MCCharacterSet == 0 .. (CharSetSize - 1) + +============================================================================= + diff --git a/specifications/LeastCircularSubstring/MCLeastCircularSubstringMedium.cfg b/specifications/LeastCircularSubstring/MCLeastCircularSubstringMedium.cfg new file mode 100644 index 00000000..f1d2d915 --- /dev/null +++ b/specifications/LeastCircularSubstring/MCLeastCircularSubstringMedium.cfg @@ -0,0 +1,12 @@ +SPECIFICATION Spec + +INVARIANT + TypeInvariant + Correctness + +CONSTANTS + CharSetSize = 3 + MaxStringLength = 8 + CharacterSet <- MCCharacterSet + Nat <- [ZSequences]ZSeqNat + diff --git a/specifications/LeastCircularSubstring/MCLeastCircularSubstringSmall.cfg b/specifications/LeastCircularSubstring/MCLeastCircularSubstringSmall.cfg new file mode 100644 index 00000000..e7b268dc --- /dev/null +++ b/specifications/LeastCircularSubstring/MCLeastCircularSubstringSmall.cfg @@ -0,0 +1,12 @@ +SPECIFICATION Spec + +INVARIANT + TypeInvariant + Correctness + +CONSTANTS + CharSetSize = 2 + MaxStringLength = 6 + CharacterSet <- MCCharacterSet + Nat <- [ZSequences]ZSeqNat + diff --git a/specifications/LeastCircularSubstring/README.md b/specifications/LeastCircularSubstring/README.md new file mode 100644 index 00000000..01f4123b --- /dev/null +++ b/specifications/LeastCircularSubstring/README.md @@ -0,0 +1,10 @@ +# Least Circular Substring + +This is a spec the least circular substring algorithm described in [*Lexicographically Least Circular Substrings*](https://doi.org/10.1016/0020-0190(80)90149-0) by Kellogg S. Booth. +The spec is notable for being a PlusCal implementation of a complicated sequential string algorithm. +It was written to explore the feasibility of using PlusCal as a replacement for pseudocode in published papers and textbooks. +You can read about the findings [here](https://ahelwer.ca/post/2023-03-30-pseudocode/). +PlusCal was compared against a Python implementation of the same algorithm; the Python implementation is also included in this directory. + +Since the algorithm as given in the paper uses 0-indexed strings and TLA⁺ uses 1-indexed sequences, a `ZSequences.tla` module was written that behaves similar to `Sequences.tla` but indexed from 0. + diff --git a/specifications/LeastCircularSubstring/ZSequences.tla b/specifications/LeastCircularSubstring/ZSequences.tla new file mode 100644 index 00000000..2ef96297 --- /dev/null +++ b/specifications/LeastCircularSubstring/ZSequences.tla @@ -0,0 +1,78 @@ +------------------------------ MODULE ZSequences ---------------------------- +(***************************************************************************) +(* Defines operators on finite zero-indexed sequences, where a sequence of *) +(* length n is represented as a function whose domain is the set 0..(n-1) *) +(* (the set {0, 1, ... , n-1}). *) +(***************************************************************************) + +LOCAL INSTANCE FiniteSets +LOCAL INSTANCE Naturals +LOCAL INSTANCE Sequences + +\* The empty zero-indexed sequence +EmptyZSeq == <<>> + +\* The set of valid indices for zero-indexed sequence s +ZIndices(s) == + IF s = EmptyZSeq + THEN {} + ELSE DOMAIN s + +\* The set of all zero-indexed sequences of elements in S with length n +LOCAL ZSeqOfLength(S, n) == + IF n = 0 + THEN {EmptyZSeq} + ELSE [0 .. (n - 1) -> S] + +\* The set of all zero-indexed sequences of elements in S +ZSeq(S) == UNION {ZSeqOfLength(S, n) : n \in Nat} + +\* The length of zero-indexed sequence s +ZLen(s) == + IF s = EmptyZSeq + THEN 0 + ELSE Cardinality(DOMAIN s) + +\* Converts from a one-indexed sequence to a zero-indexed sequence +ZSeqFromSeq(seq) == + IF seq = <<>> + THEN EmptyZSeq + ELSE [i \in 0..(Len(seq)-1) |-> seq[i+1]] + +\* Converts from a zero-indexed sequence to a one-indexed sequence +SeqFromZSeq(zseq) == + IF zseq = EmptyZSeq + THEN <<>> + ELSE [i \in 1..ZLen(zseq) |-> zseq[i-1]] + +\* Lexicographic order on zero-indexed sequences a and b +a \preceq b == + LET + s1len == ZLen(a) + s2len == ZLen(b) + RECURSIVE IsLexLeq(_, _, _) + IsLexLeq(s1, s2, i) == + CASE i = s1len \/ i = s2len -> s1len <= s2len + [] s1[i] < s2[i] -> TRUE + [] s1[i] > s2[i] -> FALSE + [] OTHER -> IsLexLeq(s1, s2, i + 1) + IN IsLexLeq(a, b, 0) + +\* Rotate the string s to the left by r indices +Rotation(s, r) == + IF s = EmptyZSeq + THEN EmptyZSeq + ELSE [i \in ZIndices(s) |-> s[(i + r) % ZLen(s)]] + +\* The set of all rotations of zero-indexed sequence s +Rotations(s) == + IF s = EmptyZSeq + THEN {} + ELSE {[ + shift |-> r, + seq |-> Rotation(s, r) + ] : r \in ZIndices(s) + } + +============================================================================= + diff --git a/specifications/LeastCircularSubstring/lcs.py b/specifications/LeastCircularSubstring/lcs.py new file mode 100644 index 00000000..a1f87344 --- /dev/null +++ b/specifications/LeastCircularSubstring/lcs.py @@ -0,0 +1,41 @@ +''' +This is an implementation of the Booth Least Circular Substrings algorithm. +To use the algorithm, import this module then call the lcs function with your +string. To run the property-based test, install Hypothesis and PyTest using +pip -r requirements.txt then run pytest lcs.py. +''' + +def lcs(b): + n = len(b) + f = [-1] * (2 * n) + k = 0 + for j in range(1, 2 * n): + i = f[j - k - 1] + while b[j % n] != b[(k + i + 1) % n] and i != -1: + if b[j % n] < b[(k + i + 1) % n]: + k = j - i - 1 + i = f[i] + if b[j % n] != b[(k + i + 1) % n] and i == -1: + if b[j % n] < b[(k + i + 1) % n]: + k = j + f[j - k] = -1 + else: + f[j - k] = i + 1 + return k + +def naive_lcs(s): + n = len(s) + if n == 0: + return 0 + rotations = [s[i:] + s[:i] for i in range(n)] + least_rotation = min(rotations) + return rotations.index(least_rotation) + +from hypothesis import given, settings +from hypothesis.strategies import text, sampled_from + +@settings(max_examples=10000) +@given(text(sampled_from("abc"))) +def test_lcs(b): + assert lcs(b) == naive_lcs(b) + diff --git a/specifications/LeastCircularSubstring/requirements.txt b/specifications/LeastCircularSubstring/requirements.txt new file mode 100644 index 00000000..847933d4 --- /dev/null +++ b/specifications/LeastCircularSubstring/requirements.txt @@ -0,0 +1,3 @@ +hypothesis == 6.70.0 +pytest == 7.2.2 +