---------------------- MODULE RegistryAvailabilityMC ----------------------
EXTENDS CommittedCompositionMC, AbilityRegistry, ActivityPublication
                                                                             
                                                                            
VJoin(base,extra) == PJoin(base,extra)
VChildDefinition == PChildDefinition
VCatalog(amount) ==
 LET d==ItemInspectionPaidDefinitionT11([NeutralValue00013 |-> IF amount=0 THEN "FacilityObserve0" ELSE "FacilityObserve1"])
 IN [key \in {1,2} |-> IF key=1 THEN [kind |-> "Paid",nativeId |-> d.syntax.id,source |-> d.syntax.source,definition |-> d]
     ELSE [kind |-> "Conditional",nativeId |-> VChildDefinition.syntax.id,source |-> VChildDefinition.syntax.source,definition |-> VChildDefinition]]
VPermissions == {"AuditPaidObserve","ProtocolReactionControl"}
VBasisObjects(q,objects) == BasisSA(q.abilityRevision,q.abilityRegistry,objects,q.rulePermissions)
VBasis(q) == VBasisObjects(q,q.objects)
VDefinitions(q) == ConditionalDefinitionsSA(q.abilityRegistry)
CONSTANT AvailabilityProfiles
VProfiles == {"baseline","paid-permission","paid-entry","initial-paid-permission","initial-paid-entry","initial-conditional-permission","initial-conditional-entry"}
VInitialPaid(NeutralValue00013) == NeutralValue00013 \in {"initial-paid-permission","initial-paid-entry"}
VInitialConditional(NeutralValue00013) == NeutralValue00013 \in {"initial-conditional-permission","initial-conditional-entry"}
VUnavailable(NeutralValue00013) == VInitialPaid(NeutralValue00013) \/ VInitialConditional(NeutralValue00013)
VPaidLoss(NeutralValue00013) == NeutralValue00013 \in {"paid-permission","paid-entry"}
VWithout(map,key) == [k \in DOMAIN map \ {key} |-> map[k]]
VPreparedBasis(amount,NeutralValue00013) ==
 LET catalog==VCatalog(amount)
     entry==IF VInitialPaid(NeutralValue00013) THEN 1 ELSE 2
     registry==IF NeutralValue00013 \in {"initial-paid-entry","initial-conditional-entry"} THEN VWithout(catalog,entry) ELSE catalog
     permissions==IF NeutralValue00013 \in {"initial-paid-permission","initial-conditional-permission"}
                  THEN VPermissions \ {catalog[entry].source.rule} ELSE VPermissions
 IN BasisSA(0,registry,PObjects,permissions)
                                                                              
                                                                              
VCapture(basis,views) == [basis |-> MinimalCaptureSA(basis),views |-> views]
VInitial(amount,moves,NeutralValue00013) ==
 LET catalog==VCatalog(amount) basis==VPreparedBasis(amount,NeutralValue00013)
     seed==NewConditionalLedger96(PInitialSnapshot)
     snapshot==ConditionalSnapshotFromRegistrySA(catalog,basis,seed,PInitialSnapshot)
 IN VJoin(PInitial(amount,moves),[catalog |-> catalog,abilityRegistry |-> basis.registry,abilityRevision |-> 0,
   rulePermissions |-> basis.rulePermissions,useIndex |-> EmptyT11,procedures |-> EmptyT11,basisHistory |-> EmptyT11,
   ledger |-> NewConditionalLedger96(snapshot),availabilityProfile |-> NeutralValue00013,nextWorld |-> 2001,
   worldHistory |-> [id \in {snapshot.id} |-> VCapture(basis,<<snapshot>>)],commitSnapshot |-> EmptyT11,
   kernelDone |-> FALSE,kernelReceipt |-> EmptyT11,declined |-> FALSE,declineReceipt |-> EmptyT11,
   noChild |-> FALSE,noChildReceipt |-> EmptyT11,noReactionCostReturned |-> FALSE,noReactionCostReceipt |-> EmptyT11])
VInit == guideCaseT11=0 /\ \E amount \in PaidAmounts,moves \in PaidMoves,NeutralValue00013 \in AvailabilityProfiles :
 /\ NeutralValue00013 \in VProfiles /\ (VUnavailable(NeutralValue00013) => ~moves) /\ qT11=VInitial(amount,moves,NeutralValue00013)
VFreshWorld(q,ids) == ids \subseteq Nat \ {0} /\ ids \cap DOMAIN q.worldHistory={}
VKeepWorld(q,basis,views) ==
 [q EXCEPT !.worldHistory=VJoin(@,[id \in {views[1].id} |-> VCapture(basis,views)]),!.nextWorld=@+1]
VSetBasis(q,basis) == [q EXCEPT !.abilityRegistry=basis.registry,!.abilityRevision=basis.revision,!.rulePermissions=basis.rulePermissions]
VInstanceCapture(i) == [definition |-> i.definition,definitionCopy |-> i.definitionCopy,member |-> i.member,
 primaryKind |-> i.primaryKind,activationEpoch |-> i.activationEpoch,checkpointId |-> i.checkpointId,
 occurrence |-> i.occurrence,hadSnapshot |-> i.hadSnapshot]
VHistoryFrame(before,after) ==
 /\ DOMAIN before.worldHistory \subseteq DOMAIN after.worldHistory
 /\ \A id \in DOMAIN before.worldHistory : after.worldHistory[id]=before.worldHistory[id]
 /\ DOMAIN before.basisHistory \subseteq DOMAIN after.basisHistory
 /\ \A id \in DOMAIN before.basisHistory : after.basisHistory[id]=before.basisHistory[id]
 /\ DOMAIN before.procedures \subseteq DOMAIN after.procedures
 /\ \A id \in DOMAIN before.procedures : after.procedures[id]=before.procedures[id]
 /\ \A id \in DOMAIN before.uses : after.uses[id]=before.uses[id] /\ after.turnUses[id]=before.turnUses[id] /\ after.useIndex[id]=before.useIndex[id]
 /\ (before.native # EmptyT11 => after.native=before.native /\ after.commitSnapshot=before.commitSnapshot)
 /\ DOMAIN before.ledger.instances \subseteq DOMAIN after.ledger.instances
 /\ \A id \in DOMAIN before.ledger.instances : VInstanceCapture(after.ledger.instances[id])=VInstanceCapture(before.ledger.instances[id])
 /\ \A id \in DOMAIN before.frames : before.frames[id].recognition.id#0 => after.frames[id].recognition=before.frames[id].recognition
VObjects == PObjects
VPrinted == PPrinted
VOwners == POwners
VItemInspectionView(q) == [itemInspection |-> IAT11(q),objects |-> q.objects,NeutralValue00013 |-> IF q.amount=0 THEN "FacilityObserve0" ELSE "FacilityObserve1",turnUses |-> q.turnUses]
VPaidDefinition(q) == q.catalog[1].definition
VContext(q,d) == PaidContextFromRegistrySA(q.catalog,VBasis(q),q.ledger,q.useIndex,q.turnUses,PContext(q,d),1)
VHistoryValid(q) == UseProvenanceValidSA(q.catalog,q.uses,q.turnUses,q.useIndex,q.procedures)
VAdmitPaid(q,d,view) ==
 IF ~BasisValidSA(q.catalog,VBasis(q)) THEN FALSE
 ELSE IF 1 \notin DOMAIN q.abilityRegistry THEN FALSE
 ELSE IF q.catalog[1].kind # "Paid" THEN FALSE
 ELSE IF d.syntax.kind # "Paid" THEN FALSE
 ELSE d=q.catalog[1].definition /\ AdmitPaidContextSA(q.catalog,VBasis(q),q.ledger,q.uses,q.turnUses,q.useIndex,q.procedures,
 PContext(q,d),1,view,MinimalCaptureSA(VBasis(q)))
VLegality(w,option,transaction) == [LegalityT11(w,option) EXCEPT !.transactionId=transaction]
VMid(q) == ItemInspectionTemporalMidT11(VItemInspectionView(q))
VPaidOption(q,w,d) == ItemInspectionPaidOptionT11(VItemInspectionView(q),w,d)
VUse(p) == ItemInspectionPaidUseT11(p)
VTurnUses(p) == ItemInspectionPaidTurnUsesT11(p)
                                                                            
                                                                                 
VChildTurnUses(q) == FamilyTurnUsesSA(q.catalog,q.useIndex,q.turnUses,"Conditional",VChildDefinition.syntax.source)
VSnapshotTemplate(q,id,point,checkpoint) == [q.ledger.lastSnapshot EXCEPT !.id=id,!.point=point,!.checkpointId=checkpoint]
VCurrentSnapshot(q,objects,ledger,id,point,checkpoint) ==
 ConditionalSnapshotFromRegistrySA(q.catalog,VBasisObjects(q,objects),ledger,VSnapshotTemplate(q,id,point,checkpoint))
VAdmitSnapshot(q,objects,ledger,view) ==
 AdmitConditionalSnapshotSA(q.catalog,VBasisObjects(q,objects),ledger,q.uses,q.turnUses,q.useIndex,q.procedures,
  VSnapshotTemplate(q,view.id,view.point,view.checkpointId),view,MinimalCaptureSA(VBasisObjects(q,objects)))
VWorld(q,f) == [id |-> f.snapshotId,objects |-> q.objects,points |-> ZeroCountsT11,
 present |-> ConditionalPresentSA(q.abilityRegistry),activity |-> CommonActivitySA(VBasis(q),q.ledger)]
VWorldBound(q,f,world) ==
 /\ BasisValidSA(q.catalog,VBasis(q)) /\ LedgerDomainSA(q.ledger) /\ VHistoryValid(q)
 /\ world=[id |-> f.snapshotId,objects |-> q.objects,points |-> ZeroCountsT11,
   present |-> ConditionalPresentSA(q.abilityRegistry),activity |-> CommonActivitySA(VBasis(q),q.ledger)]
VLex(d) == [tag |-> "NormalizedAbilityLexemes",definition |-> d,source |-> d.syntax.source,card |-> "NoValue",
 sourceSHA |-> "0186148ecd6da8170b6555aa90d3f0115a8d5150d807078b75ac2339a2a1421e",mentions |-> EmptyT11,
 origin |-> [tag |-> "AbilityTextOrigin",recipientSource |-> d.syntax.source,provider |-> d.activity.provider,rule |-> d.syntax.source.rule]]
VLexemes(q) == [k \in DOMAIN VDefinitions(q) |-> VLex(VDefinitions(q)[k])]
VInside(q) == {TimingRef9("Turn",q.flow.turn.id),TimingRef9("SchemaAtom138",q.control.traversal.id),TimingRef9("Inspection",IBT11(q).id)} \cup
 (IF StillItemInspectioning7(IAT11(q),q.objects) THEN {TimingRef9("ItemInspection",IAT11(q).id)} ELSE {})
VFrame(q) == q.frames[q.currentCP]
VSetFrame(q,f) == [q EXCEPT !.frames[f.id]=f]
VCPOccurrences(q) ==
 LET u==q.useEvents[1] IN
 [id \in {u.useId} |-> [id |-> id,kind |-> u.tag,object |-> u.source.object,actor |-> u.player,side |-> u.player,
  snapshot |-> q.commitSnapshot,scopeKind |-> "Global",scopeDefinition |-> ConditionalKey96(VChildDefinition),
  traversal |-> q.control.traversal,structure |-> TimingRef9("ItemInspection",IAT11(q).id),actualEvent |-> u,
  transaction |-> q.native.transaction,abilityInstance |-> u.abilityInstance,source |-> u.source,turnId |-> q.paid.turnId]]
VCPData(q,f) ==
 LET b==VCurrentSnapshot(q,q.objects,q.ledger,f.snapshotId,"CheckpointBeginning",f.id)
 IN [tag |-> "ConditionalCheckpoint",point |-> "ProcedureCodee605a78f5d5e",id |-> f.id,previousCheckpoint |-> q.ledger.lastCheckpoint,
  serial |-> q.ledger.serial+1,previousSnapshot |-> q.ledger.lastSnapshot,beginSnapshot |-> b,
  processingSnapshot |-> [b EXCEPT !.point="ProcedureCodee605a78f5d5e"],stepSerial |-> q.ledger.stepSerial,
  occurrences |-> IF q.cpRole="Cost" THEN VCPOccurrences(q) ELSE EmptyT11,caller |-> f.caller]
VOpenCP(kind,caller,resume,role) ==
 LET q==qT11 id==q.ledger.lastCheckpoint+1 snapshot==q.nextWorld
     event==VJoin([id |-> id,caller |-> caller,complete |-> TRUE],
       CASE kind="SchemaAtom126" -> [tag |-> "PriorityAboutToBeReceived",player |-> WindowTop9(q.stack).priority]
        [] kind="Cost" -> [tag |-> "CostPaid",transactionId |-> q.paid.transaction,nativePayment |-> q.native,useEvent |-> q.useEvents[1]]
        [] OTHER -> [tag |-> "InstructionFinished",origin |-> "Ability",instruction |-> IF role="ChildFinal" THEN "AbilityInstruction710" ELSE "AbilityInstruction700",
          instructionRef |-> InstructionWindowRef93(IF role="ChildFinal" THEN q.childPlan ELSE q.plan),
          finishedPlan |-> IF role="ChildFinal" THEN q.childPlan ELSE q.plan])
     site==[kind |-> kind,caller |-> caller,eventId |-> id,snapshotId |-> snapshot,inside |-> VInside(q)]
     frame==NewCheckpoint103(id,caller,snapshot,VInside(q))
     frames==VJoin(q.frames,[k \in {id} |-> frame])
     cpView==VCPData(q,frame)
 IN /\ VFreshWorld(q,{snapshot})
    /\ BeginCheckpointSite103(q.sites,q.sites \cup {CheckpointSiteKey103(site)},q.frames,frames,frame,id,site,event,VInside(q))
    /\ (kind="Cost" => q.paid.costPaid /\ q.wallet.checkpointDue /\ Len(q.useEvents)=1)
    /\ (kind="Instruction" => IF role="ChildFinal" THEN q.childPlan.phase="Complete" ELSE q.plan.phase="Complete")
    /\ qT11'=[VKeepWorld(q,VBasis(q),<<cpView.beginSnapshot,cpView.processingSnapshot>>) EXCEPT !.frames=frames,!.sites=@ \cup {CheckpointSiteKey103(site)},!.currentCP=id,
         !.checkpointEvents=VJoin(@,[k \in {id} |-> event]),!.basisHistory=VJoin(@,[k \in {id} |-> MinimalCaptureSA(VBasis(q))]),!.costCP=IF role="Cost" THEN id ELSE @,!.cpResume=resume,!.cpRole=role,!.stage="VCP"]
VCPNext(f) ==
 LET rest==SubSeq(f.owed,2,Len(f.owed)) IN
 [f EXCEPT !.owed=rest,!.done=@ \cup {f.point},!.point=IF rest= <<>> THEN "ProcedureCodeb74d673a0fc6" ELSE rest[1],!.phase=IF rest= <<>> THEN "Completed" ELSE "Steps"]
VLegal(selected) == selected={}
VCPWork ==
 LET q==qT11 f==VFrame(q) next==VCPNext(f) world==VWorld(q,f) IN
 CASE f.point="ProcedureCodee605a78f5d5e" ->
   LET cp==VCPData(q,f) key==[definition |-> ConditionalKey96(VChildDefinition),occurrence |-> 1]
       allocation==[k \in IF q.cpRole="Cost" /\ ConditionalActive96(VChildDefinition,cp.processingSnapshot) THEN {key} ELSE {} |-> 201]
       bindings==[k \in DOMAIN allocation |-> [kind |-> "Reaction",checkpointId |-> cp.id,windowId |-> q.childWindow,group |-> 4]]
       conditions==[k \in DOMAIN VDefinitions(q) |-> [id \in DOMAIN cp.occurrences |->
         [tag |-> "ConditionalTriggerStipulations",ability |-> 200,source |-> VChildDefinition.syntax.source,
          occurrence |-> id,snapshotId |-> cp.occurrences[id].snapshot.id,results |-> EmptyT11]]]
       ledger==ProtocolP!CPAfter9p(q.ledger,cp,allocation,bindings)
       after==[next EXCEPT !.recognition=cp,!.recognized=CheckpointMemberMap103(ledger,f.id)]
       x==[route |-> "Ordinary",cp |-> cp,definitions |-> VDefinitions(q),lexemes |-> VLexemes(q),conditions |-> conditions,
         allocation |-> allocation,bindings |-> bindings,departures |-> EmptyT11,holds |-> EmptyT11,
         usedWindows |-> q.usedWindows,cardFacts |-> CardFacts10]
   IN /\ VAdmitSnapshot(q,q.objects,q.ledger,cp.beginSnapshot)
      /\ VAdmitSnapshot(q,q.objects,q.ledger,cp.processingSnapshot)
      /\ x.definitions=ConditionalDefinitionsSA(q.abilityRegistry)
      /\ RecognizeCheckpoint103(f,after,q.ledger,ledger,q.stack,q.stack,x)
      /\ qT11'=[VSetFrame(q,after) EXCEPT !.ledger=ledger,
        !.noChild=IF q.cpRole="Cost" THEN DOMAIN after.recognized={} ELSE @,
        !.noChildReceipt=IF q.cpRole="Cost" THEN [checkpoint |-> cp.id,allocation |-> allocation,bindings |-> bindings,
          recognized |-> after.recognized,processingSnapshot |-> cp.processingSnapshot,instances |-> ledger.instances,
          actualConditionalActive |-> ConditionalActive96(VChildDefinition,cp.processingSnapshot)] ELSE @]
 [] f.point="ProcedureCode88eda145024f" ->
   LET cursor==LingeringCheckpointFrame910(q.ledger,f.recognition,world)
       cleanup==[tag |-> "LingeringCheckpointCleanup",frame |-> cursor,expired |-> {},complete |-> TRUE]
       registry==[q.registry EXCEPT !.cleanupIds=@ \cup {f.id}]
       snapshot==SnapshotWithConditionalRegistry96(q.ledger.lastSnapshot,q.ledger)
   IN /\ VWorldBound(q,f,world)
      /\ VAdmitSnapshot(q,q.objects,q.ledger,snapshot)
      /\ CheckpointCleanupEffects103(f,next,q.registry,registry,q.ledger,q.ledger,q.ledger,q.stack,q.stack,
        snapshot,snapshot,world,cursor,[cursor EXCEPT !.returned=TRUE,!.point="ProcedureCodeb681cc249a04"],cleanup)
      /\ qT11'=[VSetFrame(q,next) EXCEPT !.registry=registry]
 [] f.point="ProcedureCodeb681cc249a04" ->
   /\ CheckpointVictory103(f,next,q.objects,[id \in DOMAIN q.objects |-> 0],f.snapshotId)
   /\ qT11'=VSetFrame(q,next)
 [] f.point="ProcedureCodefe50c31480ea" ->
   /\ CheckpointUniqueRetire103(f,next,q.objects,q.objects,[id \in DOMAIN q.objects |-> q.objects[id].card],{},{},{},
        [id \in DOMAIN q.objects |-> "SideA"],EmptyT11,EmptyT11,DOMAIN q.objects,VPrinted,VOwners,{},f.snapshotId)
   /\ qT11'=VSetFrame(q,next)
 [] f.point="ProcedureCodea488e1ba6ca3" ->
   /\ CheckpointIllegalRetire103(f,next,q.objects,q.objects,{},VLegal,[id \in DOMAIN q.objects |-> "SideA"],q.flow.turn.owner,
        [s \in CentralTargetSites4 |-> [kind |-> "SchemaAtom033"]],[applies |-> FALSE],"NoValue",{},EmptyT11,DOMAIN q.objects,VPrinted,VOwners,{},f.snapshotId)
   /\ qT11'=VSetFrame(q,next)
 [] f.point \in {"ProcedureCode76ca53ad9dd0","ProcedureCode96bfa1b6a970"} ->
   /\ CheckpointHostedCleanup103(f,next,q.objects,q.objects,EmptyT11,EmptyT11,EmptyT11,
        IF q.paid=EmptyT11 THEN EmptyT11 ELSE [id \in {q.paid.id} |-> q.paid],EmptyT11,DOMAIN q.objects,VPrinted,VOwners,{},f.snapshotId)
   /\ qT11'=VSetFrame(q,next)
 [] f.point="ProcedureCode2d73b20aa788" ->
   /\ CheckpointAuxiliarySiteCleanup103(f,next,[s \in CentralTargetSites4 |-> [kind |-> "SchemaAtom033"]],
        [s \in CentralTargetSites4 |-> [kind |-> "SchemaAtom033"]],q.objects,EmptyT11,f.snapshotId)
   /\ qT11'=VSetFrame(q,next)
 [] f.point="ProcedureCode2d6279f9d639" ->
   /\ CheckpointPositionCleanup103(f,next,q.layout,q.layout,q.control.traversal.position,EmptyT11,f.snapshotId)
   /\ qT11'=VSetFrame(q,next)
 [] f.point="ProcedureCode7f181ce21011" ->
   /\ CheckpointRootAdmissions103(f,next,q.capacity,q.capacity,IBT11(q),q.objects,EmptyT11,0,q.ledger.stepSerial,{},"SideB",f.snapshotId)
   /\ qT11'=VSetFrame(q,next)
 [] f.point="ProcedureCodeda83a77a1f12" ->
   /\ CheckpointRestoreDiscard103(f,next,q.objects,q.objects,EmptyT11,EmptyT11,VPrinted,f.snapshotId)
   /\ qT11'=VSetFrame(q,next)
 [] f.point="ProcedureCode0811ebc5f40e" ->
   /\ CheckpointReturnDiscardCounters103(f,next,q.objects,q.objects,f.snapshotId)
   /\ qT11'=VSetFrame(q,next)
 [] f.point="ProcedureCodeb74d673a0fc6" ->
   IF DOMAIN f.recognized={} THEN
     LET returned==[f EXCEPT !.phase="Returned",!.returned=TRUE] IN
     /\ VWorldBound(q,f,world)
     /\ ReturnCheckpointWithoutReaction103(f,returned,q.ledger,world,PersistentCheckpointCompletion912(q.ledger,f.recognition,world),f.caller)
     /\ qT11'=[VSetFrame(q,returned) EXCEPT !.stage=q.cpResume,
         !.wallet.checkpointDue=IF q.cpRole="Cost" THEN FALSE ELSE @,
         !.noReactionCostReturned=IF q.cpRole="Cost" THEN TRUE ELSE @,
         !.noReactionCostReceipt=IF q.cpRole="Cost" THEN [frame |-> returned,caller |-> f.caller,recognized |-> f.recognized,
           currentWorld |-> world,persistent |-> PersistentCheckpointCompletion912(q.ledger,f.recognition,world)] ELSE @,
         !.checkpointHistory=Append(@,[id |-> f.id,role |-> q.cpRole,caller |-> f.caller,objects |-> q.objects,done |-> f.done])]
   ELSE
     LET members==f.recognized site==WindowTop9(q.stack).site
         opening==VJoin(IOpeningT11(q.childWindow,"Reaction",site),
           [members |-> DOMAIN members,instances |-> members,group |-> 4,modifiersExist |-> FALSE,
            preparation |-> <<"ConditionsMet","PendingGroup">>,checkpointId |-> f.id,caller |-> f.caller,
            completion |-> PersistentCheckpointCompletion912(q.ledger,f.recognition,world)])
         window==NewPriorityWindow9(q.childWindow,"Reaction",site,members,4,NoTimingRef9,[id |-> 0],0)
         after==[f EXCEPT !.phase="Reaction",!.windowId=q.childWindow]
     IN /\ VWorldBound(q,f,world)
        /\ OpenCheckpointReaction103(f,after,q.ledger,q.stack,Append(q.stack,window),site,opening,q.usedWindows)
        /\ qT11'=[VSetFrame(q,after) EXCEPT !.stack=Append(@,window),!.usedWindows=@ \cup {q.childWindow},!.stage="VReceive"]
 [] OTHER -> FALSE
VNativeAtPayment(q,selected,after) ==
 /\ q.paid.transaction=2500 /\ q.paid.windowId=WindowTop9(q.stack).id /\ q.paid.ability.caller=q.paid.windowId
 /\ q.paid.option.target=IAT11(q).object /\ q.paid.turnId=q.flow.turn.id
 /\ q.paid.definition.triggerCost=VPaidDefinition(q).triggerCost
 /\ ItemInspectionCostOwnerT11!SpendResourceUnitsOK(q.wallet,"SideB",selected,q.amount,{})
 /\ after=ItemInspectionWalletSpentT11(q.wallet,selected)
VNativeCommitted(q) ==
 /\ q.native.transaction=q.paid.transaction /\ q.native.window=q.paid.windowId /\ q.native.option=q.paid.option
 /\ q.native.source=q.paid.ability.source /\ q.native.turn=q.flow.turn.id /\ q.native.itemInspection=77 /\ q.native.siteInspection=20 /\ q.native.traversal=7
 /\ q.native.amount=q.amount /\ Cardinality(q.native.selected)=q.amount
 /\ q.native.after=ItemInspectionWalletSpentT11(q.native.before,q.native.selected)
 /\ ItemInspectionCostOwnerT11!SpendResourceUnitsOK(q.native.before,"SideB",q.native.selected,q.amount,{})
 /\ q.wallet=[q.native.after EXCEPT !.checkpointDue=~q.frames[q.costCP].returned]
 /\ q.uses=ItemInspectionPaidUsesT11(q.paid) /\ q.turnUses=VTurnUses(q.paid) /\ q.useEvents= <<VUse(q.paid)>>
VPayment(q) == [tag |-> "PriorityOptionPayment",windowId |-> q.paid.windowId,option |-> q.paid.option,transactionId |-> q.paid.transaction,
 allTriggerCostsPaid |-> VNativeCommitted(q),costCheckpointAndReactionsDrained |-> CheckpointDrained103(q.frames[q.costCP],q.ledger,q.stack)]
VChildObligation(q) ==
 IF q.costCP=0 THEN FALSE
 ELSE /\ CheckpointDrained103(q.frames[q.costCP],q.ledger,q.stack)
      /\ IF DOMAIN q.frames[q.costCP].recognized={} THEN
           q.noReactionCostReturned /\ q.child=EmptyT11 /\ ~q.childReturned
         ELSE q.childReturned /\ q.child.phase="Returned" /\ q.ledger.instances[201].status="Complete"
VReturn(q) == [tag |-> "PriorityOptionReturn",windowId |-> q.paid.windowId,option |-> q.paid.option,transactionId |-> q.paid.transaction,
 triggerPayment |-> VPayment(q),allCostsPaid |-> VNativeCommitted(q),optionComplete |-> q.paid.ability.complete,
 childrenReturned |-> VChildObligation(q) /\ q.plan.phase="Complete",reactionsDrained |-> CheckpointDrained103(q.frames[q.paid.checkpoint],q.ledger,q.stack),
 finalCheckpointId |-> q.paid.checkpoint]
VTargets(plan,targets) == [ProtocolP!Targets9p(plan) EXCEPT !.targets=targets]
VReadyCP(q) == ProtocolP!PriorityCP9p(WindowTop9(q.stack),q.currentCP)
VMidWindow ==
 LET q==qT11 w==WindowTop9(q.stack) a==IAT11(q) IN
 CASE w.stage="NeedCheckpoint" -> VOpenCP("SchemaAtom126",ConditionalPriorityCaller96(w),"VMidReady","MidPriority")
 [] w.stage="Ready" ->
   LET d==VPaidDefinition(q) option==VPaidOption(q,w,d) busy==StartPriorityOptionFrame9(w,option,2500)
       p==OpenPaidProcedure95(250,d,option,w,2500,"Rule") context==VContext(q,d) IN
   IF VInitialPaid(q.availabilityProfile) THEN
     LET itemInspection==[a EXCEPT !.midDone=TRUE] stack==ReplaceWindowTop9(q.stack,ClosePriorityWindow9(w)) IN
     /\ BasisValidSA(q.catalog,VBasis(q)) /\ VHistoryValid(q)
     /\ ~PaidEligibility95(d,context,w)
     /\ ~ReservePaidMidItemInspection95(q.stack,ReplaceWindowTop9(q.stack,busy),p,250,d,context,option,VLegality(w,option,2500),{},a,a,VMid(q),{VMid(q)},FALSE,FALSE)
     /\ PassMidItemInspection9(q.stack,stack,a,itemInspection,q.objects,{VMid(q)},FALSE,FALSE)
     /\ qT11'=[IWithItemInspectionT11(q,itemInspection) EXCEPT !.stack=stack,!.declined=TRUE,
         !.declineReceipt=[windowId |-> w.id,stage |-> w.stage,basis |-> MinimalCaptureSA(VBasis(q)),context |-> context,
           reservationRejected |-> TRUE,nativeEligibility |-> PaidEligibility95(d,context,w),bindingAccepted |-> VAdmitPaid(q,d,context),
           paid |-> q.paid,native |-> q.native,uses |-> q.uses,child |-> q.child]]
   ELSE /\ VAdmitPaid(q,d,context)
        /\ ReservePaidMidItemInspection95(q.stack,ReplaceWindowTop9(q.stack,busy),p,250,d,context,option,VLegality(w,option,2500),{},a,a,VMid(q),{VMid(q)},FALSE,FALSE)
        /\ qT11'=[q EXCEPT !.stack=ReplaceWindowTop9(@,busy),!.paid=p,!.stage="VPay"]
 [] w.stage="Closed" ->
   LET rest==SubSeq(q.stack,1,Len(q.stack)-1) IN
   /\ PopClosedPriorityWindow9(q.stack,rest)
   /\ qT11'=IRecordT11([q EXCEPT !.stack=rest],"ProcedureCode1dd0e8f05be2",{},IF a.complete THEN "ItemInspectionReturn" ELSE "ItemInspectionAdvance")
 [] OTHER -> FALSE
VProtocolWork ==
 LET q==qT11 IN
 CASE q.stage="VMidReady" ->
   LET w==WindowTop9(q.stack) ready==[w EXCEPT !.stage="Ready",!.checkpoint=q.currentCP] IN
   /\ ReceivePriorityAfterCheckpoint103(VFrame(q),q.ledger,q.stack,ReplaceWindowTop9(q.stack,ready),VReadyCP(q))
   /\ qT11'=[q EXCEPT !.stack=ReplaceWindowTop9(@,ready),!.stage="Window"]
 [] q.stage="VPay" ->
   LET p==q.paid selected==IF q.amount=0 THEN {} ELSE {100} after==ItemInspectionWalletSpentT11(q.wallet,selected)
       paid==ItemInspectionPaidCommittedFrameT11(p)
       committedSnapshot==VCurrentSnapshot(q,q.objects,q.ledger,q.nextWorld,"CommittedPaidUse",q.ledger.lastCheckpoint) a==IAT11(q) used==[a EXCEPT !.midUsed=TRUE,!.midResolving=TRUE]
       payment==[tag |-> "PaidTriggerPayment",abilityInstance |-> p.id,transactionId |-> p.transaction,
        ability |-> p.definition.syntax.id,source |-> p.ability.source,triggerCost |-> p.definition.triggerCost,
        beforeObjects |-> q.objects,afterObjects |-> q.objects,announced |-> TRUE,allPaid |-> VNativeAtPayment(q,selected,after),
        additionalCostsPaid |-> TRUE,restrictionsBefore |-> TRUE,restrictionsAfter |-> TRUE,simultaneousProcedureComplete |-> TRUE,
        sourceAfter |-> 0,sourceUninstalled |-> FALSE,sourceForfeited |-> FALSE,paidOperations |-> {},publicEvents |-> {}]
   IN /\ VFreshWorld(q,{q.nextWorld}) /\ VAdmitSnapshot(q,q.objects,q.ledger,committedSnapshot)
      /\ PayPaidMidItemInspection95(q.stack,p,paid,q.objects,q.objects,EmptyT11,EmptyT11,EmptyT11,DOMAIN q.objects,payment,
        q.uses,ItemInspectionPaidUsesT11(p),q.turnUses,VTurnUses(p),1,{VUse(p)},a,used,VMid(q),{VMid(q)},FALSE,FALSE,
        [tag |-> "MidItemInspectionBeginDrained",itemInspectionId |-> a.id,windowId |-> p.windowId,checkpointId |-> p.initialCheckpoint,
         complete |-> CheckpointDrained103(q.frames[p.initialCheckpoint],q.ledger,q.stack)],{})
      /\ qT11'=[IWithItemInspectionT11(VKeepWorld(q,VBasis(q),<<committedSnapshot>>),used) EXCEPT !.commitSnapshot=committedSnapshot,!.wallet=after,!.paid=paid,!.uses=ItemInspectionPaidUsesT11(p),!.turnUses=VTurnUses(p),
        !.useEvents= <<VUse(p)>>,!.useIndex=[id \in {1} |-> 1],!.procedures=[id \in {paid.id} |-> paid],!.native=[before |-> q.wallet,after |-> after,selected |-> selected,amount |-> q.amount,
         transaction |-> p.transaction,window |-> p.windowId,option |-> p.option,source |-> p.ability.source,
         turn |-> q.flow.turn.id,itemInspection |-> a.id,siteInspection |-> a.siteInspectionId,traversal |-> a.traversalId],!.stage="VCostOpen"]
      /\ ItemInspectionCostOwnerT11!DoSpendResourceUnits(ItemInspectionCostCommandT11(selected,q.amount))
 [] q.stage="VCostOpen" -> VOpenCP("Cost",PaidCheckpointCaller96(q.paid),"VCostResume","Cost")
 [] q.stage="VCP" -> VCPWork
 [] q.stage="VReceive" -> VOpenCP("SchemaAtom126",ConditionalPriorityCaller96(WindowTop9(q.stack)),"VChildReady","ChildPriority")
 [] q.stage="VChildReady" ->
   LET w==WindowTop9(q.stack) ready==[w EXCEPT !.stage="Ready",!.checkpoint=q.currentCP] IN
   /\ ReceivePriorityAfterCheckpoint103(VFrame(q),q.ledger,q.stack,ReplaceWindowTop9(q.stack,ready),VReadyCP(q))
   /\ qT11'=[q EXCEPT !.stack=ReplaceWindowTop9(@,ready),!.stage=IF q.childReturned THEN "VPass" ELSE "VSelect"]
 [] q.stage="VSelect" ->
   LET w==WindowTop9(q.stack) d==VChildDefinition option==PriorityOption9(70,"Conditional","SideB",200,201,d.syntax.source,0,{})
       busy==StartPriorityOptionFrame9(w,option,2600) p==OpenConditionalProcedure96(201,d,w,option,2600,"Rule")
       plan==OpenInstruction93(710,"Ability",201,d.syntax.source,"Rule",1,"NoValue",<<"CostReaction">>,FALSE)
       imminent==[p EXCEPT !.phase="Imminent",!.ability.phase="Imminent",!.ability.firstImminent=TRUE,!.ability.detached=TRUE]
       announced==[plan EXCEPT !.phase="Imminent",!.announced=TRUE] ledger==[q.ledger EXCEPT !.instances[201].status="Imminent"]
       selectedSnapshot==VCurrentSnapshot(q,q.objects,q.ledger,q.nextWorld,"Selection",q.ledger.lastCheckpoint)
   IN /\ VFreshWorld(q,{q.nextWorld}) /\ VAdmitSnapshot(q,q.objects,q.ledger,selectedSnapshot)
      /\ BeginConditionalResolution96(q.ledger,ledger,q.stack,ReplaceWindowTop9(q.stack,busy),p,imminent,d,
        selectedSnapshot,201,option,VLegality(w,option,2600),EmptyT11,plan,announced,
        VTargets(plan,{}),ProtocolP!Entry9p(plan,0),VChildTurnUses(q),
        [tag |-> "AbilityRestrictions",ability |-> 200,source |-> d.syntax.source,results |-> EmptyT11])
      /\ qT11'=[VKeepWorld(q,VBasis(q),<<selectedSnapshot>>) EXCEPT !.ledger=ledger,!.stack=ReplaceWindowTop9(@,busy),!.child=imminent,!.childPlan=announced,!.stage="VChildBegin"]
 [] q.stage="VChildBegin" ->
   LET 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[201].status="Resolving",!.instances[201].expected=[i \in {1} |->
         [instruction |-> InstructionWindowRef93(q.childPlan),effects |-> {1}]]]
   IN /\ ResolveConditionalWithoutInterrupt96(q.ledger,ledger,q.stack,q.child,p,q.childPlan,plan,
        ProtocolP!NoModifiers9p(q.childPlan),ProtocolP!Clearance9p(q.childPlan),expected)
      /\ qT11'=[q EXCEPT !.ledger=ledger,!.child=p,!.childPlan=plan,!.stage="VChildWork"]
 [] q.stage="VChildWork" ->
   LET change==VPaidLoss(q.availabilityProfile)
       cause==IF q.availabilityProfile="paid-permission" THEN "PermissionWithdraw" ELSE "EntryWithdraw"
       target==KernelTargetRA(q.catalog[1].source,IF cause="PermissionWithdraw" THEN 0 ELSE 1)
       beforeSnapshot==VCurrentSnapshot(q,q.objects,q.ledger,q.nextWorld,"InstructionBefore",q.ledger.lastCheckpoint)
       basis==IF change THEN KernelBasisRA(q.catalog,VBasis(q),cause,target) ELSE VBasis(q)
       candidateSnapshot==ConditionalSnapshotFromRegistrySA(q.catalog,basis,q.ledger,PublicationTemplateRA(beforeSnapshot,q.nextWorld+1))
       observerSnapshot==PublicationObserverSnapshotRA(q.ledger,q.ledger,beforeSnapshot,candidateSnapshot)
       intermediateLedger==IF change THEN PublicationAfterLedgerRA(q.ledger,q.ledger,beforeSnapshot,candidateSnapshot) ELSE q.ledger
       intermediateStack==IF change THEN PublicationAfterStackRA(q.stack,q.ledger,intermediateLedger) ELSE q.stack
       intermediateSnapshot==IF change THEN ConditionalSnapshotFromRegistrySA(q.catalog,basis,intermediateLedger,observerSnapshot) ELSE beforeSnapshot
       capturedBefore==VKeepWorld(q,VBasis(q),<<beforeSnapshot>>)
       mid0==[VSetBasis(capturedBefore,basis) EXCEPT !.ledger=intermediateLedger,!.stack=intermediateStack]
       mid==IF change THEN VKeepWorld(mid0,basis,<<intermediateSnapshot>>) ELSE mid0
       objects==IF q.moves THEN ItemInspectionMovedObjectsT11(q.objects,"SideADiscard") ELSE q.objects
       a==IAT11(q) itemInspection==IF q.moves THEN ItemInspectionEndedT11(a,"Moved") ELSE a
       ability==ProtocolP!FinishedAbility9p(q.child.ability,q.childPlan)
       p==[q.child EXCEPT !.ability=ability,!.phase="InstructionCheckpoint",!.checkpoint=0]
       plan==ProtocolP!FinishedPlan9p(q.childPlan)
       ledger==[intermediateLedger EXCEPT !.instances[201].status="Complete"]
       afterSnapshot==VCurrentSnapshot(mid,objects,ledger,mid.nextWorld,"InstructionAfter",q.ledger.lastCheckpoint)
       final==VKeepWorld(mid,VBasisObjects(mid,objects),<<afterSnapshot>>)
       receipt==[cause |-> cause,target |-> target,instruction |-> InstructionWindowRef93(q.childPlan),
         beforeBasis |-> MinimalCaptureSA(VBasis(q)),afterBasis |-> MinimalCaptureSA(basis),
         beforeLedger |-> q.ledger,intermediateLedger |-> intermediateLedger,finalLedger |-> ledger,
         beforeSnapshot |-> beforeSnapshot,candidateSnapshot |-> candidateSnapshot,observerSnapshot |-> observerSnapshot,
         intermediateSnapshot |-> intermediateSnapshot,afterSnapshot |-> afterSnapshot,
         paidDefinition |-> q.paid.definition,paidSource |-> q.paid.ability.source,paidCaller |-> q.paid.ability.caller,
         actualPayment |-> q.native,committedUse |-> q.useEvents[1]]
   IN /\ VFreshWorld(q,IF change THEN {q.nextWorld,q.nextWorld+1,q.nextWorld+2} ELSE {q.nextWorld,q.nextWorld+1})
      /\ q.childPlan.phase="Resolving" /\ q.child.phase="Resolve" /\ q.child.ability.detached
      /\ q.paid.costPaid /\ q.paid.ability.detached /\ VNativeCommitted(q)
      /\ VAdmitSnapshot(q,q.objects,q.ledger,beforeSnapshot)
      /\ IF change THEN
           /\ ~q.kernelDone
           /\ AdmitKernelPublicationRA(q.catalog,VBasis(q),basis,cause,target,q.nextWorld+1,
                q.ledger,q.ledger,intermediateLedger,q.stack,intermediateStack,beforeSnapshot,candidateSnapshot,observerSnapshot,intermediateSnapshot)
         ELSE intermediateLedger=q.ledger /\ intermediateStack=q.stack
      /\ VAdmitSnapshot(mid,q.objects,intermediateLedger,intermediateSnapshot)
      /\ VAdmitSnapshot(mid,objects,ledger,afterSnapshot)
      /\ RecordConditionalExecutionUse96(intermediateLedger,intermediateLedger,q.child,q.childPlan,
        [tag |-> "ConditionalEffectExecution",instruction |-> InstructionWindowRef93(q.childPlan),abilityInstance |-> q.child.id,
         source |-> q.child.ability.source,partIds |-> {1}],q.uses,q.uses,q.turnUses,q.turnUses,2,{})
      /\ CarryConditionalInstruction96(intermediateLedger,ledger,ledger,intermediateStack,intermediateStack,q.child,p,q.childPlan,plan,
        ProtocolP!Step9p(q.childPlan),intermediateSnapshot,afterSnapshot)
      /\ IF q.moves THEN
           /\ CardBatchTransfer8(q.objects,objects,{1},[id \in {1} |-> 2],{1},"SideADiscard","Up",[id \in {1} |-> <<"SideADiscard",2>>])
           /\ ItemInspectionMovementOutcome7(a,itemInspection,objects,TRUE,{ItemInspectionEndEvent7(a)})
         ELSE objects=q.objects /\ itemInspection=a
      /\ qT11'=[IWithItemInspectionT11(final,itemInspection) EXCEPT !.ledger=ledger,!.stack=intermediateStack,!.child=p,!.childPlan=plan,!.objects=objects,
        !.kernelDone=change,!.kernelReceipt=IF change THEN receipt ELSE @,
        !.work=Append(@,"CostReaction"),!.rawEvents=IF q.moves THEN Append(@,{ItemInspectionEndEvent7(a)}) ELSE @,!.stage="VChildCPOpen"]
 [] q.stage="VChildCPOpen" -> VOpenCP("Instruction",ConditionalInstructionCaller96(q.child),"VChildCPDone","ChildFinal")
 [] q.stage="VChildCPDone" ->
   LET p==[q.child EXCEPT !.phase="Complete",!.checkpoint=q.currentCP]
       receipt==[tag |-> "ConditionalInstructionCheckpoint",id |-> q.currentCP,abilityInstance |-> q.child.id,
        transactionId |-> q.child.transaction,source |-> q.child.ability.source,instruction |-> q.childPlan.id,index |-> 1,
        complete |-> TRUE,allNewerChainsComplete |-> TRUE]
   IN /\ ResumeConditionalInstructionAfterCheckpoint103(VFrame(q),q.ledger,q.stack,q.child,p,receipt)
      /\ qT11'=[q EXCEPT !.child=p,!.stage="VChildReturn"]
 [] q.stage="VChildReturn" ->
   LET p==[q.child EXCEPT !.phase="Returned",!.ability.returned=TRUE] w==WindowTop9(q.stack)
       receipt==[ProtocolP!Return9p(w,q.child.checkpoint) EXCEPT !.optionComplete=q.child.ability.complete,
         !.childrenReturned=q.child.ability.complete,!.reactionsDrained=CheckpointDrained103(q.frames[q.child.checkpoint],q.ledger,q.stack),
         !.triggerPayment.costCheckpointAndReactionsDrained=CheckpointDrained103(q.frames[q.child.checkpoint],q.ledger,q.stack)]
   IN /\ FinishConditionalProcedure96(q.stack,ReplaceWindowTop9(q.stack,CompletePriorityOptionFrame9(w)),q.child,p,receipt)
      /\ qT11'=[q EXCEPT !.child=p,!.stack=ReplaceWindowTop9(@,CompletePriorityOptionFrame9(w)),!.childReturned=TRUE,!.stage="VReceive"]
 [] q.stage="VPass" ->
   LET w==WindowTop9(q.stack) after==PassPriorityFrame9(w)
       snapshot==VCurrentSnapshot(q,q.objects,q.ledger,q.nextWorld,"Pass",q.ledger.lastCheckpoint)
   IN /\ VFreshWorld(q,{q.nextWorld}) /\ VAdmitSnapshot(q,q.objects,q.ledger,snapshot)
      /\ PassConditionalPriority96(q.ledger,q.ledger,q.ledger,q.stack,ReplaceWindowTop9(q.stack,after),w.priority,EmptyT11,snapshot,snapshot)
      /\ qT11'=[VKeepWorld(q,VBasis(q),<<snapshot>>) EXCEPT !.stack=ReplaceWindowTop9(@,after),!.stage=IF after.open THEN "VReceive" ELSE "VCostReturn"]
 [] q.stage="VCostReturn" ->
   LET f==q.frames[q.costCP] returned==[f EXCEPT !.phase="Returned",!.returned=TRUE] rest==SubSeq(q.stack,1,Len(q.stack)-1)
   IN /\ ReturnCheckpointAfterReaction103(f,returned,q.ledger,q.stack,rest,f.caller)
      /\ qT11'=[VSetFrame(q,returned) EXCEPT !.stack=rest,!.wallet.checkpointDue=FALSE,!.currentCP=q.costCP,!.stage="VCostResume",
        !.checkpointHistory=Append(@,[id |-> f.id,role |-> "Cost",caller |-> f.caller,objects |-> q.objects,done |-> f.done])]
 [] q.stage="VCostResume" ->
   LET p==[q.paid EXCEPT !.phase="Targets",!.checkpoint=q.costCP] IN
   /\ ResumePaidAfterCheckpoint103(q.frames[q.costCP],q.ledger,q.stack,q.paid,p,q.objects,EmptyT11,ItemInspectionPaidCheckpointT11(q.paid,q.costCP,TRUE))
   /\ qT11'=[q EXCEPT !.paid=p,!.stage="VTargets"]
 [] q.stage="VTargets" ->
   LET p==q.paid plan==ItemInspectionPaidPlanT11(p) targets==IF 1 \in DOMAIN q.objects THEN {1} ELSE {}
       afterPlan==[plan EXCEPT !.targets=targets,!.announced=TRUE,!.phase="Imminent"]
       imminent==[p EXCEPT !.ability.phase="Imminent",!.ability.firstImminent=TRUE,!.phase="Imminent",!.checkpoint=0]
   IN /\ EnterPaidInstruction95(q.stack,p,imminent,plan,afterPlan,VTargets(plan,targets),ItemInspectionPaidEntryT11(plan,p.checkpoint))
      /\ qT11'=[q EXCEPT !.paid=imminent,!.plan=afterPlan,!.announcement=[objects |-> q.objects,targets |-> targets,
        instruction |-> InstructionWindowRef93(afterPlan),costCheckpoint |-> q.costCP,child |-> q.child,turn |-> q.flow.turn.id],!.stage="VBegin"]
 [] q.stage="VBegin" ->
   LET p==[q.paid EXCEPT !.ability.phase="Resolving",!.phase="Resolve"] plan==[q.plan EXCEPT !.phase="Resolving"] IN
   /\ ResolvePaidWithoutInterrupt95(q.stack,q.paid,p,q.plan,plan,ItemInspectionPaidNoModifiersT11(q.plan),ItemInspectionPaidInterruptReturnT11(q.plan))
   /\ qT11'=[q EXCEPT !.paid=p,!.plan=plan,!.stage="VBody"]
 [] q.stage="VBody" ->
   LET plan==q.plan after==[plan EXCEPT !.completedSteps=Append(@,"MidEffect"),!.cursor=2] IN
   /\ q.announcement.objects=q.objects /\ plan.targets=q.announcement.targets
   /\ CarryPaidInstruction95(q.stack,q.paid,q.paid,plan,after,ProtocolP!Step9p(plan))
   /\ qT11'=[q EXCEPT !.plan=after,!.work=Append(@,"MidEffect"),!.stage="VTail"]
 [] q.stage="VTail" ->
   LET plan==ProtocolP!FinishedPlan9p(q.plan) ability==ProtocolP!FinishedAbility9p(q.paid.ability,q.plan)
       p==[q.paid EXCEPT !.ability=ability,!.phase="InstructionCheckpoint",!.checkpoint=0]
   IN /\ CarryPaidInstruction95(q.stack,q.paid,p,q.plan,plan,ProtocolP!Step9p(q.plan))
      /\ qT11'=[q EXCEPT !.paid=p,!.plan=plan,!.work=Append(@,"MidTail"),!.stage="VFinalOpen"]
 [] q.stage="VFinalOpen" -> VOpenCP("Instruction",PaidCheckpointCaller96(q.paid),"VFinalDone","PaidFinal")
 [] q.stage="VFinalDone" ->
   LET p==[q.paid EXCEPT !.phase="Complete",!.checkpoint=q.currentCP] IN
   /\ ResumePaidAfterCheckpoint103(VFrame(q),q.ledger,q.stack,q.paid,p,q.objects,EmptyT11,ItemInspectionPaidCheckpointT11(q.paid,q.currentCP,TRUE))
   /\ qT11'=[q EXCEPT !.paid=p,!.stage="VFinish"]
 [] q.stage="VFinish" ->
   LET a==IAT11(q) itemInspection==[a EXCEPT !.midResolving=FALSE,!.midDone=TRUE]
       paid==[q.paid EXCEPT !.ability.returned=TRUE,!.phase="Returned"] w==WindowTop9(q.stack)
   IN /\ FinishPaidMidItemInspection95(q.stack,ReplaceWindowTop9(q.stack,CompletePriorityOptionFrame9(w)),q.paid,paid,VReturn(q),a,itemInspection)
      /\ qT11'=[IWithItemInspectionT11(q,itemInspection) EXCEPT !.paid=paid,!.stack=ReplaceWindowTop9(@,CompletePriorityOptionFrame9(w)),!.paidReturned=TRUE,!.stage="Window"]
 [] OTHER -> FALSE
VDispatch ==
 /\ UNCHANGED guideCaseT11
 /\ IF qT11.stage="Window" /\ qT11.windowRole="Mid" THEN VMidWindow
    ELSE IF qT11.stage \in {"VMidReady","VPay","VCostOpen","VCP","VReceive","VChildReady","VSelect","VChildBegin","VChildWork",
      "VChildCPOpen","VChildCPDone","VChildReturn","VPass","VCostReturn","VCostResume","VTargets","VBegin","VBody","VTail","VFinalOpen","VFinalDone","VFinish"}
      THEN VProtocolWork ELSE IConnectedStepT11
VWork == VDispatch /\ VHistoryFrame(qT11,qT11')
VSpec == VInit /\ [][VWork]_<<guideCaseT11,qT11>> /\ WF_<<guideCaseT11,qT11>>(VWork)
VPaidCompletion == (~VUnavailable(qT11.availabilityProfile)) => <>qT11.done
VDeclineCompletion == VInitialPaid(qT11.availabilityProfile) => <>qT11.done
VNoChildCompletion == VInitialConditional(qT11.availabilityProfile) => <>qT11.done
VSourceIndexChecks(q) ==
 /\ VHistoryValid(q)
 /\ (q.paid=EmptyT11 \/ ~q.paid.costPaid => q.useIndex=EmptyT11 /\ q.procedures=EmptyT11)
 /\ (q.paid#EmptyT11 /\ q.paid.costPaid =>
    /\ q.useIndex=[id \in {1} |-> 1]
    /\ DOMAIN q.procedures={q.paid.id}
    /\ q.procedures[q.paid.id].definition=q.paid.definition
    /\ q.procedures[q.paid.id].ability.source=q.paid.ability.source
    /\ VChildTurnUses(q)=EmptyT11)
VGuardChecks(q) ==
 /\ (Len(q.stack)=3 =>
    LET p==[q.paid EXCEPT !.phase="Targets",!.checkpoint=q.costCP] IN
    /\ (WindowTop9(q.stack).open => ~ConditionalCheckpointDrained96(q.ledger,q.stack,q.costCP))
    /\ ~ResumePaidAfterCheckpoint103(q.frames[q.costCP],q.ledger,q.stack,q.paid,p,q.objects,EmptyT11,ItemInspectionPaidCheckpointT11(q.paid,q.costCP,TRUE)))
 /\ (q.stage="VCostResume" =>
    LET f==q.frames[q.costCP] p==[q.paid EXCEPT !.phase="Targets",!.checkpoint=q.costCP]
        receipt==ItemInspectionPaidCheckpointT11(q.paid,q.costCP,TRUE) IN
    /\ ResumePaidAfterCheckpoint103(f,q.ledger,q.stack,q.paid,p,q.objects,EmptyT11,receipt)
    /\ ~ResumePaidAfterCheckpoint103([f EXCEPT !.caller.transactionId=2501],q.ledger,q.stack,q.paid,p,q.objects,EmptyT11,receipt)
    /\ ~ResumePaidAfterCheckpoint103(f,q.ledger,q.stack,[q.paid EXCEPT !.transaction=2501],p,q.objects,EmptyT11,receipt)
    /\ ~ResumePaidAfterCheckpoint103(f,q.ledger,q.stack,q.paid,p,q.objects,EmptyT11,[receipt EXCEPT !.id=1]))
 /\ (q.stage="VCostReturn" =>
    LET f==q.frames[q.costCP] returned==[f EXCEPT !.phase="Returned",!.returned=TRUE]
        rest==SubSeq(q.stack,1,Len(q.stack)-1) IN
    /\ ReturnCheckpointAfterReaction103(f,returned,q.ledger,q.stack,rest,f.caller)
    /\ ~ReturnCheckpointAfterReaction103(f,returned,q.ledger,q.stack,rest,[f.caller EXCEPT !.transactionId=2501])
    /\ ~ReturnCheckpointAfterReaction103(f,returned,q.ledger,ReplaceWindowTop9(q.stack,[WindowTop9(q.stack) EXCEPT !.id=901]),rest,f.caller))
 /\ (q.stage="VFinish" =>
    LET a==IAT11(q) itemInspection==[a EXCEPT !.midResolving=FALSE,!.midDone=TRUE]
        paid==[q.paid EXCEPT !.ability.returned=TRUE,!.phase="Returned"]
        stack==ReplaceWindowTop9(q.stack,CompletePriorityOptionFrame9(WindowTop9(q.stack))) IN
    /\ FinishPaidMidItemInspection95(q.stack,stack,q.paid,paid,VReturn(q),a,itemInspection)
    /\ ~FinishPaidMidItemInspection95(q.stack,stack,q.paid,paid,[VReturn(q) EXCEPT !.finalCheckpointId=1],a,itemInspection)
    /\ ~FinishPaidMidItemInspection95(q.stack,stack,q.paid,paid,[VReturn(q) EXCEPT !.childrenReturned=FALSE],a,itemInspection)
    /\ ~FinishPaidMidItemInspection95(q.stack,stack,q.paid,paid,[VReturn(q) EXCEPT !.transactionId=2501],a,itemInspection))
 /\ (q.stage="InspectionResume" =>
    /\ ~IItemInspectionReturnReadyT11([q EXCEPT !.receipts["ItemInspection"].objects=IF q.moves THEN VObjects ELSE ItemInspectionMovedObjectsT11(q.objects,"SideADiscard")]))
 /\ (q.stage="TraversalResume" =>
    /\ ~IInspectionReturnReadyT11([q EXCEPT !.receipts["Inspection"].objects=IF q.moves THEN VObjects ELSE ItemInspectionMovedObjectsT11(q.objects,"SideADiscard")]))
 /\ (q.stage="ActionResume" =>
    /\ ~ITraversalReturnReadyT11([q EXCEPT !.receipts["SchemaAtom138"].objects=IF q.moves THEN VObjects ELSE ItemInspectionMovedObjectsT11(q.objects,"SideADiscard")]))
VCheckpointEventChecks(q) ==
 /\ DOMAIN q.checkpointEvents=DOMAIN q.frames
 /\ q.registry.cleanupIds={id \in DOMAIN q.frames : "ProcedureCode88eda145024f" \in q.frames[id].done}
 /\ \A id \in DOMAIN q.checkpointEvents :
   LET e==q.checkpointEvents[id] IN
   /\ e.id=id /\ e.caller=q.frames[id].caller /\ e.complete
   /\ (e.tag="InstructionFinished" =>
       /\ e.finishedPlan.phase="Complete" /\ e.finishedPlan.completedSteps=e.finishedPlan.steps
       /\ e.instructionRef=InstructionWindowRef93(e.finishedPlan) /\ e.instructionRef.id=e.caller.instruction
       /\ e.instruction=(IF e.instructionRef.id=710 THEN "AbilityInstruction710" ELSE "AbilityInstruction700"))
   /\ (e.tag="CostPaid" => e.transactionId=q.paid.transaction /\ e.nativePayment=q.native /\ e.useEvent=VUse(q.paid))
VExpectedTrace(q) == IF q.moves THEN SelectSeq(IntegrationOracleTrace11,LAMBDA step : step \notin {"ProcedureCode546db7cc4546","ProcedureCode662478499367"}) ELSE IntegrationOracleTrace11
VExpectedBasis(q) ==
 LET prepared==VPreparedBasis(q.amount,q.availabilityProfile)
     cause==IF q.availabilityProfile="paid-permission" THEN "PermissionWithdraw" ELSE "EntryWithdraw"
     target==KernelTargetRA(q.catalog[1].source,IF cause="PermissionWithdraw" THEN 0 ELSE 1)
 IN IF q.kernelDone THEN KernelBasisRA(q.catalog,prepared,cause,target) ELSE prepared
VCurrentPaidActivity(q) ==
 LET d==q.catalog[1].definition present==PaidPresentSA(q.abilityRegistry) IN
 FlagActivity93(d.syntax,present,AbilityActive9(d.activity,q.objects,present,SourceDefaultActivitySA(VBasis(q),d.syntax.source),
   CommonActivitySA(VBasis(q),q.ledger)),{},ZeroCountsT11)
VRegistrySafety(q) ==
 LET expected==VExpectedBasis(q) IN
 /\ q.availabilityProfile \in VProfiles /\ q.catalog=VCatalog(q.amount)
 /\ q.abilityRegistry=expected.registry /\ q.rulePermissions=expected.rulePermissions /\ q.abilityRevision=expected.revision
 /\ BasisValidSA(q.catalog,VBasis(q)) /\ LedgerDomainSA(q.ledger) /\ VHistoryValid(q)
 /\ q.ledger.activationEpoch[ConditionalKey96(VChildDefinition)]=0 /\ q.ledger.activationSerial=0
 /\ DOMAIN q.basisHistory=DOMAIN q.frames
 /\ Cardinality(DOMAIN q.worldHistory)=q.nextWorld-2000
 /\ \A world \in DOMAIN q.worldHistory :
      LET c==q.worldHistory[world] IN
      /\ c.basis.revision \in 0..1 /\ RegistryValidSA(q.catalog,c.basis.registry) /\ Len(c.views)>0
      /\ \A j \in 1..Len(c.views) :
          /\ c.views[j].id=world /\ c.views[j].definitions=ConditionalDefinitionsSA(c.basis.registry)
          /\ c.views[j].present=ConditionalPresentSA(c.basis.registry) /\ c.views[j].objects=c.basis.objects
          /\ c.views[j].activity.activeRules=c.basis.rulePermissions
 /\ \A id \in DOMAIN q.basisHistory :
      LET f==q.frames[id] capture==q.worldHistory[f.beginSnapshotId] IN
      /\ capture.basis=q.basisHistory[id] /\ Len(capture.views)=2
      /\ f.beginSnapshotId=f.snapshotId /\ capture.views[1].id=capture.views[2].id
      /\ capture.views[1].point="CheckpointBeginning" /\ capture.views[2].point="ProcedureCodee605a78f5d5e"
      /\ (f.recognition.id#0 => f.recognition.beginSnapshot=capture.views[1] /\ f.recognition.processingSnapshot=capture.views[2])
VRecognitionChecks(q) ==
 IF q.costCP=0 THEN TRUE ELSE
 LET f==q.frames[q.costCP] IN
 IF f.recognition.id=0 THEN TRUE ELSE
 LET e==f.recognition.occurrences[1] IN
 /\ e.actualEvent=q.useEvents[1] /\ e.source=q.paid.ability.source /\ e.transaction=q.paid.transaction
 /\ e.abilityInstance=q.paid.id /\ e.turnId=q.flow.turn.id /\ e.traversal.id=q.control.traversal.id
 /\ e.structure=TimingRef9("ItemInspection",IAT11(q).id) /\ e.actor="SideB"
 /\ e.snapshot=q.commitSnapshot /\ q.worldHistory[e.snapshot.id].views= <<e.snapshot>>
 /\ IF 201 \in DOMAIN q.ledger.instances THEN
      LET i==q.ledger.instances[201] IN
      /\ i.checkpointId=q.costCP /\ i.occurrence=e.id /\ i.definitionCopy=q.catalog[2].definition /\ i.member.windowId=q.childWindow
      /\ i.definition=ConditionalKey96(q.catalog[2].definition) /\ i.member.source=q.catalog[2].source
      /\ i.hadSnapshot=f.recognition.previousSnapshot /\ i.activationEpoch=f.recognition.processingSnapshot.activationEpoch[i.definition]
    ELSE q.noChild /\ DOMAIN f.recognized={} /\ q.noChildReceipt.allocation=EmptyT11 /\ q.noChildReceipt.bindings=EmptyT11
VConnectedSafety ==
 LET q==qT11 IN
 /\ VRegistrySafety(q)
 /\ SideBProcedureValid5(q.flow) /\ TraversalFrameValid6(q.control.traversal) /\ PriorityStackValid9(q.stack)
 /\ IReturnGuardChecksT11(q) /\ IActionWindowOrderT11(q) /\ VGuardChecks(q) /\ VCheckpointEventChecks(q) /\ VRecognitionChecks(q)
 /\ q.actionPointWorld.actionPoints["SideB"] \in {IntegrationOracleStartActionPoints11,IntegrationOracleEndActionPoints11}
 /\ q.trace=SubSeq(VExpectedTrace(q),1,Len(q.trace)) /\ IEventNamesT11(q) \cap IntegrationOracleAbsent11={}
 /\ \A id \in DOMAIN q.control.itemInspections : ItemInspectionProcedureValid7(q.control.itemInspections[id],q.objects)
 /\ \A id \in DOMAIN q.control.siteInspections : InspectionProcedureValid7(q.control.siteInspections[id])
 /\ (q.action.status="Nested" => q.waitTraversal.handle=q.action.nested /\ q.waitTraversal.id=q.control.traversal.id /\ q.stack[1].busy=IActionOptionT11 /\ q.stack[1].open)
 /\ ("ItemInspection" \in q.consumed => IAT11(q).returned /\ (IF VInitialPaid(q.availabilityProfile) THEN q.declined ELSE q.paidReturned))
 /\ ("Inspection" \in q.consumed => IBT11(q).returned) /\ ("SchemaAtom138" \in q.consumed => q.control.returned)
 /\ (q.done => q.trace=VExpectedTrace(q) /\ (\A name \in IntegrationOracleEvents11 : IEventCountT11(q,name)=1) /\
      q.returnOrder=IntegrationOracleReturnOrder11 /\ q.consumed={"ItemInspection","Inspection","SchemaAtom138"} /\ q.action.status="Complete" /\
      q.actionPointWorld.actionPoints["SideB"]=1 /\ q.actionPointWorld.spent["SideB"]=1 /\ Len(q.stack)=1 /\
      WindowTop9(q.stack).kind="NeutralValue00001" /\ WindowTop9(q.stack).stage="Ready")
VUnavailableSafety(q) ==
 /\ (VUnavailable(q.availabilityProfile) => ~q.moves /\ DOMAIN q.objects={1})
 /\ (VInitialPaid(q.availabilityProfile) =>
      /\ q.paid=EmptyT11 /\ q.native=EmptyT11 /\ q.uses=EmptyT11 /\ q.turnUses=EmptyT11 /\ q.useIndex=EmptyT11 /\ q.procedures=EmptyT11
      /\ q.child=EmptyT11 /\ ~q.childReturned /\ q.ledger.instances=EmptyT11 /\ q.wallet=ItemInspectionWalletInitialT11 /\ q.costCP=0
      /\ (q.declined => q.declineReceipt.stage="Ready" /\ q.declineReceipt.reservationRejected /\ IAT11(q).midDone /\ ~IAT11(q).midUsed)
      /\ (q.done => q.declined /\ ~q.paidReturned /\ DOMAIN q.frames={1} /\ Len(q.checkpointHistory)=1 /\ q.frames[1].returned))
 /\ (VInitialConditional(q.availabilityProfile) =>
      /\ q.child=EmptyT11 /\ ~q.childReturned /\ q.ledger.instances=EmptyT11 /\ ~q.declined
      /\ (q.noChild => q.noChildReceipt.allocation=EmptyT11 /\ q.noChildReceipt.bindings=EmptyT11 /\ q.noChildReceipt.recognized=EmptyT11 /\
            ~q.noChildReceipt.actualConditionalActive)
      /\ (q.noReactionCostReturned => q.noChild /\ q.noReactionCostReceipt.frame.returned /\ q.noReactionCostReceipt.recognized=EmptyT11 /\
            q.noReactionCostReceipt.caller=PaidCheckpointCaller96(q.procedures[250]))
      /\ (q.done => q.noChild /\ q.noReactionCostReturned /\ q.paidReturned /\ DOMAIN q.frames=1..3 /\
            Len(q.checkpointHistory)=3 /\ q.work= <<"MidEffect","MidTail">> /\ q.useIndex=[id \in {1} |-> 1] /\ Len(q.useEvents)=1))
VKernelSafety(q) ==
 /\ (q.kernelDone =>
      LET r==q.kernelReceipt key==ConditionalKey96(q.catalog[2].definition) IN
      /\ VPaidLoss(q.availabilityProfile) /\ q.abilityRevision=1 /\ ~VCurrentPaidActivity(q)
      /\ r.instruction.id=710 /\ r.instruction.abilityInstance=201 /\ r.instruction.index=1
      /\ r.beforeLedger.instances[201].status="Resolving" /\ r.intermediateLedger.instances[201].status="Resolving" /\ r.finalLedger.instances[201].status="Complete"
      /\ r.beforeLedger.activationEpoch[key]=0 /\ r.intermediateLedger.activationEpoch[key]=0 /\ r.finalLedger.activationEpoch[key]=0
      /\ r.paidDefinition=q.paid.definition /\ q.paid.definition=q.catalog[1].definition /\ r.paidSource=q.paid.ability.source
      /\ r.paidCaller=q.paid.windowId /\ q.paid.ability.detached /\ r.actualPayment=q.native /\ r.committedUse=q.useEvents[1]
      /\ q.worldHistory[r.beforeSnapshot.id].views= <<r.beforeSnapshot>>
      /\ q.worldHistory[r.intermediateSnapshot.id].views= <<r.intermediateSnapshot>>
      /\ q.worldHistory[r.afterSnapshot.id].views= <<r.afterSnapshot>>
      /\ (1 \in DOMAIN q.abilityRegistry)=(q.availabilityProfile="paid-permission"))
 /\ (q.done /\ VPaidLoss(q.availabilityProfile) => q.kernelDone)
VPaidSafety ==
 LET q==qT11 IN
 /\ VSourceIndexChecks(q) /\ VUnavailableSafety(q) /\ VKernelSafety(q)
 /\ q.amount \in {0,1} /\ q.moves \in BOOLEAN /\ DOMAIN q.objects \in {{1},{2}}
 /\ (q.paid#EmptyT11 /\ q.paid.costPaid =>
      /\ IAT11(q).midUsed /\ q.paid.ability.detached /\ q.paid.turnId=q.flow.turn.id
      /\ q.uses=ItemInspectionPaidUsesT11(q.paid) /\ q.turnUses=VTurnUses(q.paid) /\ q.useEvents= <<VUse(q.paid)>>
      /\ Cardinality(DOMAIN q.wallet.obj)=3-q.amount)
 /\ (q.costCP>0 => VNativeCommitted(q))
 /\ (Len(q.stack)=3 => q.paid.phase="CostCheckpoint" /\ q.stack[2].kind="MidItemInspection" /\ q.stack[2].stage="Resolving" /\ IAT11(q).midResolving)
 /\ (q.childReturned => q.child.phase="Returned" /\ q.child.ability.returned /\ q.ledger.instances[201].status="Complete" /\ q.work# <<>>)
 /\ (q.announcement#EmptyT11 =>
      /\ VChildObligation(q) /\ q.announcement.child=q.child /\ q.announcement.objects=q.objects
      /\ q.announcement.targets=(IF q.moves THEN {} ELSE {1}) /\ 2 \notin q.announcement.targets
      /\ q.announcement.instruction.id=q.plan.id /\ q.announcement.turn=q.flow.turn.id /\ CheckpointDrained103(q.frames[q.costCP],q.ledger,q.stack))
 /\ (DOMAIN q.objects={2} => q.moves /\ IAT11(q).complete /\ IAT11(q).completionReason="Moved")
 /\ (q.paidReturned =>
      /\ q.work=(IF VInitialConditional(q.availabilityProfile) THEN <<"MidEffect","MidTail">> ELSE <<"CostReaction","MidEffect","MidTail">>)
      /\ q.paid.phase="Returned" /\ q.plan.phase="Complete" /\ q.frames[q.paid.checkpoint].returned
      /\ q.frames[q.paid.checkpoint].done=CheckpointStageSet103 /\ IAT11(q).midDone /\ ~IAT11(q).midResolving)
 /\ \A row \in {q.checkpointHistory[i] : i \in 1..Len(q.checkpointHistory)} : row.done=CheckpointStageSet103
 /\ (q.done => \A id \in DOMAIN q.frames : q.frames[id].returned /\ q.frames[id].done=CheckpointStageSet103)
 /\ (q.done /\ ~VUnavailable(q.availabilityProfile) => q.paidReturned /\ q.childReturned /\ DOMAIN q.frames=1..7 /\ Len(q.checkpointHistory)=7)
VOutcome(q) == IF VInitialPaid(q.availabilityProfile) THEN "Decline" ELSE IF VInitialConditional(q.availabilityProfile) THEN "NoChild" ELSE "Paid"
VObservation(q) ==
 [tag |-> "Unit5Stage",family |-> "availability",NeutralValue00013 |-> q.availabilityProfile,stage |-> q.stage,amount |-> q.amount,moves |-> q.moves,
  cpRole |-> q.cpRole,cpPoint |-> IF q.currentCP \in DOMAIN q.frames THEN q.frames[q.currentCP].point ELSE "NoValue",
  paidPhase |-> IF q.paid=EmptyT11 THEN "NoValue" ELSE q.paid.phase,childPhase |-> IF q.child=EmptyT11 THEN "NoValue" ELSE q.child.phase,
  childStatus |-> IF 201 \in DOMAIN q.ledger.instances THEN q.ledger.instances[201].status ELSE "Absent",
  abilityRevision |-> q.abilityRevision,conditionalEpoch |-> q.ledger.activationEpoch[ConditionalKey96(VChildDefinition)],
  useCount |-> Cardinality(DOMAIN q.uses),walletCount |-> Cardinality(DOMAIN q.wallet.obj),worldHistoryCount |-> Cardinality(DOMAIN q.worldHistory),
  entries |-> DOMAIN q.abilityRegistry,permissions |-> q.rulePermissions,paidSource |-> q.catalog[1].source,conditionalSource |-> q.catalog[2].source,
  paidReturned |-> q.paidReturned,childReturned |-> q.childReturned,noChild |-> q.noChild,declined |-> q.declined,kernelDone |-> q.kernelDone,
  outcome |-> VOutcome(q),work |-> q.work,walletDue |-> q.wallet.checkpointDue,
  windowId |-> IF Len(q.stack)=0 THEN 0 ELSE WindowTop9(q.stack).id,
  windowKind |-> IF Len(q.stack)=0 THEN "Absent" ELSE WindowTop9(q.stack).kind,
  windowStage |-> IF Len(q.stack)=0 THEN "Absent" ELSE WindowTop9(q.stack).stage,complete |-> q.done]
VCompletion(q) ==
 [tag |-> "Unit5Completion",family |-> "availability",NeutralValue00013 |-> q.availabilityProfile,amount |-> q.amount,moves |-> q.moves,outcome |-> VOutcome(q),
  uses |-> q.uses,turnUses |-> q.turnUses,useIndex |-> q.useIndex,procedures |-> q.procedures,native |-> q.native,useEvents |-> q.useEvents,
  work |-> q.work,targets |-> IF q.announcement=EmptyT11 THEN {} ELSE q.announcement.targets,announcement |-> q.announcement,
  objects |-> q.objects,instances |-> q.ledger.instances,child |-> q.child,paid |-> q.paid,commitSnapshot |-> q.commitSnapshot,
  frames |-> q.frames,checkpointHistory |-> q.checkpointHistory,checkpointEvents |-> q.checkpointEvents,basisHistory |-> q.basisHistory,
  worldHistory |-> q.worldHistory,kernelDone |-> q.kernelDone,kernelReceipt |-> q.kernelReceipt,
  noChild |-> q.noChild,noChildReceipt |-> q.noChildReceipt,noReactionCostReturned |-> q.noReactionCostReturned,noReactionCostReceipt |-> q.noReactionCostReceipt,
  declined |-> q.declined,declineReceipt |-> q.declineReceipt,paidReturned |-> q.paidReturned,childReturned |-> q.childReturned,
  availabilityBasis |-> MinimalCaptureSA(VBasis(q)),returnOrder |-> q.returnOrder,consumed |-> q.consumed,trace |-> q.trace,
  action |-> q.action.status,actionPoints |-> q.actionPointWorld.actionPoints["SideB"],lastSnapshot |-> q.ledger.lastSnapshot,
  finalWindow |-> WindowTop9(q.stack)]
=============================================================================