ActivityPublication

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.

observed · operator

reference-profile · input revision 2 · CC0 1.0

observed==PublicationEpochLedgerRA(before,candidate,beforeSnapshot,candidateSnapshot)

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: PublicationEpochLedgerRA

snapshot · operator

reference-profile · input revision 2 · CC0 1.0

snapshot==PublicationObserverSnapshotRA(before,candidate,beforeSnapshot,candidateSnapshot)

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: PublicationObserverSnapshotRA

lost · operator

reference-profile · input revision 2 · CC0 1.0

lost=={id \in beforeStack[i].pending \cap DOMAIN beforeLedger.instances : afterLedger.instances[id].status # "Pending"}

Exact module download · Source bundle and reproduction instructions

keys · operator

reference-profile · input revision 2 · CC0 1.0

keys==DOMAIN before.activationEpoch \cup DOMAIN beforeSnapshot.definitions \cup DOMAIN candidateSnapshot.definitions

Exact module download · Source bundle and reproduction instructions

lost · operator

reference-profile · input revision 2 · CC0 1.0

lost==ConditionalActivityLosses96(beforeSnapshot,candidateSnapshot)

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: ConditionalActivityLosses96

observed · operator

reference-profile · input revision 2 · CC0 1.0

observed==PublicationEpochLedgerRA(before,candidate,beforeSnapshot,candidateSnapshot)

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: PublicationEpochLedgerRA

AdmitKernelPublicationRA · operator

reference-profile · input revision 2 · CC0 1.0

AdmitKernelPublicationRA(catalog,beforeBasis,afterBasis,cause,target,snapshotId,
 beforeLedger,candidateLedger,afterLedger,beforeStack,afterStack,
 beforeSnapshot,candidateSnapshot,observerSnapshot,currentSnapshot) ==
 /\ snapshotId \in Nat \ {0} /\ snapshotId # beforeSnapshot.id
 /\ KernelEffectAllowedRA(catalog,beforeBasis,cause,target)
 /\ afterBasis=KernelBasisRA(catalog,beforeBasis,cause,target) /\ BasisValidSA(catalog,afterBasis)
 /\ LedgerDomainSA(beforeLedger) /\ candidateLedger=beforeLedger
 /\ beforeSnapshot=ConditionalSnapshotFromRegistrySA(catalog,beforeBasis,beforeLedger,beforeSnapshot)
 /\ candidateSnapshot=ConditionalSnapshotFromRegistrySA(catalog,afterBasis,candidateLedger,
       PublicationTemplateRA(beforeSnapshot,snapshotId))
 /\ observerSnapshot=PublicationObserverSnapshotRA(beforeLedger,candidateLedger,beforeSnapshot,candidateSnapshot)
 /\ ObserveConditionalActivity96(beforeLedger,candidateLedger,afterLedger,beforeStack,afterStack,beforeSnapshot,observerSnapshot)
 /\ currentSnapshot=ConditionalSnapshotFromRegistrySA(catalog,afterBasis,afterLedger,observerSnapshot)

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: ObserveConditionalActivity96, BasisValidSA, ConditionalSnapshotFromRegistrySA, LedgerDomainSA, KernelBasisRA, KernelEffectAllowedRA, PublicationObserverSnapshotRA, PublicationTemplateRA

KernelBasisRA · operator

reference-profile · input revision 2 · CC0 1.0

KernelBasisRA(catalog,basis,cause,target) ==
 [basis EXCEPT !.revision=@+1,
  !.rulePermissions=CASE cause="PermissionWithdraw" -> @ \ {target.source.rule}
                    [] cause="PermissionRestore" -> @ \cup {target.source.rule} [] OTHER -> @,
  !.registry=CASE cause="EntryWithdraw" -> [key \in DOMAIN @ \ {target.entry} |-> @[key]]
              [] cause="EntryRestore" -> [key \in DOMAIN @ \cup {target.entry} |->
                   IF key=target.entry THEN catalog[key] ELSE @[key]] [] OTHER -> @]

Exact module download · Source bundle and reproduction instructions

KernelEffectAllowedRA · operator

reference-profile · input revision 2 · CC0 1.0

KernelEffectAllowedRA(catalog,basis,cause,target) ==
 IF ~BasisValidSA(catalog,basis) THEN FALSE
 ELSE IF ~RecordFieldsSA(target,{"source","entry"}) THEN FALSE
 ELSE IF ~RuleSourceValidSA(target.source) THEN FALSE
 ELSE IF ~IsNaturalValueSA(target.entry) THEN FALSE
 ELSE IF cause \in {"PermissionWithdraw","PermissionRestore"} THEN
   /\ target.entry=0 /\ target.source \in {catalog[key].source : key \in DOMAIN catalog}
   /\ IF cause="PermissionWithdraw" THEN target.source.rule \in basis.rulePermissions
      ELSE target.source.rule \notin basis.rulePermissions
 ELSE IF cause \in {"EntryWithdraw","EntryRestore"} THEN
   IF target.entry \notin DOMAIN catalog THEN FALSE
   ELSE /\ target.source=catalog[target.entry].source
        /\ IF cause="EntryWithdraw" THEN target.entry \in DOMAIN basis.registry
           ELSE target.entry \notin DOMAIN basis.registry
 ELSE FALSE

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: BasisValidSA, IsNaturalValueSA, RecordFieldsSA, RuleSourceValidSA

KernelTargetRA · operator

reference-profile · input revision 2 · CC0 1.0

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

Exact module download · Source bundle and reproduction instructions

PublicationAfterLedgerRA · operator

reference-profile · input revision 2 · CC0 1.0

PublicationAfterLedgerRA(before,candidate,beforeSnapshot,candidateSnapshot) ==
 LET snapshot==PublicationObserverSnapshotRA(before,candidate,beforeSnapshot,candidateSnapshot)
     observed==PublicationEpochLedgerRA(before,candidate,beforeSnapshot,candidateSnapshot)
 IN ConditionalActivityLedger96(observed,snapshot.definitions,snapshot)

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: ConditionalActivityLedger96, observed, snapshot

PublicationAfterStackRA · operator

reference-profile · input revision 2 · CC0 1.0

PublicationAfterStackRA(beforeStack,beforeLedger,afterLedger) ==
 [i \in 1..Len(beforeStack) |->
   LET lost=={id \in beforeStack[i].pending \cap DOMAIN beforeLedger.instances : afterLedger.instances[id].status # "Pending"}
   IN [beforeStack[i] EXCEPT !.pending=@ \ lost,!.lostPending=@ \cup lost]]

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: lost

PublicationEpochLedgerRA · operator

reference-profile · input revision 2 · CC0 1.0

PublicationEpochLedgerRA(before,candidate,beforeSnapshot,candidateSnapshot) ==
 LET lost==ConditionalActivityLosses96(beforeSnapshot,candidateSnapshot)
     keys==DOMAIN before.activationEpoch \cup DOMAIN beforeSnapshot.definitions \cup DOMAIN candidateSnapshot.definitions
 IN [candidate EXCEPT
   !.activationEpoch=[key \in keys |-> (IF key \in DOMAIN before.activationEpoch THEN before.activationEpoch[key] ELSE 0)+(IF key \in lost THEN 1 ELSE 0)],
   !.activationSerial=before.activationSerial+(IF lost={} THEN 0 ELSE 1)]

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: keys, lost

PublicationObserverSnapshotRA · operator

reference-profile · input revision 2 · CC0 1.0

PublicationObserverSnapshotRA(before,candidate,beforeSnapshot,candidateSnapshot) ==
 LET observed==PublicationEpochLedgerRA(before,candidate,beforeSnapshot,candidateSnapshot)
 IN [candidateSnapshot EXCEPT !.activationEpoch=observed.activationEpoch,!.activationSerial=observed.activationSerial]

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: observed

PublicationTemplateRA · operator

reference-profile · input revision 2 · CC0 1.0

PublicationTemplateRA(snapshot,snapshotId) ==
 [snapshot EXCEPT !.id=snapshotId,!.point="NormalizedKernelPublication"]

Exact module download · Source bundle and reproduction instructions