module arch.system.types.nullifier_properties;

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

axiom computeNullifier : Resource -> NullifierKey -> Digest;

axiom nullifierHash : Nullifier -> Digest;

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