Lane A: finish the live Rust-observation exact-head contract using the existing shell.Env.Get

ROADMAP.md

@@ -16,6 +16,9 @@ The graph has eleven lanes: SCM compatibility · namespace · P-derive · observ
   - [ ] **Have the new compiler write out Rust source itself** — Read the source, work out the types, translate, and write real Rust to disk without the old generator deciding any of it. The old runner may still be what executes this; it just stops making the decisions. Why: Until the new compiler can write Rust on its own, every improvement has to go through the generator we are trying to delete. [authority](src/v2/compiler/self_host/candidate_generation.dag)
     - [ ] **Regenerate one already-tested module with the new generator** — Take a module that already has working tests, change only which generator produces it, and confirm it still passes the same tests including the deliberately broken one. Why: Proves the whole approach works on something real before anyone builds more on the assumption that it does. [authority](src/v2/compiler/self_host/frontier.dag)
       - [ ] **Build the new generator with itself, then do it again** — The generator, and only the generator: it writes and builds a native version of itself, that native version writes and builds another, and the second one needs nothing from the old compiler. The other parts of the compiler are still produced the old way at this point. Why: This is the moment the new generator stops being something we produce and becomes something that produces itself. [authority](src/v2/compiler/self_host/frontier.dag) — requires all: v2-emitter-first-behavioral-module, pderive-error-movement-receipt
+- [ ] **See the hand-written files as they actually are, from the host** — The set of tracked Rust files is read from the repository itself at a known revision, not transcribed. Reading it can fail, and when it does it says so rather than returning a shorter list. Why: Every count of what is left to move was previously taken from whichever files someone had looked at. That understates, silently, and it understated twice here -- so no schedule built on it could be trusted. [authority](dag/gunbc/stage0_rust_host_observation.dag)
+  - [ ] **Keep an honest list of what still depends on the old compiler** — Every module is either generated by the new compiler or explicitly kept on the old one with a reason and a plan to move. Two separate questions, kept separate: whether the list found every module, and whether every module it found has been decided. A complete list of undecided modules and a decided list that missed modules are different failures and are reported differently. Why: Turns a vague sense of 'mostly done' into a finite, countable list someone can work through. [authority](dag/gunbc/v1_deletion_plan.dag)
+    - [ ] **Work through the remaining hand-written files the products need** — Move the hand-written files the shipping tools still depend on. Anything that genuinely has to stay gets an explicit reason. Why: The main command-line tool is itself one of these files, so 'the products still build' is not something we can honestly claim until this is done. [authority](dag/gunbc/v1_deletion_plan.dag)
 - [ ] **Write the closing check for: Work out what each name can see, and let that be what a file depends on** — One executable check states when this is done, transcribed from the node's own bar: A neighbour in the same file is in view; something inside a different branch of a decision is not; something written further down is not; the same name written twice in genuinely different places stays ambiguous; repeated mentions of one thing collapse to a single dependency; and nothing depends on an unrelated file happening to be loaded at the same time. Why: Turns a prose bar into a runnable verdict, so the node it gates can be dispatched and its completion checked rather than judged. [authority](docs/plans/namespace-unique-on-chain-operational-plan.md)
   - [ ] **Work out what each name can see, and let that be what a file depends on** — From where a name is written, work outward to every declaration actually in view — including ordinary neighbours in the same file — respecting where things were written relative to each other. Then record, for each name, exactly which declaration answered it, and derive what each file depends on from those answers. Why: What a file depends on is currently written out by hand as a separate statement, so it can disagree with what the file actually refers to. Hundreds of files were patched by hand to keep those two in step, which is work that should never have existed: what a file depends on is a consequence of what it refers to, not a second thing to maintain. [authority](docs/plans/namespace-unique-on-chain-operational-plan.md)
     - [ ] **Settle the names that genuinely could mean two things** — Using the real answers from the step before — not a count taken by searching text — go through every name that genuinely has more than one candidate and either refuse it on purpose or say which one is meant, by renaming or by writing it out in full. Why: Counting these by searching for text gives a number that is wrong in both directions, so it cannot tell anyone how much work is left or whether it is finished. [authority](docs/plans/namespace-unique-on-chain-operational-plan.md)
@@ -35,10 +38,6 @@ The graph has eleven lanes: SCM compatibility · namespace · P-derive · observ
                     - [ ] **Delete the old runner** — Delete it and everything now unreachable, in one change, once the rehearsal above holds. This is about the runner only — not the rest of the old code, and not hand-written Rust generally. Why: Removes the second, slower way of running everything, and with it the possibility of the two disagreeing. [authority](dag/gunbc/v1_deletion_plan.dag) — requires all: v1-interpreter-quarantine, v1-emitter-delete
                       - [ ] **Build and run every product without the old code present** — With the old runner gone and the hand-written queue worked through, the products build and run with the old directory absent. Anything that must stay gets an explicit reason. Why: Separates 'the products no longer need the old code' from 'the old runner is gone', so neither claim waits on the other's leftovers. [authority](dag/gunbc/v1_deletion_plan.dag) — requires all: v1-interpreter-delete, v1-hand-queue-drain
                         - [ ] **Get hand-written Rust in this repository down to zero** — Every Rust file we track is either generated from a description or deleted. Hand-maintaining Rust is a stage we are passing through, not where we stop. Why: Every hand-written file is a permanent tax: the behaviour and its description have to be kept in step by hand, forever. [authority](dag/gunbc/v1_deletion_plan.dag) — requires all: v1-products-v1-free, v1-test-migration, v1-seed-honesty-decision, namespace-legacy-choice-retirement, namespace-import-deletion
-- [ ] **Write the closing check for: See the hand-written files as they actually are, from the host** — One executable check states when this is done, transcribed from the node's own bar: A read that fails must not come back as an empty or partial set. Discovery and classification are separate axes and are checked separately: finding every tracked file is one question, and every found file carrying a disposition is a different one, so a roster that is complete but unclassified fails the second while passing the first. Why: Turns a prose bar into a runnable verdict, so the node it gates can be dispatched and its completion checked rather than judged. [authority](dag/gunbc/stage0_rust_host_observation.dag)
-  - [ ] **See the hand-written files as they actually are, from the host** — The set of tracked Rust files is read from the repository itself at a known revision, not transcribed. Reading it can fail, and when it does it says so rather than returning a shorter list. Why: Every count of what is left to move was previously taken from whichever files someone had looked at. That understates, silently, and it understated twice here -- so no schedule built on it could be trusted. [authority](dag/gunbc/stage0_rust_host_observation.dag)
-    - [ ] **Keep an honest list of what still depends on the old compiler** — Every module is either generated by the new compiler or explicitly kept on the old one with a reason and a plan to move. Two separate questions, kept separate: whether the list found every module, and whether every module it found has been decided. A complete list of undecided modules and a decided list that missed modules are different failures and are reported differently. Why: Turns a vague sense of 'mostly done' into a finite, countable list someone can work through. [authority](dag/gunbc/v1_deletion_plan.dag)
-      - [ ] **Work through the remaining hand-written files the products need** — Move the hand-written files the shipping tools still depend on. Anything that genuinely has to stay gets an explicit reason. Why: The main command-line tool is itself one of these files, so 'the products still build' is not something we can honestly claim until this is done. [authority](dag/gunbc/v1_deletion_plan.dag)
 - [ ] **Write the closing check for: Make exact prior results reusable across invocations** — One executable check states when this is done, transcribed from the node's own bar: Wrong content, a missing entry, and a full store each refuse rather than quietly falling back to recomputing. Why: Turns a prose bar into a runnable verdict, so the node it gates can be dispatched and its completion checked rather than judged. [authority](docs/plans/witness-realization-plan.md)
   - [ ] **Make exact prior results reusable across invocations** — Iteration-speed and runtime infrastructure: exact input identity selects a bounded materialized result that can be served after restart without compiling. The v1 exit is one consumer of this kernel, not the kernel's parent purpose. Why: Repeated invocations currently rebuild results that an exact identity could safely serve; product iteration, tests, and the v1 exit all pay that recomputation independently. [authority](docs/plans/witness-realization-plan.md)
     - [ ] **Prove old and new agree, by running them, not by waiting** — Run the whole test suite cold on both, compare compile results, check the self-rebuild, and record each family's outcome. Why: Confidence that comes from 'it has been fine for a while' is not evidence; this replaces it with runs someone chose to do. [authority](dag/gunbc/v1_deletion_plan.dag) — requires all: v1-materialization-kernel, v1-emitter-fixed-point

dag/extdeps/github/actions_environment.dag

@@ -0,0 +1,34 @@
+module extdeps.github.actions_environment
+
+import extdeps.external_authority { ExternalAuthority, ExternalModelScope, ExternalSubjectRef }
+import extdeps.uri { Uri, Https }
+import std.decl_ref { DeclarationRef, WholeDeclaration }
+import std.types { CommitSha, String }
+
+data extdeps_external_authority_anchor: ExternalAuthority = ExternalAuthority {
+  uri: Uri {
+    scheme: Https
+    locator: "docs.github.com/en/actions/reference/variables-reference"
+  }
+}
+
+data actions_environment_note: String = "GitHub Actions default environment variables, modeled as the upstream contract rather than read ad hoc. Only the fact this lane needs is carried: GITHUB_SHA, which the cited reference defines as the commit SHA that triggered the workflow run.\n\nWHY THIS EXISTS AS AN UPSTREAM FACT AND NOT A git READ. A liveness claim of the form 'the observation reached the exact revision under test' is only evidence if the EXPECTED revision comes from somewhere other than the thing being tested. Deriving it with git rev-parse and then comparing it to an observation that also ran git rev-parse compares git to itself: it is true by construction, cannot fail, and would be reflection evidence standing in for the structural proof (DESIGN recurring failure modes). GITHUB_SHA is supplied by the workflow runner, independently of the repository checkout, so the comparison can actually fail -- which is what makes it a control.\n\nEVENT SEMANTICS, STATED BECAUSE THEY DECIDE WHETHER THE COMPARISON IS EVEN WELL-FORMED. For a pull_request event the cited reference defines GITHUB_SHA as the LAST MERGE COMMIT of the pull request merge branch, which is exactly what actions/checkout leaves at HEAD under its default ref. For a push event it is the pushed commit, likewise HEAD. So on both events the runner-supplied value and the checked-out HEAD denote the same commit, and a mismatch is a real defect (a shallow or pinned-ref checkout, a mid-run mutation, or an observation that read a different tree) rather than an expected difference. Any event whose checkout ref is configured away from the default breaks that correspondence, and the honest response there is a typed refusal rather than a relaxed comparison."
+
+type ActionsShaObservation
+  = ActionsShaObserved { sha: CommitSha }
+  | ActionsShaMissing { detail: String }
+  | ActionsShaEmpty { detail: String }
+
+data github_sha_variable_name: String = "GITHUB_SHA"
+
+data extdeps_model_scope: ExternalModelScope = ExternalModelScope {
+  subject: ExternalSubjectRef {
+    declaration: DeclarationRef {
+      module_path: "extdeps.github.actions_environment",
+      decl_name: "github_sha_variable_name",
+      field: WholeDeclaration
+    }
+  },
+  first_citation: extdeps.github.actions_environment.extdeps_external_authority_anchor,
+  further_citations: []
+}

dag/gunbc/commit_workflow.dag

@@ -609,6 +609,15 @@ data commit_gate_roster: List<CommitCheckEnrollment> = [
     },
     surfaces: [FalsifierCadenceJob]
   },
+  CommitCheckEnrollment {
+    check: CommitWitnessClaim {
+      entry: "dag/test/claim/stage0_rust_host_observation_live_witness_test.dag",
+      check_fns: ["live_rust_observation_matches_actions_subject"],
+      kind: ExecutionWitnessKind,
+      span: SpanUndeclared
+    },
+    surfaces: [GithubActionsCiJob]
+  },
   CommitCheckEnrollment {
     check: CommitWitnessClaim {
       entry: "src/v2/test/claim/long/gauntlet_lane_enrollment_witness_test.dag",

dag/gunbc/extdeps_scope_frontier.dag

@@ -124,6 +124,7 @@ fn scope_placement_refused_paths(added: List<String>, carriers: List<String>, ma
 }
 
 data scope_carrier_paths: List<String> = [
+  "dag/extdeps/github/actions_environment.dag",
   "dag/extdeps/vendor/atlassian.dag",
   "dag/extdeps/vendor/microsoft.dag"
 ]