structure Output : Type

• addr : Address
• value : Value
• datum : Option Data

instance instDecidableEqOutput : DecidableEq Output

Equations

• instDecidableEqOutput = instDecidableEqOutput.decEq

def instDecidableEqOutput.decEq (x✝ x✝¹ : Output) : Decidable (x✝ = x✝¹)

Equations

• One or more equations did not get rendered due to their size.

def instHashableOutput.hash : Output → UInt64

Equations

• instHashableOutput.hash { addr := a, value := a_1, datum := a_2 } = mixHash (mixHash (mixHash 0 (hash a)) (hash a_1)) (hash a_2)

instance instHashableOutput : Hashable Output

Equations

• instHashableOutput = { hash := instHashableOutput.hash }

structure OutputRef : Type

• id : TxId
• index : ℕ

instance instDecidableEqOutputRef : DecidableEq OutputRef

Equations

• instDecidableEqOutputRef = instDecidableEqOutputRef.decEq

def instDecidableEqOutputRef.decEq (x✝ x✝¹ : OutputRef) : Decidable (x✝ = x✝¹)

Equations

• instDecidableEqOutputRef.decEq { id := a, index := a_1 } { id := b, index := b_1 } = if h : a = b then h ▸ if h : a_1 = b_1 then h ▸ isTrue ⋯ else isFalse ⋯ else isFalse ⋯

instance instHashableOutputRef : Hashable OutputRef

Equations

• instHashableOutputRef = { hash := instHashableOutputRef.hash }

def instHashableOutputRef.hash : OutputRef → UInt64

Equations

• instHashableOutputRef.hash { id := a, index := a_1 } = mixHash (mixHash 0 (hash a)) (hash a_1)

instance instLEOutputRef : LE OutputRef

Equations

• instLEOutputRef = { le := fun (r1 r2 : OutputRef) => r1.id < r2.id ∨ r1.id = r2.id ∧ r1.index ≤ r2.index }

structure Transaction_Prime (Arg : Type) : Type

• inputs : Arg
• outputs : List Output
• validityInternal : TimeInterval
• signer_hashes : List VKeyHash
• fees : Value

def instBEqTransaction_Prime.beq {Arg✝ : Type} [BEq Arg✝] : Transaction_Prime Arg✝ → Transaction_Prime Arg✝ → Bool

Equations

• One or more equations did not get rendered due to their size.
• instBEqTransaction_Prime.beq x✝¹ x✝ = false

instance instBEqTransaction_Prime {Arg✝ : Type} [BEq Arg✝] : BEq (Transaction_Prime Arg✝)

Equations

• instBEqTransaction_Prime = { beq := instBEqTransaction_Prime.beq }

instance instHashableTransaction_Prime {Arg✝ : Type} [Hashable Arg✝] : Hashable (Transaction_Prime Arg✝)

Equations

• instHashableTransaction_Prime = { hash := instHashableTransaction_Prime.hash }

def instHashableTransaction_Prime.hash {Arg✝ : Type} [Hashable Arg✝] : Transaction_Prime Arg✝ → UInt64

Equations

• One or more equations did not get rendered due to their size.

@[reducible, inline]

abbrev Transaction : Type

Equations

• Transaction = Transaction_Prime (Finset OutputRef)

@[reducible, inline]

abbrev FlattenTransaction : Type

Equations

• FlattenTransaction = Transaction_Prime (List OutputRef)

instance instHashableFlattenTransaction : Hashable FlattenTransaction

Equations

• instHashableFlattenTransaction = instHashableTransaction_Prime

structure InputInfo : Type

• validityInternal : TimeInterval
• value : Value
• fee : Value
• validator : VKeyHash
• txId : TxId

def InputInfo.empty : InputInfo

Equations

• InputInfo.empty = { validityInternal := TimeInterval.always, value := 0, fee := 0, validator := 0, txId := 0 }

structure InfoActions (α : Type) : Type

• act : α
• info : InputInfo

def Transaction.empty : Transaction

Equations

• Transaction.empty = { inputs := ∅, outputs := [], validityInternal := { lower := none, upper := none }, signer_hashes := [], fees := 0 }

@[reducible, inline]

abbrev UtxoSet : Type

Equations

• UtxoSet = List (OutputRef × Output)

def UtxoBlockchain : Type 1

Equations

• UtxoBlockchain = (UtxoSet → Transaction → UtxoSet → Type)

def TransactionHash.flatten_tx_hash (ft : FlattenTransaction) : UInt64

Equations

• TransactionHash.flatten_tx_hash ft = hash ft

axiom TransactionHash.tx_hash : Transaction → Hash_64

axiom TransactionHash.flat_tx_hash : FlattenTransaction → Hash_64

axiom TransactionHash.tx_hash_same (t1 t2 : Transaction) : tx_hash t1 = tx_hash t2 → t1 = t2

axiom TransactionHash.flat_tx_hash_same (t1 t2 : FlattenTransaction) : flat_tx_hash t1 = flat_tx_hash t2 → t1 = t2

axiom TransactionHash.output_hash : Output → Hash_64

axiom TransactionHash.output_hash_same (o o' : Output) : output_hash o = output_hash o' → o = o'