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

RegistryAvailabilityMC

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

AvailabilityProfiles · constant

reference-profile · input revision 2 · CC0 1.0

AvailabilityProfiles

Exact module download · Source bundle and reproduction instructions

VAdmitPaid · operator

reference-profile · input revision 2 · CC0 1.0

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)))

Exact module download · Source bundle and reproduction instructions

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

VAdmitSnapshot · operator

reference-profile · input revision 2 · CC0 1.0

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)))

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: AdmitConditionalSnapshotSA, MinimalCaptureSA, VBasisObjects, VSnapshotTemplate

VBasis · operator

reference-profile · input revision 2 · CC0 1.0

VBasis(q) == VBasisObjects(q,q.objects)

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: VBasisObjects

VBasisObjects · operator

reference-profile · input revision 2 · CC0 1.0

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

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: BasisSA

VCPData · operator

reference-profile · input revision 2 · CC0 1.0

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]

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: VCPOccurrences, VCurrentSnapshot, EmptyT11

VCPNext · operator

reference-profile · input revision 2 · CC0 1.0

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

Exact module download · Source bundle and reproduction instructions

VCPOccurrences · operator

reference-profile · input revision 2 · CC0 1.0

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

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: ConditionalKey96, TimingRef9, IAT11, VChildDefinition

VCPWork · operator

reference-profile · input revision 2 · CC0 1.0

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

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: ConditionalActive96, 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, VAdmitSnapshot, VCPData, VCPNext, VChildDefinition, VDefinitions, VFrame, VJoin, VLegal, VLexemes, VOwners, VPrinted, VSetFrame, VWorld, VWorldBound, EmptyT11, qT11, CardFacts10

VCapture · operator

reference-profile · input revision 2 · CC0 1.0

VCapture(basis,views) == [basis |-> MinimalCaptureSA(basis),views |-> views]

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: MinimalCaptureSA

VCatalog · operator

reference-profile · input revision 2 · CC0 1.0

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

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: ItemInspectionPaidDefinitionT11, VChildDefinition

VCheckpointEventChecks · operator

reference-profile · input revision 2 · CC0 1.0

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))

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: InstructionWindowRef93, VUse

VChildDefinition · operator

reference-profile · input revision 2 · CC0 1.0

VChildDefinition == PChildDefinition

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: PChildDefinition

VChildObligation · operator

reference-profile · input revision 2 · CC0 1.0

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"

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: CheckpointDrained103, EmptyT11

VChildTurnUses · operator

reference-profile · input revision 2 · CC0 1.0

VChildTurnUses(q) == FamilyTurnUsesSA(q.catalog,q.useIndex,q.turnUses,"Conditional",VChildDefinition.syntax.source)

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: FamilyTurnUsesSA, VChildDefinition

VCompletion · operator

reference-profile · input revision 2 · CC0 1.0

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)]

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: WindowTop9, MinimalCaptureSA, VBasis, VOutcome, EmptyT11

VConnectedSafety · operator

reference-profile · input revision 2 · CC0 1.0

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")

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, VCheckpointEventChecks, VExpectedTrace, VGuardChecks, VInitialPaid, VRecognitionChecks, VRegistrySafety, qT11, TraversalFrameValid6, SideBProcedureValid5

VContext · operator

reference-profile · input revision 2 · CC0 1.0

VContext(q,d) == PaidContextFromRegistrySA(q.catalog,VBasis(q),q.ledger,q.useIndex,q.turnUses,PContext(q,d),1)

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: PaidContextFromRegistrySA, PContext, VBasis

VCurrentPaidActivity · operator

reference-profile · input revision 2 · CC0 1.0

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)

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: AbilityActive9, FlagActivity93, CommonActivitySA, PaidPresentSA, SourceDefaultActivitySA, VBasis, ZeroCountsT11

VCurrentSnapshot · operator

reference-profile · input revision 2 · CC0 1.0

VCurrentSnapshot(q,objects,ledger,id,point,checkpoint) ==
 ConditionalSnapshotFromRegistrySA(q.catalog,VBasisObjects(q,objects),ledger,VSnapshotTemplate(q,id,point,checkpoint))

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: ConditionalSnapshotFromRegistrySA, VBasisObjects, VSnapshotTemplate

VDeclineCompletion · operator

reference-profile · input revision 2 · CC0 1.0

VDeclineCompletion == VInitialPaid(qT11.availabilityProfile) => <>qT11.done

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: VInitialPaid, qT11

VDefinitions · operator

reference-profile · input revision 2 · CC0 1.0

VDefinitions(q) == ConditionalDefinitionsSA(q.abilityRegistry)

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: ConditionalDefinitionsSA

VDispatch · operator

reference-profile · input revision 2 · CC0 1.0

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

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: IConnectedStepT11, VMidWindow, VProtocolWork, guideCaseT11, qT11

VExpectedBasis · operator

reference-profile · input revision 2 · CC0 1.0

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

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: KernelBasisRA, KernelTargetRA, VPreparedBasis

VExpectedTrace · operator

reference-profile · input revision 2 · CC0 1.0

VExpectedTrace(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

VFrame · operator

reference-profile · input revision 2 · CC0 1.0

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

Exact module download · Source bundle and reproduction instructions

VFreshWorld · operator

reference-profile · input revision 2 · CC0 1.0

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

Exact module download · Source bundle and reproduction instructions

VGuardChecks · operator

reference-profile · input revision 2 · CC0 1.0

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")]))

Exact module download · Source bundle and reproduction instructions

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

VHistoryFrame · operator

reference-profile · input revision 2 · CC0 1.0

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

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: VInstanceCapture, EmptyT11

VHistoryValid · operator

reference-profile · input revision 2 · CC0 1.0

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

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: UseProvenanceValidSA

VInit · operator

reference-profile · input revision 2 · CC0 1.0

VInit == guideCaseT11=0 /\ \E amount \in PaidAmounts,moves \in PaidMoves,NeutralValue00013 \in AvailabilityProfiles :
 /\ NeutralValue00013 \in VProfiles /\ (VUnavailable(NeutralValue00013) => ~moves) /\ qT11=VInitial(amount,moves,NeutralValue00013)

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: PaidAmounts, PaidMoves, AvailabilityProfiles, VInitial, VProfiles, VUnavailable, guideCaseT11, qT11

VInitial · operator

reference-profile · input revision 2 · CC0 1.0

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])

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: NewConditionalLedger96, ConditionalSnapshotFromRegistrySA, PInitial, PInitialSnapshot, VCapture, VCatalog, VJoin, VPreparedBasis, EmptyT11

VInitialConditional · operator

reference-profile · input revision 2 · CC0 1.0

VInitialConditional(NeutralValue00013) == NeutralValue00013 \in {"initial-conditional-permission","initial-conditional-entry"}

Exact module download · Source bundle and reproduction instructions

VInitialPaid · operator

reference-profile · input revision 2 · CC0 1.0

VInitialPaid(NeutralValue00013) == NeutralValue00013 \in {"initial-paid-permission","initial-paid-entry"}

Exact module download · Source bundle and reproduction instructions

VInside · operator

reference-profile · input revision 2 · CC0 1.0

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

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: TimingRef9, IAT11, IBT11, StillItemInspectioning7

VInstanceCapture · operator

reference-profile · input revision 2 · CC0 1.0

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]

Exact module download · Source bundle and reproduction instructions

VItemInspectionView · operator

reference-profile · input revision 2 · CC0 1.0

VItemInspectionView(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

VJoin · operator

reference-profile · input revision 2 · CC0 1.0

VJoin(base,extra) == PJoin(base,extra)

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: PJoin

VKeepWorld · operator

reference-profile · input revision 2 · CC0 1.0

VKeepWorld(q,basis,views) ==
 [q EXCEPT !.worldHistory=VJoin(@,[id \in {views[1].id} |-> VCapture(basis,views)]),!.nextWorld=@+1]

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: VCapture, VJoin

VKernelSafety · operator

reference-profile · input revision 2 · CC0 1.0

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)

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: ConditionalKey96, VCurrentPaidActivity, VPaidLoss

VLegal · operator

reference-profile · input revision 2 · CC0 1.0

VLegal(selected) == selected={}

Exact module download · Source bundle and reproduction instructions

VLegality · operator

reference-profile · input revision 2 · CC0 1.0

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

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: LegalityT11

VLex · operator

reference-profile · input revision 2 · CC0 1.0

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

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: EmptyT11

VLexemes · operator

reference-profile · input revision 2 · CC0 1.0

VLexemes(q) == [k \in DOMAIN VDefinitions(q) |-> VLex(VDefinitions(q)[k])]

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: VDefinitions, VLex

VMid · operator

reference-profile · input revision 2 · CC0 1.0

VMid(q) == ItemInspectionTemporalMidT11(VItemInspectionView(q))

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: ItemInspectionTemporalMidT11, VItemInspectionView

VMidWindow · operator

reference-profile · input revision 2 · CC0 1.0

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

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: ClosePriorityWindow9, ConditionalPriorityCaller96, OpenPaidProcedure95, PaidEligibility95, PassMidItemInspection9, PopClosedPriorityWindow9, ReplaceWindowTop9, ReservePaidMidItemInspection95, StartPriorityOptionFrame9, WindowTop9, BasisValidSA, MinimalCaptureSA, IAT11, IRecordT11, IWithItemInspectionT11, VAdmitPaid, VBasis, VContext, VHistoryValid, VInitialPaid, VLegality, VMid, VOpenCP, VPaidDefinition, VPaidOption, qT11

VNativeAtPayment · operator

reference-profile · input revision 2 · CC0 1.0

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)

Exact module download · Source bundle and reproduction instructions

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

VNativeCommitted · operator

reference-profile · input revision 2 · CC0 1.0

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)>>

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: ItemInspectionCostOwnerT11!SpendResourceUnitsOK, ItemInspectionPaidUsesT11, ItemInspectionWalletSpentT11, VTurnUses, VUse

VNoChildCompletion · operator

reference-profile · input revision 2 · CC0 1.0

VNoChildCompletion == VInitialConditional(qT11.availabilityProfile) => <>qT11.done

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: VInitialConditional, qT11

VObjects · operator

reference-profile · input revision 2 · CC0 1.0

VObjects == PObjects

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: PObjects

VObservation · operator

reference-profile · input revision 2 · CC0 1.0

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]

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: ConditionalKey96, WindowTop9, VChildDefinition, VOutcome, EmptyT11

VOpenCP · operator

reference-profile · input revision 2 · CC0 1.0

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

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: InstructionWindowRef93, WindowTop9, MinimalCaptureSA, BeginCheckpointSite103, CheckpointSiteKey103, NewCheckpoint103, VBasis, VCPData, VFreshWorld, VInside, VJoin, VKeepWorld, qT11

VOutcome · operator

reference-profile · input revision 2 · CC0 1.0

VOutcome(q) == IF VInitialPaid(q.availabilityProfile) THEN "Decline" ELSE IF VInitialConditional(q.availabilityProfile) THEN "NoChild" ELSE "Paid"

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: VInitialConditional, VInitialPaid

VOwners · operator

reference-profile · input revision 2 · CC0 1.0

VOwners == POwners

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: POwners

VPaidCompletion · operator

reference-profile · input revision 2 · CC0 1.0

VPaidCompletion == (~VUnavailable(qT11.availabilityProfile)) => <>qT11.done

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: VUnavailable, qT11

VPaidDefinition · operator

reference-profile · input revision 2 · CC0 1.0

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

Exact module download · Source bundle and reproduction instructions

VPaidLoss · operator

reference-profile · input revision 2 · CC0 1.0

VPaidLoss(NeutralValue00013) == NeutralValue00013 \in {"paid-permission","paid-entry"}

Exact module download · Source bundle and reproduction instructions

VPaidOption · operator

reference-profile · input revision 2 · CC0 1.0

VPaidOption(q,w,d) == ItemInspectionPaidOptionT11(VItemInspectionView(q),w,d)

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: ItemInspectionPaidOptionT11, VItemInspectionView

VPaidSafety · operator

reference-profile · input revision 2 · CC0 1.0

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)

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: CheckpointDrained103, CheckpointStageSet103, IAT11, ItemInspectionPaidUsesT11, VChildObligation, VInitialConditional, VKernelSafety, VNativeCommitted, VSourceIndexChecks, VTurnUses, VUnavailable, VUnavailableSafety, VUse, EmptyT11, qT11

VPayment · operator

reference-profile · input revision 2 · CC0 1.0

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)]

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: CheckpointDrained103, VNativeCommitted

VPermissions · operator

reference-profile · input revision 2 · CC0 1.0

VPermissions == {"AuditPaidObserve","ProtocolReactionControl"}

Exact module download · Source bundle and reproduction instructions

VPreparedBasis · operator

reference-profile · input revision 2 · CC0 1.0

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)

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: BasisSA, PObjects, VCatalog, VInitialPaid, VPermissions, VWithout

VPrinted · operator

reference-profile · input revision 2 · CC0 1.0

VPrinted == PPrinted

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: PPrinted

VProfiles · operator

reference-profile · input revision 2 · CC0 1.0

VProfiles == {"baseline","paid-permission","paid-entry","initial-paid-permission","initial-paid-entry","initial-conditional-permission","initial-conditional-entry"}

Exact module download · Source bundle and reproduction instructions

VProtocolWork · operator

reference-profile · input revision 2 · CC0 1.0

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

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, ConditionalSnapshotFromRegistrySA, MinimalCaptureSA, AdmitKernelPublicationRA, KernelBasisRA, KernelTargetRA, PublicationAfterLedgerRA, PublicationAfterStackRA, PublicationObserverSnapshotRA, PublicationTemplateRA, 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, VAdmitSnapshot, VBasis, VBasisObjects, VCPWork, VChildDefinition, VChildTurnUses, VCurrentSnapshot, VFrame, VFreshWorld, VKeepWorld, VLegality, VMid, VNativeAtPayment, VNativeCommitted, VOpenCP, VPaidLoss, VReadyCP, VReturn, VSetBasis, VSetFrame, VTargets, VTurnUses, VUse, EmptyT11, qT11

VReadyCP · operator

reference-profile · input revision 2 · CC0 1.0

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

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: WindowTop9, ProtocolP!PriorityCP9p

VRecognitionChecks · operator

reference-profile · input revision 2 · CC0 1.0

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

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: ConditionalKey96, TimingRef9, IAT11, EmptyT11

VRegistrySafety · operator

reference-profile · input revision 2 · CC0 1.0

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])

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: ConditionalKey96, BasisValidSA, ConditionalDefinitionsSA, ConditionalPresentSA, LedgerDomainSA, RegistryValidSA, VBasis, VCatalog, VChildDefinition, VExpectedBasis, VHistoryValid, VProfiles

VReturn · operator

reference-profile · input revision 2 · CC0 1.0

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]

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: CheckpointDrained103, VChildObligation, VNativeCommitted, VPayment

VSetBasis · operator

reference-profile · input revision 2 · CC0 1.0

VSetBasis(q,basis) == [q EXCEPT !.abilityRegistry=basis.registry,!.abilityRevision=basis.revision,!.rulePermissions=basis.rulePermissions]

Exact module download · Source bundle and reproduction instructions

VSetFrame · operator

reference-profile · input revision 2 · CC0 1.0

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

Exact module download · Source bundle and reproduction instructions

VSnapshotTemplate · operator

reference-profile · input revision 2 · CC0 1.0

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

Exact module download · Source bundle and reproduction instructions

VSourceIndexChecks · operator

reference-profile · input revision 2 · CC0 1.0

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)

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: VChildTurnUses, VHistoryValid, EmptyT11

VSpec · operator

reference-profile · input revision 2 · CC0 1.0

VSpec == VInit /\ [][VWork]_<<guideCaseT11,qT11>> /\ WF_<<guideCaseT11,qT11>>(VWork)

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: VInit, VWork, guideCaseT11, qT11

VTargets · operator

reference-profile · input revision 2 · CC0 1.0

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

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: ProtocolP!Targets9p

VTurnUses · operator

reference-profile · input revision 2 · CC0 1.0

VTurnUses(p) == ItemInspectionPaidTurnUsesT11(p)

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: ItemInspectionPaidTurnUsesT11

VUnavailable · operator

reference-profile · input revision 2 · CC0 1.0

VUnavailable(NeutralValue00013) == VInitialPaid(NeutralValue00013) \/ VInitialConditional(NeutralValue00013)

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: VInitialConditional, VInitialPaid

VUnavailableSafety · operator

reference-profile · input revision 2 · CC0 1.0

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))

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: PaidCheckpointCaller96, IAT11, ItemInspectionWalletInitialT11, VInitialConditional, VInitialPaid, VUnavailable, EmptyT11

VUse · operator

reference-profile · input revision 2 · CC0 1.0

VUse(p) == ItemInspectionPaidUseT11(p)

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: ItemInspectionPaidUseT11

VWithout · operator

reference-profile · input revision 2 · CC0 1.0

VWithout(map,key) == [k \in DOMAIN map \ {key} |-> map[k]]

Exact module download · Source bundle and reproduction instructions

VWork · operator

reference-profile · input revision 2 · CC0 1.0

VWork == VDispatch /\ VHistoryFrame(qT11,qT11')

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: VDispatch, VHistoryFrame, qT11

VWorld · operator

reference-profile · input revision 2 · CC0 1.0

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

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: CommonActivitySA, ConditionalPresentSA, VBasis, ZeroCountsT11

VWorldBound · operator

reference-profile · input revision 2 · CC0 1.0

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)]

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: BasisValidSA, CommonActivitySA, ConditionalPresentSA, LedgerDomainSA, VBasis, VHistoryValid, ZeroCountsT11