soma.cell

Minutes adoption — the corporate record cannot be edited after the fact

The stock-option backdating scandals of 2006 (over 130 companies under SEC investigation, CEOs of Brocade and Comverse criminally charged) ran on one quiet mechanic: board paperwork written or "fixed" AFTER the fact, dressed up as the record of an earlier date. Minutes are evidence — Delaware courts treat adopted minutes as the authoritative memory of what a board decided. Their value collapses the moment they can be revised after adoption. So adoption here is a one-way door. Amendments append to a numbered revision trail only while the draft circulates; `adopted` is a terminal state soma verify proves, and the adoption ledger holds at most one adoption per document — a second "corrected" adoption of the same minutes is a write the memory refuses.

A Soma program from the governance part of the verified corpus: 115 lines, cells MinuteBook, MinuteBookTests. It passes soma check with soma 3.2.4.

How it is built

The cell MinuteBook declares 5 signals in its face: circulate(doc: String) -> Map, amend(doc: String, change: String) -> Map, adopt(doc: String) -> Map, revision_count(doc: String) -> Int and adopted_once(doc: String) -> Bool; keeps 3 memory slots: adoptions (Map<String, Int>, persistent and consistent) under the invariant adoptions >= 0 && adoptions <= 1, revisions (Map<String, Int>, persistent and consistent) under the invariant revisions >= 0 and edit_log (Map<String, String>, persistent and consistent). Its state machine minutes starts in drafted and allows 2 transitions: drafted -> circulated and circulated -> adopted. adopted is terminal. Handlers: circulate (line 48), amend (line 55), adopt (line 66), revision_count (line 80) and adopted_once (line 84).

The file also holds 1 test cell (MinuteBookTests) with 14 assertions, run by soma test.

Generated from soma describe on this file.

The source

minutes_adoption.cell

// ============================================================================
// MINUTES ADOPTION — the corporate record cannot be edited after the fact
// ============================================================================
//
// The stock-option backdating scandals of 2006 (over 130 companies under
// SEC investigation, CEOs of Brocade and Comverse criminally charged)
// ran on one quiet mechanic: board paperwork written or "fixed" AFTER
// the fact, dressed up as the record of an earlier date. Minutes are
// evidence — Delaware courts treat adopted minutes as the authoritative
// memory of what a board decided. Their value collapses the moment they
// can be revised after adoption.
//
// So adoption here is a one-way door. Amendments append to a numbered
// revision trail only while the draft circulates; `adopted` is a
// terminal state soma verify proves, and the adoption ledger holds at
// most one adoption per document — a second "corrected" adoption of the
// same minutes is a write the memory refuses.
// ============================================================================

cell MinuteBook {
    face {
        signal circulate(doc: String) -> Map
        signal amend(doc: String, change: String) -> Map
        signal adopt(doc: String) -> Map
        signal revision_count(doc: String) -> Int
        signal adopted_once(doc: String) -> Bool
    }

    memory {
        // doc -> adoptions. AT MOST ONE: "re-adopting corrected minutes"
        // over the originals is unrepresentable.
        adoptions: Map<String, Int> [persistent, consistent]
        invariant adoptions >= 0 && adoptions <= 1

        revisions: Map<String, Int> [persistent, consistent]
        invariant revisions >= 0

        edit_log: Map<String, String> [persistent, consistent]
    }

    // drafted -> circulated (amendable, may loop) -> adopted (TERMINAL).
    state minutes {
        initial: drafted
        drafted -> circulated
        circulated -> adopted
    }

    on circulate(doc: String) {
        let r = try { transition(doc, "circulated") }
        if r.error != () { return map("ok", false, "reason", "{r.error}") }
        return map("ok", true, "state", "circulated")
    }

    // amendments are welcome — while the board is still looking at a draft
    on amend(doc: String, change: String) {
        if get_status(doc) != "circulated" {
            let s = get_status(doc)
            return map("ok", false, "reason", "minutes are {s}; the record does not bend")
        }
        let n = (revisions.get(doc) ?? 0) + 1
        revisions.set(doc, n)
        edit_log.set("{doc}:r{n}", change)
        return map("ok", true, "doc", doc, "revision", n)
    }

    on adopt(doc: String) {
        if get_status(doc) != "circulated" {
            let s = get_status(doc)
            return map("ok", false, "reason", "cannot adopt from {s}")
        }
        // THE WALL: one adoption, ever
        let w = try { adoptions.set(doc, (adoptions.get(doc) ?? 0) + 1) }
        if w.error != () {
            return map("ok", false, "reason", "{doc} was already adopted; the record stands")
        }
        transition(doc, "adopted")
        return map("ok", true, "state", "adopted", "revisions", revisions.get(doc) ?? 0)
    }

    on revision_count(doc: String) {
        return revisions.get(doc) ?? 0
    }

    on adopted_once(doc: String) {
        return (adoptions.get(doc) ?? 0) == 1
    }
}

cell test MinuteBookTests {
    rules {
        // nothing is amendable before circulation, nothing adoptable from draft
        assert amend("jan-meeting", "fix attendee list").ok == false
        assert adopt("jan-meeting").ok == false
        assert_fails transition("jan-meeting", "adopted")

        // circulate; the board marks up the draft freely
        assert circulate("jan-meeting").ok == true
        assert amend("jan-meeting", "fix attendee list").revision == 1
        assert amend("jan-meeting", "correct vote tally on item 4").revision == 2
        assert revision_count("jan-meeting") == 2

        // adoption closes the book
        assert adopt("jan-meeting").ok == true
        assert adopted_once("jan-meeting") == true

        // THE BACKDATER'S MOVE: edit after adoption. No state to do it in,
        // no path back, and a second adoption is a write the memory refuses.
        assert amend("jan-meeting", "option grant was 'always' dated June 1").ok == false
        assert_fails transition("jan-meeting", "circulated")
        assert_fails transition("jan-meeting", "drafted")
        assert_fails adoptions.set("jan-meeting", 2)
        assert revision_count("jan-meeting") == 2          // the trail is intact
    }
}

What the toolchain says

Run on a fresh copy of the program at build time; the outputs are pasted unedited.

$ soma check minutes_adoption.cell
✓ All checks passed.
$ soma test minutes_adoption.cell
test MinuteBookTests ...
  ✓ assert amend("jan-meeting", "fix attendee list").ok == false
  ✓ assert adopt("jan-meeting").ok == false
  ✓ assert_fails transition("jan-meeting", "adopted") — raised invalid transition: drafted → adopted. Current state: 'drafted'. Valid targets: [circulated]
  ✓ assert circulate("jan-meeting").ok == true
  ✓ assert amend("jan-meeting", "fix attendee list").revision == 1
  ✓ assert amend("jan-meeting", "correct vote tally on item 4").revision == 2
  ✓ assert revision_count("jan-meeting") == 2
  ✓ assert adopt("jan-meeting").ok == true
  ✓ assert adopted_once("jan-meeting") == true
  ✓ assert amend("jan-meeting", "option grant was 'always' dated June 1").ok == false
  ✓ assert_fails transition("jan-meeting", "circulated") — raised invalid transition: adopted → circulated. Current state: 'adopted'. Valid targets: []
  ✓ assert_fails transition("jan-meeting", "drafted") — raised invalid transition: adopted → drafted. Current state: 'adopted'. Valid targets: []
  ✓ assert_fails adoptions.set("jan-meeting", 2) — raised memory invariant violated on 'adoptions': adoptions >= 0 && adoptions <= 1 — rejected write of 2 (key "jan-meeting"); the slot is unchanged
  ✓ assert revision_count("jan-meeting") == 2

14 tests: 14 passed, 0 failed
$ soma verify minutes_adoption.cell
Verifying minutes_adoption.cell...

State machine 'minutes': 3 states, initial 'drafted'
  States: [adopted, circulated, drafted]

  ✓ 3 states, 2 transitions
  ✓ all states reachable from 'drafted'
  ✓ terminal states: [adopted]
  ✓ no deadlocks
  ✓ liveness: every state can eventually reach a terminal state
  ✓ think-isolated: CTL safety properties hold regardless of LLM output (2 handlers, 2 literal transitions, 0 dynamic)
  ✓ termination: all 5 handlers structurally terminate
  ✓ refinement: handler `circulate` ⟶ {circulated}
  ✓ refinement: handler `adopt` ⟶ {circulated → adopted}
  · transition sources: `circulate` calls transition(id, target) without declaring the source — the runtime refuses a move the graph forbids, but the proof does not see where the handler starts; `transition(id, from, to)` names the edge (checked by `soma check`, refused at run time from any other state)

MinuteBook/invariants:

  ✓ invariant adoptions >= 0 — writer 'adopt' proven by induction (writes (adoptions.get(doc) ?? 0) + 1)
  ⚠ invariant adoptions >= 0 && adoptions <= 1 — runtime-checked (computed values): adopt → adoptions [adoptions <= 1] because `adoptions` has no known range
  ✓ invariant revisions >= 0 — writer 'amend' proven by induction (writes n)

11 passed, 1 warnings, 0 failures

  Temporal properties for 'minutes':
  ✓ deadlock_free — no deadlocks in any reachable state
Temporal: 1 passed, 0 failed
VERIFY OK

Builtins used

get_status, map, transition

Source file: /corpus/governance/minutes_adoption.cell · examples/corpus/governance/minutes_adoption.cell