Skip to content

Delta

Delta proof structures for transaction validation.

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

module Goose.Anoma.Delta where

open import Foundation.BasicTypes 
open import Goose.Anoma.Compliance

Delta Proof

DeltaProof : Set
DeltaProof = String

Delta Witness

record DeltaWitness : Set where
  field
    signingKey : String

open DeltaWitness public

From Compliance Witnesses

fromComplianceWitnesses : List ComplianceWitness → DeltaWitness
fromComplianceWitnesses witnesses = record
  { signingKey = foldr _++ˢ_ "" (map (λ w → w .rcv) witnesses) }

Delta Witness Composition

compose : DeltaWitness → DeltaWitness → DeltaWitness
compose w1 w2 = record { signingKey = w1 .signingKey ++ˢ w2 .signingKey }

Empty Delta Witness

empty : DeltaWitness
empty = record { signingKey = "" }
Module References

Referenced By

This module is referenced by:

References

This module references: