/hoare-ledgers

Separation logic for UTXO-based blockchain ledgers

Primary LanguageAgda

Separation logic for UTXO-based blockchain ledgers CI

Browse the Agda code in HTML here.

This Agda formalization depends on formal-prelude, make sure you have it installed.

Design Approaches

Various design decisions are modelled in each sub-directory, answering the following dilemmas:

  • Shallow or deep embedding of states?

    • i.e. S : Part → ℕ or S : Map⟨ Part → ℕ ⟩

  • Shallow or deep embedding of logic formulas?

    • i.e. P : S → Set or data P : Set where ...

  • Shallow or deep embedding of Hoare triples?

    • i.e. {P}l{Q} = ∀ s. P(s) → Q(⟦l⟧s) or data {P}l{Q} where ...

  • Separate at the level of participants or values?

    • i.e. s₁ ⊎ s₂ ≈ s or s₁ ◇ s₂ ≈ s

  • Can we easily extend everything from simple linear ledgers to UTxO-based ledgers?