This page records a log of the contributors work, thinking, discussions, meeting notes, .. anything really. It's supposed to be a [Stream of
consciousness](https://en.wikipedia.org/wiki/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.