----------------------- MODULE PendingChecksMC -----------------------
EXTENDS RegistryChecksMC, ActivityPublication
                                                                             
                                                                                 
CONSTANT PendingProfiles
U4Profiles == {"no-loss","permission-restore","entry-restore","permission-drain","entry-drain"}
U4PaidSource == RuleAbilitySource9("RegistryPendingPaid")
U4PaidDefinition == [SPaidSA EXCEPT !.syntax.id="PendingRepeatable",!.activity.id="PendingRepeatable",
 !.syntax.source=U4PaidSource,!.activity.source=U4PaidSource,!.instructions= <<700>>]
U4ConditionalDefinition == SConditionalSA
U4Catalog == [key \in {2,3} |-> IF key=2 THEN SRowSA("Conditional",U4ConditionalDefinition) ELSE SRowSA("Paid",U4PaidDefinition)]
U4InitialBasis == BasisSA(0,U4Catalog,EmptyT11,{U4PaidSource.rule,U4ConditionalDefinition.syntax.source.rule})
U4SeedLedger == NewConditionalLedger96([PInitialSnapshot EXCEPT !.definitions=ConditionalDefinitionsSA(U4Catalog),
 !.present=ConditionalPresentSA(U4Catalog),!.objects=EmptyT11,
 !.activationEpoch=[key \in DOMAIN ConditionalDefinitionsSA(U4Catalog) |-> 0]])
U4InitialSnapshot == ConditionalSnapshotFromRegistrySA(U4Catalog,U4InitialBasis,U4SeedLedger,PInitialSnapshot)
U4InitialLedger == NewConditionalLedger96(U4InitialSnapshot)
U4Captured(basis,snapshot) == [basis |-> MinimalCaptureSA(basis),snapshot |-> snapshot]
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 |-> <<>>]
U4Init == registryCaseSA=0 /\ guideCaseT11=0 /\ \E NeutralValue00013 \in PendingProfiles : qT11=U4Initial(NeutralValue00013)
U4Loss(q) == q.NeutralValue00013 # "no-loss" /\ q.round=1
U4Restores(q) == q.NeutralValue00013 \in {"permission-restore","entry-restore"}
U4Rounds(q) == IF q.NeutralValue00013 \in {"permission-drain","entry-drain"} THEN 1 ELSE 2
U4PaidId(round) == 100+round
U4ConditionalId(round) == 200+round
U4ReactionWindow(round) == 40+round
U4OccurrenceId(round) == 10000+round
U4PaidTransaction(round) == 900+round
U4ChildTransaction(round) == 1900+round
U4Template(q,id,point,checkpoint) == [q.current EXCEPT !.id=id,!.point=point,!.checkpointId=checkpoint]
U4Snapshot(q,ledger,id,point,checkpoint) == ConditionalSnapshotFromRegistrySA(q.catalog,q.basis,ledger,U4Template(q,id,point,checkpoint))
U4Fresh(q,ids) == ids \subseteq Nat \ {0} /\ ids \cap DOMAIN q.captures={}
U4Record(q,snapshot) == [q EXCEPT !.current=snapshot,!.currentBasis=MinimalCaptureSA(q.basis),
 !.captures=PJoin(@,[id \in {snapshot.id} |-> U4Captured(q.basis,snapshot)]),!.nextSnapshot=@+1]
U4WithLedger(q,ledger,point) ==
 U4Record([q EXCEPT !.ledger=ledger],U4Snapshot(q,ledger,q.nextSnapshot,point,ledger.lastCheckpoint))
U4HistoryValid(q) == UseProvenanceValidSA(q.catalog,q.uses,q.turnUses,q.useIndex,q.procedures)
U4CurrentBound(q) == ConditionalBindingSA(q.catalog,q.basis,q.ledger,q.current,q.current,q.currentBasis)
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))
U4ContextTemplate == [STemplateSA EXCEPT !.ownRestrictions.ability=U4PaidDefinition.syntax.id,!.ownRestrictions.source=U4PaidSource,
 !.otherRestrictions.ability=U4PaidDefinition.syntax.id,!.otherRestrictions.source=U4PaidSource]
U4Context(q) == PaidContextFromRegistrySA(q.catalog,q.basis,q.ledger,q.useIndex,q.turnUses,U4ContextTemplate,3)
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))
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]
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
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)
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])]
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)]
U4PaidReceipt(q,id) == [ProtocolP!PaidCP9p(q.paid,id) EXCEPT !.complete=id \in DOMAIN q.ledger.checkpoints,
 !.allNewerChainsComplete=ConditionalCheckpointDrained96(q.ledger,q.stack,id)]
U4Legality(w,option,transaction) == [ProtocolP!Legality9p(w,option) EXCEPT !.transactionId=transaction]
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)))]
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])
U4CostOccurrences(q) == [id \in {U4OccurrenceId(q.round)} |-> q.occurrences[id]]
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"
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]
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]
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
                                                                          
                                                                       
U4CaptureFrame(before,after) ==
 /\ DOMAIN before.captures \subseteq DOMAIN after.captures
 /\ \A id \in DOMAIN before.captures : after.captures[id]=before.captures[id]
U4Next == U4Work /\ U4CaptureFrame(qT11,qT11') /\ UNCHANGED <<registryCaseSA,guideCaseT11>>
U4Spec == U4Init /\ [][U4Next]_<<qT11,registryCaseSA,guideCaseT11>> /\ WF_<<qT11,registryCaseSA,guideCaseT11>>(U4Next)
U4EventuallyDone == <> (qT11.stage="Done")
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"
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
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
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})
=============================================================================