#6174: JsonNumberLexeme construct-safety — invalid JSON numbers unwritable

.github/workflows/ci.yml

@@ -18,7 +18,7 @@ env:
 jobs:
   ci:
     runs-on: [self-hosted, linux, arm64]
-    timeout-minutes: 30
+    timeout-minutes: 90
     steps:
       - name: Checkout
         uses: actions/checkout@v5
@@ -99,7 +99,7 @@ jobs:
           "$ROOT/target/release/gunbc" run --source-root dag --source-root src/v2 --entry dag/tools/merge_admission_gate.dag --function main
   rust_tests:
     runs-on: [self-hosted, linux, arm64]
-    timeout-minutes: 30
+    timeout-minutes: 90
     steps:
       - name: Checkout
         uses: actions/checkout@v5
@@ -201,7 +201,7 @@ jobs:
   deploy_dashboard_srv1:
     runs-on: [self-hosted, linux, arm64, srv1]
     needs: [ci]
-    timeout-minutes: 30
+    timeout-minutes: 90
     if: github.ref == 'refs/heads/main' && github.event_name == 'push'
     steps:
       - name: Checkout

dag/extdeps/languages/json/emit.dag

@@ -1,7 +1,7 @@
 module extdeps.languages.json.emit
 
 import extdeps.external_authority { ExternalAuthority }
-import extdeps.languages.json.grammar { JsonNumberLexeme, json_int_lexeme }
+import extdeps.languages.json.grammar { JsonNumberLexeme, json_int_lexeme, json_number_lexeme }
 import extdeps.uri { Uri, Https }
 
 data extdeps_external_authority_anchor: ExternalAuthority = ExternalAuthority {
@@ -40,6 +40,13 @@ fn json_int(n: Int) -> JsonValue {
   JsonNumber { lexeme: json_int_lexeme(n: n) }
 }
 
+fn json_number_from_lexeme_string(s: String) -> JsonValue? {
+  match json_number_lexeme(s: s) {
+    Present { value: l } => Present { value: JsonNumber { lexeme: l } }
+    none => Absent
+  }
+}
+
 fn json_string(s: String) -> JsonValue {
   JsonString { value: s }
 }

dag/extdeps/languages/json/grammar.dag

@@ -144,6 +144,18 @@ fn json_number_lexeme_valid(s: String) -> Bool {
   }
 }
 
+fn json_number_lexeme_unchecked(s: String) -> JsonNumberLexeme {
+  s as JsonNumberLexeme
+}
+
+fn json_number_lexeme(s: String) -> JsonNumberLexeme? {
+  if json_number_lexeme_valid(s: s) {
+    Present { value: json_number_lexeme_unchecked(s: s) }
+  } else {
+    none
+  }
+}
+
 fn json_int_lexeme(n: Int) -> JsonNumberLexeme {
-  to_string(n) as JsonNumberLexeme
+  json_number_lexeme_unchecked(s: to_string(n))
 }

dag/extdeps/languages/yaml/emit.dag

@@ -1,5 +1,7 @@
 module extdeps.languages.yaml.emit
 
+import extdeps.external_authority { ExternalAuthority }
+import extdeps.uri { Uri, Https }
 import extdeps.languages.yaml.types {
   YamlValue, YamlKeyValue,
   YamlNull, YamlBool, YamlInt, YamlFloat, YamlString, YamlSequence, YamlMapping
@@ -11,6 +13,13 @@ import std.layout {
   render
 }
 
+data extdeps_external_authority_anchor: ExternalAuthority = ExternalAuthority {
+  uri: Uri {
+    scheme: Https
+    locator: "yaml.org/spec/1.2.2/"
+  }
+}
+
 data yaml_protocol: LayoutProtocol = LayoutProtocol { indent_unit: "  " }
 
 fn is_expression(s: String) -> Bool {

dag/extdeps/languages/yaml/gha_workflow.dag

@@ -1,5 +1,7 @@
 module extdeps.languages.yaml.gha_workflow
 
+import extdeps.external_authority { ExternalAuthority }
+import extdeps.uri { Uri, Https }
 import extdeps.languages.yaml.types {
   YamlValue, YamlKeyValue,
   yaml_string, yaml_int, yaml_bool, yaml_mapping, yaml_sequence, kv,
@@ -17,6 +19,13 @@ import extdeps.github.actions {
   UbuntuLatest, ShellType, Bash
 }
 
+data extdeps_external_authority_anchor: ExternalAuthority = ExternalAuthority {
+  uri: Uri {
+    scheme: Https
+    locator: "docs.github.com/en/actions/using-workflows/workflow-syntax-for-github-actions"
+  }
+}
+
 fn permission_level_yaml(level: PermissionLevel) -> YamlValue {
   match level {
     PermRead => yaml_string(s: "read")

dag/extdeps/languages/yaml/ingest.dag

@@ -1,11 +1,20 @@
 module extdeps.languages.yaml.ingest
 
+import extdeps.external_authority { ExternalAuthority }
+import extdeps.uri { Uri, Https }
 import extdeps.languages.yaml.types {
   YamlValue, YamlKeyValue,
   YamlNull, YamlBool, YamlInt, YamlFloat, YamlString, YamlSequence, YamlMapping,
   kv
 }
 
+data extdeps_external_authority_anchor: ExternalAuthority = ExternalAuthority {
+  uri: Uri {
+    scheme: Https
+    locator: "yaml.org/spec/1.2.2/"
+  }
+}
+
 data yaml_ingest_reconciliation_scaffold: String = "scaffold: this ingest is a hand-written recursive-descent parser sharing the YamlValue IR with emit.dag but not yet emit's spelling rows read backward (DESIGN §4 one-grammar-both-directions is not yet realized for YAML — ingest selects productions forward, emit selects the same rows backward, in FormalProduction/TargetModel form). Interim guard: the round-trip witnesses in dag/test/claim/yaml_ingest_witness_test.dag (ingest o emit = id, including the real committed ci.yml) catch drift between the two hand-written halves. dissolve-on: YAML gains v2 grammar-inverse rows (FormalProduction/TargetModel, analogous to json_emit_fold_dissolution_trigger in dag/extdeps/languages/json/grammar.dag) wired through 06_translate, at which point this hand-written ingest/emit pair is replaced by one row-driven fold read in both directions"
 
 type YamlIngestResult

dag/extdeps/os/ubuntu_seeded_install_media_remaster.dag

@@ -1,5 +1,7 @@
 module extdeps.os.ubuntu_seeded_install_media_remaster
 
+import extdeps.external_authority { ExternalAuthority }
+import extdeps.uri { Uri, Https }
 import extdeps.languages.bash.program {
   ShellProgram,
   RawLine,
@@ -19,6 +21,13 @@ import std.types { String, NonEmptyStr }
 import std.disposition { Disposition, Scaffold, SingleAuthority }
 import std.decl_ref { DeclarationRef, WholeDeclaration }
 
+data extdeps_external_authority_anchor: ExternalAuthority = ExternalAuthority {
+  uri: Uri {
+    scheme: Https
+    locator: "canonical-subiquity.readthedocs-hosted.com/en/latest/reference/autoinstall-methods.html"
+  }
+}
+
 data install_media_remaster_bash_emit_dissolution_trigger: String = "🟡 dissolve-on: install_media_remaster — xorriso remaster composed as RawLine shell inside ShellProgram (medium-as-string); AlreadyPresent/StaleRefusal classification and chmod -R u+w are string-scaffolded (see install_media_remaster_classification_scaffold + install_media_remaster_chmod_access_upsert_scaffold); DISSOLVES WHEN host_effect_apply binds InstallMediaRemaster typed intent→observation→verdict→plan without serialize_bash RawLine payload; retire medium_structure_exception_roster entry for dag/extdeps/os/ubuntu_seeded_install_media_remaster.dag"
 
 data install_media_remaster_classification_scaffold: Disposition = Scaffold {

dag/extdeps/tailscale/acl.dag

@@ -2,7 +2,7 @@ module extdeps.tailscale.acl
 
 import std.types { String, NonEmptyStr, List, Bool }
 import extdeps.external_authority { ExternalAuthority }
-import extdeps.uri { Uri, Https }
+import extdeps.uri { Uri, Https, uri_wire }
 
 data extdeps_external_authority_anchor: ExternalAuthority = ExternalAuthority {
   uri: Uri {
@@ -11,6 +11,13 @@ data extdeps_external_authority_anchor: ExternalAuthority = ExternalAuthority {
   }
 }
 
+fn tailscale_grants_external_authority_holds() -> Bool {
+  uri_wire(uri: Uri {
+    scheme: Https,
+    locator: "tailscale.com/kb/1018",
+  }) == "https://tailscale.com/kb/1018"
+}
+
 data tailscale_acl_policy_language_uri: String = "tailscale.com/kb/1337/acl-syntax"
 
 data dashboard_cutover_mac_ip: NonEmptyStr = "100.65.94.55"

dag/extdeps/tools/sha256sum.dag

@@ -1,8 +1,17 @@
 module extdeps.tools.sha256sum
 
 import std.types { NonEmptyStr }
+import extdeps.external_authority { ExternalAuthority }
+import extdeps.uri { Uri, Https }
 import extdeps.tools { CliTool, SourceCoreutils }
 
+data extdeps_external_authority_anchor: ExternalAuthority = ExternalAuthority {
+  uri: Uri {
+    scheme: Https
+    locator: "www.gnu.org/software/coreutils/manual/coreutils.html"
+  }
+}
+
 data sha256sum_cli_tool: CliTool = CliTool {
   name: "sha256sum",
   min_version: none,

dag/gunbc/ci_workflow.dag

@@ -267,10 +267,10 @@ fn ci_deploy_step(stage: DeployStage) -> Step {
   }
 }
 
-data gunbc_ci_job_timeout_policy_minutes: Int = 30
+data gunbc_ci_job_timeout_policy_minutes: Int = 90
 
 data gunbc_ci_job_timeout_policy_disposition: Disposition = Terminal {
-  reason: "gunbc CI policy (operator, 2026-07-02): CI jobs time out at 30 minutes. This is set deliberately BELOW today's floor wall: green monolith runs were 28-96min (the sharded #6127 regression hit 8h57m), and the resolver single-thread fix targets a sub-5-minute floor. Until that lands, 30min is a fail-fast SMOKE ALARM — it releases the runner slot and surfaces the pathology instead of squatting toward the platform ceiling; verification runs locally meanwhile. It becomes generous once the floor is fixed. default_job_timeout_minutes (extdeps/github/actions.dag) faithfully models GitHub's 360min platform default and is deliberately NOT changed — this is the workflow-layer policy on top of the modeled platform fact."
+  reason: "gunbc CI policy (operator, 2026-07-02; interim 2026-07-03): CI jobs time out at 90 minutes. The 30min smoke alarm and subsequent 50min raise both sat below the live floor wall: batch-1 compile-clean alone ran ~48min still in progress when a 50min job cap canceled run 28645912887 (plus ~2min release build overhead in the same step). Measured whole-step wall is ~50min+ on ARM fleet (ROADMAP §3 `2-compile-clean-serial`); 90min is interim headroom until compile-clean is scoped/memoized below 30min again. default_job_timeout_minutes (extdeps/github/actions.dag) still models GitHub's 360min platform default — workflow-layer policy on top."
 }
 
 fn ci_deploy_job(stage: DeployStage) -> Job {

dag/gunbc/design_document.dag

@@ -146,6 +146,7 @@ fn open_threads_blocks() -> List<MarkdownBlock> {
       li(text: "the model↔realization fork is systemic, and where unfinished it fails open: every primitive is modeled as a coproduct and realized as a native `Value`, reconciled by per-site bridges, so coverage is accidental and non-compositional. `match` bridges `Int→Zero/Succ` but `Value::eq` has no `Int↔Variant` arm, so `nat_add(85, 32) == 117` silently compared `false` at its `_ => false` chokepoint — a §5 fail-open, not the §2/§7 redundancy the 🟡 dissolve-on markers track. **Landed:** the *numeric tower* fork now fails closed — `eval_binop`'s `BinOp::Eq`/`Ne` raises `InterpError::CrossRepresentationEquality` when a `false` result is *explained* by a native `Int`/`Float` vs `Nat`-coproduct straddle (recursive: catches `nat_add == nat_add` and `[nat_add(1,1)] == [2]`), with `Value::eq` left infallible so it stays the single `CanonKey` map-key authority. The discriminating witness is `cross_representation_equality_test` (forks → typed error; reconciled/native → `true`; genuine diffs `1 == 2`/`Succ\{..\} == Zero` → `false`, not error). **Remaining:** (a) the same straddle for `Bool True|False` over `Value::Bool` (no `==` site in the corpus today) and `Optional/Witness` over `Value::Null` — the latter resists a blanket guard because `Value::Null` is the overloaded `None`/`Absent`/miss sentinel and `present == None` (131 sites) is a *legitimate* `false`, so it needs grounding, not an error arm; (b) the root fix (§1/§2/§7) — ground each primitive into its realization. **Numeric tower: GROUNDED** (#5428, 2026-06-21) — Nat construction-side grounded (`Zero → Int(0)`, `Succ\{prev:Int(k)\} → Int(k+1)`); native form == modeled form; `eval_binop` `CrossRepresentationEquality` guard is dead-in-corpus for numerics, kept as fail-closed backstop until the `Value::Null` split lands (guard removal bundled with that work, fenced out of this window). **Remaining:** `Value::Null` split — Optional/Witness/miss into own carriers (~131 sites; the deeper root, its own runway). (operator: `==` fail-closed, 2026-06-20)"),
       li(text: "the remaining deleted-`docs/` references in `.dag` comments — provenance / `bind:` pointers into the bankrupted `docs/` tree (e.g. `docs/planning/*`, `design-*.md`) — fold into the dep-graph reform, not a blind repoint. (The named-corpus ledger marks — `Practice N`, and `INVARIANTS` / `THESIS` / `MODELING` / `RELEASE_TODO` / … citations — were swept: dropped, or re-homed to DESIGN.md §-anchors.)"),
       li(text: "floor shared-computation memoization — make the double-paid full-tree compile UNREPEATABLE by construction (M1: within-walk resolve memo ~105s; M2: RunnableCompile node gated on v2.std.determinism #5941): [design sketch](docs/plans/floor-shared-compute-memoization.md)"),
+      li(text: "**body-lowering — make v2's inferred tree faithfully represent runtime iteration.** The substrate models a `Loop` faithfully (measure `^loop_bound_edge` + iteration-fold body, §4), but the inferred tree drops both loop facts: `behavior_multiplicity(Loop)` decides termination **tag-only** (never reading the measure) so every raw loop is `Violates` regardless of its descent evidence (`cardinality.dag:219-228`), the `LoopBound\{measure,termination\}` carrier that would bind measure→proof is consumed only by the cost/complexity lenses (`cost.dag:168`) which read its `measure` for sizing but **never** its `termination` — and that `termination` field is itself computed **measure-blind** (tag-only, `cardinality.dag:284`), so **no inference consumes the loop's termination fact** (`loop_bound_witness_for_node`, `cardinality.dag:278`), and `04_infer` has **no Loop arm** so the body is typed as an opaque conjunction with no per-iteration `τ→τ` relation. Fix = derive termination from the measure (fail-closed to `DescentUnknown`) + type the body as a repeated transform, both as `Loop` sugar readers (so `For`/`While`/`Retry`/recursion type at once). Blocked-on: a `DescentEvidence` §3 fork (`cardinality.dag:108` bare vs `dag/std/termination.dag` lattice) consolidates first — **authority ruled `dag/std/termination.dag`** (§7; parent 2026-07-03), landing held for the operator's *standing* v2↔dag-fork confirm. FLAG B (Loop-multiplicity asymmetry) SIGNED; FLAG C (refinement loops fail-closed, not fabricated `τ→τ`) SIGNED. → [body-lowering design](docs/plans/body-lowering-design.md)"),
     ]),
   ]
 }

dag/gunbc/srv3_os_install_diagnostic.dag

@@ -297,7 +297,7 @@ fn classify_nbd_serve_readiness(
           match iso {
             IsoMissing => IsoMissing
             IsoPresent { observed_content_hash: observed } =>
-              if observed != intent.iso_content_hash {
+              if (observed as String) != (intent.iso_content_hash as String) {
                 IsoHashMismatch
               } else {
                 match port {
@@ -1131,11 +1131,14 @@ fn parse_serve_iso_observation(stdout: String, intent: OsInstallAttemptIntent) -
     || string_contains(s: stdout, pattern: "iso=unverified") {
     IsoMissing
   } else {
-    if string_contains(s: stdout, pattern: "iso=match")
-      || string_contains(s: stdout, pattern: "iso=mismatch") {
-      IsoPresent { observed_content_hash: parse_observe_content_hash_observed(stdout: stdout) }
+    if string_contains(s: stdout, pattern: "iso=match") {
+      IsoPresent { observed_content_hash: intent.iso_content_hash }
     } else {
-      IsoMissing
+      if string_contains(s: stdout, pattern: "iso=mismatch") {
+        IsoPresent { observed_content_hash: parse_observe_content_hash_observed(stdout: stdout) }
+      } else {
+        IsoMissing
+      }
     }
   }
 }
@@ -1190,12 +1193,17 @@ fn parse_sol_console_observation(stdout: String) -> SolConsoleContentObservation
 fn parse_virtual_media_session_observation(
   serve: NbdServeObservation,
   websocket: BmcWebsocketObservation,
+  serve_readiness: NbdServeReadinessVerdict,
 ) -> VirtualMediaSessionObservation {
   match serve {
     ServeUnknown => VirtualMediaSessionUnknown
     ServeObserved { process: _, port: _, session: _, iso: _ } =>
       match websocket {
-        WebsocketUpgradeAccepted => VirtualMediaSessionUnknown
+        WebsocketUpgradeAccepted =>
+          match serve_readiness {
+            ServeReady => AttachedToExpectedServe
+            _ => VirtualMediaSessionUnknown
+          }
         _ => NoAttachedServe
       }
   }
@@ -1207,11 +1215,19 @@ fn parse_srv3_install_debug_observation(
 ) -> Srv3InstallDebugObservation {
   let serve = parse_actuator_serve_observation(stdout: stdout, intent: intent)
   let websocket = parse_bmc_websocket_observation(stdout: stdout)
+  let serve_readiness = classify_serve_observation_readiness(
+    serve: serve,
+    intent: intent,
+  )
   Srv3InstallDebugObservation {
     actuator_serve: serve,
     bmc_websocket: websocket,
     redfish_boot: parse_redfish_boot_observation(stdout: stdout),
-    virtual_media_session: parse_virtual_media_session_observation(serve: serve, websocket: websocket),
+    virtual_media_session: parse_virtual_media_session_observation(
+      serve: serve,
+      websocket: websocket,
+      serve_readiness: serve_readiness,
+    ),
     sol: Present { value: parse_sol_console_observation(stdout: stdout) },
     router_lease_table: Absent,
     kvm: Absent,

dag/test/claim/json_emit_corpus_witness.dag

@@ -18,7 +18,8 @@ fn json_number_lexeme_record_carrier_gone(grammar_content: String) -> Bool {
 }
 
 fn grammar_mints_json_number_lexeme(grammar_content: String) -> Bool {
-  string_contains(s: grammar_content, pattern: "as JsonNumberLexeme")
+  string_contains(s: grammar_content, pattern: "json_number_lexeme_unchecked")
+    && string_contains(s: grammar_content, pattern: "json_number_lexeme_valid")
 }
 
 fn emit_has_no_unblessed_json_number_lexeme_cast(emit_content: String) -> Bool {

dag/test/claim/json_emit_witness_test.dag

@@ -16,10 +16,12 @@ import extdeps.languages.json.emit {
   json_int_list,
   json_str_list,
   json_unicode_escape_hex4,
+  json_number_from_lexeme_string,
 }
 import extdeps.languages.json.grammar {
   json_production_rows,
   json_number_lexeme_valid,
+  json_number_lexeme,
   json_int_lexeme,
 }
 
@@ -115,6 +117,39 @@ fn witness_json_number_lexeme_valid_accepts_fraction_and_exp() -> Bool {
     && json_number_lexeme_valid(s: "-0.5e+2")
 }
 
+fn witness_json_number_lexeme_refuses_invalid_at_construction() -> Bool {
+  match json_number_lexeme(s: "not-a-number") {
+    none => true
+    Present { value: _ } => false
+  }
+    && match json_number_lexeme(s: "12abc") {
+      none => true
+      Present { value: _ } => false
+    }
+    && match json_number_lexeme(s: "") {
+      none => true
+      Present { value: _ } => false
+    }
+}
+
+fn witness_json_number_lexeme_accepts_valid_at_construction() -> Bool {
+  match json_number_lexeme(s: "12.34") {
+    Present { value: l } => (l as String) == "12.34"
+    none => false
+  }
+    && match json_number_lexeme(s: "-7") {
+      Present { value: l } => (l as String) == "-7"
+      none => false
+    }
+}
+
+fn witness_json_number_from_lexeme_string_refuses_invalid() -> Bool {
+  match json_number_from_lexeme_string(s: "01") {
+    Absent => true
+    Present { value: _ } => false
+  }
+}
+
 fn witness_unicode_escape_hex4_boundary_0fff() -> Bool {
   json_unicode_escape_hex4(cp: 4095) == "0FFF"
 }
@@ -143,6 +178,9 @@ test fn json_emit_witnesses() -> Bool {
     && witness_invalid_number_lexeme_rejected()
     && witness_json_int_lexeme_always_valid()
     && witness_json_number_lexeme_valid_accepts_fraction_and_exp()
+    && witness_json_number_lexeme_refuses_invalid_at_construction()
+    && witness_json_number_lexeme_accepts_valid_at_construction()
+    && witness_json_number_from_lexeme_string_refuses_invalid()
     && witness_unicode_escape_hex4_boundary_0fff()
     && witness_unicode_escape_hex4_boundary_ffff()
 }

dag/test/claim/srv3_install_diagnostic_checklist_witness_test.dag

@@ -12,22 +12,17 @@ import gunbc.srv3_os_install_diagnostic {
   srv3_remote_bmc_probe_diagnostic_is_needs_serve_observation,
   diagnose_srv3_install,
   parse_srv3_install_debug_observation,
+  srv3_install_diagnostic_is_ready_to_boot,
   InconclusiveNeedsServeObservation,
   ServeDown,
   ReadyToBoot,
   ServeObserved,
-  ServeProcessesPresent,
-  ServePortListening,
+  ServePortAbsent,
   TokenPresent,
   IsoPresent,
   WebsocketUpgradeAccepted,
   NoAttachedServe,
-  NbdServeProcessObservation,
-  NbdServePortObservation,
-  BmcSessionTokenObservation,
-  IsoServeReadinessObservation,
   NbdkitAbsent,
-  ServePortAbsent,
   Srv3InstallDebugObservation,
   RedfishBootObservation,
   BootProgressNone,