soma.cell

Peer review — double-blind where the blind cannot be lifted early

Double-blind review exists because the data says it must: when reviewers see author names, papers from famous labs are accepted at measurably higher rates (the NeurIPS 2014 and 2021 consistency experiments put numbers on how noisy and biased single-blind judging is). The whole mechanism collapses on two failure modes: an author reviewing their own paper under a conflict, and the author's identity leaking to the reviewer BEFORE the decision is locked. Both are structural here. A reviewer/author pair can hold at most one role on a paper — self-review is a write the memory refuses. And `unmasked` is reachable ONLY from `decided`: there is no edge from any pre-decision state to the unmasked world. soma verify proves it.

A Soma program from the governance part of the verified corpus: 132 lines, cells ReviewDesk, BlindTests. It passes soma check with soma 3.2.4.

How it is built

The cell ReviewDesk declares 6 signals in its face: submit_paper(paper: String, author: String) -> Map, assign_reviewer(paper: String, reviewer: String) -> Map, decide(paper: String, accept: Bool) -> Map, lift_blind(paper: String) -> Map, author_of(paper: String) -> String and verdict_of(paper: String) -> String; keeps 3 memory slots: blind_roles (Map<String, Int>, persistent and consistent) under the invariant blind_roles >= 0 && blind_roles <= 1, authors (Map<String, String>, persistent and consistent) and verdicts (Map<String, String>, persistent and consistent). Its state machine blind starts in sealed and allows 3 transitions: sealed -> in_review, in_review -> decided and decided -> unmasked. unmasked is terminal. Handlers: submit_paper (line 49), assign_reviewer (line 58), decide (line 73), lift_blind (line 81), author_of (line 88) and verdict_of (line 95).

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

Generated from soma describe on this file.

The source

peer_review.cell

// ============================================================================
// PEER REVIEW — double-blind where the blind cannot be lifted early
// ============================================================================
//
// Double-blind review exists because the data says it must: when
// reviewers see author names, papers from famous labs are accepted at
// measurably higher rates (the NeurIPS 2014 and 2021 consistency
// experiments put numbers on how noisy and biased single-blind judging
// is). The whole mechanism collapses on two failure modes: an author
// reviewing their own paper under a conflict, and the author's identity
// leaking to the reviewer BEFORE the decision is locked.
//
// Both are structural here. A reviewer/author pair can hold at most one
// role on a paper — self-review is a write the memory refuses. And
// `unmasked` is reachable ONLY from `decided`: there is no edge from any
// pre-decision state to the unmasked world. soma verify proves it.
// ============================================================================

cell ReviewDesk {
    face {
        signal submit_paper(paper: String, author: String) -> Map
        signal assign_reviewer(paper: String, reviewer: String) -> Map
        signal decide(paper: String, accept: Bool) -> Map
        signal lift_blind(paper: String) -> Map
        signal author_of(paper: String) -> String
        signal verdict_of(paper: String) -> String
    }

    memory {
        // paper:person -> roles held (author or reviewer). A 2 — the
        // same person on both sides of the blind — is unrepresentable.
        blind_roles: Map<String, Int> [persistent, consistent]
        invariant blind_roles >= 0 && blind_roles <= 1

        authors: Map<String, String> [persistent, consistent]
        verdicts: Map<String, String> [persistent, consistent]
    }

    // The blind is a place in the machine, not a flag. There is NO edge
    // from sealed/in_review to unmasked: identity stays behind the
    // decision. unmasked is terminal — once lifted, the record is final.
    state blind {
        initial: sealed
        sealed -> in_review
        in_review -> decided
        decided -> unmasked
    }

    on submit_paper(paper: String, author: String) {
        if authors.get(paper) != () {
            return map("ok", false, "reason", "paper {paper} already submitted")
        }
        authors.set(paper, author)
        blind_roles.set("{paper}:{author}", 1)
        return map("ok", true, "paper", paper)
    }

    on assign_reviewer(paper: String, reviewer: String) {
        if get_status(paper) != "sealed" {
            let s = get_status(paper)
            return map("ok", false, "reason", "cannot assign in state {s}")
        }
        // THE WALL: if the reviewer wrote the paper, this write is a 2
        let k = "{paper}:{reviewer}"
        let w = try { blind_roles.set(k, (blind_roles.get(k) ?? 0) + 1) }
        if w.error != () {
            return map("ok", false, "reason", "conflict: {reviewer} cannot review their own paper")
        }
        transition(paper, "in_review")
        return map("ok", true, "reviewer", reviewer)
    }

    on decide(paper: String, accept: Bool) {
        let r = try { transition(paper, "decided") }
        if r.error != () { return map("ok", false, "reason", "{r.error}") }
        if accept { verdicts.set(paper, "accept") }
        if !accept { verdicts.set(paper, "reject") }
        return map("ok", true, "verdict", verdicts.get(paper))
    }

    on lift_blind(paper: String) {
        let r = try { transition(paper, "unmasked") }
        if r.error != () { return map("ok", false, "reason", "{r.error}") }
        return map("ok", true, "author", authors.get(paper))
    }

    // identity is served ONLY past the decision — the machine is the gate
    on author_of(paper: String) {
        if get_status(paper) != "unmasked" {
            return "[REDACTED]"
        }
        return authors.get(paper) ?? "[unknown]"
    }

    on verdict_of(paper: String) {
        return verdicts.get(paper) ?? "pending"
    }
}

cell test BlindTests {
    rules {
        assert submit_paper("P7", "prof_x").ok == true
        assert submit_paper("P7", "prof_x").ok == false       // no resubmission

        // self-review: the role ledger cannot hold the 2
        assert assign_reviewer("P7", "prof_x").ok == false
        assert_fails blind_roles.set("P7:prof_x", 2)
        assert get_status("P7") == "sealed"

        // the blind cannot be lifted before a decision — no such edge
        assert_fails transition("P7", "unmasked")
        assert author_of("P7") == "[REDACTED]"

        // an honest reviewer goes through; identity still sealed
        assert assign_reviewer("P7", "dr_y").ok == true
        assert_fails transition("P7", "unmasked")             // mid-review leak: no edge
        assert author_of("P7") == "[REDACTED]"
        assert lift_blind("P7").ok == false

        // decision locks the verdict; only THEN may the blind lift
        assert decide("P7", true).verdict == "accept"
        assert author_of("P7") == "[REDACTED]"                // decided != unmasked yet
        assert lift_blind("P7").ok == true
        assert author_of("P7") == "prof_x"

        // unmasked is terminal: the record cannot re-enter review
        assert_fails transition("P7", "in_review")
        assert_fails transition("P7", "sealed")
        assert verdict_of("P7") == "accept"
    }
}

What the toolchain says

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

$ soma check peer_review.cell
✓ All checks passed.
$ soma test peer_review.cell
test BlindTests ...
  ✓ assert submit_paper("P7", "prof_x").ok == true
  ✓ assert submit_paper("P7", "prof_x").ok == false
  ✓ assert assign_reviewer("P7", "prof_x").ok == false
  ✓ assert_fails blind_roles.set("P7:prof_x", 2) — raised memory invariant violated on 'blind_roles': blind_roles >= 0 && blind_roles <= 1 — rejected write of 2 (key "P7:prof_x"); the slot is unchanged
  ✓ assert get_status("P7") == "sealed"
  ✓ assert_fails transition("P7", "unmasked") — raised invalid transition: sealed → unmasked. Current state: 'sealed'. Valid targets: [in_review]
  ✓ assert author_of("P7") == "[REDACTED]"
  ✓ assert assign_reviewer("P7", "dr_y").ok == true
  ✓ assert_fails transition("P7", "unmasked") — raised invalid transition: in_review → unmasked. Current state: 'in_review'. Valid targets: [decided]
  ✓ assert author_of("P7") == "[REDACTED]"
  ✓ assert lift_blind("P7").ok == false
  ✓ assert decide("P7", true).verdict == "accept"
  ✓ assert author_of("P7") == "[REDACTED]"
  ✓ assert lift_blind("P7").ok == true
  ✓ assert author_of("P7") == "prof_x"
  ✓ assert_fails transition("P7", "in_review") — raised invalid transition: unmasked → in_review. Current state: 'unmasked'. Valid targets: []
  ✓ assert_fails transition("P7", "sealed") — raised invalid transition: unmasked → sealed. Current state: 'unmasked'. Valid targets: []
  ✓ assert verdict_of("P7") == "accept"

18 tests: 18 passed, 0 failed
$ soma verify peer_review.cell
Verifying peer_review.cell...

State machine 'blind': 4 states, initial 'sealed'
  States: [decided, in_review, sealed, unmasked]

  ✓ 4 states, 3 transitions
  ✓ all states reachable from 'sealed'
  ✓ terminal states: [unmasked]
  ✓ no deadlocks
  ✓ liveness: every state can eventually reach a terminal state
  ✓ think-isolated: CTL safety properties hold regardless of LLM output (3 handlers, 3 literal transitions, 0 dynamic)
  ✓ termination: all 6 handlers structurally terminate
  ✓ refinement: handler `assign_reviewer` ⟶ {sealed → in_review}
  ✓ refinement: handler `decide` ⟶ {decided}
  ✓ refinement: handler `lift_blind` ⟶ {unmasked}
  · transition sources: `decide`, `lift_blind` call 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)

ReviewDesk/invariants:

  ✓ invariant blind_roles >= 0 — writer 'assign_reviewer' proven by induction (writes (blind_roles.get(k) ?? 0) + 1)
  ✓ invariant blind_roles >= 0 && blind_roles <= 1 — writer 'submit_paper' proven (writes 1)
  ⚠ invariant blind_roles >= 0 && blind_roles <= 1 — runtime-checked (computed values): assign_reviewer → blind_roles [blind_roles <= 1] because `blind_roles` has no known range; `k` = "{paper}:{reviewer}" — not bounded

12 passed, 1 warnings, 0 failures

  Temporal properties for 'blind':
  ✓ 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/peer_review.cell · examples/corpus/governance/peer_review.cell