[Lutar, Stephen P. (stephenlutar2-hash)]

Immutable kernel build inputs

Exact base: 2a0d363fb4dcd5b224e2273f06ac9106de6320c1
Exact head: 535e03589ade5e9ddfb5fde9dd92f09b8f03b0c2

Change

• Pin ubuntu:26.04 to OCI index digest sha256:2260313b31c8c011cd2eebe728008efac1b3982be73eb71348ea2648d2c0e09b.
• Pin szl-holdings/lutar-lean to protected-main commit 034ef1cab37c77efec57775e97e99f196def37c8, fetch that exact object, detach checkout, and fail unless HEAD matches.
• Assert the expected and actual source commit inside the built image.
• Add a dependency-free seven-case regression against mutable image/source inputs and false pin claims.

Exact scope

• Dockerfile
• .github/workflows/kernel-build-verify.yml
• tests/test_dockerfile_source_pins.py

Evidence

• Pin contract: 7/7 passed.
• Full pytest: 31 passed.
• Registry self-test: 4 verified, 0 unbacked.
• Exact SHA fetch/checkout rehearsal matched 034ef1c....
• git diff --check: pass; narrow credential scan: zero matches.
• Commit has a valid ED25519 signature and matching DCO trailer.

Truth boundary

Docker Desktop was not running locally, so no local full image-build result is claimed. The hosted exact-head kernel build must establish image/toolchain/Mathlib compatibility before promotion. No deployment, release, HF, settings, or runtime mutation is part of this PR.

[Lutar, Stephen P. (stephenlutar2-hash)]

Codex (@codex) review

Review exact signed+DCO head 535e03589ade5e9ddfb5fde9dd92f09b8f03b0c2 only. Focus on OCI digest/source-commit immutability, safe exact-SHA fetch semantics, in-image HEAD attestation, adversarial regression completeness, and whether any changed truth claim can false-green. Treat local tests as source evidence only; the hosted build-verify must establish the image/toolchain result.

[chatgpt-codex-connector]

💡 Codex Review

Here are some automated review suggestions for this pull request.

Reviewed commit: 535e03589a

ℹ️ 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 (@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 (@codex) address that feedback".

[Lutar, Stephen P. (stephenlutar2-hash)]

Codex (@codex) Please address all four current review findings without weakening immutable-input guarantees: remove or use the CodeQL-unused base_digest; explicitly check out and verify github.event.pull_request.head.sha before the image build so proof binds the signed PR head rather than the synthetic merge ref; independently fetch protected lutar-lean/main and prove LUTAR_COMMIT is its ancestor before calling it protected-main provenance; and tighten the regression to reject shell bypasses such as || true, semicolon fallthrough, subshell masking, or non-executing assertions in both workflow and Dockerfile checks. Add adversarial fixtures, publish a signed+DCO successor without force push, resolve threads after proof, rerun every hosted gate, and request fresh exact-head review.

[chatgpt-codex-connector]

To use Codex here, create an environment for this repo.

[chatgpt-codex-connector]

💡 Codex Review

Here are some automated review suggestions for this pull request.

Reviewed commit: 535e03589a

ℹ️ 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 (@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 (@codex) address that feedback".

[Lutar, Stephen P. (stephenlutar2-hash)]

Codex (@codex) review exact head 535e03589ade5e9ddfb5fde9dd92f09b8f03b0c2. Please review only this immutable head against protected base 2a0d363fb4dcd5b224e2273f06ac9106de6320c1; do not inherit prior source claims. No merge is authorized by this request.

[chatgpt-codex-connector]

💡 Codex Review

Here are some automated review suggestions for this pull request.

Reviewed commit: 535e03589a

ℹ️ 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 (@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 (@codex) address that feedback".

[Lutar, Stephen P. (stephenlutar2-hash)]

Codex (@codex) review

Please review exact head 0b27e8c, focusing on the four requested repairs: exact PR-head checkout, fail-closed diffing, independent lutar-lean/main ancestry proof, and adversarial rejection of masked source-identity guards.

[chatgpt-codex-connector]

Codex Review: Didn't find any major issues. Breezy!

Reviewed commit: 0b27e8c469

ℹ️ 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 (@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 (@codex) address that feedback".