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

RegistryCompositionMC

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 126 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.

RAdmitPaid · operator

reference-profile · input revision 2 · CC0 1.0

RAdmitPaid(q,d,view) ==
 IF ~BasisValidSA(q.catalog,RBasis(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,RBasis(q),q.ledger,q.uses,q.turnUses,q.useIndex,q.procedures,
 PContext(q,d),1,view,MinimalCaptureSA(RBasis(q)))

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: AdmitPaidContextSA, BasisValidSA, MinimalCaptureSA, PContext, RBasis

RAdmitSnapshot · operator

reference-profile · input revision 2 · CC0 1.0

RAdmitSnapshot(q,objects,ledger,view) ==
 AdmitConditionalSnapshotSA(q.catalog,RBasisObjects(q,objects),ledger,q.uses,q.turnUses,q.useIndex,q.procedures,
  RSnapshotTemplate(q,view.id,view.point,view.checkpointId),view,MinimalCaptureSA(RBasisObjects(q,objects)))

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: AdmitConditionalSnapshotSA, MinimalCaptureSA, RBasisObjects, RSnapshotTemplate

RBasis · operator

reference-profile · input revision 2 · CC0 1.0

RBasis(q) == RBasisObjects(q,q.objects)

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: RBasisObjects

RBasisObjects · operator

reference-profile · input revision 2 · CC0 1.0

RBasisObjects(q,objects) == BasisSA(q.abilityRevision,q.abilityRegistry,objects,q.rulePermissions)

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: BasisSA

RCPData · operator

reference-profile · input revision 2 · CC0 1.0

RCPData(q,f) ==
 LET b==RCurrentSnapshot(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 RCPOccurrences(q) ELSE EmptyT11,caller |-> f.caller]

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: RCPOccurrences, RCurrentSnapshot, EmptyT11

RCPNext · operator

reference-profile · input revision 2 · CC0 1.0

RCPNext(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"]

Exact module download · Source bundle and reproduction instructions

RCPOccurrences · operator

reference-profile · input revision 2 · CC0 1.0

RCPOccurrences(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.ledger.lastSnapshot,scopeKind |-> "Global",scopeDefinition |-> ConditionalKey96(RChildDefinition),
  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]]

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: ConditionalKey96, TimingRef9, IAT11, RChildDefinition

RCPWork · operator

reference-profile · input revision 2 · CC0 1.0

RCPWork ==
 LET q==qT11 f==RFrame(q) next==RCPNext(f) world==RWorld(q,f) IN
 CASE f.point="ProcedureCodee605a78f5d5e" ->
   LET cp==RCPData(q,f) key==[definition |-> ConditionalKey96(RChildDefinition),occurrence |-> 1]
       allocation==[k \in IF q.cpRole="Cost" THEN {key} ELSE {} |-> 201]
       bindings==[k \in DOMAIN allocation |-> [kind |-> "Reaction",checkpointId |-> cp.id,windowId |-> q.childWindow,group |-> 4]]
       conditions==[k \in DOMAIN RDefinitions(q) |-> [id \in DOMAIN cp.occurrences |->
         [tag |-> "ConditionalTriggerStipulations",ability |-> 200,source |-> RChildDefinition.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 |-> RDefinitions(q),lexemes |-> RLexemes(q),conditions |-> conditions,
         allocation |-> allocation,bindings |-> bindings,departures |-> EmptyT11,holds |-> EmptyT11,
         usedWindows |-> q.usedWindows,cardFacts |-> CardFacts10]
   IN /\ RAdmitSnapshot(q,q.objects,q.ledger,cp.beginSnapshot)
      /\ RAdmitSnapshot(q,q.objects,q.ledger,cp.processingSnapshot)
      /\ x.definitions=ConditionalDefinitionsSA(q.abilityRegistry)
      /\ RecognizeCheckpoint103(f,after,q.ledger,ledger,q.stack,q.stack,x)
      /\ qT11'=[RSetFrame(q,after) EXCEPT !.ledger=ledger]
 [] 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 /\ RWorldBound(q,f,world)
      /\ RAdmitSnapshot(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'=[RSetFrame(q,next) EXCEPT !.registry=registry]
 [] f.point="ProcedureCodeb681cc249a04" ->
   /\ CheckpointVictory103(f,next,q.objects,[id \in DOMAIN q.objects |-> 0],f.snapshotId)
   /\ qT11'=RSetFrame(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,RPrinted,ROwners,{},f.snapshotId)
   /\ qT11'=RSetFrame(q,next)
 [] f.point="ProcedureCodea488e1ba6ca3" ->
   /\ CheckpointIllegalRetire103(f,next,q.objects,q.objects,{},RLegal,[id \in DOMAIN q.objects |-> "SideA"],q.flow.turn.owner,
        [s \in CentralTargetSites4 |-> [kind |-> "SchemaAtom033"]],[applies |-> FALSE],"NoValue",{},EmptyT11,DOMAIN q.objects,RPrinted,ROwners,{},f.snapshotId)
   /\ qT11'=RSetFrame(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,RPrinted,ROwners,{},f.snapshotId)
   /\ qT11'=RSetFrame(q,next)
 [] f.point="ProcedureCode2d73b20aa788" ->
   /\ CheckpointAuxiliarySiteCleanup103(f,next,[s \in CentralTargetSites4 |-> [kind |-> "SchemaAtom033"]],
        [s \in CentralTargetSites4 |-> [kind |-> "SchemaAtom033"]],q.objects,EmptyT11,f.snapshotId)
   /\ qT11'=RSetFrame(q,next)
 [] f.point="ProcedureCode2d6279f9d639" ->
   /\ CheckpointPositionCleanup103(f,next,q.layout,q.layout,q.control.traversal.position,EmptyT11,f.snapshotId)
   /\ qT11'=RSetFrame(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'=RSetFrame(q,next)
 [] f.point="ProcedureCodeda83a77a1f12" ->
   /\ CheckpointRestoreDiscard103(f,next,q.objects,q.objects,EmptyT11,EmptyT11,RPrinted,f.snapshotId)
   /\ qT11'=RSetFrame(q,next)
 [] f.point="ProcedureCode0811ebc5f40e" ->
   /\ CheckpointReturnDiscardCounters103(f,next,q.objects,q.objects,f.snapshotId)
   /\ qT11'=RSetFrame(q,next)
 [] f.point="ProcedureCodeb74d673a0fc6" ->
   IF DOMAIN f.recognized={} THEN
     LET returned==[f EXCEPT !.phase="Returned",!.returned=TRUE] IN
     /\ RWorldBound(q,f,world)
     /\ ReturnCheckpointWithoutReaction103(f,returned,q.ledger,world,PersistentCheckpointCompletion912(q.ledger,f.recognition,world),f.caller)
     /\ qT11'=[RSetFrame(q,returned) EXCEPT !.stage=q.cpResume,
         !.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==RJoin(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 /\ RWorldBound(q,f,world)
        /\ OpenCheckpointReaction103(f,after,q.ledger,q.stack,Append(q.stack,window),site,opening,q.usedWindows)
        /\ qT11'=[RSetFrame(q,after) EXCEPT !.stack=Append(@,window),!.usedWindows=@ \cup {q.childWindow},!.stage="RReceive"]
 [] OTHER -> FALSE

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: ConditionalKey96, LingeringCheckpointFrame910, NewPriorityWindow9, NoTimingRef9, PersistentCheckpointCompletion912, SnapshotWithConditionalRegistry96, WindowTop9, ConditionalDefinitionsSA, CheckpointAuxiliarySiteCleanup103, CheckpointCleanupEffects103, CheckpointHostedCleanup103, CheckpointIllegalRetire103, CheckpointMemberMap103, CheckpointPositionCleanup103, CheckpointRestoreDiscard103, CheckpointReturnDiscardCounters103, CheckpointRootAdmissions103, CheckpointUniqueRetire103, CheckpointVictory103, OpenCheckpointReaction103, RecognizeCheckpoint103, ReturnCheckpointWithoutReaction103, ProtocolP!CPAfter9p, IBT11, IOpeningT11, CentralTargetSites4, RAdmitSnapshot, RCPData, RCPNext, RChildDefinition, RDefinitions, RFrame, RJoin, RLegal, RLexemes, ROwners, RPrinted, RSetFrame, RWorld, RWorldBound, EmptyT11, qT11, CardFacts10

RCatalog · operator

reference-profile · input revision 2 · CC0 1.0

RCatalog(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 |-> RChildDefinition.syntax.id,source |-> RChildDefinition.syntax.source,definition |-> RChildDefinition]]

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: ItemInspectionPaidDefinitionT11, RChildDefinition

RCheckpointEventChecks · operator

reference-profile · input revision 2 · CC0 1.0

RCheckpointEventChecks(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=RUse(q.paid))

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: InstructionWindowRef93, RUse

RChildDefinition · operator

reference-profile · input revision 2 · CC0 1.0

RChildDefinition == PChildDefinition

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: PChildDefinition

RChildTurnUses · operator

reference-profile · input revision 2 · CC0 1.0

RChildTurnUses(q) == FamilyTurnUsesSA(q.catalog,q.useIndex,q.turnUses,"Conditional",RChildDefinition.syntax.source)

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: FamilyTurnUsesSA, RChildDefinition

RConnectedSafety · operator

reference-profile · input revision 2 · CC0 1.0

RConnectedSafety ==
 LET q==qT11 IN
 /\ RRegistrySafety(q)
 /\ SideBProcedureValid5(q.flow) /\ TraversalFrameValid6(q.control.traversal) /\ PriorityStackValid9(q.stack)
 /\ IReturnGuardChecksT11(q) /\ IActionWindowOrderT11(q) /\ RGuardChecks(q) /\ RCheckpointEventChecks(q) /\ RRecognitionChecks(q)
 /\ q.actionPointWorld.actionPoints["SideB"] \in {IntegrationOracleStartActionPoints11,IntegrationOracleEndActionPoints11}
 /\ q.trace=SubSeq(RExpectedTrace(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 /\ q.paidReturned)
 /\ ("Inspection" \in q.consumed => IBT11(q).returned)
 /\ ("SchemaAtom138" \in q.consumed => q.control.returned)
 /\ (q.done => q.trace=RExpectedTrace(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")

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: PriorityStackValid9, WindowTop9, IntegrationOracleAbsent11, IntegrationOracleEndActionPoints11, IntegrationOracleEvents11, IntegrationOracleReturnOrder11, IntegrationOracleStartActionPoints11, IAT11, IActionOptionT11, IActionWindowOrderT11, IBT11, IEventCountT11, IEventNamesT11, IReturnGuardChecksT11, InspectionProcedureValid7, ItemInspectionProcedureValid7, RCheckpointEventChecks, RExpectedTrace, RGuardChecks, RRecognitionChecks, RRegistrySafety, qT11, TraversalFrameValid6, SideBProcedureValid5

RContext · operator

reference-profile · input revision 2 · CC0 1.0

RContext(q,d) == PaidContextFromRegistrySA(q.catalog,RBasis(q),q.ledger,q.useIndex,q.turnUses,PContext(q,d),1)

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: PaidContextFromRegistrySA, PContext, RBasis

RCurrentSnapshot · operator

reference-profile · input revision 2 · CC0 1.0

RCurrentSnapshot(q,objects,ledger,id,point,checkpoint) ==
 ConditionalSnapshotFromRegistrySA(q.catalog,RBasisObjects(q,objects),ledger,RSnapshotTemplate(q,id,point,checkpoint))

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: ConditionalSnapshotFromRegistrySA, RBasisObjects, RSnapshotTemplate

RDefinitions · operator

reference-profile · input revision 2 · CC0 1.0

RDefinitions(q) == ConditionalDefinitionsSA(q.abilityRegistry)

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: ConditionalDefinitionsSA

REventuallyReturns · operator

reference-profile · input revision 2 · CC0 1.0

REventuallyReturns == <>qT11.done

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: qT11

RExpectedTrace · operator

reference-profile · input revision 2 · CC0 1.0

RExpectedTrace(q) == IF q.moves THEN SelectSeq(IntegrationOracleTrace11,LAMBDA step : step \notin {"ProcedureCode546db7cc4546","ProcedureCode662478499367"}) ELSE IntegrationOracleTrace11

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: IntegrationOracleTrace11

RFrame · operator

reference-profile · input revision 2 · CC0 1.0

RFrame(q) == q.frames[q.currentCP]

Exact module download · Source bundle and reproduction instructions

RGuardChecks · operator

reference-profile · input revision 2 · CC0 1.0

RGuardChecks(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="RCostResume" =>
    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="RCostReturn" =>
    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="RFinish" =>
    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,RReturn(q),a,itemInspection)
    /\ ~FinishPaidMidItemInspection95(q.stack,stack,q.paid,paid,[RReturn(q) EXCEPT !.finalCheckpointId=1],a,itemInspection)
    /\ ~FinishPaidMidItemInspection95(q.stack,stack,q.paid,paid,[RReturn(q) EXCEPT !.childrenReturned=FALSE],a,itemInspection)
    /\ ~FinishPaidMidItemInspection95(q.stack,stack,q.paid,paid,[RReturn(q) EXCEPT !.transactionId=2501],a,itemInspection))
 /\ (q.stage="InspectionResume" =>
    /\ ~IItemInspectionReturnReadyT11([q EXCEPT !.receipts["ItemInspection"].objects=IF q.moves THEN RObjects ELSE ItemInspectionMovedObjectsT11(q.objects,"SideADiscard")]))
 /\ (q.stage="TraversalResume" =>
    /\ ~IInspectionReturnReadyT11([q EXCEPT !.receipts["Inspection"].objects=IF q.moves THEN RObjects ELSE ItemInspectionMovedObjectsT11(q.objects,"SideADiscard")]))
 /\ (q.stage="ActionResume" =>
    /\ ~ITraversalReturnReadyT11([q EXCEPT !.receipts["SchemaAtom138"].objects=IF q.moves THEN RObjects ELSE ItemInspectionMovedObjectsT11(q.objects,"SideADiscard")]))

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: CompletePriorityOptionFrame9, ConditionalCheckpointDrained96, FinishPaidMidItemInspection95, ReplaceWindowTop9, WindowTop9, ResumePaidAfterCheckpoint103, ReturnCheckpointAfterReaction103, IAT11, IInspectionReturnReadyT11, IItemInspectionReturnReadyT11, ITraversalReturnReadyT11, ItemInspectionMovedObjectsT11, ItemInspectionPaidCheckpointT11, RObjects, RReturn, EmptyT11

RHistoryValid · operator

reference-profile · input revision 2 · CC0 1.0

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

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: UseProvenanceValidSA

RInit · operator

reference-profile · input revision 2 · CC0 1.0

RInit == guideCaseT11=0 /\ \E amount \in PaidAmounts,moves \in PaidMoves : qT11=RInitial(amount,moves)

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: PaidAmounts, PaidMoves, RInitial, guideCaseT11, qT11

RInitial · operator

reference-profile · input revision 2 · CC0 1.0

RInitial(amount,moves) ==
 LET catalog==RCatalog(amount) basis==BasisSA(0,catalog,PObjects,RPermissions)
     seed==NewConditionalLedger96(PInitialSnapshot)
     snapshot==ConditionalSnapshotFromRegistrySA(catalog,basis,seed,PInitialSnapshot)
 IN RJoin(PInitial(amount,moves),[catalog |-> catalog,abilityRegistry |-> catalog,abilityRevision |-> 0,
   rulePermissions |-> RPermissions,useIndex |-> EmptyT11,procedures |-> EmptyT11,basisHistory |-> EmptyT11,
   ledger |-> NewConditionalLedger96(snapshot)])

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: NewConditionalLedger96, BasisSA, ConditionalSnapshotFromRegistrySA, PInitial, PInitialSnapshot, PObjects, RCatalog, RJoin, RPermissions, EmptyT11

RInside · operator

reference-profile · input revision 2 · CC0 1.0

RInside(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 {})

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: TimingRef9, IAT11, IBT11, StillItemInspectioning7

RItemInspectionView · operator

reference-profile · input revision 2 · CC0 1.0

RItemInspectionView(q) == [itemInspection |-> IAT11(q),objects |-> q.objects,NeutralValue00013 |-> IF q.amount=0 THEN "FacilityObserve0" ELSE "FacilityObserve1",turnUses |-> q.turnUses]

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: IAT11

RJoin · operator

reference-profile · input revision 2 · CC0 1.0

RJoin(base,extra) == PJoin(base,extra)

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: PJoin

RLegal · operator

reference-profile · input revision 2 · CC0 1.0

RLegal(selected) == selected={}

Exact module download · Source bundle and reproduction instructions

RLegality · operator

reference-profile · input revision 2 · CC0 1.0

RLegality(w,option,transaction) == [LegalityT11(w,option) EXCEPT !.transactionId=transaction]

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: LegalityT11

RLex · operator

reference-profile · input revision 2 · CC0 1.0

RLex(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]]

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: EmptyT11

RLexemes · operator

reference-profile · input revision 2 · CC0 1.0

RLexemes(q) == [k \in DOMAIN RDefinitions(q) |-> RLex(RDefinitions(q)[k])]

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: RDefinitions, RLex

RMid · operator

reference-profile · input revision 2 · CC0 1.0

RMid(q) == ItemInspectionTemporalMidT11(RItemInspectionView(q))

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: ItemInspectionTemporalMidT11, RItemInspectionView

RMidWindow · operator

reference-profile · input revision 2 · CC0 1.0

RMidWindow ==
 LET q==qT11 w==WindowTop9(q.stack) a==IAT11(q) IN
 CASE w.stage="NeedCheckpoint" -> ROpenCP("SchemaAtom126",ConditionalPriorityCaller96(w),"RMidReady","MidPriority")
 [] w.stage="Ready" ->
   LET d==RPaidDefinition(q) option==RPaidOption(q,w,d) busy==StartPriorityOptionFrame9(w,option,2500)
       p==OpenPaidProcedure95(250,d,option,w,2500,"Rule")
   IN /\ RAdmitPaid(q,d,RContext(q,d))
      /\ ReservePaidMidItemInspection95(q.stack,ReplaceWindowTop9(q.stack,busy),p,250,d,RContext(q,d),option,RLegality(w,option,2500),{},a,a,RMid(q),{RMid(q)},FALSE,FALSE)
      /\ qT11'=[q EXCEPT !.stack=ReplaceWindowTop9(@,busy),!.paid=p,!.stage="RPay"]
 [] 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

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: ConditionalPriorityCaller96, OpenPaidProcedure95, PopClosedPriorityWindow9, ReplaceWindowTop9, ReservePaidMidItemInspection95, StartPriorityOptionFrame9, WindowTop9, IAT11, IRecordT11, RAdmitPaid, RContext, RLegality, RMid, ROpenCP, RPaidDefinition, RPaidOption, qT11

RNativeAtPayment · operator

reference-profile · input revision 2 · CC0 1.0

RNativeAtPayment(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=RPaidDefinition(q).triggerCost
 /\ ItemInspectionCostOwnerT11!SpendResourceUnitsOK(q.wallet,"SideB",selected,q.amount,{})
 /\ after=ItemInspectionWalletSpentT11(q.wallet,selected)

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: WindowTop9, IAT11, ItemInspectionCostOwnerT11!SpendResourceUnitsOK, ItemInspectionWalletSpentT11, RPaidDefinition

RNativeCommitted · operator

reference-profile · input revision 2 · CC0 1.0

RNativeCommitted(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=RTurnUses(q.paid) /\ q.useEvents= <<RUse(q.paid)>>

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: ItemInspectionCostOwnerT11!SpendResourceUnitsOK, ItemInspectionPaidUsesT11, ItemInspectionWalletSpentT11, RTurnUses, RUse

RObjects · operator

reference-profile · input revision 2 · CC0 1.0

RObjects == PObjects

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: PObjects

ROpenCP · operator

reference-profile · input revision 2 · CC0 1.0

ROpenCP(kind,caller,resume,role) ==
 LET q==qT11 id==q.ledger.lastCheckpoint+1 snapshot==100+id
     event==RJoin([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 |-> RInside(q)]
     frame==NewCheckpoint103(id,caller,snapshot,RInside(q))
     frames==RJoin(q.frames,[k \in {id} |-> frame])
 IN /\ BeginCheckpointSite103(q.sites,q.sites \cup {CheckpointSiteKey103(site)},q.frames,frames,frame,id,site,event,RInside(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'=[q EXCEPT !.frames=frames,!.sites=@ \cup {CheckpointSiteKey103(site)},!.currentCP=id,
         !.checkpointEvents=RJoin(@,[k \in {id} |-> event]),!.basisHistory=RJoin(@,[k \in {id} |-> MinimalCaptureSA(RBasis(q))]),!.costCP=IF role="Cost" THEN id ELSE @,!.cpResume=resume,!.cpRole=role,!.stage="RCP"]

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: InstructionWindowRef93, WindowTop9, MinimalCaptureSA, BeginCheckpointSite103, CheckpointSiteKey103, NewCheckpoint103, RBasis, RInside, RJoin, qT11

ROwners · operator

reference-profile · input revision 2 · CC0 1.0

ROwners == POwners

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: POwners

RPaidDefinition · operator

reference-profile · input revision 2 · CC0 1.0

RPaidDefinition(q) == q.catalog[1].definition

Exact module download · Source bundle and reproduction instructions

RPaidOption · operator

reference-profile · input revision 2 · CC0 1.0

RPaidOption(q,w,d) == ItemInspectionPaidOptionT11(RItemInspectionView(q),w,d)

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: ItemInspectionPaidOptionT11, RItemInspectionView

RPaidSafety · operator

reference-profile · input revision 2 · CC0 1.0

RPaidSafety ==
 LET q==qT11 IN
 /\ RSourceIndexChecks(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=RTurnUses(q.paid) /\ q.useEvents= <<RUse(q.paid)>>
     /\ Cardinality(DOMAIN q.wallet.obj)=3-q.amount)
 /\ (q.costCP>0 => RNativeCommitted(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 =>
     /\ q.childReturned /\ 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= <<"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 => q.paidReturned /\ q.childReturned /\ DOMAIN q.frames=1..7 /\ Len(q.checkpointHistory)=7 /\
       \A id \in DOMAIN q.frames : q.frames[id].returned /\ q.frames[id].done=CheckpointStageSet103)

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: CheckpointDrained103, CheckpointStageSet103, IAT11, ItemInspectionPaidUsesT11, RNativeCommitted, RSourceIndexChecks, RTurnUses, RUse, EmptyT11, qT11

RPayment · operator

reference-profile · input revision 2 · CC0 1.0

RPayment(q) == [tag |-> "PriorityOptionPayment",windowId |-> q.paid.windowId,option |-> q.paid.option,transactionId |-> q.paid.transaction,
 allTriggerCostsPaid |-> RNativeCommitted(q),costCheckpointAndReactionsDrained |-> CheckpointDrained103(q.frames[q.costCP],q.ledger,q.stack)]

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: CheckpointDrained103, RNativeCommitted

RPermissions · operator

reference-profile · input revision 2 · CC0 1.0

RPermissions == {"AuditPaidObserve","ProtocolReactionControl"}

Exact module download · Source bundle and reproduction instructions

RPrinted · operator

reference-profile · input revision 2 · CC0 1.0

RPrinted == PPrinted

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: PPrinted

RProtocolWork · operator

reference-profile · input revision 2 · CC0 1.0

RProtocolWork ==
 LET q==qT11 IN
 CASE q.stage="RMidReady" ->
   LET w==WindowTop9(q.stack) ready==[w EXCEPT !.stage="Ready",!.checkpoint=q.currentCP] IN
   /\ ReceivePriorityAfterCheckpoint103(RFrame(q),q.ledger,q.stack,ReplaceWindowTop9(q.stack,ready),RReadyCP(q))
   /\ qT11'=[q EXCEPT !.stack=ReplaceWindowTop9(@,ready),!.stage="Window"]
 [] q.stage="RPay" ->
   LET p==q.paid selected==IF q.amount=0 THEN {} ELSE {100} after==ItemInspectionWalletSpentT11(q.wallet,selected)
       paid==ItemInspectionPaidCommittedFrameT11(p) 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 |-> RNativeAtPayment(q,selected,after),
        additionalCostsPaid |-> TRUE,restrictionsBefore |-> TRUE,restrictionsAfter |-> TRUE,simultaneousProcedureComplete |-> TRUE,
        sourceAfter |-> 0,sourceUninstalled |-> FALSE,sourceForfeited |-> FALSE,paidOperations |-> {},publicEvents |-> {}]
   IN /\ PayPaidMidItemInspection95(q.stack,p,paid,q.objects,q.objects,EmptyT11,EmptyT11,EmptyT11,DOMAIN q.objects,payment,
        q.uses,ItemInspectionPaidUsesT11(p),q.turnUses,RTurnUses(p),1,{RUse(p)},a,used,RMid(q),{RMid(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(q,used) EXCEPT !.wallet=after,!.paid=paid,!.uses=ItemInspectionPaidUsesT11(p),!.turnUses=RTurnUses(p),
        !.useEvents= <<RUse(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="RCostOpen"]
      /\ ItemInspectionCostOwnerT11!DoSpendResourceUnits(ItemInspectionCostCommandT11(selected,q.amount))
 [] q.stage="RCostOpen" -> ROpenCP("Cost",PaidCheckpointCaller96(q.paid),"RCostResume","Cost")
 [] q.stage="RCP" -> RCPWork
 [] q.stage="RReceive" -> ROpenCP("SchemaAtom126",ConditionalPriorityCaller96(WindowTop9(q.stack)),"RChildReady","ChildPriority")
 [] q.stage="RChildReady" ->
   LET w==WindowTop9(q.stack) ready==[w EXCEPT !.stage="Ready",!.checkpoint=q.currentCP] IN
   /\ ReceivePriorityAfterCheckpoint103(RFrame(q),q.ledger,q.stack,ReplaceWindowTop9(q.stack,ready),RReadyCP(q))
   /\ qT11'=[q EXCEPT !.stack=ReplaceWindowTop9(@,ready),!.stage=IF q.childReturned THEN "RPass" ELSE "RSelect"]
 [] q.stage="RSelect" ->
   LET w==WindowTop9(q.stack) d==RChildDefinition 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"]
   IN /\ RAdmitSnapshot(q,q.objects,q.ledger,RCurrentSnapshot(q,q.objects,q.ledger,q.ledger.lastSnapshot.id,"Selection",q.ledger.lastCheckpoint))
      /\ BeginConditionalResolution96(q.ledger,ledger,q.stack,ReplaceWindowTop9(q.stack,busy),p,imminent,d,
        RCurrentSnapshot(q,q.objects,q.ledger,q.ledger.lastSnapshot.id,"Selection",q.ledger.lastCheckpoint),201,option,RLegality(w,option,2600),EmptyT11,plan,announced,
        RTargets(plan,{}),ProtocolP!Entry9p(plan,0),RChildTurnUses(q),
        [tag |-> "AbilityRestrictions",ability |-> 200,source |-> d.syntax.source,results |-> EmptyT11])
      /\ qT11'=[q EXCEPT !.ledger=ledger,!.stack=ReplaceWindowTop9(@,busy),!.child=imminent,!.childPlan=announced,!.stage="RChildBegin"]
 [] q.stage="RChildBegin" ->
   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="RChildWork"]
 [] q.stage="RChildWork" ->
   LET 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==[q.ledger EXCEPT !.instances[201].status="Complete"]
       beforeSnapshot==RCurrentSnapshot(q,q.objects,q.ledger,q.ledger.lastSnapshot.id,"InstructionBefore",q.ledger.lastCheckpoint)
       afterSnapshot==RCurrentSnapshot(q,objects,ledger,q.ledger.lastSnapshot.id+1000,"InstructionAfter",q.ledger.lastCheckpoint)
   IN /\ RAdmitSnapshot(q,q.objects,q.ledger,beforeSnapshot)
      /\ RAdmitSnapshot(q,objects,ledger,afterSnapshot)
      /\ RecordConditionalExecutionUse96(q.ledger,q.ledger,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(q.ledger,ledger,ledger,q.stack,q.stack,q.child,p,q.childPlan,plan,
        ProtocolP!Step9p(q.childPlan),beforeSnapshot,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(q,itemInspection) EXCEPT !.ledger=ledger,!.child=p,!.childPlan=plan,!.objects=objects,
        !.work=Append(@,"CostReaction"),!.rawEvents=IF q.moves THEN Append(@,{ItemInspectionEndEvent7(a)}) ELSE @,!.stage="RChildCPOpen"]
 [] q.stage="RChildCPOpen" -> ROpenCP("Instruction",ConditionalInstructionCaller96(q.child),"RChildCPDone","ChildFinal")
 [] q.stage="RChildCPDone" ->
   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(RFrame(q),q.ledger,q.stack,q.child,p,receipt)
      /\ qT11'=[q EXCEPT !.child=p,!.stage="RChildReturn"]
 [] q.stage="RChildReturn" ->
   LET p==[q.child EXCEPT !.phase="Returned",!.ability.returned=TRUE] w==WindowTop9(q.stack)
       receipt==ProtocolP!Return9p(w,q.child.checkpoint)
   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="RReceive"]
 [] q.stage="RPass" ->
   LET w==WindowTop9(q.stack) after==PassPriorityFrame9(w)
       snapshot==RCurrentSnapshot(q,q.objects,q.ledger,q.ledger.lastSnapshot.id,"Pass",q.ledger.lastCheckpoint)
   IN /\ RAdmitSnapshot(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'=[q EXCEPT !.stack=ReplaceWindowTop9(@,after),!.stage=IF after.open THEN "RReceive" ELSE "RCostReturn"]
 [] q.stage="RCostReturn" ->
   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'=[RSetFrame(q,returned) EXCEPT !.stack=rest,!.wallet.checkpointDue=FALSE,!.currentCP=q.costCP,!.stage="RCostResume",
        !.checkpointHistory=Append(@,[id |-> f.id,role |-> "Cost",caller |-> f.caller,objects |-> q.objects,done |-> f.done])]
 [] q.stage="RCostResume" ->
   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="RTargets"]
 [] q.stage="RTargets" ->
   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,RTargets(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="RBegin"]
 [] q.stage="RBegin" ->
   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="RBody"]
 [] q.stage="RBody" ->
   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="RTail"]
 [] q.stage="RTail" ->
   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="RFinalOpen"]
 [] q.stage="RFinalOpen" -> ROpenCP("Instruction",PaidCheckpointCaller96(q.paid),"RFinalDone","PaidFinal")
 [] q.stage="RFinalDone" ->
   LET p==[q.paid EXCEPT !.phase="Complete",!.checkpoint=q.currentCP] IN
   /\ ResumePaidAfterCheckpoint103(RFrame(q),q.ledger,q.stack,q.paid,p,q.objects,EmptyT11,ItemInspectionPaidCheckpointT11(q.paid,q.currentCP,TRUE))
   /\ qT11'=[q EXCEPT !.paid=p,!.stage="RFinish"]
 [] q.stage="RFinish" ->
   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,RReturn(q),a,itemInspection)
      /\ qT11'=[IWithItemInspectionT11(q,itemInspection) EXCEPT !.paid=paid,!.stack=ReplaceWindowTop9(@,CompletePriorityOptionFrame9(w)),!.paidReturned=TRUE,!.stage="Window"]
 [] OTHER -> FALSE

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: BeginConditionalResolution96, CarryConditionalInstruction96, CarryPaidInstruction95, CompletePriorityOptionFrame9, ConditionalInstructionCaller96, ConditionalPriorityCaller96, EnterPaidInstruction95, FinishConditionalProcedure96, FinishPaidMidItemInspection95, InstructionWindowRef93, OpenConditionalProcedure96, OpenInstruction93, PaidCheckpointCaller96, PassConditionalPriority96, PassPriorityFrame9, PayPaidMidItemInspection95, PriorityOption9, RecordConditionalExecutionUse96, ReplaceWindowTop9, ResolveConditionalWithoutInterrupt96, ResolvePaidWithoutInterrupt95, StartPriorityOptionFrame9, WindowTop9, CheckpointDrained103, ReceivePriorityAfterCheckpoint103, ResumeConditionalInstructionAfterCheckpoint103, ResumePaidAfterCheckpoint103, ReturnCheckpointAfterReaction103, ProtocolP!Clearance9p, ProtocolP!Entry9p, ProtocolP!FinishedAbility9p, ProtocolP!FinishedPlan9p, ProtocolP!NoModifiers9p, ProtocolP!Return9p, ProtocolP!Step9p, IAT11, IWithItemInspectionT11, ItemInspectionEndEvent7, ItemInspectionMovementOutcome7, ItemInspectionCostCommandT11, ItemInspectionCostOwnerT11!DoSpendResourceUnits, ItemInspectionEndedT11, ItemInspectionMovedObjectsT11, ItemInspectionPaidCheckpointT11, ItemInspectionPaidCommittedFrameT11, ItemInspectionPaidEntryT11, ItemInspectionPaidInterruptReturnT11, ItemInspectionPaidNoModifiersT11, ItemInspectionPaidPlanT11, ItemInspectionPaidUsesT11, ItemInspectionWalletSpentT11, CardBatchTransfer8, RAdmitSnapshot, RCPWork, RChildDefinition, RChildTurnUses, RCurrentSnapshot, RFrame, RLegality, RMid, RNativeAtPayment, ROpenCP, RReadyCP, RReturn, RSetFrame, RTargets, RTurnUses, RUse, EmptyT11, qT11

RReadyCP · operator

reference-profile · input revision 2 · CC0 1.0

RReadyCP(q) == ProtocolP!PriorityCP9p(WindowTop9(q.stack),q.currentCP)

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: WindowTop9, ProtocolP!PriorityCP9p

RRecognitionChecks · operator

reference-profile · input revision 2 · CC0 1.0

RRecognitionChecks(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] i==q.ledger.instances[201] 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"
 /\ i.checkpointId=q.costCP /\ i.occurrence=e.id /\ i.definitionCopy=RChildDefinition /\ i.member.windowId=q.childWindow

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: TimingRef9, IAT11, RChildDefinition

RRegistrySafety · operator

reference-profile · input revision 2 · CC0 1.0

RRegistrySafety(q) ==
 /\ q.catalog=RCatalog(q.amount) /\ q.abilityRegistry=q.catalog /\ q.abilityRevision=0 /\ q.rulePermissions=RPermissions
 /\ BasisValidSA(q.catalog,RBasis(q)) /\ LedgerDomainSA(q.ledger) /\ RHistoryValid(q)
 /\ DOMAIN q.basisHistory=DOMAIN q.frames
 /\ \A id \in DOMAIN q.basisHistory :
     /\ q.basisHistory[id].revision=0 /\ q.basisHistory[id].registry=q.catalog /\ q.basisHistory[id].rulePermissions=RPermissions
     /\ (q.frames[id].recognition.id#0 => q.frames[id].recognition.beginSnapshot.objects=q.basisHistory[id].objects)

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: BasisValidSA, LedgerDomainSA, RBasis, RCatalog, RHistoryValid, RPermissions

RReturn · operator

reference-profile · input revision 2 · CC0 1.0

RReturn(q) == [tag |-> "PriorityOptionReturn",windowId |-> q.paid.windowId,option |-> q.paid.option,transactionId |-> q.paid.transaction,
 triggerPayment |-> RPayment(q),allCostsPaid |-> RNativeCommitted(q),optionComplete |-> q.paid.ability.complete,
 childrenReturned |-> q.childReturned /\ q.plan.phase="Complete",reactionsDrained |-> CheckpointDrained103(q.frames[q.paid.checkpoint],q.ledger,q.stack),
 finalCheckpointId |-> q.paid.checkpoint]

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: CheckpointDrained103, RNativeCommitted, RPayment

RSetFrame · operator

reference-profile · input revision 2 · CC0 1.0

RSetFrame(q,f) == [q EXCEPT !.frames[f.id]=f]

Exact module download · Source bundle and reproduction instructions

RSnapshotTemplate · operator

reference-profile · input revision 2 · CC0 1.0

RSnapshotTemplate(q,id,point,checkpoint) == [q.ledger.lastSnapshot EXCEPT !.id=id,!.point=point,!.checkpointId=checkpoint]

Exact module download · Source bundle and reproduction instructions

RSourceIndexChecks · operator

reference-profile · input revision 2 · CC0 1.0

RSourceIndexChecks(q) ==
 /\ RHistoryValid(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
    /\ RChildTurnUses(q)=EmptyT11)

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: RChildTurnUses, RHistoryValid, EmptyT11

RSpec · operator

reference-profile · input revision 2 · CC0 1.0

RSpec == RInit /\ [][RWork]_<<guideCaseT11,qT11>> /\ WF_<<guideCaseT11,qT11>>(RWork)

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: RInit, RWork, guideCaseT11, qT11

RTargets · operator

reference-profile · input revision 2 · CC0 1.0

RTargets(plan,targets) == [ProtocolP!Targets9p(plan) EXCEPT !.targets=targets]

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: ProtocolP!Targets9p

RTurnUses · operator

reference-profile · input revision 2 · CC0 1.0

RTurnUses(p) == ItemInspectionPaidTurnUsesT11(p)

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: ItemInspectionPaidTurnUsesT11

RUse · operator

reference-profile · input revision 2 · CC0 1.0

RUse(p) == ItemInspectionPaidUseT11(p)

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: ItemInspectionPaidUseT11

RWork · operator

reference-profile · input revision 2 · CC0 1.0

RWork ==
 /\ UNCHANGED guideCaseT11
 /\ IF qT11.stage="Window" /\ qT11.windowRole="Mid" THEN RMidWindow
    ELSE IF qT11.stage \in {"RMidReady","RPay","RCostOpen","RCP","RReceive","RChildReady","RSelect","RChildBegin","RChildWork",
      "RChildCPOpen","RChildCPDone","RChildReturn","RPass","RCostReturn","RCostResume","RTargets","RBegin","RBody","RTail","RFinalOpen","RFinalDone","RFinish"}
      THEN RProtocolWork ELSE IConnectedStepT11

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: IConnectedStepT11, RMidWindow, RProtocolWork, guideCaseT11, qT11

RWorld · operator

reference-profile · input revision 2 · CC0 1.0

RWorld(q,f) == [id |-> f.snapshotId,objects |-> q.objects,points |-> ZeroCountsT11,
 present |-> ConditionalPresentSA(q.abilityRegistry),activity |-> CommonActivitySA(RBasis(q),q.ledger)]

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: CommonActivitySA, ConditionalPresentSA, RBasis, ZeroCountsT11

RWorldBound · operator

reference-profile · input revision 2 · CC0 1.0

RWorldBound(q,f,world) ==
 /\ BasisValidSA(q.catalog,RBasis(q)) /\ LedgerDomainSA(q.ledger) /\ RHistoryValid(q)
 /\ world=[id |-> f.snapshotId,objects |-> q.objects,points |-> ZeroCountsT11,
   present |-> ConditionalPresentSA(q.abilityRegistry),activity |-> CommonActivitySA(RBasis(q),q.ledger)]

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: BasisValidSA, CommonActivitySA, ConditionalPresentSA, LedgerDomainSA, RBasis, RHistoryValid, ZeroCountsT11