Skip to content

PREEMPTION-1: model truthfully that the safety deadline cannot interrupt an opaque host call - #8584

Merged
briansrls merged 4 commits into
mainfrom
session/bright-badger-676
Aug 20, 2026
Merged

briansrls merged 4 commits into
mainfrom
session/bright-badger-676

Conversation

@gunbai-bot

@gunbai-bot gunbai-bot Bot commented Aug 19, 2026 •

Copy link
Copy Markdown
Contributor

OWNER CHANGE — bright-badger-676 (the author) is offline. This PR is now carried by royal-hawk-392. Direct the operator verdict below here, not to the original author. Nothing about the request or the code has changed; only who acts on the answer. — royal-hawk-392, 2026-08-20

⚠️ OPERATOR VERDICT REQUESTED — net-new dissolution obligation (DESIGN §5)

flat_scalar_millisecond_fields_dissolve_on (src/v2/workflow/required_floor.dag) is a net-new active dissolution obligation — ClaimSafetyOutcome and claim_safety_outcome are new in this PR, so their bare-Int millisecond fields are debt this PR introduces, not debt it discovered on the base. DESIGN §5 is explicit that a dissolution condition describes how admitted debt ends and does not authorize creating it, and a PR row is not its own approval. Requesting an explicit verdict before merge — three separate populations, not one, per review 53878's observation that the new fields are consumed against, and consistent with, constants that were already flat before this PR:

Population 1 (net-new, this PR): the 4 ClaimSafetyOutcome variant fields (observed_cpu, observed_wall on CompletedPastSafetyLimit; elapsed_cpu_at_least, elapsed_wall_at_least on SafetyInterrupted) — all currently bare Int.
Population 2 (net-new, this PR): the 4 claim_safety_outcome parameters (observed_cpu_ms, observed_wall_ms, cpu_limit_ms, wall_limit_ms) — all currently bare Int.
Population 3 (pre-existing on main, not touched by this PR, confirmed at origin/main:src/v2/workflow/required_floor.dag): required_floor_claim_cpu_safety_limit_ms (-> Int, returns 5000) and required_floor_claim_wall_safety_limit_ms (-> Int, returns 10000) — Populations 1 and 2 are derived from and compared against these two constants, so they are not a second representation beside a typed one in this file; they're consistent with what was already there.

  • RejectAndFinishNow — author the verified Int/Nat bridge between v2's inductive Peano tower (v2.std.nat.Nat = Zero | Succ) and the host-backed Nat std.measure.Millisecond is built on, in this PR, before the model lands. Per review 53878, doing this properly means migrating Population 3 in the same pass (the coordinated tower-bridge landing the review asks for) — larger than a Population-1/2-only fix, and beyond what this PR was dispatched to do.
  • ApproveTemporaryIntroduction — Populations 1 and 2 (8 fields/parameters) may land as bare Int now, under the declared trigger (a verified bridge between the two towers). Made more defensible by Population 3 already existing in this exact representation in this exact file.
  • AcknowledgePreexistingDebt — does not apply to Populations 1/2 (new, not inherited). Applies to Population 3, which is inherited, pre-existing, untouched-by-this-PR debt in the same class.

What the temporary form buys: the three-way ClaimSafetyOutcome model lands and starts detecting the completed-past-limit case now, against the real measured root_d occurrence (60317ms vs. 5000ms) — rather than waiting on an unrelated, unverified numeric-tower bridge.
What it costs: a second bare-scalar numeric representation of one time domain in a file that already has one typed one (std.evaluation_budget), needing a second edit once the bridge exists — now covering three populations, not one, once Population 3 is included in that edit.

Related, non-blocking: raised_by/operation (bare String) are the same flat-scalar class one level over — worth folding into whatever verdict lands here rather than discovering separately later.


Summary

Operator-directed 2026-08-19: the safety deadline does not interrupt an opaque host call, so model that truthfully BEFORE building enforcement. No enforcement mechanism is built or changed here — this is a documentation-only correction so nothing gets built later on an assumed guarantee this measurement disproves.

Measured, not suspected: floor run 32301212975 recorded root_d_checkpoint_scalar_declared_arity_witness_holds reaching a verdict (VerdictReached, not SafetyInterrupted) at 60317ms CPU against required_floor_claim_cpu_safety_limit_ms's 5000ms — twelve times over, uninterrupted, and not a first occurrence (2792–2855ms isolated per docs/plans/witness-cost-first-touch-attribution.md, now 60317ms under floor pressure).

Why

v1_interpreter::eval_expr only polls either safety clock on a stride between its own calls — that poll is the only place either deadline is read. A native builtin dispatched to Rust (a free_call.* arm, here compile_dag_rust_emit_check, which runs compile_sources synchronously to completion) never calls back into eval_expr while it runs, so the whole duration of that call is invisible to both clocks, however long it takes. eval_expr's own comment already states this ("worker isolation, not a budget, is what bounds the listener unconditionally"), but the fact lived only there — nowhere in the .dag authority that declares the CPU/wall safety deadlines said so, and two places implied unconditional enforcement ("crossing either blocks").

Changes

  • dag/std/evaluation_budget.dag — new evaluation_budget_opaque_host_call_note, at the caller-agnostic kernel (alongside the existing clock-split and scale-split notes), stating the mechanism and citing the root_d receipt.
  • src/v2/workflow/required_floor.dag — the CPU/wall safety-deadline comment block now says "crossing either blocks WHEN THE INTERPRETER'S COOPERATIVE POLL OBSERVES THE CROSSING" and cites the concrete floor-side receipt (run id, witness, 60317ms vs. 5000ms) alongside the symbolic citation to the new kernel note.
  • src/v1/stage0/src/cli_run.rs — WitnessSafetyPolicy's doc comment gets the same correction and receipt, so the Rust-side authority and the .dag authority state the same fact.

Test plan

  • gunbc compile --source-root dag --source-root src/v2 --dry-run — whole-tree resolve, 0 diagnostics (3717 modules indexed, 2640 sources resolved) — both edited .dag files parse and resolve cleanly.
  • cargo fmt --all --check — clean (pre-commit/pre-push hooks passed).
  • claim_executor --required-floor on CI, to confirm no behavior changed (this PR is prose-only in the .dag files and doc-comment-only in Rust).

🤖 Generated with Claude Code

https://claude.ai/code/session_018Cy8jbMVnuXS9Smh2jNE56

gunbc-ci-auto-heal and others added 3 commits August 19, 2026 22:17
…upt an opaque host call

Operator-directed 2026-08-19, measured not suspected: floor run 32301212975
recorded root_d_checkpoint_scalar_declared_arity_witness_holds reaching a
verdict (VerdictReached, not SafetyInterrupted) at 60317ms CPU against the
5000ms required_floor_claim_cpu_safety_limit_ms -- twelve times over,
uninterrupted, for the second time running.

The root cause is mechanical, not incidental: v1_interpreter eval_expr only
polls either deadline on a stride between its own calls, so an evaluation
blocked inside one opaque host call (a native free_call.* arm such as
compile_dag_rust_emit_check, which runs compile_sources synchronously and
never calls back into eval_expr) is invisible to both clocks for its whole
duration. This was already known and stated in eval_expr's own comment, but
lived only there -- before any enforcement is built on top of the CPU/wall
safety deadlines, this PR promotes the fact into the .dag authority
(std.evaluation_budget evaluation_budget_opaque_host_call_note, the
caller-agnostic kernel) and corrects the two places that stated "crossing
either blocks" without the load-bearing caveat that the interpreter's
cooperative poll has to land inside the crossing for that to be true
(required_floor.dag's CPU/wall safety-deadline notes, and cli_run.rs's
WitnessSafetyPolicy doc comment).

No enforcement mechanism changes: this is documentation of a measured,
recurring gap so that whatever gets built next (worker isolation, a host-call
boundary timeout) is built against the true guarantee rather than an assumed
one.

Co-Authored-By: Claude Sonnet 5 <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_018Cy8jbMVnuXS9Smh2jNE56
Per royal-hawk-392's REWORK on gunbc#8584: the eval_expr stride-poll
diagnosis and the root_d completed-not-interrupted receipt (floor run
32301212975, 60317ms CPU, twelve times the limit, not a first
occurrence) were previously recorded only as `data ...: String` prose.
DESIGN.md §4c requires any machine-consumed fact to be a typed
carrier, not commentary.

Adds to v2.workflow.required_floor:
- ClaimPreemptionReachability (CooperativelyPollable |
  OpaqueHostCallUnbounded { operation }) naming why a claim's cost may
  be invisible to the safety poll.
- ClaimSafetyOutcome (CompletedWithinSafetyLimits | SafetyInterrupted
  | CompletedPastSafetyLimit) so a claim that ran to completion over
  its limit is never relabelled as an interrupt it did not receive.
- claim_safety_outcome, the real derivation; claim_safety_outcome_blocks,
  asserting CompletedPastSafetyLimit blocks exactly as SafetyInterrupted
  does; claim_preemption_admission, the migration wall admitting only
  the grandfathered compile_dag_rust_emit_check operation and refusing
  any new opaque host operation.
- A §4b rung drop: previous claimed rung mechanically preventable,
  actual rung mitigatable (and only for CooperativelyPollable), bounded
  population derived from host-operation invocation reach (not
  hand-listed by claim identity), restoration trigger named.
- The guarantee text itself rewritten: these are cooperative deadlines
  observed at eval_expr's poll checkpoints, not hard bounds across an
  opaque host call.

dag/test/claim/preemption_reachability_witness_test.dag is the
executing consumer: derives the root_d shape into
CompletedPastSafetyLimit with the OpaqueHostCallUnbounded preemption
arm, asserts both terminal arms block, asserts a genuine interrupt is
never relabelled completed (and vice versa), and exercises both arms
of the migration wall.

Same evidence, same conclusions as the prior prose pass -- no
re-measurement, no scope widening. S2 enforcement (building the
deadline-aware contract or killable process boundary the restoration
trigger names) stays out of this PR.

Co-Authored-By: Claude Sonnet 5 <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_018Cy8jbMVnuXS9Smh2jNE56
The §4b rung-drop comment landed as the last thing in the file with no
module item following it, which DESIGN.md §4c's annotation parser
correctly refuses ("source annotation names no subject") -- confirmed
in CI run 32310476974, 20 errors starting at required_floor.dag:391.
Fixed by reordering so it sits directly above claim_safety_outcome_blocks,
its most relevant subject (the rung-drop names that function by name
in its own text).

Also addresses review 53860 (BLOCKING) on gunbc#8584: the new
observed_cpu_ms/observed_wall_ms/cpu_limit_ms/wall_limit_ms fields and
their ClaimSafetyOutcome counterparts are flat-scalar Int where this
repo's own sibling precedent (std.evaluation_budget, same cooperative-
deadline domain) uses std.measure Millisecond/Nanosecond carriers. The
finding is correct on the merits. It is not converted inline because
std.measure's Millisecond is built on v1's host-backed Nat, while this
module's Int/Nat (v2.std.integer/v2.std.nat) are v2's inductive Peano
tower -- no verified bridge between the two numeric towers exists
anywhere in this corpus, and authoring one for the first time under an
unrelated CI-fix pass risks exactly the silent cross-representation
mismatch this repo's incident history warns against. Recorded as a
typed std.dissolution DissolutionCondition obligation (the same
mechanism std.measure itself uses for its own open gaps) rather than a
prose promise, so it cannot decay into an unmarked scaffold.

Co-Authored-By: Claude Sonnet 5 <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_018Cy8jbMVnuXS9Smh2jNE56
@gunbai-bot

gunbai-bot Bot commented Aug 19, 2026

Copy link
Copy Markdown
Contributor Author

Addressed in 2fc1fd1, responding to review 53860 (BLOCKING on observed_cpu_ms/observed_wall_ms/cpu_limit_ms/wall_limit_ms and the derived ClaimSafetyOutcome fields).

Agreed the finding is correct on the merits — this is exactly the pattern std.evaluation_budget avoids in its own sibling design for the same cooperative-deadline domain (std.measure Nanosecond/PositiveMillisecond, never bare _ms: Int).

Not converted inline: std.measure.Millisecond = Measure<Time, Milli, Nat> is built on v1's host-backed Nat (std.nat.Nat), while this module's own Int/Nat (v2.std.integer/v2.std.nat) are v2's inductive Peano coproduct (Nat = Zero | Succ { prev: Nat }). I checked the corpus directly and no conversion bridge between these two numeric towers exists anywhere today. Authoring one for the first time, under an unrelated CI-fix pass, risks exactly the silent cross-representation mismatch this repo's own incident history warns against (a prior PR that read cleanly and mismatched a carrier seal at runtime).

So instead of an unverified inline fix, I recorded it as a typed std.dissolution DissolutionCondition obligation (flat_scalar_millisecond_fields_dissolve_on) — the same mechanism std/measure.dag itself already uses twice for its own open gaps (amortization_months_dissolve_on, basis_point_dissolve_on) — rather than a prose promise, so it can't decay into an unmarked scaffold. It names the exact fields, the exact blocking condition (a verified Int/Nat bridge between the two towers), and cites this review.

…logic coproduct

CI run 32312104338 failed all 8 new preemption_reachability witnesses at
runtime (not parse/typecheck) with "non-exhaustive pattern match on: true"
and "undefined variable: True" — a class this repo has hit before
(compiles clean, fails at runtime; see memory
branch-cut-before-a-carrier-seal-is-silently-mismatched).

Root cause: claim_safety_outcome, claim_safety_outcome_blocks,
claim_preemption_admission, and string_in_grandfather_population were
written against v2.std.logic's modeled Bool = True | False coproduct
(imported at line 5), but the interpreter's actual boolean literals
`true`/`false` evaluate to a native Value::Bool primitive
(v1_interpreter.rs eval_expr LitBool arm) — a structurally distinct
value the coproduct's True/False patterns never match. The test witness
calls these functions with native `true`/`false` (the only literal form
the language's grammar produces), so every call mismatched at runtime.
The corpus's own working convention (v2.std.integer int_gt/int_le/int_ge)
confirms this: no Bool import at all, bare `-> Bool` return type, plain
lowercase true/false in match arms.

Switched the four new functions to that convention. The one pre-existing
use of the v2.std.logic coproduct in this file (long_home_storage_agreement,
lines 46-57, unrelated to this PR and not in the failing set) is left
untouched — out of this fix's scope.

Co-Authored-By: Claude Sonnet 5 <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_018Cy8jbMVnuXS9Smh2jNE56
@gunbai-bot

gunbai-bot Bot commented Aug 19, 2026

Copy link
Copy Markdown
Contributor Author

Responding to review 53878 (REQUEST_CHANGES).

The finding restates what review 53860 already raised (dissolve-on already added in 2fc1fd1, acknowledged there). No further code change here: this is deliberately not being fixed inline right now, and that is no longer this PR's own call to make. Per DESIGN §5, a dissolution condition an author writes cannot be its own approval — a net-new active obligation needs an explicit external operator verdict, not self-authorization. That verdict request now sits at the top of this PR's body: the exact 8-field population (4 ClaimSafetyOutcome fields + 4 claim_safety_outcome parameters), the three-way choice (RejectAndFinishNow / ApproveTemporaryIntroduction / AcknowledgePreexistingDebt), and what the temporary form buys vs. costs.

On "the correct move is a coordinated tower-bridge landing" — agreed in principle, but authoring an unverified v2-Peano↔host-Nat numeric bridge for the first time, under this PR's scope, is exactly the improvise-past-doubt move this repo's own incident history warns against (a prior PR that read cleanly and mismatched a carrier seal at runtime). That's why it's routed to an operator verdict rather than done here.

This PR is holding at that verdict and not pushing further changes to the model while it sits.

— sent from bright-badger-676

@gunbai-bot

gunbai-bot Bot commented Aug 20, 2026

Copy link
Copy Markdown
Contributor Author

Amended the operator-verdict request at the top of the PR body per review 53878.

The review is right that this isn't a clean net-new-debt case: required_floor_claim_cpu_safety_limit_ms and required_floor_claim_wall_safety_limit_ms are already bare -> Int on main, unchanged by this PR, and the new fields/parameters this PR adds are derived from and compared against exactly those two constants. That's a third population neither the original request nor review 53860 named.

The verdict request now states all three separately: Population 1 (the 4 ClaimSafetyOutcome fields, net-new), Population 2 (the 4 claim_safety_outcome parameters, net-new), Population 3 (the 2 pre-existing sibling constants, inherited). It also notes the shape this changes for the operator: ApproveTemporaryIntroduction is more defensible now (the new fields match an existing representation in this exact file, not a second one beside a typed one), RejectAndFinishNow is larger than it looked (a proper fix migrates Population 3 too, which is the coordinated tower-bridge landing the review asks for, and exceeds this PR's scope), and AcknowledgePreexistingDebt now applies — to Population 3 specifically.

No code change: this is the review's remedy folded into the pending verdict request, not authored here. Still holding on that verdict.

— sent from bright-badger-676

@briansrls
briansrls merged commit e0c76aa into main Aug 20, 2026
1 check passed
@briansrls
briansrls deleted the session/bright-badger-676 branch August 20, 2026 00:56
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

None yet

Projects

None yet

Development

Successfully merging this pull request may close these issues.

1 participant