# Checked LSN specification and reviewer handoff

## Scope

`verification/lsn.rs` is the production source imported by `src/lib.rs`. The
verified executable core accepts byte strings with exactly one `/`, one to
eight ASCII hexadecimal digits on each side, and no other bytes. It returns
`high * 2^32 + low` as an unsigned 64-bit position. The canonical formatter
emits an uppercase, minimally padded high half, `/`, and exactly eight
uppercase low-half digits. It returns the exact bytes that the Rust wrapper
converts to `String`.

The parser's `&str::as_bytes` adapter relies on Rust's valid UTF-8 invariant;
grammar validation and numeric conversion happen in the checked byte parser.
The formatter's `String::from_utf8_unchecked` adapter relies on the verified
ASCII postcondition of `format_bytes`; allocation and UTF-8 construction are
outside the Verus model. The scope excludes PostgreSQL WAL durability,
transaction scheduling, and whole-extension correctness.

## Definitions and obligations

`valid_lsn_bytes` is the grammar predicate. `hex_value` gives the base-16
mathematical value of a valid component. `lsn_bytes_value` gives the combined
position. The executable parser carries postconditions against those
definitions, including rejection of byte strings outside the grammar.
`pack_halves` states the unsigned high/low combination. `numeric_gt` and
`numeric_gte` compare parsed positions. `format_bytes` returns the bytes used
by the production `format()` adapter and specifies uppercase hex, exactly one
separator, an eight-digit low half, and parser round-trip identity.

The CI runner requires the named obligations
`lsn_parse_value_and_bounds`, `lsn_numeric_order`, and
`lsn_format_parse_roundtrip`, captures the exact pinned Verus output, and
requires a semantic mutation of the executable `pack_halves` expression to
fail verification.

## Toolchain and evidence

The verifier image is pinned in `scripts/check_lsn_verification.py` to
`ghcr.io/verus-lang/verus:0.2025.06.23.2e59154@sha256:c4d0471379b23c3c6f52e3d7226c7dad28f488c4288e14c623002bd279a745e0`.
The exact invocation omits the unsupported `--verify` flag and runs
`verus --triggers-mode silent verification/lsn.rs`. CI fails closed if the
baseline exits unsuccessfully, omits a zero-error verification summary, reports
fewer than the required obligations, or accepts the semantic mutation.

## Caller inventory

- `src/version.rs`: LSN parse, formatting, ordering, and frontier merge.
- `src/scheduler/watermark.rs` and `src/scheduler/mod.rs`: coordinator and
  scheduled watermark conversions and persisted frontier validation.
- `src/cdc/mod.rs`: CDC writer-fence holdback and transition ordering.
- `src/api/recovery.rs` and `src/api/refresh_ops.rs`: public recovery and
  refresh validation at durable frontier boundaries.
- `src/wal_decoder.rs`: WAL transition comparison and numeric conversion.

These callers use the checked parser and numeric helpers. Invalid persisted
frontiers return errors or refuse progress before mutating committed state.

## Independent review status

Independent specification review: **pending**. The implementation stage has
not performed or claimed the independent review required by Q1097-R10. The
reviewer should check the grammar against PostgreSQL 18, the mathematical
definitions against the executable postconditions, the UTF-8/allocation trust
boundary, and the caller inventory. Record reviewer identity, source digest,
findings, and disposition in the separate review artifact before making a
verified LSN claim.

## Known verification limits

The pinned Verus command and mutation control must run successfully before the
obligations can be claimed as proven. Database runtime coverage is separate:
this artifact does not establish scheduler, CDC holdback, or WAL transition
behavior. Candidate package and installed-library identity must be bound by
`scripts/check_lsn_candidate_binding.py` and a real packaged runtime attestation.