Skip to content

Prove cast validation and exact metadata inference - #3755

Open
joshlf wants to merge 1 commit into
Gwpbseabi7fewonulzi3yhrofnc6eb5ivfrom
Gurqevo3e4xhhk2x275sikrq6qmdyzyqb
Open

joshlf wants to merge 1 commit into
Gwpbseabi7fewonulzi3yhrofnc6eb5ivfrom
Gurqevo3e4xhhk2x275sikrq6qmdyzyqb

Conversation

@joshlf

@joshlf joshlf commented Oct 2, 2026 •

Copy link
Copy Markdown
Member

Establish independent error priority, greatest-fitting metadata and exact
prefix/suffix outcomes. Keep outcome examples distinct from contract expansion,
including unattainable sizes and intentional zero-stride panic.

Compare exact-size metadata and complete cast results with independent Rust
calculations, including error precedence, greatest fitting counts, and both
prefix/suffix splits. State address overflow and zero-stride exclusions in Rust.

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: v25 — Compare vs v24

📚 Full Patch History

Links show the diff between the row version and the column version.

Version v24 v23 v22 v21 v20 v19 v18 v17 v16 v15 v14 v13 v12 v11 v10 v9 v8 v7 v6 v5 v4 v3 v2 v1 Base
v25 v24 v23 v22 v21 v20 v19 v18 v17 v16 v15 v14 v13 v12 v11 v10 v9 v8 v7 v6 v5 v4 v3 v2 v1 Base
v24 v23 v22 v21 v20 v19 v18 v17 v16 v15 v14 v13 v12 v11 v10 v9 v8 v7 v6 v5 v4 v3 v2 v1 Base
v23 v22 v21 v20 v19 v18 v17 v16 v15 v14 v13 v12 v11 v10 v9 v8 v7 v6 v5 v4 v3 v2 v1 Base
v22 v21 v20 v19 v18 v17 v16 v15 v14 v13 v12 v11 v10 v9 v8 v7 v6 v5 v4 v3 v2 v1 Base
v21 v20 v19 v18 v17 v16 v15 v14 v13 v12 v11 v10 v9 v8 v7 v6 v5 v4 v3 v2 v1 Base
v20 v19 v18 v17 v16 v15 v14 v13 v12 v11 v10 v9 v8 v7 v6 v5 v4 v3 v2 v1 Base
v19 v18 v17 v16 v15 v14 v13 v12 v11 v10 v9 v8 v7 v6 v5 v4 v3 v2 v1 Base
v18 v17 v16 v15 v14 v13 v12 v11 v10 v9 v8 v7 v6 v5 v4 v3 v2 v1 Base
v17 v16 v15 v14 v13 v12 v11 v10 v9 v8 v7 v6 v5 v4 v3 v2 v1 Base
v16 v15 v14 v13 v12 v11 v10 v9 v8 v7 v6 v5 v4 v3 v2 v1 Base
v15 v14 v13 v12 v11 v10 v9 v8 v7 v6 v5 v4 v3 v2 v1 Base
v14 v13 v12 v11 v10 v9 v8 v7 v6 v5 v4 v3 v2 v1 Base
v13 v12 v11 v10 v9 v8 v7 v6 v5 v4 v3 v2 v1 Base
v12 v11 v10 v9 v8 v7 v6 v5 v4 v3 v2 v1 Base
v11 v10 v9 v8 v7 v6 v5 v4 v3 v2 v1 Base
v10 v9 v8 v7 v6 v5 v4 v3 v2 v1 Base
v9 v8 v7 v6 v5 v4 v3 v2 v1 Base
v8 v7 v6 v5 v4 v3 v2 v1 Base
v7 v6 v5 v4 v3 v2 v1 Base
v6 v5 v4 v3 v2 v1 Base
v5 v4 v3 v2 v1 Base
v4 v3 v2 v1 Base
v3 v2 v1 Base
v2 v1 Base
v1 Base
⬇️ Download this PR

Branch

git fetch origin refs/heads/Gurqevo3e4xhhk2x275sikrq6qmdyzyqb && git checkout -b pr-Gurqevo3e4xhhk2x275sikrq6qmdyzyqb FETCH_HEAD

Checkout

git fetch origin refs/heads/Gurqevo3e4xhhk2x275sikrq6qmdyzyqb && git checkout FETCH_HEAD

Cherry Pick

git fetch origin refs/heads/Gurqevo3e4xhhk2x275sikrq6qmdyzyqb && git cherry-pick FETCH_HEAD

Pull

git pull origin refs/heads/Gurqevo3e4xhhk2x275sikrq6qmdyzyqb

Stacked PRs enabled by GHerrit.

@chatgpt-codex-connector

chatgpt-codex-connector Bot commented Oct 2, 2026 •

Copy link
Copy Markdown

Codex Review Summary

This comment shows the latest Codex review activity on this pull request.

Review Status Commit Review trigger
📝 Code Review ✅ Completed 2026-10-02T15:29:22.226121Z c1dbd14 PR opened
🔒 Security Review ✅ Completed 2026-10-02T15:30:33.557900Z c1dbd14 PR opened
ℹ️ About Codex in GitHub

Your team has set up Codex to review pull requests in this repo. Reviews are triggered when you

  • Open a pull request for review
  • Mark a draft as ready
  • Comment "@codex review" or "@codex security review".

Codex reacts with 👀 while any review is running, comments if it has suggestions, and reacts with 👍 once all reviews finish with no findings.

@codecov-commenter

codecov-commenter commented Oct 2, 2026 •

Copy link
Copy Markdown

Codecov Report

❌ Patch coverage is 0% with 85 lines in your changes missing coverage. Please review.
✅ Project coverage is 52.06%. Comparing base (1ae7fb4) to head (74f3f4d).

Files with missing lines Patch % Lines
zerocopy/src/layout/tail_checks.rs 0.00% 85 Missing ⚠️
Additional details and impacted files
@@                          Coverage Diff                          @@
##           Gwpbseabi7fewonulzi3yhrofnc6eb5iv    #3755      +/-   ##
=====================================================================
- Coverage                              52.99%   52.06%   -0.94%     
=====================================================================
  Files                                     27       27              
  Lines                                   4308     4393      +85     
=====================================================================
+ Hits                                    2283     2287       +4     
- Misses                                  2025     2106      +81     

☔ View full report in Codecov by Harness.
📢 Have feedback on the report? Share it here.

🚀 New features to boost your workflow:
  • ❄️ Test Analytics: Detect flaky tests, report on failures, and find test suite problems.

@joshlf
joshlf force-pushed the G5ef3gjdnvnuoek33bzy6bovxsxprq4wm branch from f014f78 to c0e1417 Compare October 2, 2026 15:39
@joshlf
joshlf force-pushed the Gurqevo3e4xhhk2x275sikrq6qmdyzyqb branch 2 times, most recently from 5dcba4c to d864120 Compare October 2, 2026 19:39
@joshlf
joshlf force-pushed the G5ef3gjdnvnuoek33bzy6bovxsxprq4wm branch 2 times, most recently from 7d2e3fc to f6fe0a2 Compare October 2, 2026 21:06
@joshlf
joshlf force-pushed the Gurqevo3e4xhhk2x275sikrq6qmdyzyqb branch 2 times, most recently from 08ba060 to d96b201 Compare October 3, 2026 16:09
@joshlf
joshlf force-pushed the G5ef3gjdnvnuoek33bzy6bovxsxprq4wm branch from 15d6133 to 51bd649 Compare October 4, 2026 02:57
@joshlf
joshlf force-pushed the Gurqevo3e4xhhk2x275sikrq6qmdyzyqb branch 2 times, most recently from 072407b to 2b94912 Compare October 4, 2026 12:42
@joshlf
joshlf force-pushed the G5ef3gjdnvnuoek33bzy6bovxsxprq4wm branch from 7e58c20 to 7ce24d0 Compare October 5, 2026 13:03
@joshlf
joshlf force-pushed the Gurqevo3e4xhhk2x275sikrq6qmdyzyqb branch 2 times, most recently from 39cee76 to 7be5eac Compare October 5, 2026 15:25
@joshlf
joshlf force-pushed the G5ef3gjdnvnuoek33bzy6bovxsxprq4wm branch from 7ce24d0 to 4f6c164 Compare October 5, 2026 15:25
@joshlf
joshlf force-pushed the G5ef3gjdnvnuoek33bzy6bovxsxprq4wm branch from 4f6c164 to 8c39f39 Compare October 5, 2026 21:12
@joshlf
joshlf force-pushed the Gurqevo3e4xhhk2x275sikrq6qmdyzyqb branch from 7be5eac to 846d308 Compare October 5, 2026 21:12
@joshlf
joshlf force-pushed the G5ef3gjdnvnuoek33bzy6bovxsxprq4wm branch from 8c39f39 to cb90a9e Compare October 5, 2026 21:44
@joshlf
joshlf force-pushed the Gurqevo3e4xhhk2x275sikrq6qmdyzyqb branch from 846d308 to 5a71a9d Compare October 5, 2026 21:44
@joshlf
joshlf force-pushed the G5ef3gjdnvnuoek33bzy6bovxsxprq4wm branch from cb90a9e to 60bf34c Compare October 5, 2026 22:08
@joshlf
joshlf force-pushed the Gurqevo3e4xhhk2x275sikrq6qmdyzyqb branch 2 times, most recently from 080cb21 to f17e6fd Compare October 6, 2026 00:32
@joshlf
joshlf changed the base branch from G5ef3gjdnvnuoek33bzy6bovxsxprq4wm to Gwpbseabi7fewonulzi3yhrofnc6eb5iv October 6, 2026 00:32
@joshlf
joshlf force-pushed the Gurqevo3e4xhhk2x275sikrq6qmdyzyqb branch from f17e6fd to 0c664e5 Compare October 6, 2026 15:45
@joshlf
joshlf force-pushed the Gwpbseabi7fewonulzi3yhrofnc6eb5iv branch from 39f7ffc to 1d67cd7 Compare October 6, 2026 15:45
Establish independent error priority, greatest-fitting metadata and exact
prefix/suffix outcomes. Keep outcome examples distinct from contract expansion,
including unattainable sizes and intentional zero-stride panic.

Compare exact-size metadata and complete cast results with independent Rust
calculations, including error precedence, greatest fitting counts, and both
prefix/suffix splits. State address overflow and zero-stride exclusions 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: Gurqevo3e4xhhk2x275sikrq6qmdyzyqb
Agent-authored-by: AI agent acting on joshlf's behalf

This branch has not been deployed

No deployments
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

None yet

Projects

None yet

Development

Successfully merging this pull request may close these issues.

2 participants