module arch.node.engines.wall_clock_environment;

import prelude open;
import arch.node.engines.wall_clock_messages open;
import arch.node.types.engine open;
import arch.node.types.messages open;
import arch.node.types.identities open;
import arch.node.types.anoma_message as Anoma open;

Wall Clock Environment¶

Overview¶

The Local Wall Clock Engine provides and keeps track of a local time.

Mailbox states¶

The wall clock engine does not require complex mailbox states. We define the mailbox state as Unit.

syntax alias WallClockMailboxState := Unit;

Local state¶

type WallClockLocalState := mkWallClockLocalState@{currentTime : EpochTimestamp};

Timer Handle¶

The wall clock engine does not require a timer handle type. Therefore, we define the timer handle type as Unit.

syntax alias WallClockTimerHandle := Unit;

The Wall Clock Environment¶

Auxiliary abstraction Functions¶

axiom advanceTime : EpochTimestamp -> EpochTimestamp;

WallClockEnv¶

WallClockEnv : Type :=
  EngineEnv
    WallClockLocalState
    WallClockMailboxState
    WallClockTimerHandle
    Anoma.Msg;

Instantiation¶

wallClockEnv : WallClockEnv :=
  mkEngineEnv@{
    localState :=
      mkWallClockLocalState@{
        currentTime := 0;
      };
    mailboxCluster := Map.empty;
    acquaintances := Set.empty;
    timers := [];
  };