Compliance

view source: Compliance.lagda.md

Compliance structures for zero-knowledge proofs in the Anoma Resource Machine.

{-# OPTIONS --without-K --type-in-type #-}

module RM.Types.Compliance where

open import Foundation.BasicTypes
open import RM.Types.Resource
open import RM.Types.NullifierKey

Merkle Path

MerklePath : Set
MerklePath = List ℕ

Compliance Witness

record ComplianceWitness : Set where
  field
    consumedResource : Resource
    createdResource : Resource
    nfKey : NullifierKey
    rcv : String
    merklePath : MerklePath
    ephemeralRoot : String

open ComplianceWitness public

Compliance Instance

record ComplianceInstance : Set where

open ComplianceInstance public

Compliance Proof

ComplianceProof : Set
ComplianceProof = String

Compliance Unit

record ComplianceUnit : Set where
  field
    proof : ComplianceProof
    inst : ComplianceInstance

open ComplianceUnit public

Create Compliance Unit

createComplianceUnit : ComplianceWitness → ComplianceUnit
createComplianceUnit witness = record
  { proof = ""
  ; inst = record {} }

Note: Placeholder implementation for proof generation.

Module References

Referenced By

This module is referenced by:

• RM.Types.Action
  • Symbols: ComplianceUnit
• RM.Types.Delta
  • Symbols: ComplianceWitness

References

This module references:

• Foundation.BasicTypes
  • Imports: List, ℕ
• RM.Types.NullifierKey
  • Imports: NullifierKey
• RM.Types.Resource
  • Imports: Resource