Skip to main content

Module gate_verify

Module gate_verify 

Source
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§

GatePredicate
Typed proof/disproof predicate carried inline on a gated [/] item.

Enums§

VerifyOutcome
Result of scanning ops.log for a gate predicate.

Constants§

S760_CLEAR_DECISION_CLEAR_TRUE_MARKER
Built-in verifier for the #s760 destructive clear proof. Use in a predicate as verify=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 a GatePredicate.
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.log content 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.