DetachedChecksMC

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

DetachedProfiles · constant

reference-profile · input revision 2 · CC0 1.0

DetachedProfiles

Exact module download · Source bundle and reproduction instructions

DCompletion · operator

reference-profile · input revision 2 · CC0 1.0

DCompletion(q) == [tag |-> "Unit5Completion",family |-> "detached",NeutralValue00013 |-> q.detachedProfile,
 native |-> q.native,uses |-> q.uses,turnUses |-> q.turnUses,useIndex |-> q.useIndex,procedures |-> q.procedures,
 instances |-> q.ledger.instances,returnedPaid |-> q.returnedPaid,returnedChildren |-> q.returnedChildren,
 work |-> q.work,closedWindows |-> q.closedWindows,checkpointIds |-> DOMAIN q.checkpointHistory,
 captures |-> [id \in DOMAIN q.captures |-> [revision |-> q.captures[id].basis.revision,entries |-> DOMAIN q.captures[id].basis.registry,
      permissions |-> q.captures[id].basis.rulePermissions,snapshotId |-> q.captures[id].snapshot.id]],
 publications |-> [i \in 1..Len(q.publications) |-> LET p==q.publications[i] IN
      [cause |-> p.cause,target |-> p.target,beforeStatus |-> p.beforeLedger.instances[201].status,
       afterStatus |-> p.afterLedger.instances[201].status,beforeEpoch |-> p.beforeLedger.activationEpoch[ConditionalKey96(q.catalog[2].definition)],
       afterEpoch |-> p.afterLedger.activationEpoch[ConditionalKey96(q.catalog[2].definition)],capturedDefinition |-> p.beforeLedger.instances[201].definitionCopy,
       capturedSource |-> p.beforeLedger.instances[201].member.source,afterCurrentRows |-> p.currentSnapshot.activity.instances]]]

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: ConditionalKey96

DEventuallyDone · operator

reference-profile · input revision 2 · CC0 1.0

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

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: qT11

DImminent · operator

reference-profile · input revision 2 · CC0 1.0

DImminent(q) == q.detachedProfile \in {"imminent-permission","imminent-entry"}

Exact module download · Source bundle and reproduction instructions

DInit · operator

reference-profile · input revision 2 · CC0 1.0

DInit == registryCaseSA=0 /\ guideCaseT11=0 /\ \E NeutralValue00013 \in DetachedProfiles : qT11=DInitial(NeutralValue00013)

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: DetachedProfiles, DInitial, registryCaseSA, guideCaseT11, qT11

DInitial · operator

reference-profile · input revision 2 · CC0 1.0

DInitial(NeutralValue00013) == PJoin(U4Initial("no-loss"),[detachedProfile |-> NeutralValue00013])

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: PJoin, U4Initial

DInstanceCapture · operator

reference-profile · input revision 2 · CC0 1.0

DInstanceCapture(i) == [member |-> i.member,definition |-> i.definition,definitionCopy |-> i.definitionCopy,
 activationEpoch |-> i.activationEpoch,checkpointId |-> i.checkpointId,occurrence |-> i.occurrence,hadSnapshot |-> i.hadSnapshot]

Exact module download · Source bundle and reproduction instructions

DNext · operator

reference-profile · input revision 2 · CC0 1.0

DNext == DWork /\ U4CaptureFrame(qT11,qT11') /\ UNCHANGED <<registryCaseSA,guideCaseT11>>

Exact module download · Source bundle and reproduction instructions

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

DObservation · operator

reference-profile · input revision 2 · CC0 1.0

DObservation(q) == [tag |-> "Unit5Stage",family |-> "detached",NeutralValue00013 |-> q.detachedProfile,stage |-> q.stage,
 conditionalStatus |-> IF 201 \in DOMAIN q.ledger.instances THEN q.ledger.instances[201].status ELSE "Absent",
 childPhase |-> IF q.child=EmptyT11 THEN "NoValue" ELSE q.child.phase,paidPhase |-> IF q.paid=EmptyT11 THEN "NoValue" ELSE q.paid.phase,
 active |-> ConditionalActive96(q.catalog[2].definition,q.current),present |-> 2 \in DOMAIN q.basis.registry,
 revision |-> q.basis.revision,epoch |-> q.ledger.activationEpoch[ConditionalKey96(q.catalog[2].definition)],
 publicationCount |-> Len(q.publications),useCount |-> Cardinality(DOMAIN q.uses),walletCount |-> Cardinality(DOMAIN q.wallet.obj),
 captureCount |-> Cardinality(DOMAIN q.captures),windowId |-> IF Len(q.stack)=0 THEN 0 ELSE WindowTop9(q.stack).id,
 windowStage |-> IF Len(q.stack)=0 THEN "Absent" ELSE WindowTop9(q.stack).stage,done |-> q.stage="Done"]

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: ConditionalActive96, ConditionalKey96, WindowTop9, EmptyT11

DPermission · operator

reference-profile · input revision 2 · CC0 1.0

DPermission(q) == q.detachedProfile \in {"imminent-permission","resolving-permission"}

Exact module download · Source bundle and reproduction instructions

DProfiles · operator

reference-profile · input revision 2 · CC0 1.0

DProfiles == {"none","imminent-permission","imminent-entry","resolving-permission","resolving-entry"}

Exact module download · Source bundle and reproduction instructions

DRecognitionCapture · operator

reference-profile · input revision 2 · CC0 1.0

DRecognitionCapture(q) ==
 /\ DOMAIN q.ledger.instances \subseteq {201}
 /\ \A id \in DOMAIN q.ledger.instances :
      LET i==q.ledger.instances[id] cp==q.checkpointHistory[i.checkpointId]
          original==NewConditionalInstance96(201,q.catalog[2].definition,cp,U4OccurrenceId(1),U4ReactionWindow(1),5)
      IN /\ i.checkpointId=q.costCheckpoint /\ DInstanceCapture(i)=DInstanceCapture(original)

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: NewConditionalInstance96, DInstanceCapture, U4OccurrenceId, U4ReactionWindow

DSafety · operator

reference-profile · input revision 2 · CC0 1.0

DSafety ==
 LET q==qT11 IN
 /\ U4Safety /\ U4CaptureSafety /\ DRecognitionCapture(q) /\ q.detachedProfile \in DProfiles /\ q.round=1
 /\ (201 \in DOMAIN q.ledger.instances => q.ledger.instances[201].status # "Lost" /\ q.ledger.instances[201].definitionCopy=q.catalog[2].definition)
 /\ (q.child # EmptyT11 => q.child.definition=q.catalog[2].definition /\ q.child.ability.detached /\ ConditionalProcedureBound96(q.ledger,q.child))
 /\ (Len(q.publications)>0 =>
       LET p==q.publications[1] expected==IF DImminent(q) THEN "Imminent" ELSE "Resolving" IN
       /\ Len(q.publications)=1 /\ p.beforeLedger.instances[201].status=expected /\ p.afterLedger.instances[201].status=expected
       /\ q.ledger.activationEpoch[ConditionalKey96(q.catalog[2].definition)]=1 /\ q.ledger.instances[201].activationEpoch=0
       /\ ~ConditionalActive96(q.catalog[2].definition,q.current)
       /\ (2 \in DOMAIN q.basis.registry)=DPermission(q)
       /\ q.child.definition=p.beforeLedger.instances[201].definitionCopy)
 /\ (q.stage="Done" =>
       /\ q.stack= <<>> /\ DOMAIN q.uses={1} /\ DOMAIN q.returnedPaid={101} /\ DOMAIN q.returnedChildren={201}
       /\ q.ledger.instances[201].status="Complete" /\ ~q.ledger.instances[201].used /\ Cardinality(DOMAIN q.wallet.obj)=2
       /\ q.work= <<[round |-> 1,kind |-> "Conditional"],[round |-> 1,kind |-> "Paid"]>>
       /\ Len(q.publications)=(IF q.detachedProfile="none" THEN 0 ELSE 1))

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: ConditionalActive96, ConditionalKey96, ConditionalProcedureBound96, DImminent, DPermission, DProfiles, DRecognitionCapture, U4CaptureSafety, U4Safety, EmptyT11, qT11

DSpec · operator

reference-profile · input revision 2 · CC0 1.0

DSpec == DInit /\ [][DNext]_<<qT11,registryCaseSA,guideCaseT11>> /\ WF_<<qT11,registryCaseSA,guideCaseT11>>(DNext)

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: DInit, DNext, registryCaseSA, guideCaseT11, qT11

DWork · operator

reference-profile · input revision 2 · CC0 1.0

DWork ==
 LET q==qT11 IN
 IF q.stage="PaidReturn" THEN
   LET p==[q.paid EXCEPT !.phase="Returned",!.ability.returned=TRUE]
       stack==ReplaceWindowTop9(q.stack,CompletePriorityOptionFrame9(WindowTop9(q.stack))) IN
   /\ FinishPaidProcedure95(q.stack,stack,q.paid,p,U4ReturnReceipt(q,q.paid,FALSE))
   /\ qT11'=[q EXCEPT !.paid=p,!.stack=stack,!.returnedPaid=PJoin(@,[id \in {p.id} |-> p]),!.stage="Receive",!.resume="Pass"]
 ELSE IF q.detachedProfile # "none" /\ Len(q.publications)=0 /\
     ((DImminent(q) /\ q.stage="ChildBegin") \/ (~DImminent(q) /\ q.stage="ChildWork"))
 THEN /\ q.child.ability.detached /\ q.child.definition=q.catalog[2].definition
      /\ U4Kernel(IF DPermission(q) THEN "PermissionWithdraw" ELSE "EntryWithdraw",q.stage)
 ELSE U4Work

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: CompletePriorityOptionFrame9, FinishPaidProcedure95, ReplaceWindowTop9, WindowTop9, PJoin, DImminent, DPermission, U4Kernel, U4ReturnReceipt, U4Work, qT11