ActivityChecksMC

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

ActivityProfiles · constant

reference-profile · input revision 2 · CC0 1.0

ActivityProfiles

Exact module download · Source bundle and reproduction instructions

AEntryOps · operator

reference-profile · input revision 2 · CC0 1.0

AEntryOps(entry) == <<AOperation("EntryWithdraw",SCatalogSA[entry].source,entry),AOperation("EntryRestore",SCatalogSA[entry].source,entry)>>

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: AOperation, SCatalogSA

AEpochSafety · operator

reference-profile · input revision 2 · CC0 1.0

AEpochSafety ==
 LET q==qT11 losses==IF q.NeutralValue00013="alternating" THEN (IF q.stage>=3 THEN 2 ELSE IF q.stage>=1 THEN 1 ELSE 0)
                    ELSE IF q.NeutralValue00013 \in {"permission","conditional-entry","overlap"} /\ q.stage>=1 THEN 1 ELSE 0
 IN q.ledger.activationEpoch[ConditionalKey96(SConditionalSA)]=losses /\ q.ledger.activationSerial=losses

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: ConditionalKey96, SConditionalSA, qT11

AEventuallyPublished · operator

reference-profile · input revision 2 · CC0 1.0

AEventuallyPublished == <> (qT11.stage=Len(AOperations(qT11.NeutralValue00013)))

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: AOperations, qT11

AHistoricalCapture · operator

reference-profile · input revision 2 · CC0 1.0

AHistoricalCapture == [basis |-> MinimalCaptureSA(AInitialBasis),snapshot |-> AInitialSnapshot]

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: MinimalCaptureSA, AInitialBasis, AInitialSnapshot

AHistoricalSafety · operator

reference-profile · input revision 2 · CC0 1.0

AHistoricalSafety == qT11.history=AHistoricalCapture

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: AHistoricalCapture, qT11

AInit · operator

reference-profile · input revision 2 · CC0 1.0

AInit == registryCaseSA=0 /\ guideCaseT11=0 /\ \E NeutralValue00013 \in ActivityProfiles : qT11=AInitial(NeutralValue00013)

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: ActivityProfiles, AInitial, registryCaseSA, guideCaseT11, qT11

AInitial · operator

reference-profile · input revision 2 · CC0 1.0

AInitial(NeutralValue00013) == [catalog |-> SCatalogSA,basis |-> AInitialBasis,ledger |-> AInitialLedger,
 stack |-> <<SWindowSA>>,history |-> AHistoricalCapture,current |-> AInitialSnapshot,
 snapshotIds |-> {AInitialSnapshot.id},currentBasis |-> MinimalCaptureSA(AInitialBasis),publication |-> EmptyT11,NeutralValue00013 |-> NeutralValue00013,stage |-> 0]

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: MinimalCaptureSA, AHistoricalCapture, AInitialBasis, AInitialLedger, AInitialSnapshot, SCatalogSA, SWindowSA, EmptyT11

AInitialBasis · operator

reference-profile · input revision 2 · CC0 1.0

AInitialBasis == BasisSA(0,SCatalogSA,EmptyT11,{"SharedRegistryControl","Specimen0070RegistryControl"})

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: BasisSA, SCatalogSA, EmptyT11

AInitialLedger · operator

reference-profile · input revision 2 · CC0 1.0

AInitialLedger == NewConditionalLedger96(AInitialSnapshot)

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: NewConditionalLedger96, AInitialSnapshot

AInitialSnapshot · operator

reference-profile · input revision 2 · CC0 1.0

AInitialSnapshot == ConditionalSnapshotFromRegistrySA(SCatalogSA,AInitialBasis,ASeedLedger,PInitialSnapshot)

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: ConditionalSnapshotFromRegistrySA, AInitialBasis, ASeedLedger, PInitialSnapshot, SCatalogSA

ANativeActivitySafety · operator

reference-profile · input revision 2 · CC0 1.0

ANativeActivitySafety ==
 LET q==qT11 paid==PaidContextFromRegistrySA(q.catalog,q.basis,q.ledger,EmptyT11,EmptyT11,STemplateSA,3)
     conditional==ConditionalActive96(SConditionalSA,q.current)
     paidActive==PaidEligibility95(SPaidSA,paid,SWindowSA)
     expectedConditional==IF q.NeutralValue00013="permission" THEN q.stage # 1 ELSE IF q.NeutralValue00013="conditional-entry" THEN q.stage # 1
        ELSE IF q.NeutralValue00013="alternating" THEN q.stage \notin {1,3} ELSE IF q.NeutralValue00013="overlap" THEN q.stage \notin {1,2,3} ELSE TRUE
     expectedPaid==IF q.NeutralValue00013="permission" THEN q.stage # 1 ELSE IF q.NeutralValue00013="paid-entry" THEN q.stage # 1
        ELSE IF q.NeutralValue00013="alternating" THEN q.stage \notin {1,5} ELSE IF q.NeutralValue00013="overlap" THEN q.stage \notin {2,3} ELSE TRUE
 IN /\ conditional=expectedConditional /\ paidActive=expectedPaid
    /\ 1 \in DOMAIN q.basis.registry
    /\ (2 \in DOMAIN q.basis.registry)=(IF q.NeutralValue00013="conditional-entry" THEN q.stage # 1 ELSE IF q.NeutralValue00013="alternating" THEN q.stage # 3 ELSE IF q.NeutralValue00013="overlap" THEN q.stage \notin {1,2} ELSE TRUE)
    /\ (3 \in DOMAIN q.basis.registry)=(IF q.NeutralValue00013="paid-entry" THEN q.stage # 1 ELSE IF q.NeutralValue00013="alternating" THEN q.stage # 5 ELSE TRUE)

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: ConditionalActive96, PaidEligibility95, PaidContextFromRegistrySA, SConditionalSA, SPaidSA, STemplateSA, SWindowSA, EmptyT11, qT11

ANativeCatalogSafety · operator

reference-profile · input revision 2 · CC0 1.0

ANativeCatalogSafety ==
 LET q==qT11 IN \A key \in DOMAIN q.catalog :
   LET row==q.catalog[key]
       expected==key \in DOMAIN q.basis.registry /\ row.source.rule \in q.basis.rulePermissions
       actual==IF row.kind="Conditional" THEN ConditionalActive96(row.definition,q.current)
               ELSE FlagActivity93(row.definition.syntax,PaidPresentSA(q.basis.registry),
                 AbilityActive9(row.definition.activity,q.basis.objects,PaidPresentSA(q.basis.registry),
                   SourceDefaultActivitySA(q.basis,row.source),CommonActivitySA(q.basis,q.ledger)),{},ZeroCountsT11)
   IN actual=expected

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: AbilityActive9, ConditionalActive96, FlagActivity93, CommonActivitySA, PaidPresentSA, SourceDefaultActivitySA, ZeroCountsT11, qT11

ANext · operator

reference-profile · input revision 2 · CC0 1.0

ANext == IF qT11.stage < Len(AOperations(qT11.NeutralValue00013)) THEN APublish ELSE UNCHANGED <<qT11,registryCaseSA,guideCaseT11>>

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: AOperations, APublish, registryCaseSA, guideCaseT11, qT11

AOperation · operator

reference-profile · input revision 2 · CC0 1.0

AOperation(cause,source,entry) == [cause |-> cause,target |-> KernelTargetRA(source,entry)]

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: KernelTargetRA

AOperations · operator

reference-profile · input revision 2 · CC0 1.0

AOperations(NeutralValue00013) == CASE NeutralValue00013="permission" -> APermissionOps(SRuleSA)
 [] NeutralValue00013="conditional-entry" -> AEntryOps(2) [] NeutralValue00013="paid-entry" -> AEntryOps(3)
 [] NeutralValue00013="alternating" -> APermissionOps(SRuleSA) \o AEntryOps(2) \o AEntryOps(3)
 [] NeutralValue00013="overlap" -> <<AOperation("EntryWithdraw",SRuleSA,2),AOperation("PermissionWithdraw",SRuleSA,0),
                          AOperation("EntryRestore",SRuleSA,2),AOperation("PermissionRestore",SRuleSA,0)>>
 [] OTHER -> APermissionOps(SCatalogSA[4].source)

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: AEntryOps, AOperation, APermissionOps, SCatalogSA, SRuleSA

APermissionOps · operator

reference-profile · input revision 2 · CC0 1.0

APermissionOps(source) == <<AOperation("PermissionWithdraw",source,0),AOperation("PermissionRestore",source,0)>>

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: AOperation

AProfiles · operator

reference-profile · input revision 2 · CC0 1.0

AProfiles == {"permission","conditional-entry","paid-entry","alternating","decoy-permission","overlap"}

Exact module download · Source bundle and reproduction instructions

APublicationSafety · operator

reference-profile · input revision 2 · CC0 1.0

APublicationSafety ==
 LET q==qT11 IN
 /\ q.NeutralValue00013 \in AProfiles /\ q.catalog=SCatalogSA /\ BasisValidSA(q.catalog,q.basis)
 /\ q.basis.revision=q.stage /\ q.basis.objects=AInitialBasis.objects /\ q.ledger.instances=EmptyT11
 /\ q.snapshotIds={AInitialSnapshot.id} \cup {1000+i : i \in 1..q.stage}
 /\ ConditionalBindingSA(q.catalog,q.basis,q.ledger,q.current,q.current,q.currentBasis)
 /\ q.ledger.lastSnapshot=AInitialSnapshot
 /\ IF q.stage=0 THEN TRUE ELSE
   LET p==q.publication IN
   /\ p.snapshotId \notin p.beforeSnapshotIds /\ p.afterSnapshotIds=p.beforeSnapshotIds \cup {p.snapshotId}
   /\ p.afterSnapshotIds=q.snapshotIds
   /\ p.afterBasis=MinimalCaptureSA(q.basis) /\ p.afterLedger=q.ledger /\ p.afterStack=q.stack /\ p.currentSnapshot=q.current
   /\ AdmitKernelPublicationRA(q.catalog,p.beforeBasis,p.afterBasis,p.cause,p.target,p.snapshotId,
      p.beforeLedger,p.candidateLedger,p.afterLedger,p.beforeStack,p.afterStack,
      p.beforeSnapshot,p.candidateSnapshot,p.observerSnapshot,p.currentSnapshot)

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: BasisValidSA, ConditionalBindingSA, MinimalCaptureSA, AInitialBasis, AInitialSnapshot, AProfiles, AdmitKernelPublicationRA, SCatalogSA, EmptyT11, qT11

APublish · operator

reference-profile · input revision 2 · CC0 1.0

APublish ==
 LET q==qT11 op==AOperations(q.NeutralValue00013)[q.stage+1]
     snapshotId==1001+q.stage
     basis==KernelBasisRA(q.catalog,q.basis,op.cause,op.target)
     before==ConditionalSnapshotFromRegistrySA(q.catalog,q.basis,q.ledger,q.current)
     candidateLedger==q.ledger
     candidate==ConditionalSnapshotFromRegistrySA(q.catalog,basis,candidateLedger,PublicationTemplateRA(before,snapshotId))
     observer==PublicationObserverSnapshotRA(q.ledger,candidateLedger,before,candidate)
     ledger==PublicationAfterLedgerRA(q.ledger,candidateLedger,before,candidate)
     stack==PublicationAfterStackRA(q.stack,q.ledger,ledger)
     current==ConditionalSnapshotFromRegistrySA(q.catalog,basis,ledger,observer)
     receipt==[snapshotId |-> snapshotId,cause |-> op.cause,target |-> op.target,beforeBasis |-> MinimalCaptureSA(q.basis),afterBasis |-> MinimalCaptureSA(basis),
       beforeSnapshotIds |-> q.snapshotIds,afterSnapshotIds |-> q.snapshotIds \cup {snapshotId},
       beforeLedger |-> q.ledger,candidateLedger |-> candidateLedger,afterLedger |-> ledger,beforeStack |-> q.stack,afterStack |-> stack,
       beforeSnapshot |-> before,candidateSnapshot |-> candidate,observerSnapshot |-> observer,currentSnapshot |-> current]
 IN /\ q.stage < Len(AOperations(q.NeutralValue00013))
    /\ ConditionalBindingSA(q.catalog,q.basis,q.ledger,q.current,q.current,q.currentBasis)
    /\ snapshotId \notin q.snapshotIds
    /\ AdmitKernelPublicationRA(q.catalog,q.basis,basis,op.cause,op.target,snapshotId,q.ledger,candidateLedger,ledger,q.stack,stack,before,candidate,observer,current)
    /\ qT11'=[q EXCEPT !.basis=basis,!.ledger=ledger,!.stack=stack,!.current=current,
       !.snapshotIds=@ \cup {snapshotId},!.currentBasis=MinimalCaptureSA(basis),!.publication=receipt,!.stage=@+1]
    /\ UNCHANGED <<registryCaseSA,guideCaseT11>>

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: ConditionalBindingSA, ConditionalSnapshotFromRegistrySA, MinimalCaptureSA, AOperations, AdmitKernelPublicationRA, KernelBasisRA, PublicationAfterLedgerRA, PublicationAfterStackRA, PublicationObserverSnapshotRA, PublicationTemplateRA, registryCaseSA, guideCaseT11, qT11

ARejectionSafety · operator

reference-profile · input revision 2 · CC0 1.0

ARejectionSafety ==
 LET q==qT11 next==KernelBasisRA(q.catalog,AInitialBasis,"EntryWithdraw",KernelTargetRA(SRuleSA,2))
     replacement==[KernelBasisRA(q.catalog,next,"EntryRestore",KernelTargetRA(SRuleSA,2)) EXCEPT !.registry[2].definition.primaryCondition=2]
 IN /\ ~RegistryValidSA(q.catalog,replacement.registry)
    /\ ~KernelEffectAllowedRA(q.catalog,AInitialBasis,"PermissionRestore",KernelTargetRA(SRuleSA,0))
    /\ ~KernelEffectAllowedRA(q.catalog,AInitialBasis,"EntryRestore",KernelTargetRA(SRuleSA,2))
    /\ ~KernelEffectAllowedRA(q.catalog,AInitialBasis,"EntryWithdraw",KernelTargetRA(SCatalogSA[4].source,2))
    /\ ~KernelEffectAllowedRA(q.catalog,AInitialBasis,"EntryWithdraw",KernelTargetRA(SRuleSA,99))
    /\ ~KernelEffectAllowedRA(q.catalog,AInitialBasis,"UnknownEffect",KernelTargetRA(SRuleSA,0))

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: RegistryValidSA, AInitialBasis, KernelBasisRA, KernelEffectAllowedRA, KernelTargetRA, SCatalogSA, SRuleSA, qT11

ASeedLedger · operator

reference-profile · input revision 2 · CC0 1.0

ASeedLedger == NewConditionalLedger96([PInitialSnapshot EXCEPT !.definitions=ConditionalDefinitionsSA(SCatalogSA),
 !.present=ConditionalPresentSA(SCatalogSA),!.objects=EmptyT11,
 !.activationEpoch=[key \in DOMAIN ConditionalDefinitionsSA(SCatalogSA) |-> 0]])

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: NewConditionalLedger96, ConditionalDefinitionsSA, ConditionalPresentSA, PInitialSnapshot, SCatalogSA, EmptyT11

ASpec · operator

reference-profile · input revision 2 · CC0 1.0

ASpec == AInit /\ [][ANext]_<<qT11,registryCaseSA,guideCaseT11>> /\ WF_<<qT11,registryCaseSA,guideCaseT11>>(ANext)

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: AInit, ANext, registryCaseSA, guideCaseT11, qT11