Data Layer

Simple representation of the Data Layer functionality as a Hash-reversal function. We are missing the (deterministic) hash oracle definitions, how to add elemets to the maps.

structure DataLayer.DA : Type

• utxo : NHash → Option (List OutputRef)
• transaction : NHash → Option (List TxId)
• wts : NHash → Option Withdrawals

def DataLayer.DA.init : DA

Equations

• DataLayer.DA.init = { utxo := fun (x : NHash) => none, transaction := fun (x : NHash) => none, wts := fun (x : NHash) => none }