ci: make the verification gates report what they actually ran - #118
Open
rrrodzilla wants to merge 3 commits into
Open
rrrodzilla wants to merge 3 commits into
rrrodzilla wants to merge 3 commits into
Conversation
The first scheduled run after #115 unblocked it failed twice over, both times in the gates rather than in the crates. The fuzz jobs installed nothing and said so in a step that went green. `taiki-e/install-action@cargo-fuzz` is a branch, not a tag, abandoned at a 2024 commit that leaves the tool unset: it warns, exits successfully, and installs nothing, so all seven targets then failed with "no such command: fuzz". The same ref form was used for nextest, cargo-deny, and cargo-audit, which work today only because upstream still maintains those branches. All four now name the tool through `with: tool:`, which does not depend on how a ref happens to resolve. The kani job killed its runner having proved two of nineteen harnesses. It spent twenty-two minutes inside `builder_missing_issuer_errors` — a harness that takes no symbolic input at all — while CBMC unwound the panic-formatting path for an out-of-bounds string slice, until the machine went down under it. One command for nineteen harnesses reports whichever it reached first and abandons the rest, so the split is one harness per job with a timeout: an expensive harness now costs its own job and is named in the report. Which harnesses need tighter bounds is a question for the next run, since this one could not reach them. Locally `task kani` runs the whole set, which is what had been taking the terminal session with it. README and Taskfile now say so, and `task kani:harness -- <name>` runs one.
With the install step fixed, cargo-fuzz ran and stopped at "sanitizer is incompatible with statically linked libc". It defaults to the triple it was itself built for, and install-action ships a musl-linked binary, so every target was being built for x86_64-unknown-linux-musl. Naming the host triple keeps that a property of how the tool was packaged rather than of what gets fuzzed. Also records what splitting the Kani job showed, now that there is a result to record: nine of the thirteen attestation harnesses prove in minutes, and none of the six agent-uri harnesses converge. Four of those exhaust the runner in about six minutes, which is before any job timeout can fire, so `timeout-minutes` bounds some of this and not all of it.
With the target fixed, cargo-fuzz built and libFuzzer started, then refused: "The required directory fuzz/corpus/parse_query does not exist". The corpus is a growing build artifact and is gitignored, so a fresh checkout has no such directory, and libFuzzer will not create the one it writes to. Anyone who has fuzzed locally already has it, which is what kept this hidden behind the two earlier faults: the gate had never once run on a checkout that had not fuzzed before. The Taskfile has the same gap for a fresh clone, so both create the directory now. Verified locally by moving the corpus aside to reproduce the CI failure exactly, then confirming the fix: 448,693 runs in 11 seconds.
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.
Closes #117.
The first scheduled verification run after #115 unblocked it
(run 30672101564)
failed in two independent ways, neither of them a defect in the crates.
Miri passed in the same run:
agent-uri196 tests,agent-uri-attestation193 tests, 0 failures, under
-Zmiri-disable-isolation.The fuzz gate installed nothing and went green
cargo-fuzzis a branch on that action, not a tag, pinned at a commit dated2024-03-02;
cargo-denyresolves to 2026-07-30. The stale code leaves the toolunset, warns, and exits successfully having installed nothing, after which
all seven targets failed with
no such command: 'fuzz'.The failing jobs are the symptom. The defect is an install step that no-ops
and still reports success.
nextest,cargo-deny, andcargo-auditused thesame ref form and work today only because upstream still maintains those
branches — not because of anything this repository controls. All four now name
the tool through
with: tool:on@v2.The kani gate killed its runner having proved 2 of 19
Exit 143,
The runner has received a shutdown signal, ~24 minutes in, with notimeout-minuteson the job. Not a cancellation:miricontinued in the samerun for another 25 minutes and passed.
Checking harness proofs::claims_proofs::builder_construction_never_panicsVERIFICATION:- SUCCESSFULChecking harness proofs::claims_proofs::builder_missing_issuer_errorsTwenty-two minutes in one harness, CBMC unwinding
floor_char_boundary→slice_error_fail_rt→slice_error_fail: thepanic-message formatting for an out-of-bounds string slice.
The harness takes no symbolic input at all, and the one directly below it —
identical but for the
.build()call — finishes in a second.build()returnsat the missing
agent_keybefore reachingAgentUri::parse, so the cost is inwhat the goto-program contains, not what the concrete path runs. Reading a
harness does not predict its cost.
So this PR fixes the structure and leaves the bounds alone: one harness per job
with
timeout-minutes: 20,fail-fast: false. An expensive harness now costsits own job and is named in the report instead of starving the other 18. The
Kani toolchain cache is extended to
~/.cargo/binso 19 jobs do not each buildthe verifier from source.
This PR does not make the Kani gate green. Whichever harnesses do not
converge will now time out individually, which is the point: that is the data
needed to bound them, and this run could not produce it. Until then a
timed-out harness is an unproved property, not a failed one.
Local runs
task kaniruns the whole set, and it has been killing the terminal session itwas launched from — consistent with the same non-convergence meeting the OOM
killer. README and Taskfile now say so, and
task kani:harness -- <name>runsone harness.
Verification
ci.ymlparses and the matrix expands to 19 entries across the two crates;task --listshows both Kani tasks. The gates themselves areworkflow_dispatchonly, so they are exercised by dispatching this branch rather than by the PR
checks — results to follow on the PR.