Skip to content

Nullifier Key

A secret value used to assign ownership to a resource.

{-# OPTIONS --without-K #-}

module RM.Types.NullifierKey where

open import Foundation.BasicTypes

Nullifier Key

data NullifierKey : Set where
  universal : NullifierKey
  secret    : ℕ → NullifierKey

Nullifier Key Commitment

Commitment to a nullifier key used to prove ownership without revealing the key.

data NullifierKeyCommitment : Set where
  universal : NullifierKeyCommitment
  ofSecret  : ℕ → NullifierKeyCommitment

Nullifier Key Matches Commitment

Proof that a NullifierKey matches a NullifierKeyCommitment.

data NullifierKeyMatchesCommitment : NullifierKey → NullifierKeyCommitment → Set where
  universal : NullifierKeyMatchesCommitment universal universal
  secret    : {n m : ℕ} → n ≡ m → NullifierKeyMatchesCommitment (secret n) (ofSecret m)

Decidable Nullifier Key Check

checkNullifierKey : (key : NullifierKey) → (nfc : NullifierKeyCommitment)
  → Dec (NullifierKeyMatchesCommitment key nfc)
checkNullifierKey universal universal = yes universal
checkNullifierKey universal (ofSecret _) = no (λ ())
checkNullifierKey (secret _) universal = no (λ ())
checkNullifierKey (secret n) (ofSecret m) with n ≟ℕ m
... | yes p = yes (secret p)
... | no ¬p = no (λ { (secret p) → ¬p p })

Nullifier Key Commitment Function

Computes the commitment of a NullifierKey.

commitment : NullifierKey → NullifierKeyCommitment
commitment universal  = universal
commitment (secret s) = ofSecret s
Module References

Referenced By

This module is referenced by:

References

This module references: