Repository navigation
Conversation
This was referenced Oct 2, 2026
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. |
This was referenced Oct 2, 2026
Codecov Report❌ Patch coverage is
Additional details and impacted files@@ Coverage Diff @@
## Glbefkopwxutlxlg5qgtbtb3p6a5o73ow #3752 +/- ##
=====================================================================
- Coverage 59.30% 58.41% -0.90%
=====================================================================
Files 23 24 +1
Lines 3853 3912 +59
=====================================================================
Hits 2285 2285
- Misses 1568 1627 +59 ☔ View full report in Codecov by Harness. 🚀 New features to boost your workflow:
|
joshlf
force-pushed
the
Gsnkt6couze5saom2wzruz5yjl6gkrcsg
branch
from
October 2, 2026 15:39
fe68755 to
c35cd54
Compare
joshlf
force-pushed
the
Glbefkopwxutlxlg5qgtbtb3p6a5o73ow
branch
2 times, most recently
from
October 2, 2026 19:39
5b1b61e to
cb6ca5a
Compare
joshlf
force-pushed
the
Gsnkt6couze5saom2wzruz5yjl6gkrcsg
branch
from
October 2, 2026 19:39
c35cd54 to
657e05b
Compare
joshlf
force-pushed
the
Gsnkt6couze5saom2wzruz5yjl6gkrcsg
branch
from
October 2, 2026 21:06
657e05b to
9542042
Compare
joshlf
force-pushed
the
Glbefkopwxutlxlg5qgtbtb3p6a5o73ow
branch
from
October 2, 2026 21:06
cb6ca5a to
1aa345d
Compare
joshlf
force-pushed
the
Gsnkt6couze5saom2wzruz5yjl6gkrcsg
branch
from
October 3, 2026 16:09
9542042 to
e1bee78
Compare
joshlf
force-pushed
the
Glbefkopwxutlxlg5qgtbtb3p6a5o73ow
branch
from
October 3, 2026 16:09
1aa345d to
2753b1b
Compare
joshlf
changed the title
joshlf
force-pushed
the
Glbefkopwxutlxlg5qgtbtb3p6a5o73ow
branch
from
October 4, 2026 02:57
2753b1b to
500ee0e
Compare
joshlf
force-pushed
the
Gsnkt6couze5saom2wzruz5yjl6gkrcsg
branch
from
October 5, 2026 13:03
6e23a28 to
0fea328
Compare
joshlf
force-pushed
the
Glbefkopwxutlxlg5qgtbtb3p6a5o73ow
branch
from
October 5, 2026 15:25
ec1f50b to
738e6cc
Compare
joshlf
force-pushed
the
Gsnkt6couze5saom2wzruz5yjl6gkrcsg
branch
from
October 5, 2026 15:25
0fea328 to
40ec1d7
Compare
This was referenced Oct 5, 2026
joshlf
force-pushed
the
Glbefkopwxutlxlg5qgtbtb3p6a5o73ow
branch
from
October 5, 2026 21:12
738e6cc to
c215a36
Compare
joshlf
force-pushed
the
Gsnkt6couze5saom2wzruz5yjl6gkrcsg
branch
from
October 5, 2026 21:12
40ec1d7 to
8351f15
Compare
joshlf
force-pushed
the
Gsnkt6couze5saom2wzruz5yjl6gkrcsg
branch
from
October 5, 2026 21:44
8351f15 to
984e4fa
Compare
joshlf
force-pushed
the
Glbefkopwxutlxlg5qgtbtb3p6a5o73ow
branch
2 times, most recently
from
October 5, 2026 22:08
93a8437 to
fcab386
Compare
joshlf
force-pushed
the
Gsnkt6couze5saom2wzruz5yjl6gkrcsg
branch
from
October 5, 2026 22:08
984e4fa to
c562dfa
Compare
joshlf
force-pushed
the
Glbefkopwxutlxlg5qgtbtb3p6a5o73ow
branch
from
October 6, 2026 00:32
fcab386 to
629db99
Compare
joshlf
force-pushed
the
Gsnkt6couze5saom2wzruz5yjl6gkrcsg
branch
from
October 6, 2026 00:32
c562dfa to
0b2a91f
Compare
This was referenced Oct 6, 2026
joshlf
force-pushed
the
Glbefkopwxutlxlg5qgtbtb3p6a5o73ow
branch
from
October 6, 2026 15:45
629db99 to
4f5bd34
Compare
joshlf
force-pushed
the
Gsnkt6couze5saom2wzruz5yjl6gkrcsg
branch
2 times, most recently
from
October 7, 2026 11:10
28ab520 to
fc39dac
Compare
This was referenced Oct 7, 2026
Connect conditional trailing-layout contracts to independent unbounded formulas for size, capacity, wrapping padding and checked overflow. Preserve the broad Raw arithmetic lemmas used by composition proofs. Express trailing-size specifications through the existing mathematical formula and optional decoded size. Prove that the compact contract still implies the independently authored exact representation obligations. Compare complete optional trailing sizes and capacities with independent checked Rust arithmetic. Visible alignment/phase witnesses cover every nonzero encoding without restricting physical offsets or imposing extra size bounds. Validation: fresh pinned extraction and complete-model golden comparison; independent golden/live Lean builds, required-contract checks, and the transitive axiom audit. gherrit-pr-id: Gsnkt6couze5saom2wzruz5yjl6gkrcsg Agent-authored-by: AI agent acting on joshlf's behalf
joshlf
force-pushed
the
Glbefkopwxutlxlg5qgtbtb3p6a5o73ow
branch
from
October 13, 2026 16:33
0f679b9 to
7be8c70
Compare
joshlf
force-pushed
the
Gsnkt6couze5saom2wzruz5yjl6gkrcsg
branch
from
October 13, 2026 16:33
fc39dac to
777bc82
Compare
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
2 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.
Connect conditional trailing-layout contracts to independent unbounded formulas
for size, capacity, wrapping padding and checked overflow. Preserve the broad
Raw arithmetic lemmas used by composition proofs.
Express trailing-size specifications through the existing mathematical
formula and optional decoded size. Prove that the compact contract still
implies the independently authored exact representation obligations.
Compare complete optional trailing sizes and capacities with independent
checked Rust arithmetic. Visible alignment/phase witnesses cover every nonzero
encoding without restricting physical offsets or imposing extra size bounds.
Validation: fresh pinned extraction and complete-model golden comparison;
independent golden/live Lean builds, required-contract checks, and the
transitive axiom audit.
Agent-authored-by: AI agent acting on joshlf's behalf
Latest Update: v26 — Compare vs v25
📚 Full Patch History
Links show the diff between the row version and the column version.
⬇️ Download this PR
Branch
git fetch origin refs/heads/Gsnkt6couze5saom2wzruz5yjl6gkrcsg && git checkout -b pr-Gsnkt6couze5saom2wzruz5yjl6gkrcsg FETCH_HEADCheckout
git fetch origin refs/heads/Gsnkt6couze5saom2wzruz5yjl6gkrcsg && git checkout FETCH_HEADCherry Pick
git fetch origin refs/heads/Gsnkt6couze5saom2wzruz5yjl6gkrcsg && git cherry-pick FETCH_HEADPull
Stacked PRs enabled by GHerrit.