Formal Card-Game Systems
r1 qualified Selected asymmetric formal reference: 2,502 contracts across nine families; bounded evidence and three separate teaching models Read the evidence scope

PendingChecksMC

Complete selected asymmetric reference profile. Definitions and supplied fixtures are distinct from the three teaching specializations; review and qualification are stated in the bound evidence and release.

Package reference-profile, input revision 2. Exact prepared source; CC0 1.0.

This is a definition inventory. Start with the learning chapters for the contract and its assumptions.

This model/fact module also contains 118 local fixture helpers outside the selected contract inventory. Their complete executable text remains in the exact module download and owning definition bodies. Listed dependencies include paths through those helpers. All selected contracts and frozen nested helpers retain their own entries.

PendingProfiles · constant

reference-profile · input revision 2 · CC0 1.0

PendingProfiles

Exact module download · Source bundle and reproduction instructions

U4Admit · operator

reference-profile · input revision 2 · CC0 1.0

U4Admit(q,ledger,snapshot) == /\ U4CurrentBound(q)
 /\ AdmitConditionalSnapshotSA(q.catalog,q.basis,ledger,q.uses,q.turnUses,q.useIndex,q.procedures,
 U4Template(q,snapshot.id,snapshot.point,snapshot.checkpointId),snapshot,MinimalCaptureSA(q.basis))

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: AdmitConditionalSnapshotSA, MinimalCaptureSA, U4CurrentBound, U4Template

U4BeginAllowed · operator

reference-profile · input revision 2 · CC0 1.0

U4BeginAllowed(q,id) ==
 LET c==U4Choice(q,id) d==q.catalog[2].definition IN
 /\ U4Admit(q,q.ledger,q.current)
 /\ BeginConditionalResolution96(q.ledger,c.ledger,q.stack,c.stack,c.p,c.afterP,d,q.current,id,c.option,
      U4Legality(WindowTop9(q.stack),c.option,U4ChildTransaction(q.round)),EmptyT11,c.plan,c.afterPlan,
      ProtocolP!Targets9p(c.plan),ProtocolP!Entry9p(c.plan,0),
      FamilyTurnUsesSA(q.catalog,q.useIndex,q.turnUses,"Conditional",d.syntax.source),
      [tag |-> "AbilityRestrictions",ability |-> d.syntax.id,source |-> d.syntax.source,results |-> EmptyT11])

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: BeginConditionalResolution96, WindowTop9, FamilyTurnUsesSA, ProtocolP!Entry9p, ProtocolP!Targets9p, U4Admit, U4ChildTransaction, U4Choice, U4Legality, EmptyT11

U4CP · operator

reference-profile · input revision 2 · CC0 1.0

U4CP(q,caller,events) ==
 LET id==q.ledger.lastCheckpoint+1
     beginning==U4Snapshot(q,q.ledger,q.nextSnapshot,"CheckpointBeginning",id)
     processing==U4Snapshot(q,q.ledger,q.nextSnapshot+1,"ProcedureCodee605a78f5d5e",id)
 IN [tag |-> "ConditionalCheckpoint",point |-> "ProcedureCodee605a78f5d5e",id |-> id,previousCheckpoint |-> q.ledger.lastCheckpoint,
 serial |-> q.ledger.serial+1,previousSnapshot |-> q.ledger.lastSnapshot,beginSnapshot |-> beginning,
 processingSnapshot |-> processing,stepSerial |-> q.ledger.stepSerial,occurrences |-> events,caller |-> caller]

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: U4Snapshot

U4CaptureFrame · operator

reference-profile · input revision 2 · CC0 1.0

U4CaptureFrame(before,after) ==
 /\ DOMAIN before.captures \subseteq DOMAIN after.captures
 /\ \A id \in DOMAIN before.captures : after.captures[id]=before.captures[id]

Exact module download · Source bundle and reproduction instructions

U4CaptureSafety · operator

reference-profile · input revision 2 · CC0 1.0

U4CaptureSafety ==
 LET q==qT11 IN
 /\ q.captures[U4InitialSnapshot.id]=U4Captured(U4InitialBasis,U4InitialSnapshot)
 /\ Cardinality(DOMAIN q.captures)=q.nextSnapshot-1000
 /\ \A id \in DOMAIN q.captures :
      LET c==q.captures[id] IN /\ c.snapshot.id=id /\ RegistryValidSA(q.catalog,c.basis.registry)
        /\ c.snapshot.definitions=ConditionalDefinitionsSA(c.basis.registry) /\ c.snapshot.present=ConditionalPresentSA(c.basis.registry)
        /\ c.snapshot.objects=c.basis.objects /\ c.snapshot.activity.activeRules=c.basis.rulePermissions
 /\ \A id \in DOMAIN q.checkpointHistory :
      /\ q.checkpointHistory[id].beginSnapshot=q.captures[q.checkpointHistory[id].beginSnapshot.id].snapshot
      /\ q.checkpointHistory[id].processingSnapshot=q.captures[q.checkpointHistory[id].processingSnapshot.id].snapshot
 /\ q.ledger.lastSnapshot=IF q.ledger.lastCheckpoint=0 THEN U4InitialSnapshot ELSE q.checkpointHistory[q.ledger.lastCheckpoint].processingSnapshot

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: ConditionalDefinitionsSA, ConditionalPresentSA, RegistryValidSA, U4Captured, U4InitialBasis, U4InitialSnapshot, qT11

U4Captured · operator

reference-profile · input revision 2 · CC0 1.0

U4Captured(basis,snapshot) == [basis |-> MinimalCaptureSA(basis),snapshot |-> snapshot]

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: MinimalCaptureSA

U4Catalog · operator

reference-profile · input revision 2 · CC0 1.0

U4Catalog == [key \in {2,3} |-> IF key=2 THEN SRowSA("Conditional",U4ConditionalDefinition) ELSE SRowSA("Paid",U4PaidDefinition)]

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: U4ConditionalDefinition, U4PaidDefinition, SRowSA

U4ChildTransaction · operator

reference-profile · input revision 2 · CC0 1.0

U4ChildTransaction(round) == 1900+round

Exact module download · Source bundle and reproduction instructions

U4Choice · operator

reference-profile · input revision 2 · CC0 1.0

U4Choice(q,id) ==
 LET w==WindowTop9(q.stack) d==q.catalog[2].definition
     option==PriorityOption9(70+q.round,"Conditional","SideB",d.syntax.id,id,d.syntax.source,0,{})
     p==OpenConditionalProcedure96(id,d,w,option,U4ChildTransaction(q.round),"Rule")
     plan==OpenInstruction93(710,"Ability",id,d.syntax.source,"Rule",1,"NoValue",<<"PendingReaction">>,FALSE)
 IN [option |-> option,p |-> p,afterP |-> [p EXCEPT !.phase="Imminent",!.ability.phase="Imminent",!.ability.firstImminent=TRUE,!.ability.detached=TRUE],
 plan |-> plan,afterPlan |-> [plan EXCEPT !.phase="Imminent",!.announced=TRUE],
 ledger |-> [q.ledger EXCEPT !.instances[id].status="Imminent"],
 stack |-> ReplaceWindowTop9(q.stack,StartPriorityOptionFrame9(w,option,U4ChildTransaction(q.round)))]

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: OpenConditionalProcedure96, OpenInstruction93, PriorityOption9, ReplaceWindowTop9, StartPriorityOptionFrame9, WindowTop9, U4ChildTransaction

U4ConditionalDefinition · operator

reference-profile · input revision 2 · CC0 1.0

U4ConditionalDefinition == SConditionalSA

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: SConditionalSA

U4ConditionalId · operator

reference-profile · input revision 2 · CC0 1.0

U4ConditionalId(round) == 200+round

Exact module download · Source bundle and reproduction instructions

U4Context · operator

reference-profile · input revision 2 · CC0 1.0

U4Context(q) == PaidContextFromRegistrySA(q.catalog,q.basis,q.ledger,q.useIndex,q.turnUses,U4ContextTemplate,3)

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: PaidContextFromRegistrySA, U4ContextTemplate

U4ContextTemplate · operator

reference-profile · input revision 2 · CC0 1.0

U4ContextTemplate == [STemplateSA EXCEPT !.ownRestrictions.ability=U4PaidDefinition.syntax.id,!.ownRestrictions.source=U4PaidSource,
 !.otherRestrictions.ability=U4PaidDefinition.syntax.id,!.otherRestrictions.source=U4PaidSource]

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: U4PaidDefinition, U4PaidSource, STemplateSA

U4CostOccurrences · operator

reference-profile · input revision 2 · CC0 1.0

U4CostOccurrences(q) == [id \in {U4OccurrenceId(q.round)} |-> q.occurrences[id]]

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: U4OccurrenceId

U4CurrentBound · operator

reference-profile · input revision 2 · CC0 1.0

U4CurrentBound(q) == ConditionalBindingSA(q.catalog,q.basis,q.ledger,q.current,q.current,q.currentBasis)

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: ConditionalBindingSA

U4DoneSafety · operator

reference-profile · input revision 2 · CC0 1.0

U4DoneSafety ==
 LET q==qT11 IN q.stage="Done" =>
 /\ q.stack= <<>> /\ Cardinality(DOMAIN q.uses)=U4Rounds(q) /\ Cardinality(DOMAIN q.returnedPaid)=U4Rounds(q)
 /\ ~q.wallet.checkpointDue
 /\ (q.NeutralValue00013 # "no-loss" => "RejectLost" \in DOMAIN q.rejections /\ 201 \notin DOMAIN q.returnedChildren)
 /\ (U4Restores(q) => "RejectRestored" \in DOMAIN q.rejections /\ q.ledger.instances[202].status="Complete")
 /\ (q.NeutralValue00013="no-loss" => DOMAIN q.returnedChildren={201,202})

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: U4Restores, U4Rounds, qT11

U4EventuallyDone · operator

reference-profile · input revision 2 · CC0 1.0

U4EventuallyDone == <> (qT11.stage="Done")

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: qT11

U4Fresh · operator

reference-profile · input revision 2 · CC0 1.0

U4Fresh(q,ids) == ids \subseteq Nat \ {0} /\ ids \cap DOMAIN q.captures={}

Exact module download · Source bundle and reproduction instructions

U4HistoryValid · operator

reference-profile · input revision 2 · CC0 1.0

U4HistoryValid(q) == UseProvenanceValidSA(q.catalog,q.uses,q.turnUses,q.useIndex,q.procedures)

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: UseProvenanceValidSA

U4Init · operator

reference-profile · input revision 2 · CC0 1.0

U4Init == registryCaseSA=0 /\ guideCaseT11=0 /\ \E NeutralValue00013 \in PendingProfiles : qT11=U4Initial(NeutralValue00013)

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: PendingProfiles, U4Initial, registryCaseSA, guideCaseT11, qT11

U4Initial · operator

reference-profile · input revision 2 · CC0 1.0

U4Initial(NeutralValue00013) == [catalog |-> U4Catalog,basis |-> U4InitialBasis,ledger |-> U4InitialLedger,stack |-> <<>>,
 current |-> U4InitialSnapshot,currentBasis |-> MinimalCaptureSA(U4InitialBasis),
 captures |-> [id \in {U4InitialSnapshot.id} |-> U4Captured(U4InitialBasis,U4InitialSnapshot)],nextSnapshot |-> 1001,
 NeutralValue00013 |-> NeutralValue00013,round |-> 1,stage |-> "Open",resume |-> "Reserve",wallet |-> ItemInspectionWalletInitialT11,
 paid |-> EmptyT11,plan |-> EmptyT11,child |-> EmptyT11,childPlan |-> EmptyT11,uses |-> EmptyT11,turnUses |-> EmptyT11,
 useIndex |-> EmptyT11,procedures |-> EmptyT11,native |-> EmptyT11,occurrences |-> EmptyT11,
 usedWindows |-> {},usedInstances |-> {},usedTransactions |-> {},usedUses |-> {},checkpointHistory |-> EmptyT11,
 costCheckpoint |-> 0,closedWindows |-> EmptyT11,returnedPaid |-> EmptyT11,returnedChildren |-> EmptyT11,
 readyAdmissions |-> EmptyT11,rejections |-> EmptyT11,publications |-> <<>>,work |-> <<>>]

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: MinimalCaptureSA, ItemInspectionWalletInitialT11, U4Captured, U4Catalog, U4InitialBasis, U4InitialLedger, U4InitialSnapshot, EmptyT11

U4InitialBasis · operator

reference-profile · input revision 2 · CC0 1.0

U4InitialBasis == BasisSA(0,U4Catalog,EmptyT11,{U4PaidSource.rule,U4ConditionalDefinition.syntax.source.rule})

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: BasisSA, U4Catalog, U4ConditionalDefinition, U4PaidSource, EmptyT11

U4InitialLedger · operator

reference-profile · input revision 2 · CC0 1.0

U4InitialLedger == NewConditionalLedger96(U4InitialSnapshot)

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: NewConditionalLedger96, U4InitialSnapshot

U4InitialSnapshot · operator

reference-profile · input revision 2 · CC0 1.0

U4InitialSnapshot == ConditionalSnapshotFromRegistrySA(U4Catalog,U4InitialBasis,U4SeedLedger,PInitialSnapshot)

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: ConditionalSnapshotFromRegistrySA, PInitialSnapshot, U4Catalog, U4InitialBasis, U4SeedLedger

U4Kernel · operator

reference-profile · input revision 2 · CC0 1.0

U4Kernel(cause,nextStage) ==
 LET q==qT11 d==q.catalog[2].definition
     target==KernelTargetRA(d.syntax.source,IF cause \in {"PermissionWithdraw","PermissionRestore"} THEN 0 ELSE 2)
     basis==KernelBasisRA(q.catalog,q.basis,cause,target)
     before==q.current candidateLedger==q.ledger
     candidate==ConditionalSnapshotFromRegistrySA(q.catalog,basis,candidateLedger,PublicationTemplateRA(before,q.nextSnapshot))
     observer==PublicationObserverSnapshotRA(q.ledger,candidateLedger,before,candidate)
     ledger==PublicationAfterLedgerRA(q.ledger,candidateLedger,before,candidate)
     stack==PublicationAfterStackRA(q.stack,q.ledger,ledger)
     current==ConditionalSnapshotFromRegistrySA(q.catalog,basis,ledger,observer)
     receipt==[cause |-> cause,target |-> target,beforeBasis |-> MinimalCaptureSA(q.basis),afterBasis |-> MinimalCaptureSA(basis),
       beforeLedger |-> q.ledger,candidateLedger |-> candidateLedger,afterLedger |-> ledger,beforeStack |-> q.stack,afterStack |-> stack,
       beforeSnapshot |-> before,candidateSnapshot |-> candidate,observerSnapshot |-> observer,currentSnapshot |-> current]
 IN /\ U4Fresh(q,{q.nextSnapshot}) /\ U4Admit(q,q.ledger,q.current)
    /\ AdmitKernelPublicationRA(q.catalog,q.basis,basis,cause,target,q.nextSnapshot,q.ledger,candidateLedger,ledger,q.stack,stack,
        before,candidate,observer,current)
    /\ qT11'=[U4Record([q EXCEPT !.basis=basis,!.ledger=ledger,!.stack=stack],current) EXCEPT
         !.publications=Append(@,receipt),!.stage=nextStage]

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: ConditionalSnapshotFromRegistrySA, MinimalCaptureSA, AdmitKernelPublicationRA, KernelBasisRA, KernelTargetRA, PublicationAfterLedgerRA, PublicationAfterStackRA, PublicationObserverSnapshotRA, PublicationTemplateRA, U4Admit, U4Fresh, U4Record, qT11

U4Legality · operator

reference-profile · input revision 2 · CC0 1.0

U4Legality(w,option,transaction) == [ProtocolP!Legality9p(w,option) EXCEPT !.transactionId=transaction]

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: ProtocolP!Legality9p

U4Loss · operator

reference-profile · input revision 2 · CC0 1.0

U4Loss(q) == q.NeutralValue00013 # "no-loss" /\ q.round=1

Exact module download · Source bundle and reproduction instructions

U4NativeValid · operator

reference-profile · input revision 2 · CC0 1.0

U4NativeValid(q,use) ==
 LET n==q.native[use] p==q.procedures[q.uses[use].abilityInstance] IN
 /\ n.amount=1 /\ n.procedure=p.id /\ n.transaction=p.transaction /\ n.source=p.ability.source /\ n.turn=p.turnId
 /\ n.after=ItemInspectionWalletSpentT11(n.before,n.selected)
 /\ ItemInspectionCostOwnerT11!SpendResourceUnitsOK(n.before,"SideB",n.selected,1,{})
 /\ p.costPaid /\ p.ability.detached /\ p.phase="CostCheckpoint"

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: ItemInspectionCostOwnerT11!SpendResourceUnitsOK, ItemInspectionWalletSpentT11

U4Next · operator

reference-profile · input revision 2 · CC0 1.0

U4Next == U4Work /\ U4CaptureFrame(qT11,qT11') /\ UNCHANGED <<registryCaseSA,guideCaseT11>>

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: U4CaptureFrame, U4Work, registryCaseSA, guideCaseT11, qT11

U4OccurrenceBound · operator

reference-profile · input revision 2 · CC0 1.0

U4OccurrenceBound(q,event) ==
 IF event.useId \notin DOMAIN q.uses THEN FALSE
 ELSE IF event.id \notin DOMAIN q.occurrences THEN FALSE
 ELSE LET used==q.uses[event.useId] p==q.procedures[used.abilityInstance] IN
 /\ event=q.occurrences[event.id] /\ event.actualEvent=used /\ event.kind=used.tag
 /\ event.abilityInstance=used.abilityInstance /\ event.transaction=p.transaction /\ event.source=p.ability.source
 /\ event.turnId=p.turnId /\ event.snapshot=q.captures[event.snapshot.id].snapshot
 /\ q.native[event.useId].procedure=p.id /\ q.native[event.useId].transaction=p.transaction

Exact module download · Source bundle and reproduction instructions

U4OccurrenceId · operator

reference-profile · input revision 2 · CC0 1.0

U4OccurrenceId(round) == 10000+round

Exact module download · Source bundle and reproduction instructions

U4PaidAdmission · operator

reference-profile · input revision 2 · CC0 1.0

U4PaidAdmission(q,context) == /\ U4CurrentBound(q)
 /\ AdmitPaidContextSA(q.catalog,q.basis,q.ledger,q.uses,q.turnUses,q.useIndex,q.procedures,
 U4ContextTemplate,3,context,MinimalCaptureSA(q.basis))

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: AdmitPaidContextSA, MinimalCaptureSA, U4ContextTemplate, U4CurrentBound

U4PaidDefinition · operator

reference-profile · input revision 2 · CC0 1.0

U4PaidDefinition == [SPaidSA EXCEPT !.syntax.id="PendingRepeatable",!.activity.id="PendingRepeatable",
 !.syntax.source=U4PaidSource,!.activity.source=U4PaidSource,!.instructions= <<700>>]

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: U4PaidSource, SPaidSA

U4PaidId · operator

reference-profile · input revision 2 · CC0 1.0

U4PaidId(round) == 100+round

Exact module download · Source bundle and reproduction instructions

U4PaidReceipt · operator

reference-profile · input revision 2 · CC0 1.0

U4PaidReceipt(q,id) == [ProtocolP!PaidCP9p(q.paid,id) EXCEPT !.complete=id \in DOMAIN q.ledger.checkpoints,
 !.allNewerChainsComplete=ConditionalCheckpointDrained96(q.ledger,q.stack,id)]

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: ConditionalCheckpointDrained96, ProtocolP!PaidCP9p

U4PaidSource · operator

reference-profile · input revision 2 · CC0 1.0

U4PaidSource == RuleAbilitySource9("RegistryPendingPaid")

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: RuleAbilitySource9

U4PaidTransaction · operator

reference-profile · input revision 2 · CC0 1.0

U4PaidTransaction(round) == 900+round

Exact module download · Source bundle and reproduction instructions

U4PendingSafety · operator

reference-profile · input revision 2 · CC0 1.0

U4PendingSafety ==
 LET q==qT11 key==ConditionalKey96(q.catalog[2].definition) IN
 /\ q.ledger.activationSerial=q.ledger.activationEpoch[key]
 /\ q.ledger.activationEpoch[key]=(IF Len(q.publications)>0 THEN 1 ELSE 0)
 /\ \A id \in DOMAIN q.ledger.instances :
      /\ q.ledger.instances[id].definitionCopy=q.catalog[2].definition
      /\ q.ledger.instances[id].hadSnapshot=q.checkpointHistory[q.ledger.instances[id].checkpointId].previousSnapshot
 /\ (Len(q.publications)>0 => q.ledger.instances[201].status="Lost" /\ q.ledger.instances[201].activationEpoch=0)
 /\ (202 \in DOMAIN q.ledger.instances =>
       /\ q.ledger.instances[202].activationEpoch=q.ledger.activationEpoch[key]
       /\ q.ledger.instances[202].occurrence=U4OccurrenceId(2)
       /\ q.ledger.instances[202].member.windowId=U4ReactionWindow(2)
       /\ U4PaidId(1) \in DOMAIN q.returnedPaid /\ DOMAIN q.uses={1,2})
 /\ \A i \in 1..Len(q.stack) :
      /\ \A id \in q.stack[i].pending : q.ledger.instances[id].status="Pending"
      /\ \A id \in DOMAIN q.ledger.instances :
          (q.ledger.instances[id].member.windowId=q.stack[i].id /\ q.ledger.instances[id].status="Lost") =>
              id \notin q.stack[i].pending /\ id \in q.stack[i].lostPending
 /\ (q.stage="RejectLost" =>
       /\ ~ConditionalActive96(q.catalog[2].definition,q.current)
       /\ IF q.NeutralValue00013 \in {"permission-restore","permission-drain"}
             THEN 2 \in DOMAIN q.basis.registry /\ q.catalog[2].source.rule \notin q.basis.rulePermissions
             ELSE 2 \notin DOMAIN q.basis.registry /\ q.catalog[2].source.rule \in q.basis.rulePermissions)
 /\ (q.stage="RejectRestored" =>
       /\ q.basis.registry[2]=q.catalog[2] /\ ConditionalActive96(q.catalog[2].definition,q.current)
       /\ ~ConditionalInstanceCurrent96(q.ledger.instances[201],q.current.definitions,q.current))
 /\ \A tag \in DOMAIN q.rejections : q.rejections[tag].status="Lost" /\ q.rejections[tag].windowStage="Ready" /\ q.rejections[tag].window=41

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: ConditionalActive96, ConditionalInstanceCurrent96, ConditionalKey96, U4OccurrenceId, U4PaidId, U4ReactionWindow, qT11

U4PriorityReceipt · operator

reference-profile · input revision 2 · CC0 1.0

U4PriorityReceipt(q,ledger,cp) == [ProtocolP!PriorityCP9p(WindowTop9(q.stack),cp.id) EXCEPT
 !.complete=cp.id \in DOMAIN ledger.checkpoints,!.reactionsDrained=ConditionalCheckpointDrained96(ledger,q.stack,cp.id)]

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: ConditionalCheckpointDrained96, WindowTop9, ProtocolP!PriorityCP9p

U4Process · operator

reference-profile · input revision 2 · CC0 1.0

U4Process(q,ledger,cp,conditions,allocation,bindings) ==
 /\ U4HistoryValid(q) /\ U4Admit(q,q.ledger,cp.beginSnapshot) /\ U4Admit(q,q.ledger,cp.processingSnapshot)
 /\ Cardinality({cp.beginSnapshot.id,cp.processingSnapshot.id,q.nextSnapshot+2})=3
 /\ U4Fresh(q,{cp.beginSnapshot.id,cp.processingSnapshot.id,q.nextSnapshot+2})
 /\ \A id \in DOMAIN cp.occurrences : U4OccurrenceBound(q,cp.occurrences[id])
 /\ ProcessConditionalCheckpoint96(q.ledger,ledger,q.stack,q.stack,ConditionalDefinitionsSA(q.basis.registry),cp,
      conditions,allocation,bindings,EmptyT11,EmptyT11,q.usedWindows)

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: ProcessConditionalCheckpoint96, ConditionalDefinitionsSA, U4Admit, U4Fresh, U4HistoryValid, U4OccurrenceBound, EmptyT11

U4Profiles · operator

reference-profile · input revision 2 · CC0 1.0

U4Profiles == {"no-loss","permission-restore","entry-restore","permission-drain","entry-drain"}

Exact module download · Source bundle and reproduction instructions

U4ReactionWindow · operator

reference-profile · input revision 2 · CC0 1.0

U4ReactionWindow(round) == 40+round

Exact module download · Source bundle and reproduction instructions

U4Record · operator

reference-profile · input revision 2 · CC0 1.0

U4Record(q,snapshot) == [q EXCEPT !.current=snapshot,!.currentBasis=MinimalCaptureSA(q.basis),
 !.captures=PJoin(@,[id \in {snapshot.id} |-> U4Captured(q.basis,snapshot)]),!.nextSnapshot=@+1]

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: MinimalCaptureSA, PJoin, U4Captured

U4RecordCP · operator

reference-profile · input revision 2 · CC0 1.0

U4RecordCP(q,ledger,cp) ==
 LET a==U4Record(q,cp.beginSnapshot) b==U4Record(a,cp.processingSnapshot)
     c==U4WithLedger(b,ledger,"AfterRecognition")
 IN [c EXCEPT !.checkpointHistory=PJoin(@,[id \in {cp.id} |-> cp])]

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: PJoin, U4Record, U4WithLedger

U4Restores · operator

reference-profile · input revision 2 · CC0 1.0

U4Restores(q) == q.NeutralValue00013 \in {"permission-restore","entry-restore"}

Exact module download · Source bundle and reproduction instructions

U4ReturnReceipt · operator

reference-profile · input revision 2 · CC0 1.0

U4ReturnReceipt(q,p,conditional) ==
 LET w==WindowTop9(q.stack) drained==ConditionalCheckpointDrained96(q.ledger,q.stack,p.checkpoint)
     costDrained==ConditionalCheckpointDrained96(q.ledger,q.stack,q.costCheckpoint)
     native==U4NativeValid(q,q.round)
 IN [ProtocolP!Return9p(w,p.checkpoint) EXCEPT
 !.triggerPayment.allTriggerCostsPaid=IF conditional THEN TRUE ELSE native,
 !.triggerPayment.costCheckpointAndReactionsDrained=IF conditional THEN drained ELSE costDrained,
 !.allCostsPaid=IF conditional THEN TRUE ELSE native,!.optionComplete=p.ability.complete,
 !.childrenReturned=IF conditional THEN p.ability.complete ELSE costDrained,
 !.reactionsDrained=drained]

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: ConditionalCheckpointDrained96, WindowTop9, ProtocolP!Return9p, U4NativeValid

U4Rounds · operator

reference-profile · input revision 2 · CC0 1.0

U4Rounds(q) == IF q.NeutralValue00013 \in {"permission-drain","entry-drain"} THEN 1 ELSE 2

Exact module download · Source bundle and reproduction instructions

U4Safety · operator

reference-profile · input revision 2 · CC0 1.0

U4Safety ==
 LET q==qT11 IN
 /\ U4PaidDefinition.triggerCost= <<[kind |-> "ResourceUnits",amount |-> 1]>>
 /\ U4PaidDefinition.instructions= <<700>> /\ ~FlagPresent93(U4PaidDefinition.syntax.units,"ItemInspection")
 /\ ~FlagPresent93(U4PaidDefinition.syntax.units,"OncePerTurn")
 /\ q.NeutralValue00013 \in U4Profiles /\ q.catalog=U4Catalog /\ BasisValidSA(q.catalog,q.basis) /\ U4HistoryValid(q)
 /\ ConditionalBindingSA(q.catalog,q.basis,q.ledger,q.current,q.current,q.currentBasis)
 /\ q.basis.objects=EmptyT11 /\ q.basis.revision=Len(q.publications) /\ 3 \in DOMAIN q.basis.registry
 /\ DOMAIN q.native=DOMAIN q.uses /\ q.usedUses=DOMAIN q.uses
 /\ Cardinality(DOMAIN q.wallet.obj)=3-Cardinality(DOMAIN q.native)
 /\ \A use \in DOMAIN q.native : U4NativeValid(q,use)
 /\ \A id \in DOMAIN q.occurrences : U4OccurrenceBound(q,q.occurrences[id])
 /\ \A round \in DOMAIN q.readyAdmissions : q.readyAdmissions[round].stage="Ready" /\ q.readyAdmissions[round].window=U4ReactionWindow(round)
 /\ \A id \in DOMAIN q.returnedPaid : q.returnedPaid[id].phase="Returned" /\ q.returnedPaid[id].ability.complete
 /\ \A id \in DOMAIN q.returnedChildren : q.returnedChildren[id].phase="Returned" /\ q.ledger.instances[id].status="Complete"

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: FlagPresent93, BasisValidSA, ConditionalBindingSA, U4Catalog, U4HistoryValid, U4NativeValid, U4OccurrenceBound, U4PaidDefinition, U4Profiles, U4ReactionWindow, EmptyT11, qT11

U4SeedLedger · operator

reference-profile · input revision 2 · CC0 1.0

U4SeedLedger == NewConditionalLedger96([PInitialSnapshot EXCEPT !.definitions=ConditionalDefinitionsSA(U4Catalog),
 !.present=ConditionalPresentSA(U4Catalog),!.objects=EmptyT11,
 !.activationEpoch=[key \in DOMAIN ConditionalDefinitionsSA(U4Catalog) |-> 0]])

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: NewConditionalLedger96, ConditionalDefinitionsSA, ConditionalPresentSA, PInitialSnapshot, U4Catalog, EmptyT11

U4Snapshot · operator

reference-profile · input revision 2 · CC0 1.0

U4Snapshot(q,ledger,id,point,checkpoint) == ConditionalSnapshotFromRegistrySA(q.catalog,q.basis,ledger,U4Template(q,id,point,checkpoint))

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: ConditionalSnapshotFromRegistrySA, U4Template

U4Spec · operator

reference-profile · input revision 2 · CC0 1.0

U4Spec == U4Init /\ [][U4Next]_<<qT11,registryCaseSA,guideCaseT11>> /\ WF_<<qT11,registryCaseSA,guideCaseT11>>(U4Next)

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: U4Init, U4Next, registryCaseSA, guideCaseT11, qT11

U4Template · operator

reference-profile · input revision 2 · CC0 1.0

U4Template(q,id,point,checkpoint) == [q.current EXCEPT !.id=id,!.point=point,!.checkpointId=checkpoint]

Exact module download · Source bundle and reproduction instructions

U4WithLedger · operator

reference-profile · input revision 2 · CC0 1.0

U4WithLedger(q,ledger,point) ==
 U4Record([q EXCEPT !.ledger=ledger],U4Snapshot(q,ledger,q.nextSnapshot,point,ledger.lastCheckpoint))

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: U4Record, U4Snapshot

U4Work · operator

reference-profile · input revision 2 · CC0 1.0

U4Work ==
 LET q==qT11 IN
 CASE q.stage="Open" ->
   LET w==ProtocolP!Window9p(30,"Paid",EmptyT11,0) IN
   /\ OpenPriorityWindow9(q.stack,<<w>>,30,"Paid",ProtocolP!Site9p,EmptyT11,ProtocolP!Opening9p(30,"Paid",EmptyT11,0),q.usedWindows)
   /\ qT11'=[q EXCEPT !.stack= <<w>>,!.usedWindows=@ \cup {30},!.stage="Receive",!.resume="Reserve"]
 [] q.stage="Receive" ->
   LET w==WindowTop9(q.stack) cp==U4CP(q,ConditionalPriorityCaller96(w),EmptyT11)
       ledger==ProtocolP!CPAfter9p(q.ledger,cp,EmptyT11,EmptyT11)
       stack==ReplaceWindowTop9(q.stack,[w EXCEPT !.stage="Ready",!.checkpoint=cp.id]) IN
   /\ U4Process(q,ledger,cp,EmptyT11,EmptyT11,EmptyT11)
   /\ CheckpointPriorityWithConditionals96(ledger,q.stack,stack,U4PriorityReceipt(q,ledger,cp))
   /\ qT11'=[U4RecordCP(q,ledger,cp) EXCEPT !.stack=stack,!.stage=q.resume]
 [] q.stage="Reserve" ->
   LET w==WindowTop9(q.stack) d==q.catalog[3].definition context==U4Context(q)
       option==PriorityOption9(60+q.round,"RegularPaid","SideB",d.syntax.id,0,d.syntax.source,0,{})
       transaction==U4PaidTransaction(q.round) p==OpenPaidProcedure95(U4PaidId(q.round),d,option,w,transaction,"Rule")
       stack==ReplaceWindowTop9(q.stack,StartPriorityOptionFrame9(w,option,transaction)) IN
   /\ (q.round=1 \/ (U4PaidId(1) \in DOMAIN q.returnedPaid /\ q.returnedPaid[U4PaidId(1)].phase="Returned"))
   /\ transaction \notin q.usedTransactions /\ U4PaidAdmission(q,context)
   /\ ReservePaidAbility95(q.stack,stack,p,U4PaidId(q.round),d,context,option,U4Legality(w,option,transaction),q.usedInstances)
   /\ qT11'=[q EXCEPT !.paid=p,!.stack=stack,!.usedInstances=@ \cup {p.id},!.usedTransactions=@ \cup {transaction},!.stage="Pay"]
 [] q.stage="Pay" ->
   LET p==q.paid selected=={ItemInspectionCostOwnerT11!Least(DOMAIN q.wallet.obj)} wallet==ItemInspectionWalletSpentT11(q.wallet,selected)
       paid==[p EXCEPT !.ability.detached=TRUE,!.phase="CostCheckpoint",!.costPaid=TRUE]
       use==q.round event==[tag |-> "AbilityUsed",useId |-> use,abilityInstance |-> p.id,source |-> p.ability.source,player |-> "SideB"]
       uses==PJoin(q.uses,[id \in {use} |-> event])
       turns==PJoin(q.turnUses,[id \in {use} |-> [turnId |-> p.turnId,ability |-> p.definition.syntax.id,source |-> p.ability.source,useId |-> use]])
       procedures==PJoin(q.procedures,[id \in {p.id} |-> paid]) index==PJoin(q.useIndex,[id \in {use} |-> 3])
       snapshot==U4Snapshot(q,q.ledger,q.nextSnapshot,"CommittedPaidOccurrence",q.ledger.lastCheckpoint)
       occurrence==[id |-> U4OccurrenceId(q.round),kind |-> event.tag,object |-> 0,actor |-> event.player,side |-> event.player,
         snapshot |-> snapshot,scopeKind |-> "Global",scopeDefinition |-> ConditionalKey96(q.catalog[2].definition),
         traversal |-> NoTraversal6,structure |-> NoTimingRef9,actualEvent |-> event,useId |-> use,abilityInstance |-> p.id,
         transaction |-> p.transaction,source |-> p.ability.source,turnId |-> p.turnId]
       native==[before |-> q.wallet,after |-> wallet,selected |-> selected,amount |-> 1,procedure |-> p.id,
         transaction |-> p.transaction,source |-> p.ability.source,turn |-> p.turnId]
       payment==[tag |-> "PaidTriggerPayment",abilityInstance |-> p.id,transactionId |-> p.transaction,ability |-> p.definition.syntax.id,
         source |-> p.ability.source,triggerCost |-> p.definition.triggerCost,beforeObjects |-> q.basis.objects,afterObjects |-> q.basis.objects,
         announced |-> TRUE,allPaid |-> ItemInspectionCostOwnerT11!SpendResourceUnitsOK(q.wallet,"SideB",selected,1,{}) /\ wallet=ItemInspectionWalletSpentT11(q.wallet,selected),
         additionalCostsPaid |-> TRUE,restrictionsBefore |-> TRUE,restrictionsAfter |-> TRUE,simultaneousProcedureComplete |-> TRUE,
         sourceAfter |-> 0,sourceUninstalled |-> FALSE,sourceForfeited |-> FALSE,paidOperations |-> {},publicEvents |-> {}]
   IN /\ use \notin q.usedUses /\ occurrence.id \notin DOMAIN q.occurrences /\ U4Fresh(q,{snapshot.id})
      /\ PayPaidTrigger95(q.stack,p,paid,q.basis.objects,q.basis.objects,EmptyT11,EmptyT11,EmptyT11,DOMAIN q.basis.objects,
           payment,q.uses,uses,q.turnUses,turns,use,{event})
      /\ UseProvenanceValidSA(q.catalog,uses,turns,index,procedures)
      /\ qT11'=[U4Record(q,snapshot) EXCEPT !.paid=paid,!.wallet=wallet,!.uses=uses,!.turnUses=turns,!.useIndex=index,!.procedures=procedures,
           !.usedUses=@ \cup {use},!.native=PJoin(@,[id \in {use} |-> native]),
           !.occurrences=PJoin(@,[id \in {occurrence.id} |-> occurrence]),!.stage="CostCP"]
      /\ ItemInspectionCostOwnerT11!DoSpendResourceUnits(ItemInspectionCostCommandT11(selected,1))
 [] q.stage="CostCP" ->
   LET d==q.catalog[2].definition events==U4CostOccurrences(q)
       cp==U4CP(q,PaidCheckpointCaller96(q.paid),events)
       key==[definition |-> ConditionalKey96(d),occurrence |-> U4OccurrenceId(q.round)]
       allocation==[k \in {key} |-> U4ConditionalId(q.round)]
       bindings==[k \in {key} |-> [kind |-> "Reaction",checkpointId |-> cp.id,windowId |-> U4ReactionWindow(q.round),group |-> 4+q.round]]
       conditions==[k \in DOMAIN ConditionalDefinitionsSA(q.basis.registry) |-> [id \in DOMAIN events |->
         [tag |-> "ConditionalTriggerStipulations",ability |-> d.syntax.id,source |-> d.syntax.source,occurrence |-> id,snapshotId |-> events[id].snapshot.id,results |-> EmptyT11]]]
       ledger==ProtocolP!CPAfter9p(q.ledger,cp,allocation,bindings) IN
   /\ U4Process(q,ledger,cp,conditions,allocation,bindings)
   /\ qT11'=[U4RecordCP(q,ledger,cp) EXCEPT !.usedInstances=@ \cup {U4ConditionalId(q.round)},!.costCheckpoint=cp.id,!.stage="OpenReaction"]
 [] q.stage="OpenReaction" ->
   LET id==U4ReactionWindow(q.round) members==ConditionalWindowMembers96(q.ledger.instances,id)
       w==ProtocolP!Window9p(id,"Reaction",members,4+q.round) IN
   /\ OpenConditionalReaction96(q.stack,Append(q.stack,w),q.ledger,id,ProtocolP!Site9p,ProtocolP!Opening9p(id,"Reaction",members,4+q.round),q.usedWindows)
   /\ qT11'=[q EXCEPT !.stack=Append(@,w),!.usedWindows=@ \cup {id},!.stage="Receive",!.resume="ReadyCheck"]
 [] q.stage="ReadyCheck" ->
   /\ U4BeginAllowed(q,U4ConditionalId(q.round))
   /\ qT11'=[q EXCEPT !.readyAdmissions=PJoin(@,[id \in {q.round} |-> [snapshot |-> q.current.id,window |-> WindowTop9(q.stack).id,
          instance |-> U4ConditionalId(q.round),stage |-> WindowTop9(q.stack).stage]]),!.stage=IF U4Loss(q) THEN "Lose" ELSE "Select"]
 [] q.stage="Lose" -> U4Kernel(IF q.NeutralValue00013 \in {"permission-restore","permission-drain"} THEN "PermissionWithdraw" ELSE "EntryWithdraw","RejectLost")
 [] q.stage \in {"RejectLost","RejectRestored"} ->
   /\ WindowTop9(q.stack).id=U4ReactionWindow(1) /\ WindowTop9(q.stack).stage="Ready" /\ WindowTop9(q.stack).priority="SideB"
   /\ ~U4BeginAllowed(q,U4ConditionalId(1))
   /\ qT11'=[q EXCEPT !.rejections=PJoin(@,[key \in {q.stage} |-> [snapshot |-> q.current.id,window |-> WindowTop9(q.stack).id,
       windowStage |-> WindowTop9(q.stack).stage,status |-> q.ledger.instances[201].status,epoch |-> q.ledger.activationEpoch[ConditionalKey96(q.catalog[2].definition)]]]),
       !.stage=IF q.stage="RejectLost" /\ U4Restores(q) THEN "Restore" ELSE "Pass"]
 [] q.stage="Restore" -> U4Kernel(IF q.NeutralValue00013="permission-restore" THEN "PermissionRestore" ELSE "EntryRestore","RejectRestored")
 [] q.stage="Select" ->
   LET id==U4ConditionalId(q.round) c==U4Choice(q,id) IN
   /\ U4Fresh(q,{q.nextSnapshot}) /\ U4BeginAllowed(q,id) /\ U4ChildTransaction(q.round) \notin q.usedTransactions
   /\ qT11'=[U4WithLedger(q,c.ledger,"SelectedConditional") EXCEPT !.stack=c.stack,!.child=c.afterP,!.childPlan=c.afterPlan,
       !.usedTransactions=@ \cup {U4ChildTransaction(q.round)},!.stage="ChildBegin"]
 [] q.stage="ChildBegin" ->
   LET id==q.child.id p==[q.child EXCEPT !.phase="Resolve",!.ability.phase="Resolving"] plan==[q.childPlan EXCEPT !.phase="Resolving"]
       expected==[tag |-> "ConditionalExpectedEffects",point |-> "ExpectedEffectsBeforeInterrupt",instruction |-> InstructionWindowRef93(q.childPlan),effects |-> {1}]
       ledger==[q.ledger EXCEPT !.instances[id].status="Resolving",!.instances[id].expected=[i \in {1} |-> [instruction |-> InstructionWindowRef93(q.childPlan),effects |-> {1}]]] IN
   /\ U4Fresh(q,{q.nextSnapshot}) /\ U4Admit(q,q.ledger,q.current)
   /\ ResolveConditionalWithoutInterrupt96(q.ledger,ledger,q.stack,q.child,p,q.childPlan,plan,ProtocolP!NoModifiers9p(q.childPlan),ProtocolP!Clearance9p(q.childPlan),expected)
   /\ qT11'=[U4WithLedger(q,ledger,"ResolvingConditional") EXCEPT !.child=p,!.childPlan=plan,!.stage="ChildWork"]
 [] q.stage="ChildWork" ->
   LET id==q.child.id ability==ProtocolP!FinishedAbility9p(q.child.ability,q.childPlan)
       p==[q.child EXCEPT !.ability=ability,!.phase="InstructionCheckpoint",!.checkpoint=0] plan==ProtocolP!FinishedPlan9p(q.childPlan)
       candidate==[q.ledger EXCEPT !.instances[id].status="Complete"]
       snapshot==U4Snapshot(q,candidate,q.nextSnapshot,"ConditionalInstructionAfter",q.ledger.lastCheckpoint) IN
   /\ U4Fresh(q,{q.nextSnapshot}) /\ U4Admit(q,q.ledger,q.current) /\ U4Admit(q,candidate,snapshot)
   /\ RecordConditionalExecutionUse96(q.ledger,q.ledger,q.child,q.childPlan,
       [tag |-> "ConditionalEffectExecution",instruction |-> InstructionWindowRef93(q.childPlan),abilityInstance |-> id,source |-> q.child.ability.source,partIds |-> {1}],
       q.uses,q.uses,q.turnUses,q.turnUses,100+q.round,{})
   /\ CarryConditionalInstruction96(q.ledger,candidate,candidate,q.stack,q.stack,q.child,p,q.childPlan,plan,ProtocolP!Step9p(q.childPlan),q.current,snapshot)
   /\ qT11'=[U4Record([q EXCEPT !.ledger=candidate],snapshot) EXCEPT !.child=p,!.childPlan=plan,!.work=Append(@,[round |-> q.round,kind |-> "Conditional"]),!.stage="ChildCP"]
 [] q.stage="ChildCP" ->
   LET cp==U4CP(q,ConditionalInstructionCaller96(q.child),EmptyT11) ledger==ProtocolP!CPAfter9p(q.ledger,cp,EmptyT11,EmptyT11)
       p==[q.child EXCEPT !.phase="Complete",!.checkpoint=cp.id]
       receipt==[tag |-> "ConditionalInstructionCheckpoint",id |-> cp.id,abilityInstance |-> q.child.id,transactionId |-> q.child.transaction,
          source |-> q.child.ability.source,instruction |-> q.childPlan.id,index |-> 1,
          complete |-> cp.id \in DOMAIN ledger.checkpoints,allNewerChainsComplete |-> ConditionalCheckpointDrained96(ledger,q.stack,cp.id)] IN
   /\ U4Process(q,ledger,cp,EmptyT11,EmptyT11,EmptyT11)
   /\ ConditionalInstructionCheckpoint96(ledger,q.stack,q.child,p,receipt)
   /\ qT11'=[U4RecordCP(q,ledger,cp) EXCEPT !.child=p,!.stage="ChildReturn"]
 [] q.stage="ChildReturn" ->
   LET p==[q.child EXCEPT !.phase="Returned",!.ability.returned=TRUE]
       stack==ReplaceWindowTop9(q.stack,CompletePriorityOptionFrame9(WindowTop9(q.stack))) IN
   /\ FinishConditionalProcedure96(q.stack,stack,q.child,p,U4ReturnReceipt(q,q.child,TRUE))
   /\ qT11'=[q EXCEPT !.child=p,!.stack=stack,!.returnedChildren=PJoin(@,[id \in {p.id} |-> p]),!.stage="Receive",!.resume="Pass"]
 [] q.stage="Pass" ->
   LET w==WindowTop9(q.stack) candidateStack==ReplaceWindowTop9(q.stack,PassPriorityFrame9(w))
       candidate==ConditionalPendingAfterWindows96(q.ledger,candidateStack)
       snapshot==U4Snapshot(q,candidate,q.nextSnapshot,"PriorityPassAfter",q.ledger.lastCheckpoint) IN
   /\ U4Fresh(q,{q.nextSnapshot}) /\ U4Admit(q,q.ledger,q.current) /\ U4Admit(q,candidate,snapshot)
   /\ PassConditionalPriority96(q.ledger,candidate,candidate,q.stack,candidateStack,w.priority,EmptyT11,q.current,snapshot)
   /\ qT11'=[U4Record([q EXCEPT !.ledger=candidate],snapshot) EXCEPT !.stack=candidateStack,
       !.stage=IF WindowTop9(candidateStack).open THEN "Receive" ELSE IF Len(candidateStack)=2 THEN "PopReaction" ELSE "PopPaid",!.resume="Pass"]
 [] q.stage="PopReaction" ->
   LET w==WindowTop9(q.stack) stack==SubSeq(q.stack,1,Len(q.stack)-1) IN
   /\ PopClosedPriorityWindow9(q.stack,stack)
   /\ qT11'=[q EXCEPT !.stack=stack,!.closedWindows=PJoin(@,[id \in {w.id} |-> w]),!.stage="CostResume"]
 [] q.stage="CostResume" ->
   LET p==[q.paid EXCEPT !.phase="Targets",!.checkpoint=q.costCheckpoint] IN
   /\ PaidCheckpointWithConditionals96(q.ledger,q.stack,q.paid,p,q.basis.objects,EmptyT11,U4PaidReceipt(q,q.costCheckpoint))
   /\ qT11'=[q EXCEPT !.paid=p,!.wallet.checkpointDue=FALSE,!.stage="PaidEnter"]
 [] q.stage="PaidEnter" ->
   LET plan==OpenInstruction93(700,"Ability",q.paid.id,q.paid.ability.source,"Rule",1,"NoValue",<<"RepeatablePaidBody">>,FALSE)
       p==[q.paid EXCEPT !.phase="Imminent",!.checkpoint=0,!.ability.phase="Imminent",!.ability.firstImminent=TRUE]
       announced==[plan EXCEPT !.phase="Imminent",!.announced=TRUE] IN
   /\ EnterPaidInstruction95(q.stack,q.paid,p,plan,announced,ProtocolP!Targets9p(plan),ProtocolP!Entry9p(plan,q.paid.checkpoint))
   /\ qT11'=[q EXCEPT !.paid=p,!.plan=announced,!.stage="PaidBegin"]
 [] q.stage="PaidBegin" ->
   LET p==[q.paid EXCEPT !.phase="Resolve",!.ability.phase="Resolving"] plan==[q.plan EXCEPT !.phase="Resolving"] IN
   /\ ResolvePaidWithoutInterrupt95(q.stack,q.paid,p,q.plan,plan,ProtocolP!NoModifiers9p(q.plan),ProtocolP!Clearance9p(q.plan))
   /\ qT11'=[q EXCEPT !.paid=p,!.plan=plan,!.stage="PaidWork"]
 [] q.stage="PaidWork" ->
   LET plan==ProtocolP!FinishedPlan9p(q.plan) ability==ProtocolP!FinishedAbility9p(q.paid.ability,q.plan)
       p==[q.paid EXCEPT !.ability=ability,!.checkpoint=0,!.phase="InstructionCheckpoint"] IN
   /\ CarryPaidInstruction95(q.stack,q.paid,p,q.plan,plan,ProtocolP!Step9p(q.plan))
   /\ qT11'=[q EXCEPT !.paid=p,!.plan=plan,!.work=Append(@,[round |-> q.round,kind |-> "Paid"]),!.stage="PaidCP"]
 [] q.stage="PaidCP" ->
   LET cp==U4CP(q,PaidCheckpointCaller96(q.paid),EmptyT11) ledger==ProtocolP!CPAfter9p(q.ledger,cp,EmptyT11,EmptyT11)
       p==[q.paid EXCEPT !.phase="Complete",!.checkpoint=cp.id] after==U4RecordCP(q,ledger,cp) IN
   /\ U4Process(q,ledger,cp,EmptyT11,EmptyT11,EmptyT11)
   /\ PaidCheckpointWithConditionals96(ledger,q.stack,q.paid,p,q.basis.objects,EmptyT11,U4PaidReceipt(after,cp.id))
   /\ qT11'=[after EXCEPT !.paid=p,!.stage="PaidReturn"]
 [] q.stage="PaidReturn" ->
   LET p==[q.paid EXCEPT !.phase="Returned",!.ability.returned=TRUE]
       stack==ReplaceWindowTop9(q.stack,CompletePriorityOptionFrame9(WindowTop9(q.stack)))
       again==q.round<U4Rounds(q) IN
   /\ FinishPaidProcedure95(q.stack,stack,q.paid,p,U4ReturnReceipt(q,q.paid,FALSE))
   /\ qT11'=[q EXCEPT !.paid=p,!.stack=stack,!.returnedPaid=PJoin(@,[id \in {p.id} |-> p]),!.round=IF again THEN @+1 ELSE @,
       !.child=EmptyT11,!.childPlan=EmptyT11,!.stage="Receive",!.resume=IF again THEN "Reserve" ELSE "Pass"]
 [] q.stage="PopPaid" ->
   /\ PopClosedPriorityWindow9(q.stack,<<>>)
   /\ qT11'=[q EXCEPT !.stack= <<>>,!.stage="Done"]
 [] OTHER -> FALSE

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: CarryConditionalInstruction96, CarryPaidInstruction95, CheckpointPriorityWithConditionals96, CompletePriorityOptionFrame9, ConditionalCheckpointDrained96, ConditionalInstructionCaller96, ConditionalInstructionCheckpoint96, ConditionalKey96, ConditionalPendingAfterWindows96, ConditionalPriorityCaller96, ConditionalWindowMembers96, EnterPaidInstruction95, FinishConditionalProcedure96, FinishPaidProcedure95, InstructionWindowRef93, NoTimingRef9, OpenConditionalReaction96, OpenInstruction93, OpenPaidProcedure95, OpenPriorityWindow9, PaidCheckpointCaller96, PaidCheckpointWithConditionals96, PassConditionalPriority96, PassPriorityFrame9, PayPaidTrigger95, PopClosedPriorityWindow9, PriorityOption9, RecordConditionalExecutionUse96, ReplaceWindowTop9, ReservePaidAbility95, ResolveConditionalWithoutInterrupt96, ResolvePaidWithoutInterrupt95, StartPriorityOptionFrame9, WindowTop9, ConditionalDefinitionsSA, UseProvenanceValidSA, PJoin, ProtocolP!CPAfter9p, ProtocolP!Clearance9p, ProtocolP!Entry9p, ProtocolP!FinishedAbility9p, ProtocolP!FinishedPlan9p, ProtocolP!NoModifiers9p, ProtocolP!Opening9p, ProtocolP!Site9p, ProtocolP!Step9p, ProtocolP!Targets9p, ProtocolP!Window9p, ItemInspectionCostCommandT11, ItemInspectionCostOwnerT11!DoSpendResourceUnits, ItemInspectionCostOwnerT11!Least, ItemInspectionCostOwnerT11!SpendResourceUnitsOK, ItemInspectionWalletSpentT11, U4Admit, U4BeginAllowed, U4CP, U4ChildTransaction, U4Choice, U4ConditionalId, U4Context, U4CostOccurrences, U4Fresh, U4Kernel, U4Legality, U4Loss, U4OccurrenceId, U4PaidAdmission, U4PaidId, U4PaidReceipt, U4PaidTransaction, U4PriorityReceipt, U4Process, U4ReactionWindow, U4Record, U4RecordCP, U4Restores, U4ReturnReceipt, U4Rounds, U4Snapshot, U4WithLedger, EmptyT11, qT11, NoTraversal6