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. |
![chatgpt-codex-connector[bot]](https://avatars.githubusercontent.com/in/1144995?s=60&v=4){kind=small}
There was a problem hiding this comment.
💡 Codex Review
Here are some automated review suggestions for this pull request.
Reviewed commit: a5dbd07757
ℹ️ 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".
If Codex has suggestions, it will comment; otherwise it will react with 👍.
Codex can also answer questions or update the PR. Try commenting "@codex address that feedback".
| "superseded_direct_registry_entries": { | ||
| "archived_from": "audit/assumptions.yaml", | ||
| "source_commit": "0e38bf80ed60dbf3f0927312ebb598bb6f731895", | ||
| "note": "Historical summaries removed from the active registry. Original snapshot entries above are preserved unchanged.", | ||
| "assumptions": [ |
There was a problem hiding this comment.
Moving these IDs out of audit/assumptions.yaml leaves still-built Lean modules pointing auditors to the wrong registry: for example, Eip8282/Audit/UniversalBoundary.lean:96-100 says that A-ABSTRACT-TX and its components are recorded in that file, while numerous Trust.lean comments likewise identify it as the current named open gap. Anyone auditing those historical parents now sees an unregistered obligation unless they independently discover this new JSON subsection. Keep the IDs in the active registry or update the surviving references to the archived location.
AGENTS.md reference: AGENTS.md:L3-L5
Useful? React with 👍 / 👎.
Th0rgal
changed the title
There was a problem hiding this comment.
💡 Codex Review
Here are some automated review suggestions for this pull request.
Reviewed commit: 8ef5bc2307
ℹ️ 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".
If Codex has suggestions, it will comment; otherwise it will react with 👍.
Codex can also answer questions or update the PR. Try commenting "@codex address that feedback".
| files={'.'.join(p.relative_to(ROOT).with_suffix('').parts):p for p in (ROOT/'Eip8282').rglob('*.lean')} | ||
| edges={n:set(re.findall(r'^import\s+(\S+)',p.read_text(),re.M)) for n,p in files.items()} |
There was a problem hiding this comment.
Build files and edges from the three root facades as well as Eip8282/**/*.lean. As written, imports in Eip8282.lean, Eip8282Candidates.lean, and Eip8282Tests.lean are never inspected, so a future cross-tier import—or another root-level Lean module—can leave python3 scripts/library_layout.py green while the advertised core/candidate/test partition is violated. This makes the required library-partition check fail open.
AGENTS.md reference: AGENTS.md:L12-L14
Useful? React with 👍 / 👎.
Th0rgal
changed the title
There was a problem hiding this comment.
💡 Codex Review
Here are some automated review suggestions for this pull request.
Reviewed commit: 2aa144f250
ℹ️ 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".
If Codex has suggestions, it will comment; otherwise it will react with 👍.
Codex can also answer questions or update the PR. Try commenting "@codex address that feedback".
| - Seven source/provenance archives under `audit/receipts` supply pinned external | ||
| source bodies, genesis data provenance and the factory-regression input. |
There was a problem hiding this comment.
The retained audit/receipts/direct-genesis-funding-input-20260910.json names audit/receipts/genesis-funding-input-mainnet.json as its source_asset, and its embedded reproduction script immediately reads that path, but this cleanup deletes the asset; a repo-wide search finds no replacement. Consequently, a fresh checkout cannot reproduce or independently verify the genesis extraction despite this section claiming that the retained archives supply genesis provenance. Restore the source asset or update the reproduction chain to materialize it from a pinned location.
AGENTS.md reference: AGENTS.md:L22-L24
Useful? React with 👍 / 👎.
1 participant
The registered guarantees previously pulled in the superseded model/CFG/Ξ proof campaign, and the delivery tree contained hundreds of obsolete campaign artifacts. This extracts the execution support the current proofs actually use and removes the unused campaigns and artifacts.
Result
make check.Tests.MutationReceiptsretains the required fixtures and exactly five original native receipts; the six registered refutations keep their statements.ResourceAssumptions.leanis byte-identical to the merged resource proof. All five retained native receipt commands are copied exactly from the original source..pr27-receipts, campaign setup/logs, frozen release metadata, unused protocol slot/withdrawal extraction, and other unreachable modules. Earlier small-module consolidation is recorded in the migration map.audit/CLEANUP.mdgives the deletion inventory and retention reasons.audit/delivery-roots.jsonnames the current evidence roots. Checks reject orphan modules, superseded core imports, unreferenced receipts and unexpected correctness/refutation/resource axioms.Validation
Full
make checkpassed in GitHub CI for head2aa144f250f0f37eee357e3ab43e00eb4a19d42e: successful prove job. This covers the complete library partition, registered guarantees, all retained tests, resource proof and axiom guards.Also passed: deployment/pin verification, exact generator reproduction, the direct-call, nested-rollback and factory Anvil suites, and negative checks for the import-partition guard.
The three correctness parents, funded LOG0 witness and eight resource theorems retain only standard Lean axioms. The five drain/control receipts retain A-NATIVE-DECIDE. Canonical Ethereum applicability remains an explicit boundary. Bytecode, interpreter and normative pins are unchanged.