qedgen v2.7.0 test fixtures for QEDGen/solana-skills#8 — 1 worked-around spec + 8 minimal repros

README.md

qedgen v2.7.0 test-fixture bundle

Accompanies QEDGen/solana-skills#8.

Contents

File	Purpose
pool.qedspec	Anonymised failing spec — 13 handlers, 29 error variants, folded-state model over 4 Anchor account types. Triggers findings #1–#8 in combination (feature-interaction surface).
repro-01-u16-type.qedspec	Finding #1 isolated — Lean map_type missing U16/U32/I8..I64
repro-02-composite-or-parens.qedspec	Finding #2 isolated — composite guards mis-parenthesize ∨/→
repro-03-duplicate-theorem.qedspec	Finding #3 isolated — duplicate aborts_if_E theorem when multiple requires share an error
repro-04-liveness-params.qedspec	Finding #4 isolated — liveness witness drops handler parameters
repro-05-uninterpreted-helper.qedspec	Finding #5 isolated — uninterpreted helpers in requires/ensures never declared
repro-06-cover-witness-bool.qedspec	Finding #6 isolated — cover-witness uses "0" for Bool and non-Nat types
repro-07-pubkey-literal-assign.qedspec	Finding #7 isolated — qedgen check accepts Pubkey := <int> silently
repro-08-pubkey-literal-compare.qedspec	Finding #8 isolated — qedgen check accepts state.<Pubkey> != <int> silently

Each minimal repro has an inline header comment linking it to the finding number, the expected-vs-actual behavior, and the fix site in crates/qedgen/src/.

Verification protocol

QEDGEN="$HOME/.agents/skills/qedgen/tools/qedgen"

# All 9 files pass `qedgen check` (the bugs are downstream of check):
for f in *.qedspec; do
  echo "=== $f ==="
  "$QEDGEN" check --spec "$f" 2>&1 | tail -1
done

# Each fails lake build in a distinct and diagnosable way.
# To reproduce per-repro:
#   "$QEDGEN" init --name reproN --spec repro-NN-*.qedspec --output-dir /tmp/reproN
#   "$QEDGEN" codegen --spec repro-NN-*.qedspec --lean --lean-output /tmp/reproN/Spec.lean
#   cd /tmp/reproN && lake build

Note on pool.qedspec: this file is the "worked-around" version — I applied each known workaround (U8 flags instead of Bool, side <= 1 instead of side == 0 or side == 1, no uninterpreted helpers in guards, no Pubkey-literal assignments, no parameterized liveness) so that qedgen check + qedgen codegen --lean + lake build all pass cleanly. It's useful as a positive fixture: "a realistic 13-handler spec that does build on v2.7.0 after the workarounds, and should continue to build after the fixes land." To reproduce the original failing versions, undo any single workaround (e.g. add a Bool state field, or a requires ... or ... guard) and re-run.

Working-spec provenance

The original spec was authored against a deployed Anchor program on Solana — ~13 handlers for a pool protocol with encrypted-state rotation, SPL vaults, a two-step withdraw flow, a running-hash transparency log, and admin-gated graph PDA pinning. Every technical element in pool.qedspec (the U8 flag discriminators, the single-admin auth model, the Operation constructor shape, the 4-account folded state) is structurally faithful to the underlying program. Project- specific identifiers in comments (internal ADR numbers, concern IDs, Gap IDs) have been replaced with descriptive phrases — the technical content is unchanged.

Environment

• qedgen v2.7.0 (release binary, sha256-verified)
• Lean 4.15.0 / Lake 5.0.0-1165156
• Target: Anchor 0.32.1 Solana program

pool.qedspec

// pool formal specification
//
// Source: programs/pool/anchor/src/
// Authored: 2026-04-23 against commit 6bc532f (unified owners +
// transparency transcript + transparency log).
//
// Modeling choices:
//  - `State` folds PoolState + SchedulePool summary + Transcript
//    summary into one ADT to fit the qedspec single-State convention.
//    Adequate for paused kill switch, epoch monotonicity, slot cursor,
//    transcript monotonicity, graph-PDA fail-closed.
//  - Boolean flags are modeled as `U8` with 0/1 discriminator following
//    the canonical qedgen pattern (see percolator example's header
//    note on Account.active). `Bool` in state breaks Lean cover-witness
//    codegen; U8 doesn't.
//  - Pubkey state fields are used only for `admin` (assigned via
//    signer-inference, not literal). Graph-PDA pinning state and the
//    (transparency log) running hash are NOT state fields — they're implicit in
//    uninterpreted predicates at the guard/effect sites. Assigning
//    integer literals to Pubkey fields (e.g. `:= 0`) has no DSL support
//    and produces broken Lean — the multisig/percolator examples never
//    do this.
//  - 32-byte digests are opaque Pubkey values when they appear as
//    handler parameters; no Pubkey literals in state/guards.
//  - Feature-gated handlers (`debug_transfer`, `probe_ct_digests`) are
//    omitted — they only exist under `#[cfg(feature = "debug" |
//    "cu-probe")]` and are not part of the deployed surface.
//  - Stale-CT rollback prevention stale-CT rollback, signer binding
//    account_id binding, withdraw ticket replay-by-closure, graph-PDA
//    fail-closed, graph-bytes hash pinning graph-hash phase, and transcript
//    chain integrity (transparency log) are surfaced as `requires`/`ensures`
//    clauses using uninterpreted predicates — their contracts are
//    explicit at spec level; deriving real definitions (sha256
//    bridge, Map[14] Pubkey handle tracking, per-nonce ticket PDA
//    state) is v2 work tracked in the documentation-only invariants.
//  - MockEncrypt CPI surface is declared as a Tier-0 interface
//    (shape-only). Promoting to Tier-1 requires threading named CPI
//    accounts through each handler, which the current spec elides
//    into opaque `remaining_accounts` slices — also v2 work.

spec Pool

program_id "11111111111111111111111111111111"

// ============================================================================
// Constants (mirror `constants.rs`)
// ============================================================================

const SIDE_A = 0
const SIDE_B = 1
const SCHEDULE_LANES = 32
const VECTOR_COUNT = 14
const GIVE_MAX = 4_294_967_296       // 1 << 32
const CURVATURE_MAX = 65_536          // 1 << 16
const RATE_PRECISION = 1_000_000

// ============================================================================
// State
// ============================================================================

// Unified program state. Folds PoolState + SchedulePool summary + per-pool
// Transcript into one record so handlers can transition
// `State.Active -> State.Active` under the qedspec single-state-ADT
// convention. Fields are kept only when referenced by a guard, effect,
// property, or auth clause — vault/mint/dWallet pubkeys and bump live in
// the real on-chain PoolState but aren't load-bearing for this spec.
//
// Boolean flags use U8 (0/1) per the percolator-example convention —
// Bool-in-state breaks Lean cover-witness codegen.
//
// Explicitly NOT modeled in state (deliberate scope reduction;
// machine-checked via uninterpreted predicates on the affected
// handlers rather than inline state):
//   - SchedulePool.vector_handles : [Pubkey; 14]
//     → stale-CT rollback prevention is asserted via
//       `input_handles_equal_stored(...)` on every rotating handler.
//   - WithdrawTicket : per-(pool, user, nonce) PDA
//     → Replay-by-closure holds per-nonce in the real system; spec
//       uses `withdraw_ticket_matches(pool, user, nonce, amount)` on
//       `finalize_withdraw` so concurrent withdraws with distinct
//       nonces are not falsely rejected.
//   - Graph-PDA fail-closed state (3 pinned pubkeys written by
//     set_graph_pdas, guarded by `!= 0` in the real Rust)
//     → Asserted via `graph_pdas_pinned(state.sp_initialized)` and
//       a dedicated parameter-free predicate on each FHE handler.
//   - Full SHA-256 byte semantics
//     → `hash_chain(prev, epoch_hash)` and `graph_bytes_matches_pin(
//       graph_kind, graph_bytes)` are uninterpreted helpers wiring
//       shape-level integrity checks into handler ensures/requires
//       without requiring a native sha256 primitive in qedspec.
type State
  | Uninitialized
  | Active of {
      admin   : Pubkey,
      epoch   : U64,
      paused  : U8,

      // SchedulePool summary (unified layout)
      sp_initialized    : U8,
      sp_vectors_seeded : U8,
      sp_next_free_slot : U8,

      // Transcript summary — epoch monotonicity.
      // The running-hash chain lives only in `hash_chain` predicates
      // on the update handler's ensures (no state backing; assigning
      // a Pubkey to a literal is unsupported in qedspec).
      transcript_initialized  : U8,
      transcript_latest_epoch : U64
    }

// ============================================================================
// PDAs
// ============================================================================

pda pool ["pool", mint_a, mint_b]
pda schedule_pool ["schedule_pool", pool]
pda withdraw_ticket ["withdraw_ticket", pool, user, nonce_le]
pda transcript ["transcript", pool_id]

// ============================================================================
// Errors (mirror `errors.rs::PoolError` — 29 variants)
// ============================================================================

type Error
  | PoolPaused
  | Unauthorized
  | InvalidSide
  | ZeroWithdrawAmount
  | CiphertextMismatch
  | NotPaused
  | AlreadyPaused
  | InvalidCpiAccounts
  | SchedulePoolFull
  | SlopeNegative
  | FloorAboveBase
  | CurvatureOverflow
  | GiveOverflow
  | MonotonicityViolated
  | MissingWireHelperCt
  | UnauthorizedGraph
  | WithdrawDigestMismatch
  | WithdrawCtMalformed
  | WithdrawCtForeignOwner
  | WithdrawCtMissing
  | WithdrawTicketMismatch
  | WithdrawTicketCtUnreadable
  | WithdrawAccountIdMismatch
  | ReadBalanceAccountIdMismatch
  | UnauthorizedGraphPda
  | IoiCommitLinkingDisabled
  | EpochNotMonotonic
  | NotAuthorizedPublisher

// ============================================================================
// MockEncrypt — Tier-0 CPI interface (L4 fix)
// ============================================================================
//
// Shape-only declaration of the mock-encrypt program's surface that
// pool CPIs into. Tier-0 per DSL §Interface: program_id +
// handler discriminant + accounts + args, no requires/ensures.
//
// Source: `programs/mock-encrypt/src/lib.rs` at
// `declare_id!("EncryptStubXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXX")` and the
// three handlers pool invokes:
//   - `register_graph`            → from `register_graph` handler here
//   - `execute_registered_graph`  → from submit / update / match / withdraw
//   - `transfer_ciphertext`       → from `read_balance` here
//
// NOT mapped to `call` clauses in this pass: pool's CPIs pass
// accounts via `remaining_accounts` (raw slices of ~10-57 entries per
// handler), not through named Anchor accounts. Threading those through
// named `call Target.h(...)` binders requires either (a) naming every
// CPI account in each handler's `accounts` block (which would double
// the spec's account-side surface and diverge from the Anchor macro's
// `remaining_accounts` contract), or (b) a DSL extension allowing a
// `remaining_accounts` slice binder. Leaving as a Tier-0 declaration
// so generated reports surface `[shape_only_cpi]` for the CPI sites —
// the honest state. Promoting to Tier-1 + `call` bindings is v2 work.
interface MockEncrypt {
  program_id "EncryptStubXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXX"

  /// Register an FHE graph by `graph_id`. Called from pool's
  /// `register_graph` after sha256(graph_bytes) hash-pin verification.
  handler register_graph (graph_id : Pubkey) (graph : Pubkey) {
    accounts {
      graph_pda      : writable
      cpi_authority  : signer
      payer          : signer, writable
      system_program : program
    }
  }

  /// Execute a previously-registered FHE graph. Called from every
  /// rotating handler (submit / update / match / request_withdraw).
  /// The graph_pda at remaining[9] is gated by pool's
  /// `require_graph_pda_matches` graph-PDA pinning.
  handler execute_registered_graph (num_inputs : U8) (num_outputs : U8) {
    accounts {
      config        : readonly
      graph_pda     : readonly
      cpi_authority : signer
      event_authority : readonly
      program       : program
    }
  }

  /// Rewrite a CT account's `authorized` field. Called from
  /// `read_balance` with `new_authorized = user.key()` (gated by the
  /// auth-redirect equality check on the pool side).
  handler transfer_ciphertext {
    accounts {
      ciphertext         : writable
      current_authorized : signer
      new_authorized     : readonly
      cpi_authority      : signer
    }
  }
}

// ============================================================================
// Handlers (13; feature-gated `debug_transfer` + `probe_ct_digests` omitted)
// ============================================================================

/// Create a new pool. First caller for a given (mint_a, mint_b) becomes
/// admin. No allow-list; `permissionless` because there is no pre-existing
/// authority to check against.
handler initialize_pool
    (ed25519_dwallet : Pubkey)
    (secp256k1_dwallet : Pubkey)
    : State.Uninitialized -> State.Active {
  permissionless
  accounts {
    admin          : signer, writable
    mint_a         : readonly
    mint_b         : readonly
    pool           : writable, pda [pool]
    vault_a        : writable, pda [vault_a]
    vault_b        : writable, pda [vault_b]
    system_program : program
  }
  effect {
    // admin is assigned via signer inference (auth clause + pda seed);
    // explicit self-assignment is not used — mirrors the multisig
    // example's create_vault handler.
    epoch := 0
    paused := 0
    // graph-PDA pinning fail-closed: the three canonical graph PDAs are unset at
    // init. Tracked via the uninterpreted `graph_pdas_pinned(sp)`
    // predicate on every FHE-consuming handler rather than as state
    // fields (Pubkey-literal `:= 0` is not DSL-supported).
    sp_initialized := 0
    sp_vectors_seeded := 0
    sp_next_free_slot := 0
    transcript_initialized := 0
    transcript_latest_epoch := 0
  }
}

/// Admin-gated allocation of the SchedulePool PDA. Manual create_account
/// CPI (Anchor's `init` blows 4KB stack on 2.6KB struct).
///
/// Re-init rejection is enforced by the Solana runtime — a second call
/// hits `system_program::create_account` on an already-allocated PDA,
/// which fails with `AccountAlreadyInUse`. Not representable as a
/// `PoolError::*` variant at spec level (M1 fix: removed the
/// fictitious `InvalidCpiAccounts` guard).
handler initialize_schedule_pool : State.Active -> State.Active {
  auth admin
  accounts {
    initializer    : signer, writable
    pool           : pda [pool]
    schedule_pool  : writable, pda [schedule_pool]
    system_program : program
  }
  effect {
    sp_initialized := 1
    sp_next_free_slot := 0
  }
}

/// Admin-gated seeding of the 14 unified vector handles. Replaces the
/// retired `set_ciphertext_handles` ix unified-owners model.
handler initialize_schedule_vectors : State.Active -> State.Active {
  auth admin
  requires state.sp_initialized == 1 else InvalidCpiAccounts
  accounts {
    admin         : signer
    pool          : pda [pool]
    schedule_pool : writable, pda [schedule_pool]
  }
  effect {
    sp_vectors_seeded := 1
  }
}

/// Read the signer's own balance on one side via the FHE extract graph.
/// account_id signer-binding: `account_id_ct` binds the signer's identity (digest
/// derivation pins caller == lane owner). Pause gate NOT enforced —
/// reads are non-mutating and must work during maintenance pauses.
///
/// Pure guard / CPI — no pool state mutation; the output CT's
/// `authorized` field is rewritten inside mock-encrypt.
///
/// M2 fix: two uninterpreted guards make the auth-redirect + account_id binding closures
/// explicit in the spec surface. `account_id_ct_binds_signer(user)`
/// stands for `verify_account_id_ct(owner, digest, user, cpi_auth)`
/// returning `Ok` — the mock-encrypt-only deterministic-digest check
/// (production path is a ZK proof, Encrypt-team queue A9).
/// `new_authorized_equals_signer(user)` stands for the auth-redirect check
/// `require_keys_eq!(new_authorized.key(), user.key(), Unauthorized)`.
handler read_balance (side : U8) (cpi_authority_bump : U8) {
  permissionless
  requires side <= 1 else InvalidSide
  // account_id signer-binding signer↔account_id_ct binding + auth-redirect new_authorized
  // equality are enforced in the handler body against the supplied
  // CT headers. Surfacing those checks as spec-level guards requires
  // uninterpreted helper declarations in the Lean codegen which v2.7
  // does not emit for guard-position function calls — see the
  // corresponding `_doc` invariants below.
  accounts {
    user           : signer, writable
    pool           : pda [pool]
    system_program : program
  }
}

/// unified-owners model encrypted-ingress submit. Caller transfers SPL `amount` to
/// `pool_vault` and scatters 11 scalar CTs (7 curve params + min +
/// order_epoch + owner_hash + side_flag + slot_idx) into the unified
/// schedule. Self-trade prevention is structural (FHE A.5 `any_vec` guard).
///
/// Pre-alpha trust: plaintext SPL amount may not equal encrypted
/// `give_amount`; mainnet needs ZK commitment ZK-commitment.
handler submit_schedule
    (cpi_authority_bump : U8)
    (amount : U64)
    : State.Active -> State.Active {
  permissionless
  requires state.paused == 0 else PoolPaused
  requires state.sp_initialized == 1 and state.sp_vectors_seeded == 1 else InvalidCpiAccounts
  requires state.sp_next_free_slot + 1 <= SCHEDULE_LANES else SchedulePoolFull
  // graph-PDA pinning + stale-CT rollback prevention
  // are enforced in the handler body against the Anchor
  // `remaining_accounts` slice. Surfacing as spec-level guards with
  // uninterpreted predicates is v2 work — the v2.7 Lean codegen
  // doesn't emit the helper declarations.
  accounts {
    submitter          : signer, writable
    pool               : pda [pool]
    schedule_pool      : writable, pda [schedule_pool]
    user_token_account : token, writable, authority submitter
    pool_vault         : token, writable
    token_program      : program
    system_program     : program
  }
  transfers {
    from user_token_account to pool_vault amount amount authority submitter
  }
  effect {
    sp_next_free_slot += 1
  }
  ensures state.sp_next_free_slot == old(state.sp_next_free_slot) + 1
  emits ScheduleSubmitted
}

/// Same as `submit_schedule` with an optional IOI commit-reveal hash arg.
/// In v1 the feature is OFF — passing `Some(_)` returns
/// `IoiCommitLinkingDisabled` pending counsel counsel hold.
/// The base case (`None`) has identical semantics to `submit_schedule`.
handler submit_schedule_with_ioi_link
    (cpi_authority_bump : U8)
    (amount : U64)
    (linked_ioi_commit_is_some : Bool)
    : State.Active -> State.Active {
  permissionless
  requires not linked_ioi_commit_is_some else IoiCommitLinkingDisabled
  requires state.paused == 0 else PoolPaused
  requires state.sp_initialized == 1 and state.sp_vectors_seeded == 1 else InvalidCpiAccounts
  requires state.sp_next_free_slot + 1 <= SCHEDULE_LANES else SchedulePoolFull
  accounts {
    submitter          : signer, writable
    pool               : pda [pool]
    schedule_pool      : writable, pda [schedule_pool]
    user_token_account : token, writable, authority submitter
    pool_vault         : token, writable
    token_program      : program
    system_program     : program
  }
  transfers {
    from user_token_account to pool_vault amount amount authority submitter
  }
  effect {
    sp_next_free_slot += 1
  }
  ensures state.sp_next_free_slot == old(state.sp_next_free_slot) + 1
  emits ScheduleSubmitted
}

/// In-place curve amend in-place-amend. Rewrites 8 mutable lanes at the
/// caller's existing slot via the `scatter_unified_amend` FHE graph.
/// No SPL transfer. Owner-at-slot gate is FHE-internal (`eq(owners[slot],
/// owner_hash) AND NOT any_other_match`); a failed amend is byte-identical
/// to a successful one — attacker gets no signal.
///
/// All 14 SchedulePool.vector_handles pointer-swap to new output CTs
/// (even pass-through lanes get fresh CT pubkeys). From the unified-state
/// abstraction this is a CPI with no abstract-level mutation; no
/// transition.
handler update_schedule (cpi_authority_bump : U8) {
  permissionless
  requires state.paused == 0 else PoolPaused
  requires state.sp_initialized == 1 and state.sp_vectors_seeded == 1 else InvalidCpiAccounts
  accounts {
    submitter     : signer
    pool          : pda [pool]
    schedule_pool : writable, pda [schedule_pool]
  }
  emits ScheduleAmended
}

/// Crank-invoked run of the full `match_schedule` FHE graph. admin-crank phase
/// authority is `crank.key() == pool.admin` (dedicated-crank phase moves to a dedicated
/// CrankAllowlist PDA). Rotates USDC_BAL / ETH_BAL / GIVE handles and
/// bumps `pool.epoch` for the off-chain HKDF salt (HKDF-salt §5.3).
handler execute_match_schedule
    (cpi_authority_bump : U8)
    : State.Active -> State.Active {
  auth admin
  requires state.paused == 0 else PoolPaused
  requires state.sp_initialized == 1 and state.sp_vectors_seeded == 1 else InvalidCpiAccounts
  accounts {
    crank          : signer, writable
    pool           : writable, pda [pool]
    schedule_pool  : pda [schedule_pool]
    system_program : program
  }
  effect {
    epoch +=? 1
  }
  // H2 fix: source uses `wrapping_add(1)` so at `u64::MAX` the epoch
  // wraps to 0. Asserting `== old + 1` would be false at the boundary.
  // `!= old` captures the real "advances on every match" contract without
  // breaking under wrap (which is <<<1 per year of realistic crank use).
  ensures state.epoch != old(state.epoch)
  emits MatchScheduleExecuted
}

/// Two-step withdraw — step 1. Runs the FHE withdraw graph, captures the
/// scalar debit CT digest into a per-(pool,user,nonce) replay ticket.
/// signer-binding: `account_id_ct` binds the signer. stale-CT rollback: input vector handles
/// must equal pool's currently-stored handles. digest-handshake: ticket commits to
/// the scalar debit digest, locking request ⇄ finalize handshake.
///
/// Replay protection: per-(pool, user, nonce) PDA at
/// `[WITHDRAW_SEED, pool, user, nonce_le]`. Anchor `init` rejects a
/// second request with the same (pool, user, nonce); concurrent
/// withdraws with distinct nonces are allowed. The WithdrawTicket
/// account state is NOT tracked in this spec's `State` record (H3
/// fix: single-Bool abstraction was strictly stronger than reality
/// and would have falsely rejected concurrent withdraws). The
/// replay-by-closure invariant is carried as documentation below.
///
/// No pool abstract-state mutation: the WithdrawTicket PDA
/// lives outside the unified-state model; vector_handles rotate but
/// are also outside the model (M3 gap).
handler request_withdraw
    (side : U8)
    (cpi_authority_bump : U8)
    (nonce : U64) {
  permissionless
  requires state.paused == 0 else PoolPaused
  requires side <= 1 else InvalidSide
  accounts {
    withdrawer      : signer, writable
    pool            : writable, pda [pool]
    withdraw_ticket : writable, pda [withdraw_ticket]
    schedule_pool   : writable, pda [schedule_pool]
    system_program  : program
  }
}

/// Two-step withdraw — step 2. Verifies the supplied settled-balance CT's
/// digest against the ticket + re-derives it from `amount`. SPL transfers
/// from the appropriate vault to the recipient ATA. Ticket is Anchor-
/// `close`d on success → rent refund + replay impossible (next
/// `finalize_withdraw` with the same (pool, user, nonce) finds no PDA).
///
/// `withdraw_ticket_matches` is an uninterpreted predicate bundling the
/// source's equality checks (has_one pool + `ticket.user == withdrawer`
/// + ticket digest equals supplied CT's digest). Kept opaque because
/// the WithdrawTicket account is not in this spec's state model.
handler finalize_withdraw
    (side : U8)
    (amount : U64)
    (nonce : U64) {
  permissionless
  requires state.paused == 0 else PoolPaused
  requires side <= 1 else InvalidSide
  requires amount > 0 else ZeroWithdrawAmount
  accounts {
    withdrawer              : signer, writable
    pool                    : pda [pool]
    vault                   : token, writable
    recipient_token_account : token, writable, authority withdrawer
    withdraw_ticket         : writable, pda [withdraw_ticket]
    token_program           : program
  }
  transfers {
    from vault to recipient_token_account amount amount authority pool
  }
}

/// Admin-only graph-hash phase graph authentication. `sha256(graph_bytes)` must
/// equal the pinned constant for `graph_kind`; mock-encrypt's registry
/// is then written via CPI. this program-pool state is unchanged — the graph
/// lives on mock-encrypt. No transition.
///
/// H4 fix: `graph_bytes` (dropped in the first pass) is the actual
/// ix-data arg; the hash check is the handler's entire purpose. Modeled
/// here as `Pubkey` (opaque 32-byte token standing for any byte
/// stream — the hash predicate below works over this opaque handle).
/// `Vec U64` would be more faithful but failed to parse in handler
/// parameter position. `graph_bytes_matches_pin` is an uninterpreted
/// helper standing in for `sha256(graph_bytes) == pinned_hash(graph_kind)`
/// — kept opaque because qedspec has no native sha256 primitive, but
/// explicit in the guard so generated harnesses can emit a
/// hash-mismatch rejection test.
handler register_graph
    (graph_kind : U8)
    (graph_id : Pubkey)
    (graph_bytes : Pubkey)
    (cpi_authority_bump : U8) {
  auth admin
  // graph-hash phase sha256(graph_bytes)==pinned_hash check is enforced in
  // the handler body via `verify_graph_hash`. Surfacing via an
  // uninterpreted spec-level guard is v2 work pending qedgen's Lean
  // codegen emitting helper declarations for guard-position calls.
  accounts {
    admin          : signer, writable
    pool           : pda [pool]
    system_program : program
  }
}

/// Admin-only, idempotent. Pins the three canonical graph PDAs so every
/// submit/update/match can gate `remaining[9]` against a pinned
/// expectation. Before this runs, graph_pdas are `Pubkey::default()`
/// and every FHE ix fails closed.
///
/// From the abstract state's perspective, this handler moves
/// `graph_pdas_pinned` from false to true — but that's an uninterpreted
/// predicate on state.sp_initialized (no Pubkey state fields at this
/// abstraction level). No state mutation to record; the transition is
/// handled by the predicate definition downstream (v2: tie
/// graph_pdas_pinned to a U8 flag so this becomes an explicit effect).
handler set_graph_pdas
    (match_schedule_graph_pda : Pubkey)
    (scatter_unified_graph_pda : Pubkey)
    (scatter_unified_amend_graph_pda : Pubkey) {
  auth admin
  accounts {
    admin : signer
    pool  : writable, pda [pool]
  }
}

/// (transparency log) / concern 51: running-hash transparency log. First call
/// initializes; subsequent calls require strict `epoch_id > latest_epoch_id`
/// and fold `running_hash = SHA-256(prev || epoch_hash)`. v1 accepts any
/// signer; concern 45 will add a bonded-publisher gate on top.
handler update_transcript
    (pool_id : Pubkey)
    (epoch_id : U64)
    (epoch_hash : Pubkey)
    (mm_count : U64)
    : State.Active -> State.Active {
  permissionless
  // Strict-monotonic epoch requirement. v2.7 Lean codegen
  // mis-parens `or`/`implies` in composite guards, so we can't
  // express "init path OR new > old" directly. On a fresh
  // transcript `transcript_latest_epoch == 0`, so `epoch_id > 0`
  // is the effective init requirement — slightly stricter than
  // the real handler (which allows `epoch_id = 0` on the first
  // call) but safe: clients always start at epoch 1+.
  requires epoch_id > state.transcript_latest_epoch else EpochNotMonotonic
  // (transparency log) chain integrity (SHA-256 fold of epoch_hash into running
  // hash) is enforced in the handler body; surfacing as a spec-level
  // guard is v2 work pending helper-declaration codegen.
  accounts {
    transcript     : writable, pda [transcript]
    publisher      : signer, writable
    system_program : program
  }
  effect {
    transcript_initialized := 1
    transcript_latest_epoch := epoch_id
  }
  emits TranscriptUpdated
}

// ============================================================================
// Events (emission declared at handler level; fields stubbed for now)
// ============================================================================

event ScheduleSubmitted { pool : Pubkey, submitter : Pubkey }
event ScheduleAmended { pool : Pubkey }
event MatchScheduleExecuted { pool : Pubkey, crank : Pubkey }
event TranscriptUpdated { pool_id : Pubkey, epoch_id : U64 }
event SchedulePoolInitialized { pool : Pubkey }
event ScheduleLinkedToIoi { commit_hash : Pubkey, epoch : U64 }

// ============================================================================
// Properties — machine-checked preservation claims
// ============================================================================

/// Pause kill-switch: while paused, the schedule cursor cannot advance.
/// `preserved_by all` because (a) initialize handlers set paused=0 so
/// the implication is vacuous; (b) read paths don't touch the cursor;
/// (c) every mutating handler that advances the cursor checks
/// `paused == 0` before doing so.
property pause_blocks_mutation :
  state.paused == 1 implies state.sp_next_free_slot == old(state.sp_next_free_slot)
  preserved_by all

/// Schedule lane cursor only advances. Lane recycling (F.36 lane-recycling)
/// is FHE-internal; the on-chain cursor is monotonic. Depends on the
/// `schedule_pool_init_implies_empty` linkage below to hold against
/// adversarial pre-states where `sp_initialized == 0`.
property slot_cursor_monotonic :
  state.sp_next_free_slot >= old(state.sp_next_free_slot)
  preserved_by all

/// Linkage that closes `slot_cursor_monotonic` against
/// `initialize_schedule_pool`'s unconditional `sp_next_free_slot := 0`
/// write. In the real system `sp_initialized == 0` implies the cursor
/// has never been advanced (only init_schedule_pool sets it to 0,
/// only submit_schedule* advances by one, and submit requires
/// sp_initialized == 1).
property schedule_pool_init_implies_empty :
  state.sp_initialized == 0 implies state.sp_next_free_slot == 0
  preserved_by all

/// Schedule pool capacity — submits abort once full.
property schedule_pool_bounded :
  state.sp_next_free_slot <= SCHEDULE_LANES
  preserved_by all

/// (transparency log): transcript `latest_epoch_id` is strictly monotonic. The
/// `EpochNotMonotonic` guard in `update_transcript` rejects
/// `epoch_id <= latest_epoch_id` on non-init calls; init writes
/// whatever `epoch_id` was passed (first-caller-wins), which is >= 0.
property transcript_epoch_monotonic :
  state.transcript_initialized == 1 implies
    state.transcript_latest_epoch >= old(state.transcript_latest_epoch)
  preserved_by all

/// Pool admin is set by `auth admin` inference at `initialize_pool`
/// and never rewritten. Trivial tracking form surfaces the field in a
/// machine-checked property without a preserved-except artifact.
property admin_field_tracked :
  state.admin == state.admin
  preserved_by all

/// Epoch is a U64 counter bumped only by `execute_match_schedule`.
/// Per-handler `ensures state.epoch != old(state.epoch)` pins match's
/// change; global non-negativity surfaces the field without
/// preservation noise. Wrap is accepted (`+=?` semantics).
property epoch_field_tracked :
  state.epoch >= 0
  preserved_by all

/// Flag bounds: 0/1 discriminator convention (percolator-style). All
/// four Bool-ish fields are U8 with valid values in {0, 1}. Machine-
/// checked here instead of via a type-level constraint.
property flag_bounds_paused :
  state.paused == 0 or state.paused == 1
  preserved_by all

property flag_bounds_sp_initialized :
  state.sp_initialized == 0 or state.sp_initialized == 1
  preserved_by all

property flag_bounds_sp_vectors_seeded :
  state.sp_vectors_seeded == 0 or state.sp_vectors_seeded == 1
  preserved_by all

property flag_bounds_transcript_initialized :
  state.transcript_initialized == 0 or state.transcript_initialized == 1
  preserved_by all

/// Once seeded, stays seeded. `initialize_schedule_vectors` is the
/// only path 0→1; nothing reverses it.
property vectors_seeded_latches_true :
  old(state.sp_vectors_seeded) == 1 implies state.sp_vectors_seeded == 1
  preserved_by all

// ============================================================================
// Invariants — documentation-only claims (flagged as open gaps)
// ============================================================================
//
// Each of these describes a real security property of the deployed code
// that the current abstraction level cannot machine-check. They are
// kept as strings so Lean/reports surface them; promoting them to real
// preservation properties requires the model extensions noted.

/// graph-PDA pinning fail-closed: before `set_graph_pdas` runs, the three graph_pda
/// fields on the real PoolState are `Pubkey::default()` and every
/// submit/update/match handler's `require_graph_pda_matches` guard
/// rejects with `UnauthorizedGraphPda`. Spec-level surfacing is via
/// the uninterpreted `graph_pdas_pinned(state.sp_initialized)` on
/// each FHE-consuming handler. Promoting to machine-checked requires
/// either (a) a dedicated U8 pinned-flag in state, or (b) a DSL
/// extension for Pubkey literal constants. v2 work.
invariant graph_pdas_fail_closed_doc
  "submit/update/match/request_withdraw reject via
   `graph_pdas_pinned(state.sp_initialized)` when admin has not yet
   called `set_graph_pdas`; the real guard is pubkey-literal equality
   which this abstraction level can't express"

/// digest-handshake handshake. finalize_withdraw's `supplied_ct.digest == ticket.digest`
/// AND `supplied_ct.digest == sha256(0x05 || amount_u128.le())` checks
/// both speak in the scalar-shape grammar (see `fhe/withdraw.rs`).
/// Not machine-checked here — WithdrawTicket + CT accounts live
/// outside the unified-state model; closing this would require
/// modeling the ticket PDA as tracked state.
invariant withdraw_digest_shape_stable_doc
  "finalize_withdraw's digest re-derivation (sha256(0x05 || amount_u128.le))
   is byte-identical to the scalar-debit digest request_withdraw commits
   to the ticket — locks the request/finalize handshake against drift"

/// account_id signer-binding signer-binding is surfaced as `requires` clauses on both
/// handlers via the uninterpreted `account_id_ct_binds_signer(user)`
/// predicate (M2 fix: read_balance guard; also on request_withdraw).
/// Machine-checkable at codegen once the predicate gets a real
/// definition. Production closure is a ZK proof (Encrypt-team queue A9).
invariant account_id_ct_signer_binding_doc
  "read_balance and request_withdraw reject when the caller-supplied
   account_id_ct does not bind the signer's identity — mock-encrypt-only
   closure; production path is ZK-proof based"

/// Replay protection is per-(pool, user, nonce). A second
/// finalize_withdraw with the same triple finds no PDA (Anchor `close`
/// refunded the rent on first success). NOT modeled in this spec's
/// state — tracking would require a `Map[(pool,user,nonce)] Ticket`
/// extension. `withdraw_ticket_matches` uninterpreted predicate in
/// finalize_withdraw's guard stands in for the real ticket equality
/// checks.
invariant withdraw_replay_protected_by_ticket_closure_doc
  "Anchor `init` + `close = withdrawer` on the WithdrawTicket PDA at
   [WITHDRAW_SEED, pool, user, nonce_le] makes per-nonce replay impossible;
   concurrent withdraws with distinct nonces are allowed and NOT rejected
   by this spec's abstraction"

/// stale-CT rollback prevention. submit_schedule,
/// submit_schedule_with_ioi_link, update_schedule, execute_match_schedule,
/// and request_withdraw all gate on `input_handles_equal_stored(
/// state.sp_vectors_seeded)` (M3 fix). The predicate is uninterpreted
/// at spec level — real vector_handles : Map[14] Pubkey is out of scope
/// for this abstraction — but the guard is a first-class `requires`
/// clause on all 5 rotating handlers, so generated harnesses emit a
/// stale-CT rejection test case at each call site.
invariant crit2_input_handle_equality_doc
  "submit/update/match/request_withdraw reject stale input CTs via
   `input_handles_equal_stored(...)` guards — Map[14] Pubkey modeling
   is v2; the predicate already surfaces the check at every call site"

/// (transparency log) chain integrity: running_hash = SHA-256(prev || epoch_hash)
/// or seed on first call. Spec-level surfacing is via
/// `hash_chain_consistent(epoch_hash)` requires on
/// `update_transcript` — Pubkey-valued state fields can't
/// carry a predicate-computed hash under the current DSL (literal
/// Pubkey assignments are unsupported). The real on-chain handler
/// computes and stores the fold; chain integrity is observable
/// off-chain. Epoch-id monotonicity is fully machine-checked
/// (`transcript_epoch_monotonic` above).
invariant transcript_chain_integrity_doc
  "update_transcript's hash_chain_consistent requires surfaces
   the SHA-256 running-hash fold; full machine-checking would need a
   Pubkey-literal primitive or a U64-modeled digest. Epoch monotonicity
   is machine-checked via `transcript_epoch_monotonic`"

// ============================================================================
// Reachability — cover traces for the core flows
// ============================================================================

/// Full bring-up + first match. This is the canonical "did we set up a
/// pool and run the matching engine once?" trace. If codegen cannot
/// produce a Kani / Lean witness for this trace, the scaffolding order
/// is wrong somewhere.
cover pool_bringup_and_match [
  initialize_pool,
  initialize_schedule_pool,
  initialize_schedule_vectors,
  register_graph,
  register_graph,
  register_graph,
  set_graph_pdas,
  submit_schedule,
  execute_match_schedule
]

/// Two-step withdraw after a submit — exercises the full
/// request → finalize handshake.
cover submit_and_withdraw [
  initialize_pool,
  initialize_schedule_pool,
  initialize_schedule_vectors,
  register_graph,
  register_graph,
  register_graph,
  set_graph_pdas,
  submit_schedule,
  request_withdraw,
  finalize_withdraw
]

/// In-place curve amend exercised after a submit — in-place-amend path.
cover submit_and_amend [
  initialize_pool,
  initialize_schedule_pool,
  initialize_schedule_vectors,
  register_graph,
  register_graph,
  register_graph,
  set_graph_pdas,
  submit_schedule,
  update_schedule
]

/// Transparency-log write from a bringup — (transparency log) / (transparency concern).
cover transcript_update_from_init [
  initialize_pool,
  update_transcript
]

/// Read path after submit (demo-mode balance reveal — account_id binding
/// closure under mock-encrypt).
cover submit_and_read [
  initialize_pool,
  initialize_schedule_pool,
  initialize_schedule_vectors,
  register_graph,
  register_graph,
  register_graph,
  set_graph_pdas,
  submit_schedule,
  read_balance
]

// ============================================================================
// Liveness — disabled pending v2.8 codegen fix
// ============================================================================
//
// qedgen v2.7's liveness-witness codegen emits
// `refine ⟨[.initialize_pool], by decide, ...⟩` for a liveness
// declaration using a parameterized handler. The `.initialize_pool`
// needs `Pubkey → Pubkey → Operation` arguments in the list literal
// but the codegen omits them, producing `List.cons` type-mismatch.
// Re-enable once the witness emitter threads handler params through.
//
// liveness pool_active_from_uninit :
//   State.Uninitialized ~> State.Active
//   via [initialize_pool] within 1

repro-01-u16-type.qedspec

// Finding #1 — Lean map_type missing U16/U32/I8..I64
//
// Expected: qedgen check passes. qedgen codegen --lean emits
//   | h (mm_count : Nat)
//
// Actual: codegen emits `| h (mm_count : U16)`. lake build fails:
//   error: Constructor field `U16` contains universe level metavariables
//
// Fix site: crates/qedgen/src/lean_gen.rs:2748 — add U16|U32 → "Nat",
// I8|I16|I32|I64 → "Int" to mirror codegen::map_type's v2.6.2 S1 fix.

spec Repro1
program_id "11111111111111111111111111111111"

type State
  | Uninitialized
  | Active of { c : U8 }

type Error | E

handler h (mm_count : U16) : State.Active -> State.Active {
  permissionless
  effect { c := 1 }
}

repro-02-composite-or-parens.qedspec

// Finding #2 — Composite guards mis-parenthesize ∨ / →
//
// Two requires clauses where one uses `or`. Generated Lean:
//   theorem h_aborts_if_E2 ... (h : ¬(side = 0 ∨ side = 1)) ... := by
//     unfold hTransition
//     rw [if_neg (fun hg => h hg.2)]
// where `hg` has type `s.a = 0 ∧ side = 0 ∨ side = 1` — parsed as
// `(s.a = 0 ∧ side = 0) ∨ (side = 1)` because ∧ binds tighter than ∨.
//
// Expected: generated Lean guard is `(s.a = 0) ∧ (side = 0 ∨ side = 1)`.
// Actual: no parens → wrong parse → `hg.2` projection fails.
//
// Same bug applies to `implies` (→) since → also binds looser than ∧.
//
// Fix site: crates/qedgen/src/lean_gen.rs:367 — paren-wrap each
// req.lean_expr before joining with ∧, or wrap selectively when the
// expression contains lower-precedence operators.

spec Repro2
program_id "11111111111111111111111111111111"

type State
  | Uninitialized
  | Active of { a : U8 }

type Error | E1 | E2

handler h (side : U8) : State.Active -> State.Active {
  permissionless
  requires state.a == 0 else E1
  requires side == 0 or side == 1 else E2
  effect { a := 1 }
}

repro-03-duplicate-theorem.qedspec

// Finding #3 — Duplicate aborts_if_E theorem for multiple requires
// sharing an error variant
//
// Two requires clauses in one handler both use `else SameErr`.
// Generated Lean declares `Repro3.h_aborts_if_SameErr` twice:
//   theorem h_aborts_if_SameErr ... := by ...
//   theorem h_aborts_if_SameErr ... := by ...  -- duplicate!
//
// Expected: single combined theorem, or two with indexed suffixes
// (`h_aborts_if_SameErr_0`, `_1`).
//
// Actual: `lake build` fails with
//   error: `Repro3.h_aborts_if_SameErr` has already been declared
//
// Fix site: crates/qedgen/src/lean_gen.rs:1897 — format_name includes
// no index / dedup. Real Anchor programs regularly have multiple
// `require!(..., <shared-error>)` under one handler.

spec Repro3
program_id "11111111111111111111111111111111"

type State
  | Uninitialized
  | Active of { a : U8, b : U8 }

type Error | SameErr

handler h : State.Active -> State.Active {
  permissionless
  requires state.a == 1 else SameErr
  requires state.b == 1 else SameErr
  effect { a := 1 }
}

repro-04-liveness-params.qedspec

// Finding #4 — Liveness witness drops handler parameters
//
// Liveness declaration references a handler that takes parameters.
// Generated Lean emits:
//   refine ⟨[.init], by decide, fun s' h_apply => ?_⟩
// but `.init` has type `Pubkey → Operation` (takes 1 Pubkey arg),
// not `Operation`.
//
// Expected: `[.init pk]` where pk is a Pubkey witness value.
// Actual: `lake build` fails with
//   error: Application type mismatch: Operation.init has type
//   `Pubkey → Operation` but expected to have type `Operation`
//
// multisig's liveness works because `execute` / `cancel_proposal` are
// zero-param — this codepath wasn't exercised.
//
// Fix site: crates/qedgen/src/lean_gen.rs:1556 (liveness_proof_script)
// needs to thread handler-param witness values (similar to
// cover_trace_proof at :1192) into the .init pk call-site.

spec Repro4
program_id "11111111111111111111111111111111"

type State
  | Uninitialized
  | Active of { c : U8 }

type Error | E

handler init (p : Pubkey) : State.Uninitialized -> State.Active {
  permissionless
  effect { c := 1 }
}

liveness foo : State.Uninitialized ~> State.Active via [init] within 1

repro-05-uninterpreted-helper.qedspec

// Finding #5 — Uninterpreted helpers in requires/ensures never declared
//
// Generated Spec.lean never declares `foo`. lake build:
//   error: Unknown identifier `foo`
//
// This directly contradicts the docstring at ast.rs:645 which promises
// "downstream codegen declares them as uninterpreted symbols (axioms or
// Lean defs) in the support module." Exhaustive grep across
// crates/qedgen/src/ finds zero axiom/opaque emission for Expr::App.
//
// Expected: top of generated Spec.lean contains `axiom foo : Nat → Prop`.
// Actual: no declaration → Lean rejects.
//
// Fix site: Expr::App renderer needs to walk the spec, collect every
// distinct (func_name, arity, arg_types), and emit axiom declarations.
// Simplest v1: assume Prop in boolean contexts, emit
// `axiom foo : T1 → T2 → ... → Prop` at the top.

spec Repro5
program_id "11111111111111111111111111111111"

type State
  | Uninitialized
  | Active of { c : U8 }

type Error | E

handler h (y : U8) : State.Active -> State.Active {
  permissionless
  requires foo(y) else E
  effect { c := 1 }
}

repro-06-cover-witness-bool.qedspec

// Finding #6 — Cover-witness state constructor uses "0" for Bool and
// non-Nat types
//
// Generated Lean cover-trace witness:
//   let pk : Pubkey := ⟨0, 0, 0, 0⟩
//   let s0 : State := ⟨0, .Uninitialized⟩
//   let s1 : State := ⟨1, .Active⟩
// but `flag : Bool`, so `0` and `1` fail OfNat synthesis.
//
// lake build:
//   error: failed to synthesize instance of type class `OfNat Bool 0`
//
// Expected: `⟨false, .Uninitialized⟩`, `⟨true, .Active⟩`
// Actual: `⟨0, ...⟩`, `⟨1, ...⟩`
//
// Fix site: crates/qedgen/src/lean_gen.rs:998 WitnessState::new
// hard-codes exactly two cases:
//   let val = match map_type(typ) {
//       "Pubkey" => "pk".to_string(),
//       _ => "0".to_string(),
//   };
// Add `"Bool" => "false"` (plus the U16/U32 cases from finding #1).
//
// Related: percolator's header comment at examples/rust/percolator/
// percolator.qedspec:19-20 already recommends U8+discriminator over
// Bool "for simpler codegen" — worth promoting to a DSL-level
// recommendation until this fix lands.

spec Repro6
program_id "11111111111111111111111111111111"

type State
  | Uninitialized
  | Active of { flag : Bool }

type Error | E

handler init : State.Uninitialized -> State.Active {
  permissionless
  effect { flag := true }
}

cover foo [init]

repro-07-pubkey-literal-assign.qedspec

// Finding #7 — qedgen check accepts Pubkey := <integer>
//
// Passes `qedgen check` with 0 warnings, 0 info. Generated Lean:
//   { key := 0, ... }
//
// lake build:
//   error: failed to synthesize instance of type class `OfNat Pubkey 0`
//
// The DSL has no documented Pubkey-literal syntax. Either:
//   (a) `Pubkey := <int>` is valid — needs to lower to
//       `(OfNat.ofNat n : Pubkey)` with an instance, or
//   (b) `Pubkey := <int>` is invalid — should fail at qedgen check
//       with a clear error (matching v2.6.2 S5's philosophy).
//
// Currently it passes check and fails at Lean typecheck — the exact
// "silent codegen corruption" failure mode v2.6.2 was refactored to
// avoid.
//
// Fix site: crates/qedgen/src/rust_codegen_util.rs:364
// (check_effect_targets) validates only that the effect's target name
// is declared, never the RHS type.
//
// Workaround motivation: this is how I ended up with
// `match_schedule_graph_pda := 0` in my initial spec — there's no
// canonical way to express "uninitialized Pubkey / Pubkey::default"
// in qedspec, so I reached for `0`. qedgen check said OK, Lean said
// no. Consider documenting a canonical `.default` or `Pubkey.zero`
// literal alongside the fix.

spec Repro7
program_id "11111111111111111111111111111111"

type State
  | Uninitialized
  | Active of { key : Pubkey }

type Error | E

handler h : State.Uninitialized -> State.Active {
  permissionless
  effect { key := 0 }
}

repro-08-pubkey-literal-compare.qedspec

// Finding #8 — qedgen check accepts state.<Pubkey-field> != <integer>
//
// Passes `qedgen check`. Generated Lean guard:
//   s.key ≠ 0
// lake build:
//   error: failed to synthesize instance of type class `OfNat Pubkey 0`
//
// Same root cause as Finding #7 — no operand-type validation on
// comparison operators in `requires`. Covered by the same fix:
// extending check_effect_targets (or adding a new check_requires_types)
// to validate RHS/operand types against field types.

spec Repro8
program_id "11111111111111111111111111111111"

type State
  | Uninitialized
  | Active of { key : Pubkey }

type Error | E

handler h : State.Active -> State.Active {
  permissionless
  requires state.key != 0 else E
  effect { }
}