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. |
This was referenced Oct 2, 2026
Codecov Report❌ Patch coverage is
Additional details and impacted files@@ Coverage Diff @@
## Gng7s74f35a4f6jjd5xjjmvxbwqqnnx7q #3748 +/- ##
====================================================================
Coverage ? 61.95%
====================================================================
Files ? 21
Lines ? 3709
Branches ? 0
====================================================================
Hits ? 2298
Misses ? 1411
Partials ? 0 ☔ View full report in Codecov by Harness. 🚀 New features to boost your workflow:
|
joshlf
force-pushed
the
Gcrebpateb5cosfnz4zvqhnx2xldzt6vv
branch
from
October 2, 2026 15:39
af4e7c1 to
ba7e20f
Compare
joshlf
force-pushed
the
Gng7s74f35a4f6jjd5xjjmvxbwqqnnx7q
branch
from
October 2, 2026 19:39
34c980f to
52acb9c
Compare
joshlf
force-pushed
the
Gcrebpateb5cosfnz4zvqhnx2xldzt6vv
branch
from
October 2, 2026 19:39
ba7e20f to
3f134f9
Compare
joshlf
force-pushed
the
Gng7s74f35a4f6jjd5xjjmvxbwqqnnx7q
branch
from
October 2, 2026 21:06
52acb9c to
c4e1902
Compare
joshlf
force-pushed
the
Gcrebpateb5cosfnz4zvqhnx2xldzt6vv
branch
2 times, most recently
from
October 3, 2026 16:09
663dcca to
db36ff4
Compare
joshlf
force-pushed
the
Gng7s74f35a4f6jjd5xjjmvxbwqqnnx7q
branch
2 times, most recently
from
October 4, 2026 02:57
c6b8589 to
2277ec1
Compare
joshlf
force-pushed
the
Gcrebpateb5cosfnz4zvqhnx2xldzt6vv
branch
from
October 4, 2026 02:57
db36ff4 to
24ab6aa
Compare
joshlf
force-pushed
the
Gng7s74f35a4f6jjd5xjjmvxbwqqnnx7q
branch
from
October 4, 2026 12:42
2277ec1 to
f03687c
Compare
joshlf
force-pushed
the
Gcrebpateb5cosfnz4zvqhnx2xldzt6vv
branch
from
October 5, 2026 06:11
6232850 to
1d027de
Compare
joshlf
force-pushed
the
Gng7s74f35a4f6jjd5xjjmvxbwqqnnx7q
branch
from
October 5, 2026 06:11
697ee4b to
100befe
Compare
joshlf
force-pushed
the
Gcrebpateb5cosfnz4zvqhnx2xldzt6vv
branch
from
October 5, 2026 08:19
1d027de to
eaada22
Compare
joshlf
force-pushed
the
Gng7s74f35a4f6jjd5xjjmvxbwqqnnx7q
branch
from
October 5, 2026 08:19
100befe to
6814934
Compare
Keep independent native examples for successful returns, named assumptions and tuple results. Total contracts reject panic and divergence; partial contracts admit divergence while rejecting panic and incorrect successful returns. 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: Gmasez6fvx2c6chogoybuzpgyoykiaupc Agent-authored-by: AI agent acting on joshlf's behalf
Prove exact extrema, least padding and the greatest aligned predecessor. Preserve broad Raw arithmetic results and derive recursive mathematical models contracts; compose extrema and round-down corollaries. Layout padding is introduced with its normalized implementation in the later padding proof layer. Add total Rust assertion harnesses comparing padding and round-down with independent division/remainder calculations, including usize boundary values. Keep the comparisons and their power-of-two guard visible in Rust. 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: Gxi6wprpgshggdrhvt64jphmjwhociog5 Agent-authored-by: AI agent acting on joshlf's behalf
Add mathematical-view composition and an indexed-loop adapter using upstream specifications. Independent native examples check successful outcomes, overflow and the loop progress requirements. 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: Gjr7bhllf5hkdhoipwvk4k5zbqa5q7qs7 Agent-authored-by: AI agent acting on joshlf's behalf
Develop unbounded size, alignment and capacity formulas and prove their normalization laws. Keep arithmetic assumptions explicit and independent of generated function proofs. 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: Geshtqcmx24d4schhoccr2bfxlmhdz4yi Agent-authored-by: AI agent acting on joshlf's behalf
Define recursive record semantics and prove normalization across nested fields and trailing metadata. Preserve complete inner sizes when composing layouts. 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: Gorv7wy3hyn76t7fgbuh776b3o6yz5teg Agent-authored-by: AI agent acting on joshlf's behalf
Retain the nominal Rust wrapper and define its mathematical model inline. Decode its already-positive NonZero field into alignment and phase with power-of-two, phase-bound and representability proofs. Prove the accepted domain, representation relation and round trips independently of method proofs. Encoding and decoding specifications use the mathematical pair; broad Raw lemmas preserve the original representation guarantees. Construct the rounding model using only its data fields; decoder-scoped completion proves its unchanged constraints in the construction context. Independent meaning, admission and round-trip guarantees remain explicit. Validation: fresh pinned extraction, complete golden comparison, separate golden/live builds, independent required contracts and axiom audits. gherrit-pr-id: Gng7s74f35a4f6jjd5xjjmvxbwqqnnx7q Agent-authored-by: AI agent acting on joshlf's behalf
Represent trailing layouts with their rounding alignment and phase so runtime normalization preserves complete nested sizes. Keep this implementation change separate from the later primitive, trailing and padding proof layers. The packed regression has size 10 where the former calculation produced 8. Preserve compiler-layout regressions, Kani harnesses and generated expectations with the runtime change; the next change adds the independent recursive arithmetic oracle. Validation: fresh pinned extraction and complete-model golden comparison; independent golden/live Lean builds, required-contract checks, and the transitive axiom audit. Makes progress on #3617 gherrit-pr-id: Gcrebpateb5cosfnz4zvqhnx2xldzt6vv Agent-authored-by: AI agent acting on joshlf's behalf
joshlf
force-pushed
the
Gcrebpateb5cosfnz4zvqhnx2xldzt6vv
branch
from
October 5, 2026 10:33
eaada22 to
ec1d457
Compare
joshlf
force-pushed
the
Gng7s74f35a4f6jjd5xjjmvxbwqqnnx7q
branch
from
October 5, 2026 10:33
6814934 to
5848e6d
Compare
joshlf
force-pushed
the
Gcrebpateb5cosfnz4zvqhnx2xldzt6vv
branch
from
October 5, 2026 11:34
ec1d457 to
b84a6e8
Compare
joshlf
force-pushed
the
Gng7s74f35a4f6jjd5xjjmvxbwqqnnx7q
branch
from
October 5, 2026 11:34
5848e6d to
36a472e
Compare
joshlf
force-pushed
the
Gcrebpateb5cosfnz4zvqhnx2xldzt6vv
branch
from
October 5, 2026 12:18
b84a6e8 to
30c60a1
Compare
joshlf
force-pushed
the
Gng7s74f35a4f6jjd5xjjmvxbwqqnnx7q
branch
from
October 5, 2026 12:18
36a472e to
1518357
Compare
joshlf
force-pushed
the
Gcrebpateb5cosfnz4zvqhnx2xldzt6vv
branch
2 times, most recently
from
October 5, 2026 13:03
180ebba to
5be32d8
Compare
joshlf
force-pushed
the
Gng7s74f35a4f6jjd5xjjmvxbwqqnnx7q
branch
from
October 5, 2026 13:03
1518357 to
5581ce0
Compare
Move the inline cast_from module to layout/cast_from.rs without changing its implementation. Use layout/mod.rs as the root of the resulting multi-file module, and update existing source-path references. Agent-authored-by: AI agent acting on joshlf's behalf gherrit-pr-id: Gvvdmej5q7tk5o76yu4c26esuzqpvpdca
Hoist the numerical CastPlan out of the generic pointer method. Keep CastParams<Src, Dst> as the private connection to the selected KnownLayout pair, and select its plan through an associated constant instead of the local Params trait. Project then reads metadata, applies the selected plan, and reconstructs the destination pointer. Preserve the existing offset/stride selection and unchecked arithmetic. The nested-padding correction and Aeneas proofs remain later changes. Agent-authored-by: AI agent acting on joshlf's behalf gherrit-pr-id: Gysrrwrr4oyfrqso6dw7gdmpjocmskwtx
Associate spec-only Rust doc fences with their syntax owners and derive original binders from verified signatures. Recursively decode fields into nominal mathematical carriers; inline type models may refine those fields with a fallible decoder. Plain clauses and dependent ghosts use decoded values, while explicit raw clauses retain extracted representations. Freeze native providers and thread every original type parameter's dictionary explicitly. Successful execution must produce a decodable result shared by all postconditions. Check ordinary canonical proofs and independent expectations against both complete models. The initial scope covers four arithmetic helpers; broad Raw lemmas retain their representation domains. Preserve nominal tuple structs using a reproducible patch exposing the existing upstream option. Audit source snapshots, exact annotation ownership and axioms; retain source maps and a stable Lean development project. Define generic shapes solely over mathematical carrier types. Generate structural decoder decomposition with retained child witnesses. Complete only omitted proposition proofs at decoder construction sites, bounded by the caller heartbeat budget, and preserve native module exports. Protect edited Lean projections and inspect compiled effective specs. Add native Lean edit regions and guarded copy-back into owned Rust doc fences. Preserve unrelated edits and bytes, reject stale source or generated scaffolding changes, and recover interrupted source/baseline replacements. Validate native editor/copy/regeneration round trips at the first and final stack stages and preserve byte-identical CI assembly throughout the stack. Compare every inline contract with its independent expectation for arbitrary execution outcomes, then specialize to the canonical implementation proof. Record the complete design and deferred decisions in DESIGN.md. Derive fixed registration names from their owner and share nominal case assembly. Normalize source ownership once, retain generated lines with their locations, and reuse checked editing regions. Share file rosters while keeping independent source ownership and contract adequacy checks separate. Explain the pipeline and the purpose of its guards for readers new to the integration. Derive extraction roots solely from present annotations. Every discovered specification is mandatory in both builds; removing a specification and its proof deliberately removes that claim. No method roster or root marker is required. Preserve Unit decoding through reduction so total assertion harnesses use the same contract path as ordinary value-returning functions. Validation: fresh pinned extraction, complete golden comparison, separate golden/live builds, independent required contracts and axiom audits. gherrit-pr-id: Gf75ukj4vvtufg6dwjpfa3bx5a457sw74 Agent-authored-by: AI agent acting on joshlf's behalf
joshlf
force-pushed
the
Gcrebpateb5cosfnz4zvqhnx2xldzt6vv
branch
from
October 5, 2026 15:25
5be32d8 to
a71947f
Compare
This was referenced Oct 5, 2026
joshlf
force-pushed
the
Gng7s74f35a4f6jjd5xjjmvxbwqqnnx7q
branch
from
October 5, 2026 21:12
371fbd1 to
0da47ce
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
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.
Represent trailing layouts with their rounding alignment and phase so runtime
normalization preserves complete nested sizes. Keep this implementation change
separate from the later primitive, trailing and padding proof layers. The
packed regression has size 10 where the former calculation produced 8. Preserve
compiler-layout regressions, Kani harnesses and generated expectations with the
runtime change; the next change adds the independent recursive arithmetic
oracle.
Validation: fresh pinned extraction and complete-model golden comparison;
independent golden/live Lean builds, required-contract checks, and the
transitive axiom audit.
Makes progress on #3617
Agent-authored-by: AI agent acting on joshlf'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/Gcrebpateb5cosfnz4zvqhnx2xldzt6vv && git checkout -b pr-Gcrebpateb5cosfnz4zvqhnx2xldzt6vv FETCH_HEADCheckout
git fetch origin refs/heads/Gcrebpateb5cosfnz4zvqhnx2xldzt6vv && git checkout FETCH_HEADCherry Pick
git fetch origin refs/heads/Gcrebpateb5cosfnz4zvqhnx2xldzt6vv && git cherry-pick FETCH_HEADPull
Stacked PRs enabled by GHerrit.