Skip to content

t27os: real launch proof finalize (evidence + repro, Closes #13578) - #13579

Merged
gHashTag merged 1 commit into
masterfrom
lane/launch-proof-finalize
Nov 10, 2026
Merged

t27os: real launch proof finalize (evidence + repro, Closes #13578)#13579
gHashTag merged 1 commit into
masterfrom
lane/launch-proof-finalize

Conversation

@gHashTag

@gHashTag gHashTag commented Nov 10, 2026 •
edited by cursor Bot
Loading

Copy link
Copy Markdown
Collaborator

Closes #13578

What

Preserve and reproduce the already-proven real launch (launch_proof.t27, ORDER T27_REAL_LAUNCH_PROOF_FINALIZE_V1):

  • specs/t27os/launch_proof.t27: the proven spec (admission allowlist -> posix_spawn -> waitpid -> observed output -> exit).
  • docs/t27os/launch_proof_evidence.md: exact build/link/run commands, raw transcript, pid evidence (2671 fresh; 6465 original), denial transcripts (exit 7), evidence table, and the NOT-claims section.

Repro (verified 2026-11-10)

t27b build specs/t27os/launch_proof.t27 -o target/t27os/launch_proof.o --macho
ld -arch arm64 -platform_version macos 11.0 26.5 -syslibroot <MacOSX.sdk> -e _main -lSystem -o target/t27os/launch_proof target/t27os/launch_proof.o
T27OS_TARGET=/bin/echo   ./target/t27os/launch_proof   # exit 0, SPAWNED pid=..., T27-REAL-LAUNCH-PROOF
T27OS_TARGET=/usr/bin/wc ./target/t27os/launch_proof   # DENIED, exit 7
T27OS_TARGET=/bin/sh     ./target/t27os/launch_proof   # DENIED, exit 7

Out of scope (per order)

No pty_sys.t27 changes, no adapters, no production integration, no merge without CI/review. The 8 adapter_spawn_direct.t27 tests remain behavior-model only.

LAUNCH_PROOF_STATUS: EXECUTED (reproduced)

Note

Low Risk
Additive spec and documentation only; no changes to production spawn or PTY integration paths.

Overview
Adds a bounded real-launch demonstration for t27os: a new specs/t27os/launch_proof.t27 that reads T27OS_TARGET, allows only /bin/echo, otherwise prints DENIED and exits 7 before posix_spawn, and on success spawns via libSystem, logs SPAWNED pid=… on stderr, and waitpids the child.

Also adds docs/t27os/launch_proof_evidence.md with exact t27b/ld/run steps, 2026-11-10 transcripts (allowed stdout token, denied paths), an evidence checklist, and documented exit codes. The docs explicitly scope this as proof only—no pty_sys.t27, adapters, or production spawn path changes.

Reviewed by Cursor Bugbot for commit aeebb8d. Bugbot is set up for automated code reviews on this repo. Configure here.

@cursor

cursor Bot commented Nov 10, 2026

Copy link
Copy Markdown
Contributor

This PR is too large for Bugbot to review. It changes 17,632 lines and 3,995,267 characters. Split the change into smaller pull requests to get a review.

@gHashTag
gHashTag force-pushed the lane/launch-proof-finalize branch from 12797ca to aeebb8d Compare November 10, 2026 14:53
@cursor

cursor Bot commented Nov 10, 2026

Copy link
Copy Markdown
Contributor

Bugbot couldn't run - usage limit reached

Bugbot is counted against Cursor usage for this user or team, and this run hit a usage or spend limit.

A user or team admin can review and increase usage limits in the Cursor dashboard.

(requestId: 7b77c860-88c3-4d8d-817c-9ef7664cfb8f)

@github-actions

github-actions Bot commented Nov 10, 2026

Copy link
Copy Markdown
Contributor

PR Dashboard

Generated at: 2026-11-10 14:53:43 UTC

Summary

Status Count
Total Open PRs 32
PRs with Failing Checks 30
PRs with All Checks Green 2
READY 0
FAILING 30
PENDING 0
NO CHECKS YET 0

These columns do not partition: 0 + 30 + 0 + 0 = 30, and there are 32 open PRs. A PR is being counted twice or not at all.

Seal Status

  • ⚠️ STALE -- sha256(compiler.rs)=b882be1e4933 != manifest seal=87e5cbd3ad94.
    The committed NMSE numbers were certified against an older compiler.rs.
    Run scripts/reseal-check.sh locally for the two-step reseal command (advisory; not a merge gate).

@gHashTag

gHashTag commented Nov 10, 2026

Copy link
Copy Markdown
Collaborator Author

CI triage (2026-11-10): both failing checks are pre-existing repo-wide reds, not caused by this PR's 2 added files.

  • build (Coq kernel, coq-kernel.yml): fails on every recent branch (opam git fetch of the archive repo exits 128 -> exit 40). Infra, no relation to .t27/docs changes.
  • duplicate-bodies: fails on master itself (run 2026-11-10T14:43Z). The flagged bodies (entity_count, find, verify_trinity_identity, put_bytes, put_dec) include names not present in this PR; the ratchet is red at base.

All PR-relevant gates pass: check-linked-issue, budget, build-and-test, claw-*, gate-topology, L1. PR is MERGEABLE with exactly 2 files (specs/t27os/launch_proof.t27, docs/t27os/launch_proof_evidence.md). Not merging; merge remains gated on owner confirmation per order T27_LAUNCH_PROOF_PR_WATCH_V1.

@github-actions github-actions Bot mentioned this pull request Nov 10, 2026
Open
@gHashTag
gHashTag merged commit 32b4e94 into master Nov 10, 2026
47 of 57 checks passed
@gHashTag
gHashTag deleted the lane/launch-proof-finalize branch November 10, 2026 15:03
@gHashTag gHashTag mentioned this pull request Nov 10, 2026
Open
@gHashTag

gHashTag commented Nov 10, 2026

Copy link
Copy Markdown
Collaborator Author

Superseded by #13581 (lane/launch-proof-finalize-v2 → master). Branch lane/launch-proof-finalize remains unchanged; no force-push performed. Both commits b44f57e and 7c27b69 are preserved in #13581.

This was referenced Nov 11, 2026
Closed
Closed
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Reviewers

No reviews

Assignees

No one assigned

Labels

None yet

Projects

None yet

Milestone

No milestone

Development

Successfully merging this pull request may close these issues.

Real launch proof finalize: preserve and reproduce the launch_proof.t27 EXECUTED result

1 participant

@gHashTag