Skip to content

Logbook

Jump to bottom
Sebastian Nagel edited this page Feb 10, 2025 · 3 revisions

This page records a log of the contributors work, thinking, discussions, meeting notes, .. anything really. It's supposed to be a Stream of consciousness that can read, searched, or referenced if needed.

It is not a complete record of things happening and entirely opt-in.

2025-02-10

SN chat with Andre

  • Ledger specs in Agda - Formalisation started before Conway
    • Conway features got prioritized to get a conway spec
    • LaTeX as fallback as previous specs were done that way
  • Interface to ledger team?
    • Ledger reads and implements the spec
    • In parts 1:1, even anticipating problems with solutions, implementors simplify and only get into the insight after simplifying
    • Performance sometimes reason for divergence
      • eg. counting votes for governance actions
      • in principle: count all at once, but rollbacks across epoch boundaries would result int multiple counts
      • instead delay things to distribute work
    • Implementation (of STS rules) is tested against spec
      • Agda compiled into a Haskell lib
      • Constraint based generators to generate transitions of individual STS relations
      • Bi-simulation of Agda (spec) lib and Haskell implementation
      • Slight variant of the Agda spec that is actually used for the tests - which is checked through Agda equivalence
        • Provability of this variant is less good
        • State is better aligned with implementation in this variant
        • Deposit migration to conway was an example for this
  • What's the overall interface?
    • A pure function that transforms state through transations
    • Consensus interfaces: applyTx and tick (?)
    • In shelley spec though: CHAIN sts defines how a block is processed
    • New consensus spec: using same style as ledger spec (Javier?)
      • Should be fairly complete, quite small
    • Refining the interface of ledger to the consensus spec
      • BBODY and TICK?
  • Conformance tests using bi-simulation a good idea?
    • Hard to write good generators for tests -> with good "resolution"
    • Positive and negative testing
    • Quantity vs. Quality? (generators vs. labeled test data)
  • Similar approach to equivalent agda model thinkable for other implementation "style"
    • To peek "into the blackbox" which you would get from the bi-simulation approach (at a high level)
  • Using the Agda model directly (Haskell or WASM backends)?
    • Hopes are high on lambdabox
    • Unrealistic to use as implementation directly -> performance!
    • Obvious performance problems in Agda (e.g. set theory is good for provability, not performance)
      • Could improve, but never going to be at par (80/20 rule!?)
      • MAlonzo code is about 50% to hand-written Haskell
    • More flexible to get "oracles" in various target contexts, i.e. compile to a native library to compare with
    • Also interesting to test the model against real, historic data
  • How to get people to accept the ledger specs as ground truth?

    • Explained such that you "want to implement it"

    • Test driver included

    • Interactive model? A sandbox to play with? -> a playground

      • How does the Agda model deal with a transaction we "click together"
      • Could be used to collect transaction test data?
      • Also to understand the model (Agda repl?)

    • Simplified ledger: a subset formal spec that contains the core things and which would validate only parts and core functionality -> could be used as an easier entry and use Agda to ensure it is a proper subset

    • In summary: we rather be unhappy about some things (to make it useful for others), than dogmatic, obscure and unused.

Clone this wiki locally