Skip to content

Failure

[9 of 9] Compiling arch.node.engines.commitment_environment /home/runner/work/nspec/nspec/docs/arch/node/engines/commitment_environment.juvix.md:99:7-11: error: Unexpected argument node


icon: octicons/container-24 search: exclude: false categories: - engine-behaviour tags: - commitment - engine-environment


Juvix imports
module arch.node.engines.commitment_environment;
import prelude open;
import arch.system.identity.identity open using {Signer; mkSigner};
import arch.node.engines.commitment_messages open;
import arch.node.types.crypto open;
import arch.node.types.engine_environment open;
import arch.node.types.identities open;
import arch.node.types.messages open;

Commitment Environment

Overview

The Commitment Engine environment maintains the state necessary for generating commitments (signatures) for a specific identity. It includes the identity's signing capabilities and any necessary signing keys or handles.

Mailbox states

The Commitment Engine does not require complex mailbox states. We define the mailbox state as Unit.

CommitmentMailboxState

syntax alias CommitmentMailboxState := Unit;

Local state

The local state of a Commitment Engine instance includes the identity's signing capabilities.

CommitmentLocalState

type CommitmentLocalState := mkCommitmentLocalState@{
  signer : Signer Backend Signable Commitment;
  backend : Backend;
};
Arguments
signer:
The signer for the identity.
backend:
The backend to use for signing.

Timer Handle

The Commitment Engine does not require a timer handle type. Therefore, we define the timer handle type as Unit.

CommitmentTimerHandle

syntax alias CommitmentTimerHandle := Unit;

The Commitment Environment

CommitmentEnvironment

CommitmentEnvironment : Type :=
  EngineEnv
    CommitmentLocalState
    CommitmentMailboxState
    CommitmentTimerHandle;

Instantiation

module commitment_environment_example;

axiom dummyExternalIdentity : ExternalIdentity;
axiom dummyIDBackend : Backend;
axiom dummySigningKey : SigningKey;

commitmentEnvironment : CommitmentEnvironment :=
    mkEngineEnv@{
      node := Curve25519PubKey "0xabcd1234";
      name := "commitment";
      localState := mkCommitmentLocalState@{
        signer := mkSigner@{
          sign := \{_ x := Ed25519Signature "0xabcd1234"};
        };
        backend := BackendLocalMemory;
      };
      mailboxCluster := Map.empty;
      acquaintances := Set.empty;
      timers := []
    }
  ;
end;