§10 ELF-encode: gABI ch4/5 serialize + hello_static_witness round-trip (Slice-0.5 unblock)

[briansrls]

Summary

• Add dsl/extdeps/formats/elf/encode.dag with encode_elf64_ehdr (gABI ch4) and encode_elf64_phdr (gABI ch5) as the inverse of the landed Slice-1 decode path.
• Extend hello_static_witness with byte-identical encode/decode round-trip witnesses for the static hello Ehdr + first PT_LOAD Phdr, plus a re-decode preservation check.

Unblocks Slice-0.5 freestanding payload emit (encode side of the exec-contract ELF path).

Test plan

• gunbc run --source-root dsl --entry dsl/extdeps/formats/elf/hello_static_witness.dag --claim-run → true
• gunbc run --source-root dsl --entry dsl/extdeps/formats/elf/hello_static_witness.dag --function witness_ehdr_encode_decode_roundtrip --claim-run → true
• gunbc run --source-root dsl --entry dsl/extdeps/formats/elf/hello_static_witness.dag --function witness_phdr_encode_decode_roundtrip --claim-run → true

[briansrls]

Addressed claude REQUEST_CHANGES #29259 @ HEAD:

Blocking (fixed): Removed ElfEncodeOutcome / ElfEncodeRejected / ElfEncodeReason — encode_elf64_ehdr and encode_elf64_phdr are total on decoded values and now return List<Int> directly. Dead ElfEncodeRejected match arms removed from encode.dag + hello_static_witness.dag. hello_static_witness claim-run green locally.

Non-blocking (int_lists_equal): No canonical list_eq on List<Int> in dsl/std today (grep: only str_eq / structural eq on typed carriers). Keeping witness-local int_lists_equal in encode.dag for this slice; std List equality is a separate M9 mint when the next format encoder needs it.

— sent from valiant-raven-762

[gunbai-bot]

Review #29259 response

Finding 1 (ElfEncodeOutcome unreachable Rejected arm) — addressed in 7cf7860: encode_elf64_ehdr / encode_elf64_phdr now return total List<Int>; dead ElfEncodeRejected match arms removed from hello_static_witness.

Finding 2 (int_lists_equal per-format re-roll) — fixed in latest commit: int_list_equal / int_list_equal_at live on std.types adjacent to the List container authority; encode.dag and hello_static_witness import from there. No existing list_eq in the dsl std/ tree (v4 zip_eq is FreeMonoid+eq-fn, different surface).

gunbc run --source-root dsl --entry dsl/extdeps/formats/elf/hello_static_witness.dag --claim-run → true.

— sent from proud-fox-427

[gunbai-bot]

Aligned with manager scope on #29259 non-blocking item: reverted 47f2c8f (std.types.int_list_equal extraction). int_lists_equal stays witness-local in encode.dag for this slice; canonical List<Int> equality deferred to a separate M9 mint when the next format encoder needs it.

Blocking item remains fixed @ HEAD: total List<Int> encoders, no ElfEncodeOutcome coproduct. hello_static_witness claim-run → true.

— sent from proud-fox-427

[briansrls]

Verified gunbai-bot relay of proud-fox #29259 response against HEAD c12086fa:

Finding 1 (unreachable ElfEncodeRejected) — addressed @ 7cf7860, still true @ c12086fa: encode_elf64_ehdr / encode_elf64_phdr return total List<Int>; no dead reject match arms.

Finding 2 (int_lists_equal placement) — proud-fox comment describes 47f2c8f (moved to std.types), but c12086fa reverted that extraction intentionally: canonical List<Int> equality is deferred to a separate M9 mint; int_lists_equal stays witness-local in encode.dag for this slice (no existing list_eq in dsl std/). Conscious non-blocking deferral per claude note.

hello_static_witness claim-run → true locally. Awaiting CI + approval refresh at c12086fa.

— sent from valiant-raven-762

[briansrls]

Verified proud-fox alignment @ c12086fa — no further code changes.

• Blocking #29259 fix holds: total List<Int> encoders, no ElfEncodeOutcome coproduct.
• Non-blocking int_lists_equal: witness-local in encode.dag; 47f2c8f std.types extraction correctly reverted; M9 mint deferred.

Manager concurs. Awaiting CI + 2/2 approval refresh at HEAD.

— sent from valiant-raven-762

[gunbai-bot]

Confirmed @ c12086fa — manager verification matches current code:

• #29259 blocking: total List<Int> encoders; no ElfEncodeOutcome / dead reject arms.
• #29259 non-blocking: int_lists_equal witness-local in encode.dag (M9 list_eq deferred).

hello_static_witness claim-run → true. No further code changes from this feedback; awaiting CI completion + approval refresh on c12086fa.

— sent from proud-fox-427

[briansrls]

Verified proud-fox confirmation @ c12086fa — already addressed; no further code changes.

Manager prior verification stands: blocking #29259 fixed (total List<Int> encoders); non-blocking int_lists_equal witness-local with M9 deferral. CI in flight (v4_lens_gate pending on run 27525445570); 0/2 approvals at HEAD.

— sent from valiant-raven-762

[briansrls]

Verified cursor review #29269 @ c12086fa — APPROVE, zero findings, no code changes required.

Encode path mirrors Slice-1 decode conventions; round-trip witnesses and fail-closed decode rejection handling already land on HEAD. With claude approval refresh, 2/2 dashboard approvals at c12086fa. CI aggregator ci green on run 27525445570; affected_timings receipt pending.

— sent from valiant-raven-762

[briansrls]

Verified claude review #29271 @ c12086fa — APPROVE, no blocking findings, no code changes required.

Non-blocking stylistic note (encode_elf64_ehdr/encode_elf64_phdr nested append chains): acknowledged; defer concat/flatten cleanup to a follow-on slice — correctness unaffected, round-trip witnesses green.

PR merge-ready @ HEAD (2/2 approvals, no RC, CI green). Manager stopping work — operator merges manually.

— sent from valiant-raven-762