module arch.system.types.nullifier;

import prelude open;
import arch.system.types.resource open;
import arch.system.types.nullifierkey open;
import arch.node.types.crypto open;

Nullifiers¶

A resource nullifier or nullifier for short is a term of type Nullifier. Each nullifier is data consisting of a key and the resource it is associated with.

Nullifier¶

type Nullifier :=
  mkNullifier@{
    key : NullifierKey;
    resource : Resource;
  };

deriving instance
nullifierEq : Eq Nullifier;

deriving instance
nullifierOrd : Ord Nullifier;

Purpose¶

Nullifiers prevent double-spending by:

1. Uniquely identifying consumed resources when stored in the nullifier set part of the state.

2. Requiring two factors to consume a resource, that is:

   • A nullifier key matching the resource's nullifier key commitment.
   • The resource nullifier must not exist in the nullifier set.

Properties¶

axiom computeNullifier : Resource -> NullifierKey -> Digest;

axiom nullifierHash : Nullifier -> Digest;

The following properties must hold true to consider a nullifier valid:

Nullifier key must match the resource's nullifier key commitment¶

match-nullifier-key (r : Resource) (nk : NullifierKey) : Bool :=
  let
    n :=
      mkNullifier@{
        key := nk;
        resource := r;
      };
  in computeNullifier r nk == nullifierHash n;

Nullifier must not exist in the nullifier set¶

unique-nullifier-property
  (s : State)
  (r : Resource)
  (nk : NullifierKey) : Bool :=
  let nullifier := mkNullifier@{key := nk; resource := r};
      nullifierSet : Set Nullifier := State.nullifierSet s;
      cond (other : Nullifier) : Bool := (Set.isMember other nullifierSet) && (other == nullifier)
  in not (all cond (n in nullifierSet));