Repository navigation
Conversation
Codex Review SummaryThis comment shows the latest Codex review activity on this pull request.
ℹ️ About Codex in GitHubYour team has set up Codex to review pull requests in this repo. Reviews are triggered when you
Codex reacts with 👀 while any review is running, comments if it has suggestions, and reacts with 👍 once all reviews finish with no findings. |
Codecov Report✅ All modified and coverable lines are covered by tests. Additional details and impacted files@@ Coverage Diff @@
## Gvlifygrl474ib42743gciqjrsgpm27ix #3797 +/- ##
==================================================================
Coverage 92.94% 92.94%
==================================================================
Files 16 16
Lines 2466 2466
==================================================================
Hits 2292 2292
Misses 174 174 ☔ View full report in Codecov by Harness. 🚀 New features to boost your workflow:
|
joshlf
changed the title
joshlf
force-pushed
the
Gum62fph6nc5t4h6fpqbuck4qgm2jz2ht
branch
2 times, most recently
from
October 7, 2026 08:29
ed3e62f to
87a1133
Compare
joshlf
force-pushed
the
Gvlifygrl474ib42743gciqjrsgpm27ix
branch
from
October 7, 2026 08:43
78eade4 to
e2adb94
Compare
joshlf
force-pushed
the
Gum62fph6nc5t4h6fpqbuck4qgm2jz2ht
branch
from
October 7, 2026 08:43
87a1133 to
c3c1df7
Compare
joshlf
force-pushed
the
Gvlifygrl474ib42743gciqjrsgpm27ix
branch
from
October 7, 2026 09:10
e2adb94 to
40e1852
Compare
joshlf
force-pushed
the
Gum62fph6nc5t4h6fpqbuck4qgm2jz2ht
branch
from
October 7, 2026 09:10
c3c1df7 to
ae3bad7
Compare
joshlf
force-pushed
the
Gvlifygrl474ib42743gciqjrsgpm27ix
branch
from
October 7, 2026 09:13
40e1852 to
6f0386d
Compare
joshlf
force-pushed
the
Gum62fph6nc5t4h6fpqbuck4qgm2jz2ht
branch
2 times, most recently
from
October 7, 2026 09:39
dd6c51b to
bb739ca
Compare
joshlf
changed the title
joshlf
force-pushed
the
Gvlifygrl474ib42743gciqjrsgpm27ix
branch
2 times, most recently
from
October 7, 2026 10:08
0825ffb to
d93a15f
Compare
joshlf
force-pushed
the
Gum62fph6nc5t4h6fpqbuck4qgm2jz2ht
branch
3 times, most recently
from
October 7, 2026 11:33
ae95724 to
527a5db
Compare
joshlf
changed the title
joshlf
force-pushed
the
Gvlifygrl474ib42743gciqjrsgpm27ix
branch
from
October 7, 2026 18:10
d93a15f to
361f486
Compare
joshlf
force-pushed
the
Gum62fph6nc5t4h6fpqbuck4qgm2jz2ht
branch
2 times, most recently
from
October 7, 2026 20:06
19884d0 to
f4cb3b5
Compare
joshlf
force-pushed
the
Gvlifygrl474ib42743gciqjrsgpm27ix
branch
from
October 7, 2026 20:06
361f486 to
da49a8a
Compare
joshlf
force-pushed
the
Gum62fph6nc5t4h6fpqbuck4qgm2jz2ht
branch
2 times, most recently
from
October 7, 2026 22:09
c127687 to
1f47790
Compare
joshlf
force-pushed
the
Gvlifygrl474ib42743gciqjrsgpm27ix
branch
from
October 8, 2026 09:20
da49a8a to
d43cf40
Compare
joshlf
force-pushed
the
Gum62fph6nc5t4h6fpqbuck4qgm2jz2ht
branch
from
October 8, 2026 09:20
1f47790 to
d385738
Compare
Keep every production implementation, including element sizing and rounding word decoding, identical to upstream main. The new upstream Ref benchmarks expose regressions in the earlier checked-add byte helper, so remove that helper and restore the original element-sizing body and its comments. Retain the new runtime-layout benchmark, measured against the unchanged upstream implementation; no pre-existing upstream snapshot is changed. Normalize sizing specifications with independent widened arithmetic and prove equivalence with checked arithmetic. Use equivalent modular and quotient/remainder specifications for padding and metadata. Preserve the independent capacity and selected-size evidence. Partition endian proofs and generate only the requested sized branch in layout proofs. Use the macro's checked acyclic contract dependencies for rounding decoders, capacity, padding and element sizing. All substituted providers must pass unrestricted implementation proofs in the same configuration. Preserve upstream's broadened byte-count bound proof and duplicate-proof removal. Remove the duplicate handwritten padding harness, retaining the unrestricted generated contract. Replace the misleading expected-panic Kani harness with an ordinary regression using the existing pre-1.57 gate. This PR adds no duplicate CI/Python machinery. The parent removes every kani_slow gate, explicitly ignores only the two resource-limited metadata contracts, and rejects enabled proofs that substitute ignored providers. The final compiled graph selects 80 enabled harnesses, inspects two ignored proofs and validates 30 generated providers. Failed or timed-out proofs establish nothing; no verification safety or contract checks are disabled. Validation: all 107 codegen benchmarks and 155 MSRV library tests pass. The restored original sizing proof times out at the 300-second local limit. It remains enabled; no successful contract or full-suite result is claimed. Makes progress on #3792 Agent-authored-by: AI agent acting on Josh Liebow-Feeser's behalf gherrit-pr-id: Gum62fph6nc5t4h6fpqbuck4qgm2jz2ht
joshlf
force-pushed
the
Gum62fph6nc5t4h6fpqbuck4qgm2jz2ht
branch
from
October 8, 2026 10:02
d385738 to
ff91257
Compare
joshlf
changed the title
joshlf
force-pushed
the
Gvlifygrl474ib42743gciqjrsgpm27ix
branch
from
October 8, 2026 10:02
d43cf40 to
c5aa42d
Compare
jswrenn
requested changes
Oct 8, 2026
Collaborator
There was a problem hiding this comment.
Would prefer to remove this benchmark. We basically don't ever work over runtime layouts, and so benchmarks involving them are highly misleading.
This branch has not been deployed
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
3 participants
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.
Reduce Kani verification cost with independent specifications and checked
acyclic contract dependencies. Preserve every upstream production algorithm,
including element sizing and rounding-word decoding. Normalize padding and
metadata specifications while keeping independent capacity and selected-size
evidence. Partition endian proofs and specialize sized proof generation.
Upstream's new Ref codegen benchmarks exposed regressions in the earlier
byte-size helper. Remove that helper and restore the original sizing body
and comments. Retain the added runtime-layout benchmark with a baseline
measured against upstream's unchanged implementation. No pre-existing upstream
assembly or LLVM-MCA snapshot is changed.
Rebased on upstream
main(dcb8149). The parent removes the entirekani_slowmechanism and keeps only the two metadata ignores justified bylocal results. Preserve upstream's independent duplicate-proof removal and
strengthened unrestricted byte-count bound proof, which passes in 6.8 seconds.
The final compiled graph checks 30 providers and selects 80 enabled harnesses
with exactly two skips. No duplicate CI/Python machinery or disabled safety
checks are added. Ignored contracts remain unverified; enabled-suite CI is
pending.
Validation: all 107 assembly/LLVM-MCA benchmarks and 155 MSRV library tests
pass, along with repository pre-push checks. The runtime benchmark matches
the unchanged upstream implementation. The restored original sizing proof timed out at the 300-second local
limit. It remains enabled, and callers must verify its provider; no successful
contract or complete-suite verification is claimed. CI verification is pending.
Makes progress on #3792.
Authored by an AI agent acting on Josh Liebow-Feeser's behalf.
Latest Update: v19 — Compare vs v18
📚 Full Patch History
Links show the diff between the row version and the column version.
⬇️ Download this PR
Branch
git fetch origin refs/heads/Gum62fph6nc5t4h6fpqbuck4qgm2jz2ht && git checkout -b pr-Gum62fph6nc5t4h6fpqbuck4qgm2jz2ht FETCH_HEADCheckout
git fetch origin refs/heads/Gum62fph6nc5t4h6fpqbuck4qgm2jz2ht && git checkout FETCH_HEADCherry Pick
git fetch origin refs/heads/Gum62fph6nc5t4h6fpqbuck4qgm2jz2ht && git cherry-pick FETCH_HEADPull
Stacked PRs enabled by GHerrit.