Expand description
§Module: gate_verify
Typed proof/disproof predicates for gated [/] review items (#optverify).
A gated review item often names an exact ops.log marker that PROVES it
(e.g. live_prompt_drift_auto_recovered) and an exact string that DISPROVES
it (e.g. looks like a manual cleanup). When the gate carries those as a
typed predicate, the binary can decide proof/disproof itself every time it
already reads ops.log — turning a standing human gate into an automatic
check (no dedicated live-verify session).
§Persistence (#optv1)
The predicate is carried inline on the item text as an HTML-comment
annotation so it round-trips verbatim through the pending parser without
touching the [/<gate_type>] checkbox grammar:
- [/] [#saev] early receipt ... <!-- gate-verify verify="early_receipt_accepted" disproof="false receipt-timeout" set_at="1749526200" -->Only markers emitted at or after set_at count, so a stale pre-gate
marker can never falsely prove a freshly re-opened gate.
§Scan (#optv2)
scan_ops_log is a pure function over (predicate, ops.log content) →
VerifyOutcome. Disproof wins ties (a disproved gate must never
auto-resolve); neither marker → Pending.
§Prose exclusion (#gng8)
Several ops.log entries embed document content (for example
queue_diff_active_prompt_differs ... prompt_changes=["..."], route
prompt={:?}, session tail={:?}). Backlog or response text that merely
mentions a marker token would otherwise prove the gate from its own
description. Embedded content always arrives through {:?} debug
formatting, which wraps strings in double quotes — so the scan strips
double-quoted spans from each message before matching. Structured marker
emissions ([claim] cross-session-reject pane_id=...,
[ipc-socket] early_receipt_accepted ..., [s760] clear-decision ...) are
plain unquoted message text and must stay that way to remain provable. The
built-in s760_clear_decision_clear_true verifier is stricter than a
substring: it accepts only anchored [<epoch>] [s760] clear-decision ...
lines and checks optIn=true, pct >= threshold, and clear=true.
Structs§
- Gate
Predicate - Typed proof/disproof predicate carried inline on a gated
[/]item.
Enums§
- Verify
Outcome - Result of scanning
ops.logfor a gate predicate.
Constants§
- S760_
CLEAR_ DECISION_ CLEAR_ TRUE_ MARKER - Built-in verifier for the
#s760destructive clear proof. Use in a predicate asverify=ops_log:s760_clear_decision_clear_true.
Functions§
- parse_
gate_ predicate - Parse the inline
<!-- gate-verify ... -->annotation out of item text. - parse_
predicate_ spec - Parse a
verify=...;disproof=...predicate spec (the value half of a CLI--pending-set-verify id=<spec>argument) into aGatePredicate. - render_
annotation - Render the predicate to its canonical inline annotation. Empty fields are omitted. Returns an empty string when the predicate has no fields at all.
- scan_
ops_ log - Scan
ops.logcontent for a gate predicate (#optv2, pure). - strip_
annotation - Strip any existing
<!-- gate-verify ... -->annotation from item text, trimming the trailing whitespace it leaves behind. - upsert_
annotation - Replace (or insert) the gate-verify annotation in item text. Existing annotations are removed first so the operation is idempotent.