fix(trace): the published schema rejected traces flowproof itself writes - #325
Merged
Conversation
There was a problem hiding this comment.
Pull request overview
Fixes a contract mismatch in flowproof-trace where the published JSON Schema rejected valid traces that flowproof itself records/replays, by bringing the schema (and its conformance fixture) back into alignment with emitted action variants.
Changes:
- Added missing
captureandset_checkedvariants (and their param shapes) totrace-v1.schema.json. - Extended the schema conformance fixture to include
capture(including counted capture) andset_checked, and updated the test’s expected step count. - Updated documentation and changelog to reflect the corrected action set and the contract fix.
Reviewed changes
Copilot reviewed 5 out of 5 changed files in this pull request and generated 2 comments.
Show a summary per file
| File | Description |
|---|---|
| docs/trace-format.md | Updates the documented action.type enum list to include upload, capture, and set_checked. |
| crates/flowproof-trace/tests/schema_conformance.rs | Adjusts the conformance test expectations/comments for the expanded fixture. |
| crates/flowproof-trace/tests/fixtures/sample.trace.jsonl | Adds fixture steps exercising capture (text + counted) and set_checked. |
| crates/flowproof-trace/schema/trace-v1.schema.json | Adds capture and set_checked to the action enum and specifies their param requirements. |
| CHANGELOG.md | Documents the schema/contract fix and why it previously went undetected. |
💡 Add Copilot custom instructions for smarter, more guided reviews. Learn how to get started.
Comment on lines
+5
to
+7
| {"id": "s0004", "intent": "Remember the order total", "action": {"type": "capture", "params": {"name": "total"}}, "selectors": [{"tier": "native_id", "provenance": "web", "confidence": 1.0, "payload": {"id": "orderTotal"}}], "sync": {"pre": [{"kind": "element_exists", "selector_ref": 0, "timeout_ms": 10000}], "post": []}, "artifacts": {}} | ||
| {"id": "s0005", "intent": "Remember how many order rows appear", "action": {"type": "capture", "params": {"name": "rows", "count": true}}, "selectors": [{"tier": "native_id", "provenance": "web", "confidence": 1.0, "payload": {"css": ".order-row"}}], "sync": {"pre": [{"kind": "element_exists", "selector_ref": 0, "timeout_ms": 10000}], "post": []}, "artifacts": {}} | ||
| {"id": "s0006", "intent": "Accept the terms", "action": {"type": "set_checked", "params": {"checked": true}}, "selectors": [{"tier": "native_id", "provenance": "web", "confidence": 1.0, "payload": {"id": "terms"}}], "sync": {"pre": [{"kind": "element_exists", "selector_ref": 0, "timeout_ms": 10000}], "post": []}, "artifacts": {}} |
Comment on lines
+52
to
+55
| // s0004/s0005 are the text and COUNTED capture readings and s0006 is | ||
| // `set_checked` - the three action types the schema did not list, which | ||
| // is exactly why this fixture has to carry one of each: the enum was | ||
| // wrong for as long as nothing here exercised them. |
AminChirazi
force-pushed
the
fix/schema-missing-actions
branch
from
August 1, 2026 09:46
373ec5c to
ed69eb7
Compare
The action `type` enum in trace-v1.schema.json listed thirteen of the fifteen actions the engine emits. `capture` and `set_checked` were missing, so any trace containing a `Remember …` or a `Check …` step failed validation against the schema this repository publishes as the contract. Nothing caught it, and the reason is the interesting part: the conformance test validates one fixture, and that fixture contained neither action. The schema was wrong for exactly as long as nothing exercised it — a gap that fails green, on the artifact external consumers validate against rather than on anything our own code reads. Both are in the enum now with their param shapes, and the fixture carries one of each — including the counted `capture` reading — so the enum cannot drift from the emitted actions again without a red test. Verified the other way too: with the old enum restored, the extended fixture fails. Co-Authored-By: Claude Opus 5 <noreply@anthropic.com>
AminChirazi
force-pushed
the
fix/schema-missing-actions
branch
from
August 1, 2026 09:56
ed69eb7 to
98387c1
Compare
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
Independent of the grammar-gap stack (#316 → #322) and of #324 — branched off
main, mergeable on its own.What was wrong
Actioninflowproof-traceserialises fifteen action types. Thetypeenum in the publishedtrace-v1.schema.jsonlisted thirteen. Missing:captureandset_checked.So any trace containing a
Remember …step or aCheck …step fails validation against the schema this repository publishes as its contract — while being a perfectly correct trace that flowproof records and replays.Why nothing caught it
The conformance test validates exactly one fixture, and that fixture contained neither action. The schema was wrong for precisely as long as nothing exercised it.
That is the shape worth naming: it fails green, and it fails on the artifact external consumers validate against rather than on anything our own code reads. Our engine never consults the schema, so nothing in the normal loop would ever notice.
The fix
captureandset_checkedadded to the enum, with their param shapes in the sameallOfstyle as the existing actions — includingcapture's optionalcount(the counted reading) andset_checked'scheckedstate.docs/trace-format.md's action list updated in the same commit — it was missinguploadtoo, which had drifted the same way.Verified in both directions
Adding to the fixture only proves the schema accepts what we write. So I also checked the negative: with the old enum restored, the extended fixture fails validation. That is the evidence that the new fixture lines are load-bearing rather than decorative.
Notes for the reviewer
cargo test --workspacehas one failure on macOS,a_control_record_states_the_containment_tier_it_ran_under— pre-existing on cleanmain, and fixed separately in fix(cli): the suite was red off Linux, for a wording #324. It is untouched here rather than fixed twice across two PRs.cargo fmt --checkandcargo clippy --workspace --all-targets -- -D warningsare clean.🤖 Generated with Claude Code