fix(verify): fail closed on unsupported safety invariants (ARN-213) - #397
fix(verify): fail closed on unsupported safety invariants (ARN-213)#397rita-aga wants to merge 4 commits into
Conversation
ADR-0178: InvariantKind::Unverifiable is a hard cascade failure, not a warning. CascadeResult gains structured diagnostics with source spans; SMT, Stateright, composite, simulation, and property evaluation all treat unsupported safety as not holding. ORDER fixture declares payment_captured so the supported path stays green.
Independent Grok code review (ARN-213 / ADR-0178)SummaryCorrect fail-closed fix for unsupported safety invariants: cascade capability gate forces What was done well
FindingsImportantNone that block the capability-gate contract. Suggestions
Plan alignmentMeets ADR-0178 readiness gates: no cascade with Unverifiable reports Residual risks
No Critical or Important must-fix defects on the verification contract. Verdict: PASS |
|
@greptile review |
ARENA SHIPPABLE · Grok · 2026-07-14 11:57 PDTPR: #397 Checklist
Summaryunsupported invariants fail closed |
![greptile-apps[bot]](https://avatars.githubusercontent.com/in/867647?s=60&v=4){kind=small}
| fn find_invariant_source_span(source: &str, name: &str) -> Option<SourceSpan> { | ||
| let bytes = source.as_bytes(); | ||
| let mut search_from = 0usize; | ||
| while let Some(rel) = source[search_from..].find("[[invariant]]") { | ||
| let table_start = search_from + rel; | ||
| let after_header = table_start + "[[invariant]]".len(); | ||
| let next_table = source[after_header..] | ||
| .find("\n[") | ||
| .map(|i| after_header + i) | ||
| .unwrap_or(source.len()); | ||
| let table_body = &source[table_start..next_table]; | ||
| if invariant_table_name_matches(table_body, name) { | ||
| let end = trim_trailing_ws_end(bytes, next_table); | ||
| return Some(byte_range_to_source_span(source, table_start, end)); | ||
| } | ||
| search_from = after_header; | ||
| } | ||
| None |
There was a problem hiding this comment.
find_invariant_source_span uses "\n[" to locate the next table header and bound the current invariant's body. This will incorrectly truncate the span if any TOML value within the invariant block uses a multiline literal string (triple-quoted """ or ''') that has a line starting with [. For example, a description = """ field containing [example text] on its own continuation line would cause next_table to land inside the string body, producing a span that is shorter than the actual invariant table. The ADR (Risks section) acknowledges source-location extraction could drift; the tests cover only the happy-path and repeated-table cases and would not catch this.
Prompt To Fix With AI
This is a comment left during a code review.
Path: crates/temper-verify/src/cascade.rs
Line: 665-682
Comment:
**TOML boundary detection fragile against multiline string values**
`find_invariant_source_span` uses `"\n["` to locate the next table header and bound the current invariant's body. This will incorrectly truncate the span if any TOML value within the invariant block uses a multiline literal string (triple-quoted `"""` or `'''`) that has a line starting with `[`. For example, a `description = """` field containing `[example text]` on its own continuation line would cause `next_table` to land inside the string body, producing a span that is shorter than the actual invariant table. The ADR (Risks section) acknowledges source-location extraction could drift; the tests cover only the happy-path and repeated-table cases and would not catch this.
How can I resolve this? If you propose a fix, please make it concise.
| /// Structured diagnostic for a safety invariant the verifier cannot encode. | ||
| #[derive(Debug, Clone, PartialEq, Eq, serde::Serialize, serde::Deserialize)] | ||
| pub struct UnsupportedInvariantDiagnostic { | ||
| /// Stable machine-readable code ([`UNSUPPORTED_SAFETY_INVARIANT_CODE`]). | ||
| pub code: String, |
There was a problem hiding this comment.
UnsupportedInvariantDiagnostic.code is typed as String even though it can only ever hold the single compile-time constant UNSUPPORTED_SAFETY_INVARIANT_CODE. This allocates a heap string per diagnostic and allows callers to construct diagnostics with arbitrary codes, weakening the stable-code contract. Typing it as &'static str enforces the invariant at the type level and eliminates the allocation.
| /// Structured diagnostic for a safety invariant the verifier cannot encode. | |
| #[derive(Debug, Clone, PartialEq, Eq, serde::Serialize, serde::Deserialize)] | |
| pub struct UnsupportedInvariantDiagnostic { | |
| /// Stable machine-readable code ([`UNSUPPORTED_SAFETY_INVARIANT_CODE`]). | |
| pub code: String, | |
| /// Structured diagnostic for a safety invariant the verifier cannot encode. | |
| #[derive(Debug, Clone, PartialEq, Eq, serde::Serialize, serde::Deserialize)] | |
| pub struct UnsupportedInvariantDiagnostic { | |
| /// Stable machine-readable code ([`UNSUPPORTED_SAFETY_INVARIANT_CODE`]). | |
| pub code: &'static str, |
Prompt To Fix With AI
This is a comment left during a code review.
Path: crates/temper-verify/src/cascade.rs
Line: 102-106
Comment:
`UnsupportedInvariantDiagnostic.code` is typed as `String` even though it can only ever hold the single compile-time constant `UNSUPPORTED_SAFETY_INVARIANT_CODE`. This allocates a heap string per diagnostic and allows callers to construct diagnostics with arbitrary codes, weakening the stable-code contract. Typing it as `&'static str` enforces the invariant at the type level and eliminates the allocation.
```suggestion
/// Structured diagnostic for a safety invariant the verifier cannot encode.
#[derive(Debug, Clone, PartialEq, Eq, serde::Serialize, serde::Deserialize)]
pub struct UnsupportedInvariantDiagnostic {
/// Stable machine-readable code ([`UNSUPPORTED_SAFETY_INVARIANT_CODE`]).
pub code: &'static str,
```
How can I resolve this? If you propose a fix, please make it concise.…uth claim (ARN-213) Split cascade diagnostics/tests into submodules for the readability ratchet. Remove ordering(...) fixture invariant that was Unverifiable under ADR-0178 fail-closed and broke reference-spec verification.
CI fix follow-up (HEAD after 5997b3b+)Fixed CI failures from fail-closed ARN-213:
Local: |
|
@greptile review |
…-213) - Parse literal true as Tautology; accept is_true <bool> sugar - Wire Tautology through model check, prop tests, sim, SMT, runtime SpecAssert - Remove never-checked != '' and used_bytes<=quota_limit claims from specs - rustfmt cascade module split; document corpus remediation in ADR-0178
|
@greptile review Greptile follow-up (ARN-213)
|
1 participant
Summary
InvariantKind::Unverifiableis a hard verification failure (supersedes ADR-0016 warning-only handling).all_passedis never true when any safety invariant is unsupported;fail_fastskips level exploration.CascadeResult.unsupported_invariantswith stable codeVERIFY_UNSUPPORTED_SAFETY_INVARIANT, name, expression, and IOA source spans (byte + 1-based line/col).payment_capturedso the supported happy-path corpus stays green; unsupported forms covered by dedicated cascade tests (counter-to-counter, etc.).Competitor
codex/arn-213-unsupported-safety-invariantswas docs-only (ADR-0171); this PR implements the full fix under unique ADR-0178.Linear
ARN-213
Test plan
cargo test -p temper-verify— 117 lib tests + 1 integration test greentest_cascade_fails_closed_on_unsupported_safety_invarianttest_cascade_unsupported_span_multiline_and_repeatedtest_fail_fast_stops_on_unsupported_before_levelstest_cascade_fully_supported_spec_passesResidual risks
os-apps/temper-fsused_bytes <= quota_limit) will fail deploy until the verifier gains the encoding or the spec is corrected — intentional per ADR-0178.--no-verifylocally becausecargo run -p temper-cli/ full-workspace clippy cold-builds contended for disk; rely on CI.Greptile Summary
This PR implements ADR-0178:
InvariantKind::Unverifiableis now a hard cascade failure instead of a soft warning, closing the gap where the verifier could reportall_passed = truefor specs it could not fully check. All five verification backends (SMT induction, Stateright model check, composite eval, simulation, and property tests) are updated to treat unsupported invariants as standing violations, andCascadeResultgains a structuredunsupported_invariantsfield with stable error codes and TOML source spans.all_passedis gated onunsupported_invariants.is_empty();fail_fastshort-circuits before level exploration when unsupported invariants are detected; each backend independently rejects them so backend-only callers cannot paper over the gap.assert = \"true\"is nowParsedAssert::Tautology(always holds),is_true <bool>is accepted as sugar, and!= ''/ cross-counter assertions that were never model-checked are removed from platform and os-app specs; the ORDER fixture gains a declaredpayment_capturedbool so itsShipRequiresPaymentinvariant becomesBoolRequiredrather thanUnverifiable.cascade.rsmodule split intocascade/mod.rs,cascade/diagnostics.rs, andcascade/tests.rs, keeping the file under the 500-line CLAUDE.md ratchet; four new ADR-0178 regression tests cover the fail-closed path, multiline span extraction,fail_fastpre-level short-circuit, and the fully-supported happy path.Confidence Score: 5/5
The core fail-closed logic is sound and consistent across all five verification backends; the cascade gate and structured diagnostics are correct and well-tested.
Every backend independently rejects unsupported invariants, the cascade-level gate ensures all_passed cannot be true when any unsupported invariant exists, and four new regression tests cover the key scenarios. The two style findings do not affect runtime behavior.
No files require special attention for correctness; the doc comment issues are confined to types.rs and cascade/mod.rs and are purely cosmetic.
Important Files Changed
Flowchart
%%{init: {'theme': 'neutral'}}%% flowchart TD A[VerificationCascade::run] --> B[build_temper_model] B --> C[collect_unsupported_invariant_diagnostics] C --> D{unsupported_invariants empty?} D -- no + fail_fast --> E[CascadeResult all_passed=false levels=empty] D -- no + not fail_fast --> F[Run all levels each backend fails independently] D -- yes --> G[Run all levels normally] F --> H{levels_passed?} G --> H H -- yes + empty unsupported --> I[all_passed = true] H -- no OR unsupported non-empty --> J[all_passed = false] subgraph Backend fail-closed behavior L0[L0 SMT: Unverifiable not inductive] L1[L1 Stateright: standing Property always false] L2[L2 Simulation: sim_kind_violated true] L3[L3 PropTest: kind_violated true] CE[Composite eval: evaluate_one false] end F --> L0 F --> L1 F --> L2 F --> L3 F --> CE%%{init: {'theme': 'base', 'themeVariables': {"darkMode": true, "background": "#0d1117", "primaryColor": "#21262d", "primaryTextColor": "#e6edf3", "primaryBorderColor": "#8b949e", "lineColor": "#8b949e", "textColor": "#e6edf3", "edgeLabelBackground": "#161b22", "actorBkg": "#21262d", "actorBorder": "#8b949e", "actorTextColor": "#e6edf3", "actorLineColor": "#8b949e", "signalColor": "#8b949e", "signalTextColor": "#e6edf3", "noteBkgColor": "#373320", "noteBorderColor": "#d4a72c", "noteTextColor": "#f0e6c0", "labelBoxBkgColor": "#21262d", "labelBoxBorderColor": "#8b949e", "labelTextColor": "#e6edf3", "loopTextColor": "#e6edf3", "activationBkgColor": "#30363d", "activationBorderColor": "#8b949e"}}}%% flowchart TD A[VerificationCascade::run] --> B[build_temper_model] B --> C[collect_unsupported_invariant_diagnostics] C --> D{unsupported_invariants empty?} D -- no + fail_fast --> E[CascadeResult all_passed=false levels=empty] D -- no + not fail_fast --> F[Run all levels each backend fails independently] D -- yes --> G[Run all levels normally] F --> H{levels_passed?} G --> H H -- yes + empty unsupported --> I[all_passed = true] H -- no OR unsupported non-empty --> J[all_passed = false] subgraph Backend fail-closed behavior L0[L0 SMT: Unverifiable not inductive] L1[L1 Stateright: standing Property always false] L2[L2 Simulation: sim_kind_violated true] L3[L3 PropTest: kind_violated true] CE[Composite eval: evaluate_one false] end F --> L0 F --> L1 F --> L2 F --> L3 F --> CEComments Outside Diff (1)
crates/temper-platform/src/deploy.rs, line 251-265 (link)When a spec has unsupported invariants and
fail_fastis false (the current deploy pipeline default), all levels run and each backend's fail-closed handling causes every level to fail. The loop at line 251–265 broadcasts aPlatformEvent::VerifyStatusper level, so operators will see per-level failures. However, theresult.unsupported_invariantsfield is never emitted as a platform event — meaning Datadog/telemetry will surface "cascade failed" without distinguishing "verifier capability gap" from "property counterexample found." Given that the ADR calls outos-apps/temper-fsas an immediately-affected production spec, operators hitting this gate post-deploy will need to dig into span attributes rather than receiving a clear structured event.Prompt To Fix With AI
Note: If this suggestion doesn't match your team's coding style, reply to this and let me know. I'll remember it for next time!
Reviews (3): Last reviewed commit: "fix(verify): remediate corpus for fail-c..." | Re-trigger Greptile