diff --git a/.github/workflows/ci.yml b/.github/workflows/ci.yml index 7867ad9be5e..9e97df32cfe 100644 --- a/.github/workflows/ci.yml +++ b/.github/workflows/ci.yml @@ -232,6 +232,12 @@ jobs: - name: RELEASE §5 v4 workflow release model/YAML binding smoke if: needs.affected.outputs.v4 == 'true' || needs.affected.outputs.workflow_policy == 'true' || needs.affected.outputs.release_distribution == 'true' || (github.event_name == 'push' && github.ref == 'refs/heads/main') run: cargo test -p v3-compiler --test integration v4_workflow_release_dag_smoke_test -- --quiet + # Phase 1 leaf-model R1 — gunbc#846 bypass: v3 job skips integration execution; run boundary + # rustc receipt here (docs/planning/v4-leaf-model-verification-2026-05-30.md §7; pairs with + # scripts/v4-leaf-model-rust-r1-verify.sh). Dissolution: modeled run_target_verification. + - name: Phase 1 leaf-model R1 rustc boundary (gunbc#846 bypass) + if: needs.affected.outputs.v4 == 'true' || needs.affected.outputs.workflow_policy == 'true' + run: cargo test -p v3-compiler --test integration v4_leaf_model_rust_r1_rustc_test -- --quiet # v4 compile gates — parallel with ci_integration. Standalone `v4` jobs hit a ~5m Ubicloud # shutdown mid-emit; per-job budgets keep one runner lifecycle per concern. The `v4` job is a # receipt-only stub so required check names stay stable. MVP-1 + v4 bootstrap share the @@ -307,13 +313,26 @@ jobs: V4_M1_RUST_EMIT_OUT: ${{ runner.temp }}/v4-rust-emit V4_M1_CARGO_CHECK_JOBS: "4" run: bash scripts/v4-m1-rust-emit-probe.sh + # Fixture-scoped gate: full rung gate only for fixture/transport or gate *execution* + # edits; scope-detector / if-routing narrowing uses policy_check (Gate #103 ratchet). + - name: Detect phase1/nat_semiring fixture scope (PR diff) + id: phase1_nat_semiring_fixture_scope + if: needs.affected.outputs.v4 == 'true' || needs.affected.outputs.workflow_policy == 'true' + run: bash scripts/detect-phase1-nat-semiring-gate-scope.sh "${{ github.event_name }}" "$GITHUB_OUTPUT" + - name: phase1/nat_semiring gate policy ratchet (workflow-policy edits) + if: steps.phase1_nat_semiring_fixture_scope.outputs.policy_check == 'true' + run: | + set -euo pipefail + bash scripts/check-workflow-path-regex-inventory.sh + bash scripts/detect-phase1-nat-semiring-gate-scope.sh "${{ github.event_name }}" "${RUNNER_TEMP}/phase1-gate-scope-smoke.out" + grep -q '^should_run=' "${RUNNER_TEMP}/phase1-gate-scope-smoke.out" # Phase 1 rung gate setup: provision Go on the self-hosted runner. The gate # invokes `go build` for R0-go-parse / R2-go-compile; without this step the # script's host-toolchain guard would fail-closed with # phase1/nat_semiring/setup/host_toolchain_missing (setup gap, not fixture # gap). Python3 is pre-installed on srv1/srv2. setup-go@v5 is cached. - name: Setup Go (phase1/nat_semiring rung gate prerequisite) - if: needs.affected.outputs.v4 == 'true' || needs.affected.outputs.workflow_policy == 'true' + if: steps.phase1_nat_semiring_fixture_scope.outputs.should_run == 'true' uses: actions/setup-go@v5 with: go-version: 'stable' @@ -325,7 +344,7 @@ jobs: # V4_PHASE1_NAT_SEMIRING_STRICT=1 still logs fail-closed rung receipts (#3955 §6); rust rung # not rustc-clean on main until emit substrate lands — workflow continue-on-error interim. - name: phase1/nat_semiring rungs 0-2 gate (dag rust python go) - if: needs.affected.outputs.v4 == 'true' || needs.affected.outputs.workflow_policy == 'true' + if: steps.phase1_nat_semiring_fixture_scope.outputs.should_run == 'true' timeout-minutes: 20 continue-on-error: true env: @@ -339,7 +358,7 @@ jobs: timeout-minutes: 35 continue-on-error: true env: - V4_BOOTSTRAP_TIMEOUT_SECS: 480 + V4_BOOTSTRAP_TIMEOUT_SECS: '480' run: | set +euo pipefail bash scripts/v4-bootstrap-viability.sh @@ -370,8 +389,9 @@ jobs: exit 1 - name: 'T-22 TestClaim corpus structural bridge — manual .dag corpus' if: needs.affected.outputs.v4 == 'true' || needs.affected.outputs.workflow_policy == 'true' + timeout-minutes: 15 env: - V4_TESTCLAIM_TIMEOUT_SECS: 480 + V4_TESTCLAIM_TIMEOUT_SECS: '480' run: bash scripts/v4-testclaim-corpus-gate.sh # Branch protection requires the `ci` check name (docs/admin/branch-protection-recommendation- # 2026-05-09.md). This job is the fail-closed aggregator over discipline + parallel lanes; diff --git a/_internal/INVARIANTS_OPS.md b/_internal/INVARIANTS_OPS.md index 213b627443f..0c8bf2f13bb 100644 --- a/_internal/INVARIANTS_OPS.md +++ b/_internal/INVARIANTS_OPS.md @@ -46,6 +46,7 @@ Per **Dispatch-Discipline Mechanisms (b)** above, each **new** path added to `EX | `src/v3/compiler/tests/integration/v4_workflow_release_dag_smoke_test.rs` | **RELEASE_TODO.md** §5 Phase 1a (`src/v4/workflow/release.dag` — tag `v*` trigger, six-target matrix [musl linux x2, darwin x2, windows msvc x2], musl `cross` + native darwin/windows builds, `release_published_target_triples` + `release_published_artifact_names` with `.exe` on windows rows, GH Release upload of matrix `artifact_basename` assets only; hand-synced `.github/workflows/release.yml`). Install (`install.sh`, target detection) deferred to Phase 1b (`install.dag`). **ROADMAP:** `_internal/ROADMAP_OPS.md` § **Nine lanes** row **T-PB-B** / `pb_rust_tests_outside_residual_zero`. **PR receipt (P5 Mechanism (b)):** this INVARIANTS row + matching `EXPECTED_HAND_AUTHORED_TEST` line in `sg0_census_test.rs` + `scripts/ci-merge/sg0-pr-body-append.3859.txt` land in the same PR as the smoke harness. **Dissolution:** remove when `release_pipeline` YamlStatic emits `release.yml` and generated harness exercises release facts without this parse probe. **Interim ratchet:** `v4_workflow_release_dag_tokenizes_and_parses`; `v4_workflow_release_semantics_modeled`; `v4_workflow_release_modeled_and_bound_to_release_yml`; `v4_workflow_release_published_authority_single_writer` — tokenize+parse + release.yml binding + published triple/artifact basename parity across `release.dag` and `release.yml` (reads `release.dag`, `release.yml`, `src/v2/stage0/Cargo.toml` only). | | `src/v3/compiler/tests/integration/v4_test_bootstrap_infra_closeout_test.rs` | **ROADMAP:** `_internal/ROADMAP_OPS.md` § **Nine lanes** row **T-PB-B** / `pb_rust_tests_outside_residual_zero`; **TASKS.md** **T-19** (`src/v4/lens/testgen.dag`) + **T-20** (`src/v4/workflow/bootstrap.dag`) + **T-22** (`src/v4/compiler/05_eval.dag` DiagnosticAssert execution / `eval_rejected_assert_kind_deferred` dissolution; witnesses in `src/v4/test/claim/manual/diagnostic_assert_eval.dag`). **PR receipt (P5 Mechanism (b)):** this INVARIANTS row + matching `EXPECTED_HAND_AUTHORED_TEST` line in `sg0_census_test.rs` land in the same PR as the closeout ratchet; T-22 expansion in its PR updates this row; T-19 AlgebraLaw Nat corpus expansion (this PR) further updates this row (same path — no new census line); T-19 deferral lane: TASKS.md §T-19 `algebra_law_conformance.dag` corpus, _internal/ROADMAP_OPS.md § Nine lanes row T-PB-B. **Dissolution:** remove when the T-19/T-20/T-22 closeout checks are expressed as `.dag` `TestClaim` rows or generated harness coverage without this host parse-surface ratchet. **Interim ratchet:** `testgen_concept_surface_stays_closed_and_classified` checks the closed testgen scheduling arms and the `Generator` claim kind / anchor / classification / slot field set; `language_behavior_equivalence_generated_claims_parse` / `language_behavior_equivalence_run_test_claim_receipts_present` pin the LBE generator slice; `idempotent_operation_generated_claims_parse_and_pin_emission` pins the idempotent-operation generator slice (`src/v4/std/effects.dag` canonical `IdempotentShape`/`EffectShape` witnesses + `idempotent_operation_witness_node`; outside the six-way `TestgenConcept` coproduct; label-only skip); `manual_manifest_matches_claim_anchor_discriminants` checks manual claim anchors join to the manifest by `ManualAnchorKey`; `claim_corpus_has_no_direct_manual_anchor_assignments` scans `src/v4/test/claim/**/*.dag` so `TestClaim.anchor` literals cannot bypass `manual_claim_anchor(...)` after the `ClaimAnchorKey` split; `coproduct_exhaustiveness_generated_claim_parse_and_witnesses_present` checks the generated coproduct-exhaustiveness corpus parses, derives the invalid `Node` and generated claim anchor from one `GeneratedCoproductExhaustiveness` source, uses canonical `node_locus`, and schedules the generated `DiagnosticExhaustiveness` claim under `GeneratedClaimAnchor`; `t20_bootstrap_plan_keeps_self_hosting_chain_as_data` checks the seed/self0/self1/fixpt bootstrap chain is encoded as `CompileStage` / `BootstrapPlan` data; `t22_diagnostic_assert_eval_witnesses_parse` checks `diagnostic_assert_eval.dag` parses; `t22_eval_diagnostic_assert_not_deferred_in_substrate` checks `05_eval.dag` no longer contains `eval_rejected_assert_kind_deferred`, executes `DiagnosticAssert`, and routes `run_test_claim` through `aggregate_verdicts`; `t19_algebra_law_generated_claims_parse_and_use_testgen_emit` checks `algebra_law_conformance.dag` parses and asserts the testgen emit helpers + tautological-sides guard in `lens/testgen.dag`. | | `src/v3/compiler/tests/integration/coverage_defect_acceptance_dag_test.rs` | **Coverage-defect acceptance keys:** `src/v4/lens/coverage.dag` carries the canonical coverage-key set for `docs/design-dissolution-lens.md` §5.1; the old emit-template key is retired into `TemplateHole`, and the old string-escape key is split into `TemplateHole` plus `CanonicalCarrier`. **ROADMAP:** `_internal/ROADMAP_OPS.md` § **Nine lanes** row **T-PB-B** / `pb_rust_tests_outside_residual_zero`. **PR receipt (P5 Mechanism (b)):** this INVARIANTS row + matching `EXPECTED_HAND_AUTHORED_TEST` line in `sg0_census_test.rs` land in the same PR as the parse-level ratchet. **Dissolution:** remove when the v4 coverage lens runs as `.dag` / generated coverage and can assert the same acceptance rows without this host parser check. **Interim ratchet:** `coverage_defect_acceptance_keys_match_declared_rows` tokenizes/parses `src/v4/lens/coverage.dag` and asserts the exact parsed `(coverage_defect_* data row, CoverageDefectKey variant)` set matches the expected acceptance-key table while rejecting retired emit-template / string-escape names. | +| `src/v3/compiler/tests/boundary/v4_leaf_model_rust_r1_rustc_test.rs` | **Phase 1 leaf-model verification** (`docs/planning/v4-leaf-model-verification-2026-05-30.md` §7 R1): boundary `rustc` exercise for `src/v4/lens/leaf_model_verification.dag` happy + falsification fixtures; interim host runner `scripts/v4-leaf-model-rust-r1-verify.sh`. **ROADMAP:** `_internal/ROADMAP_OPS.md` § **Nine lanes** row **T-PB-B** / `pb_rust_tests_outside_residual_zero`; **TASKS.md** T-22/T-38 (Runtime/TestClaim verdict surface). **PR receipt (P5 Mechanism (b)):** this INVARIANTS row + matching `EXPECTED_HAND_AUTHORED_TEST` line in `sg0_census_test.rs` land in the same PR as the harness. **Dissolution:** delete when modeled `run_target_verification` exercises `src/v4/test/claim/language_model/rust_r1.dag` without this hand-Rust bridge. **Interim ratchet:** `v4_leaf_model_rust_r1_fixture_strings_match_dag_authority`, `v4_leaf_model_rust_r1_happy_fixture_rustc_accepts`, `v4_leaf_model_rust_r1_falsification_fixture_rustc_e0308`. | | `src/v3/compiler/tests/integration/v4_bin_main_dag_smoke_test.rs` | **T-15** (`src/v4/bin/main.dag` — trampoline **`String`** authority + B1 digest **placeholder** `Node`s; closed-tree invariant #2 / pure-bootstrap zero-floor per `docs/design-pure-bootstrap-zero.md`). **Grounded-indicator authoring on `main.dag` is HOLD** pending hub-relayed canonical spec (operator-direct format under-spec; pending canonical spec). **ROADMAP:** `_internal/ROADMAP_OPS.md` § **Nine lanes** row **T-PB-B** / `pb_rust_tests_outside_residual_zero`. **PR receipt (P5 Mechanism (b)):** this INVARIANTS row + matching `EXPECTED_HAND_AUTHORED_TEST` line in `sg0_census_test.rs` land in the same PR as the smoke harness. **Dissolution:** remove when `main.dag` is exercised only by `.dag` `TestClaim` rows / a generated harness without this per-file Rust probe. **Interim ratchet:** `v4_bin_main_dag_tokenizes_and_parses_with_trampoline_source_anchor` runs `tokenize_for_test` + `parse_for_test` on the pinned `include_str!` source and asserts the trampoline / stub `data` identifiers plus the escaped `include!` spelling remain present in source text (full `compile_to_dag` on `main.dag` alone is deferred: `import v4.std.node` is not linked in the single-file harness). | | `src/v3/compiler/tests/integration/v4_t15_self_host_fixed_point_harness_test.rs` | **T-15** (`src/v4/TASKS.md` §T-15 — `bin/main.dag` trampoline authority + bootstrap `FixptStage1Stage2` stage1==stage2 wiring, **not** stage0==stage1; `claim_t15_self_host_fixed_point.dag` EqualsClaim over digest operand placeholders; optional v2 `gunbc compile` with `main.dag` entry root when `target/release/gunbc` exists). **ROADMAP:** `_internal/ROADMAP_OPS.md` § **Nine lanes** row **T-PB-B** / `pb_rust_tests_outside_residual_zero`. **PR receipt (P5 Mechanism (b)):** this INVARIANTS row + matching `EXPECTED_HAND_AUTHORED_TEST` line in `sg0_census_test.rs` land in the same PR as the harness + `claim_t15_self_host_fixed_point.dag`. **Dissolution:** remove when B1 merkle `content_hash` pins + T-22 eval execute the Equals probe and bootstrap fixpt without host structural receipts. **Interim ratchet:** `t_15_self_host_fixed_point` (TASKS.md CI gate name) tokenize/parse `main.dag`, `bootstrap.dag`, `self_host.dag`, and the T-15 claim; assert trampoline + fixpt stage1/stage2 digest convergence strings in `bootstrap_plan_well_formed`; assert `self_host_fixed_point_validate` stays fail-closed; optional v2 entry-root compile receipt. | | `src/v3/compiler/tests/integration/v4_compiler_emit_translate_smoke_test.rs` | **TASKS.md** T-10 / Wave-3-B (`src/v4/compiler/06_translate.dag` — `fold_node` translate + `coercion_fold` wrapper, `TargetSelectionPolicy` from target-model bundle; `src/v4/compiler/05_emit.dag` — `serialize_target ∘ translate`, grammar-as-bidir serialize via bundle `emitted`/`source` keys; `src/v4/test/claim/manual/mvp1_rust_add_translate.dag` structural TestClaim anchors). **ROADMAP:** `_internal/ROADMAP_OPS.md` § **Nine lanes** row **T-PB-B** / `pb_rust_tests_outside_residual_zero`. **PR receipt (P5 Mechanism (b)):** this INVARIANTS row + matching `EXPECTED_HAND_AUTHORED_TEST` line in `sg0_census_test.rs` land in the same PR as the smoke harness. **This PR (+0 paths):** replaces fixed `translate_default_serialize_fuel` with structural `Outcome` serialize measures in `06_translate.dag`; expands the existing harness (no new census path) to ratchet parsed-surface declarations for `target_translation_rules_budget`, `translate_serialize_measure`, `target_serialize_source_from_model`, `bind_outcome` import, and absence of `translate_default_serialize_fuel` data — semantic fail-closed behavior is exercised by `run_mvp1_serialize_rejects_missing_translation_rules` in `mvp1_rust_add_translate.dag` (not host `str::contains` probes). **PR #3778 same-path expansion (+0 SG-0 paths):** adds `v4_wasm_wat_lex_boundary_uses_trivia_and_numeric_literal_authority` to pin the T-4.17 WAT lex/grammar dissolution receipt: stale whitespace-bearing wasm fixture tokens stay deleted, atomic keyword/trivia/numeric-literal authorities are present, and typed numeric-literal grammar productions exist for `i32`/`i64`/`f32`/`f64` const operands. **This PR same-path expansion (+0 SG-0 paths):** adds `v4_python_language_model_declares_wave2b_algebra_inhabitance` to pin T-4.17 Python Wave 2b type-deepening: `python.dag` consumes `AlgebraInhabitanceDecl` plus grounded `std.algebra` Node constructors (`ordered_ring_node`, `approximate_field_node`, `boolean_algebra_node`) and declares int/float/bool witness + inhabitance rows feeding `python_model_core_wave1`; the ratchet also asserts zero complex/singleton algebra witness/inhabitance helper declarations, so complex and singleton facts remain mechanically outside faithful algebra inhabitance until the relevant carrier exists. The Python T-11 grammar ratchet now additionally requires canonical `FormalProduction` with a flat formal-symbol RHS, requires the shared `std.grammar` `formal_production_to_node` projection, rejects legacy `GrammarExpr`/`Sequence`/`Terminal` imports in `python.dag`, and asserts zero Python-owned formal-production projection helpers. **This PR same-path expansion (+0 SG-0 paths):** adds `v4_wasm_language_model_declares_wave2b_algebra_inhabitance` to pin T-4.17 Wasm Wave 2b type-deepening: `wasm.dag` consumes `AlgebraInhabitanceDecl` plus grounded `std.algebra` type-node constructors (`commutative_semiring_type_node`, `approximate_field_type_node`) and declares integer/float witness + inhabitance rows feeding `wasm_model_core_wave2b`; the ratchet pins wave-2b entrypoints without adding a new SG-0 census path. **PR #3840 same-path expansion (+0 SG-0 paths):** adds `v4_mvp1_python_add_claim_tokenizes_and_parses`, `v4_mvp1_go_add_claim_tokenizes_and_parses`, `v4_mvp1_cpp_add_claim_tokenizes_and_parses`, `v4_mvp1_typescript_add_claim_tokenizes_and_parses`, and `v4_mvp1_shape_a_add_claims_import_compile_inferred` to ratchet T-11 grammar-inverse compile-inferred TestClaim parse/import receipts for python/go/cpp/typescript Shape-A MVP-1 add-fn fixtures (`mvp1_*_add_translate.dag`); dissolves `feature:T-11-grammar-inverse-serializer-remaining-targets` status mark in `06_translate.dag`. This is explicitly deferred under **ROADMAP** § **Nine lanes** row **T-PB-B** / `pb_rust_tests_outside_residual_zero`; dissolve these same-path Rust ratchets when the language boundary facts are asserted by `.dag` `TestClaim` rows, T-22 execution, or a generated harness instead of host `SurfaceExpr` traversal. Prior T-11 ratchet rows remain: `v4_emit_dag_tokenizes_and_parses`, `v4_emit_dag_module_path_is_compiler_emit`, `v4_emit_dag_imports_translate_stage`, `v4_emit_dag_declares_emit_entrypoint`, `v4_emit_dag_does_not_import_find_witness`, `v4_mvp1_rust_add_claim_imports_translate_and_emit`, `v4_translate_dag_dispatches_token_sequence_items`, and the language-model T-11 rows. **Dissolution:** remove when translate/emit/MVP-1 surfaces are exercised only by `.dag` `TestClaim` rows / a generated harness without this per-file Rust probe (full `compile_to_dag` over v4 compiler modules deferred until multi-module load). | diff --git a/scripts/ci-merge/sg0-pr-body-append.3972.txt b/scripts/ci-merge/sg0-pr-body-append.3972.txt new file mode 100644 index 00000000000..58641d6ce0e --- /dev/null +++ b/scripts/ci-merge/sg0-pr-body-append.3972.txt @@ -0,0 +1,3 @@ +SG-0 hand-path delta: +1 + +SG-0 pairing: (c) Net +1 on `EXPECTED_HAND_AUTHORED_TEST` for `v4_leaf_model_rust_r1_rustc_test.rs` (INVARIANTS §P5(b) Phase 1 leaf-model R1 boundary `rustc` ratchet per `docs/planning/v4-leaf-model-verification-2026-05-30.md` §7; pairs with `scripts/v4-leaf-model-rust-r1-verify.sh`). Follow-up dispatch: retire when T-22 modeled `run_target_verification` exercises `src/v4/test/claim/language_model/rust_r1.dag` without this hand-Rust bridge — gunb-ai/gunbc#3972 / T-PB-B `pb_rust_tests_outside_residual_zero` in `_internal/ROADMAP_OPS.md`. diff --git a/scripts/detect-phase1-nat-semiring-gate-scope.sh b/scripts/detect-phase1-nat-semiring-gate-scope.sh new file mode 100755 index 00000000000..36c5fe0b514 --- /dev/null +++ b/scripts/detect-phase1-nat-semiring-gate-scope.sh @@ -0,0 +1,60 @@ +#!/usr/bin/env bash +# scripts/detect-phase1-nat-semiring-gate-scope.sh +# +# Host transport for phase1/nat_semiring rung gate CI gating (Gate #103: git diff +# selection must not live in .github/workflows/*.yml — see +# scripts/workflow-path-regex-forbidden-substrings.txt). +# +# Emits to GITHUB_OUTPUT (or the given file): +# should_run=true|false — run the full fixture-scoped rung gate (emit + rustc/…) +# policy_check=true|false — run the lightweight workflow-policy ratchet only +# +# Full gate: fixture paths, or workflow edits to gate *execution* (script invoke, +# STRICT env, modeled ci.dag rung signal). Scope-detector / if-routing narrowing +# alone triggers policy_check (Gate #103 inventory + detector smoke), not the +# substrate-red rung gate (ladder §6 appendix). +# +# Usage: +# detect-phase1-nat-semiring-gate-scope.sh + +set -euo pipefail + +root="$(git rev-parse --show-toplevel 2>/dev/null || pwd)" +cd "$root" + +event_name="${1:-pull_request}" +output_file="${2:-}" + +if [[ -z "$output_file" ]]; then + echo "usage: detect-phase1-nat-semiring-gate-scope.sh " >&2 + exit 2 +fi + +range="origin/main...HEAD" +if [[ "$event_name" == "push" && "${GITHUB_REF:-}" == "refs/heads/main" ]]; then + range="HEAD~1..HEAD" +fi + +should_run=false +policy_check=false + +if git diff --name-only "$range" | grep -qE '^(src/v4/test/claim/(algebra_laws/nat_semiring|nat_semiring/)|scripts/v4-phase1-nat-semiring-rung-gate\.sh)'; then + should_run=true +fi + +workflow_paths='^(\.github/workflows/ci\.yml|src/v4/workflow/ci\.dag|dsl/gunbc/ci_github_actions_workflow\.dag|scripts/detect-phase1-nat-semiring-gate-scope\.sh)' +if git diff --name-only "$range" | grep -qE "$workflow_paths"; then + policy_check=true + if [[ "$should_run" != true ]]; then + if git diff "$range" -- .github/workflows/ci.yml src/v4/workflow/ci.dag dsl/gunbc/ci_github_actions_workflow.dag 2>/dev/null \ + | grep '^[-+]' | grep -v '^[-+][[:space:]]*#' \ + | grep -qE 'v4-phase1-nat-semiring-rung-gate\.sh|V4_PHASE1_NAT_SEMIRING_STRICT|phase1_nat_semiring_rung_gate'; then + should_run=true + fi + fi +fi + +{ + echo "should_run=${should_run}" + echo "policy_check=${policy_check}" +} >>"$output_file" diff --git a/scripts/v4-bootstrap-viability.sh b/scripts/v4-bootstrap-viability.sh index 8f145fef112..32867493b44 100755 --- a/scripts/v4-bootstrap-viability.sh +++ b/scripts/v4-bootstrap-viability.sh @@ -25,7 +25,8 @@ mkdir -p "$out" compile_timeout="${V4_BOOTSTRAP_TIMEOUT_SECS:-}" if [[ -n "${GITHUB_ACTIONS:-}" && -z "$compile_timeout" ]]; then - compile_timeout=180 + # 480s: full src/v4 --target dag on loaded self-hosted runners (exit 143 at lower caps). + compile_timeout=480 fi set +e diff --git a/scripts/v4-leaf-model-rust-r1-verify.sh b/scripts/v4-leaf-model-rust-r1-verify.sh new file mode 100755 index 00000000000..db27d79e940 --- /dev/null +++ b/scripts/v4-leaf-model-rust-r1-verify.sh @@ -0,0 +1,170 @@ +#!/usr/bin/env bash +# scripts/v4-leaf-model-rust-r1-verify.sh +# +# Phase 1 leaf-model verification host runner — rust.dag R1 (i32 surface spelling). +# Authority: src/v4/lens/leaf_model_verification.dag (fixture sources) + +# src/v4/test/claim/language_model/rust_r1.dag (claim + receipt shape). +# +# Exercises rustc on happy + falsification fixtures; emits JSON receipt. +# Falsification probe expects E0308 (type mismatch) per +# docs/planning/v4-leaf-model-verification-2026-05-30.md §7. +# +# Dissolve-on-arrival: delete when T-22 modeled `run_target_verification` owns rustc +# invocation and structured TestClaimRun verdicts replace this host bridge (same +# trigger as src/v3/compiler/tests/boundary/v4_leaf_model_rust_r1_rustc_test.rs). + +set -euo pipefail + +root="$(git rev-parse --show-toplevel 2>/dev/null || pwd)" +cd "$root" + +fixture_dag="src/v4/lens/leaf_model_verification.dag" +if [[ ! -f "$fixture_dag" ]]; then + echo "error: missing fixture authority at $fixture_dag" >&2 + exit 1 +fi + +if ! command -v rustc >/dev/null 2>&1; then + echo "error: rustc not on PATH — install a Rust toolchain to run leaf-model R1 verification" >&2 + exit 1 +fi + +eval "$(python3 - "$fixture_dag" <<'PY' +from __future__ import annotations + +import re +import shlex +import sys +from pathlib import Path + +path = Path(sys.argv[1]) +text = path.read_text() + +def extract(name: str) -> str: + pattern = rf'^data {name}: String = "(.*)"\s*$' + for line in text.splitlines(): + m = re.match(pattern, line) + if m: + return bytes(m.group(1), "utf-8").decode("unicode_escape") + raise SystemExit(f"error: {path}: missing data {name}: String = ...") + +happy = extract("rust_r1_happy_fixture_source") +falsification = extract("rust_r1_falsification_fixture_source") +print(f"happy_source={shlex.quote(happy)}") +print(f"falsification_source={shlex.quote(falsification)}") +PY +)" + +run_suffix="${GITHUB_RUN_ID:-local}-${GITHUB_RUN_ATTEMPT:-$$}" +tmp_root="${RUNNER_TEMP:-/tmp}" +scratch="${tmp_root}/v4-leaf-model-rust-r1-${run_suffix}" +rm -rf "$scratch" +mkdir -p "$scratch" + +compile_rust_lib() { + local label="$1" + local source="$2" + local src_path="${scratch}/${label}.rs" + local stderr_path="${scratch}/${label}.stderr" + printf '%s' "$source" >"$src_path" + set +e + env -u RUSTC_BOOTSTRAP rustc \ + --edition=2021 \ + --crate-type lib \ + "$src_path" \ + -o "${scratch}/${label}.rlib" \ + 2>"$stderr_path" + local status=$? + set -e + echo "$status" >"${scratch}/${label}.exit" + cat "$stderr_path" +} + +echo "=== leaf-model R1: rustc happy fixture (rust.dag i32 surface spelling) ===" +happy_stderr="$(compile_rust_lib happy "$happy_source")" +happy_status="$(cat "${scratch}/happy.exit")" + +echo "=== leaf-model R1: rustc falsification fixture (E0308 probe) ===" +falsification_stderr="$(compile_rust_lib falsification "$falsification_source")" +falsification_status="$(cat "${scratch}/falsification.exit")" + +happy_pass=false +falsification_pass=false +if [[ "$happy_status" -eq 0 ]]; then + happy_pass=true +fi +if [[ "$falsification_status" -ne 0 ]] && grep -qE 'E0308' <<<"$falsification_stderr"; then + falsification_pass=true +fi + +proven=false +if [[ "$happy_pass" == true && "$falsification_pass" == true ]]; then + proven=true +fi + +export V4_R1_HAPPY_STATUS="$happy_status" +export V4_R1_FALSIFICATION_STATUS="$falsification_status" +export V4_R1_HAPPY_PASS="$happy_pass" +export V4_R1_FALSIFICATION_PASS="$falsification_pass" +export V4_R1_PROVEN="$proven" +export V4_R1_FALSIFICATION_STDERR="$falsification_stderr" + +python3 - <<'PY' +import json +import os +import re + +stderr = os.environ.get("V4_R1_FALSIFICATION_STDERR", "") +print( + json.dumps( + { + "schema": "scripts/v4-leaf-model-rust-r1-verify.sh::host_receipt_v1", + "claim_id": "RustR1I32SurfaceSpelling", + "happy": { + "rustc_exit": int(os.environ["V4_R1_HAPPY_STATUS"]), + "verdict": "Pass" + if os.environ["V4_R1_HAPPY_PASS"] == "true" + else "Fail", + }, + "falsification": { + "rustc_exit": int(os.environ["V4_R1_FALSIFICATION_STATUS"]), + "expected_diagnostic": "E0308", + "e0308_observed": bool(re.search(r"E0308", stderr)), + "verdict": "Pass" + if os.environ["V4_R1_FALSIFICATION_PASS"] == "true" + else "Fail", + }, + "proven": os.environ["V4_R1_PROVEN"] == "true", + }, + indent=2, + ) +) +PY + +if [[ "$proven" != true ]]; then + echo "error: leaf-model R1 verification failed (happy_pass=${happy_pass} falsification_pass=${falsification_pass})" >&2 + if [[ "$happy_pass" != true ]]; then + echo "--- happy rustc stderr ---" >&2 + printf '%s\n' "$happy_stderr" >&2 + fi + if [[ "$falsification_pass" != true ]]; then + echo "--- falsification rustc stderr ---" >&2 + printf '%s\n' "$falsification_stderr" >&2 + fi + exit 1 +fi + +if [[ -n "${GITHUB_STEP_SUMMARY:-}" ]]; then + { + echo "### Leaf-model verification — rust.dag R1 (i32 surface spelling)" + echo "" + echo "| path | verdict |" + echo "| --- | --- |" + echo "| happy \`pub fn r1_test() -> i32 { 0i32 }\` | Pass (rustc clean) |" + echo "| falsification \`... { \"string\" }\` | Pass (rustc E0308) |" + echo "" + echo "_Authority: \`${fixture_dag}\` + \`src/v4/test/claim/language_model/rust_r1.dag\`_" + } >> "$GITHUB_STEP_SUMMARY" +fi + +echo "leaf-model R1 verification PROVEN: happy compiles; falsification rejected with E0308" diff --git a/scripts/v4-testclaim-corpus-gate.sh b/scripts/v4-testclaim-corpus-gate.sh index f75b26ed42b..0cf56193131 100755 --- a/scripts/v4-testclaim-corpus-gate.sh +++ b/scripts/v4-testclaim-corpus-gate.sh @@ -64,6 +64,7 @@ mkdir -p "$out" "$rust_out" "$(dirname "$log")" "$(dirname "$rust_log")" compile_timeout="${V4_TESTCLAIM_TIMEOUT_SECS:-}" if [[ -n "${GITHUB_ACTIONS:-}" && -z "$compile_timeout" ]]; then + # 480s: full src/v4 --target rust on loaded self-hosted runners (exit 143 at lower caps). compile_timeout=480 fi diff --git a/src/v3/compiler/tests/boundary/v4_leaf_model_rust_r1_rustc_test.rs b/src/v3/compiler/tests/boundary/v4_leaf_model_rust_r1_rustc_test.rs new file mode 100644 index 00000000000..9faa1d79405 --- /dev/null +++ b/src/v3/compiler/tests/boundary/v4_leaf_model_rust_r1_rustc_test.rs @@ -0,0 +1,112 @@ +//! **Layer:** boundary (TESTING.md § test layers — rustc target exercise for v4 leaf-model R1). +//! +//! Phase 1: rust.dag claim R1 (i32 surface spelling) — fixture authority in +//! `src/v4/lens/leaf_model_verification.dag`; host runner +//! `scripts/v4-leaf-model-rust-r1-verify.sh`. +//! +//! **P5 receipt:** matching `_internal/INVARIANTS_OPS.md` row + +//! `EXPECTED_HAND_AUTHORED_TEST` literal in `sg0_census_test.rs` (same PR). +//! **Dissolution:** retire when T-22 eval + modeled `run_target_verification` owns +//! rustc invocation without this hand-Rust bridge. + +use std::io::Write; +use std::process::Command; + +use crate::common::RustcHarness; + +const FIXTURE_DAG: &str = include_str!("../../../../v4/lens/leaf_model_verification.dag"); +const CLAIM_DAG: &str = include_str!("../../../../v4/test/claim/language_model/rust_r1.dag"); + +const HAPPY_FIXTURE: &str = "pub fn r1_test() -> i32 { 0i32 }\n"; +const FALSIFICATION_FIXTURE: &str = "pub fn r1_test() -> i32 { \"string\" }\n"; + +fn unescape_dag_string_literal(body: &str) -> String { + let mut out = String::new(); + let mut chars = body.chars(); + while let Some(c) = chars.next() { + if c == '\\' { + match chars.next() { + Some('n') => out.push('\n'), + Some('"') => out.push('"'), + Some('\\') => out.push('\\'), + Some(other) => { + out.push('\\'); + out.push(other); + } + None => out.push('\\'), + } + } else { + out.push(c); + } + } + out +} + +fn extract_fixture_source(dag_text: &str, data_name: &str) -> Option { + let needle = format!("data {data_name}: String = \""); + let line = dag_text.lines().find(|l| l.starts_with(&needle))?; + let rest = line.strip_prefix(&needle)?.strip_suffix('"')?; + Some(unescape_dag_string_literal(rest)) +} + +fn compile_lib(harness: &RustcHarness, label: &str, source: &str) -> (bool, String) { + let tmp_dir = harness.next_child_dir(); + let src_path = tmp_dir.join(format!("{label}.rs")); + let out_path = tmp_dir.join(format!("{label}.rlib")); + std::fs::File::create(&src_path) + .and_then(|mut f| f.write_all(source.as_bytes())) + .expect("write fixture source"); + + let output = Command::new("rustc") + .env_remove("RUSTC_BOOTSTRAP") + .arg("--edition=2021") + .arg("--crate-type") + .arg("lib") + .arg(&src_path) + .arg("-o") + .arg(&out_path) + .output() + .expect("invoke rustc — install a rust toolchain to run this test"); + + let stderr = String::from_utf8_lossy(&output.stderr).into_owned(); + (output.status.success(), stderr) +} + +#[test] +fn v4_leaf_model_rust_r1_fixture_strings_match_dag_authority() { + let happy = extract_fixture_source(FIXTURE_DAG, "rust_r1_happy_fixture_source") + .expect("rust_r1_happy_fixture_source in lens/leaf_model_verification.dag"); + let falsification = extract_fixture_source(FIXTURE_DAG, "rust_r1_falsification_fixture_source") + .expect("rust_r1_falsification_fixture_source in lens/leaf_model_verification.dag"); + assert_eq!(happy, HAPPY_FIXTURE); + assert_eq!(falsification, FALSIFICATION_FIXTURE); + assert!( + CLAIM_DAG.contains("rust_r1_happy_fixture_source") + && CLAIM_DAG.contains("rust_surface_spelling_i32"), + "claim module must reference fixture + fact anchors" + ); +} + +#[test] +fn v4_leaf_model_rust_r1_happy_fixture_rustc_accepts() { + let harness = RustcHarness::new("v4_leaf_model_rust_r1"); + let (ok, stderr) = compile_lib(&harness, "happy", HAPPY_FIXTURE); + assert!( + ok, + "rustc should accept R1 happy fixture; stderr:\n{stderr}" + ); +} + +#[test] +fn v4_leaf_model_rust_r1_falsification_fixture_rustc_e0308() { + let harness = RustcHarness::new("v4_leaf_model_rust_r1"); + let (ok, stderr) = compile_lib(&harness, "falsification", FALSIFICATION_FIXTURE); + assert!( + !ok, + "falsification fixture must not compile (type mismatch probe)" + ); + assert!( + stderr.contains("E0308"), + "expected rustc E0308 type mismatch; stderr:\n{stderr}" + ); +} diff --git a/src/v3/compiler/tests/integration.rs b/src/v3/compiler/tests/integration.rs index 3fcf9ed7f04..3a93cd94479 100644 --- a/src/v3/compiler/tests/integration.rs +++ b/src/v3/compiler/tests/integration.rs @@ -297,6 +297,8 @@ mod v4_extdeps_file_system_dag_smoke_test; mod v4_extdeps_formatters_black_dag_smoke_test; #[path = "integration/v4_extdeps_react_dag_smoke_test.rs"] mod v4_extdeps_react_dag_smoke_test; +#[path = "boundary/v4_leaf_model_rust_r1_rustc_test.rs"] +mod v4_leaf_model_rust_r1_rustc_test; #[path = "integration/v4_lens_affected_set_dag_smoke_test.rs"] mod v4_lens_affected_set_dag_smoke_test; #[path = "integration/v4_lens_application_dag_smoke_test.rs"] diff --git a/src/v3/compiler/tests/integration/sg0_census_test.rs b/src/v3/compiler/tests/integration/sg0_census_test.rs index a52f9977fc5..20e1b56dc5f 100644 --- a/src/v3/compiler/tests/integration/sg0_census_test.rs +++ b/src/v3/compiler/tests/integration/sg0_census_test.rs @@ -392,6 +392,17 @@ const EXPECTED_HAND_AUTHORED_TEST: &[&str] = &[ "src/v3/compiler/tests/boundary/m1_4_emit_python_test.rs", "src/v3/compiler/tests/boundary/m1_5_emit_omni_demo_test.rs", "src/v3/compiler/tests/boundary/m2_emit_multi_field_struct_variant_test.rs", + // Phase 1 leaf-model verification R1 (`docs/planning/v4-leaf-model-verification-2026-05-30.md` §7): + // boundary rustc exercise for `src/v4/lens/leaf_model_verification.dag` fixtures until + // T-22 modeled `run_target_verification` owns target verdicts. + // + // **P5 receipt (INVARIANTS.md §P5 — SG-0 `EXPECTED_HAND_AUTHORED_TEST`):** explicit + // deferral to **ROADMAP.md** `### Nine lanes` row **T-PB-B** / + // `pb_rust_tests_outside_residual_zero` + **TASKS.md** T-22/T-38 (Runtime/TestClaim + // verdict surface; interim host runner `scripts/v4-leaf-model-rust-r1-verify.sh`). + // Dissolution: delete when modeled runner exercises + // `src/v4/test/claim/language_model/rust_r1.dag` without this hand-Rust bridge. + "src/v3/compiler/tests/boundary/v4_leaf_model_rust_r1_rustc_test.rs", "src/v3/compiler/tests/determinism_test.rs", "src/v3/compiler/tests/integration.rs", "src/v3/compiler/tests/integration/anthropic_messages_callable_test.rs", diff --git a/src/v4/lens/leaf_model_verification.dag b/src/v4/lens/leaf_model_verification.dag new file mode 100644 index 00000000000..c78965b9403 --- /dev/null +++ b/src/v4/lens/leaf_model_verification.dag @@ -0,0 +1,72 @@ +// src/v4/lens/leaf_model_verification.dag +// Scope: Layer B fixture generators for leaf-model verification (T-19 testgen extension, Phase 1 R1). +// Status: R1 happy + falsification rustc source fixtures for rust.dag i32 surface spelling. + +module v4.lens.leaf_model_verification + + +import v4.extdeps.languages.rust { + rust_coercion_field_i32_spelling, + rust_surface_spelling_i32 +} +import v4.std.leaf_model_verification { + LeafModelFixturePair, + LeafModelFalsificationCase, + LeafModelRustFixture, + leaf_model_claim_rust_r1_i32_surface_spelling, + leaf_model_rust_crate_type_lib, + TargetCompileAccepted, + TargetCompileRejected, + target_diagnostic_e0308_type_mismatch +} +import v4.std.node { Symbol } +import v4.std.text { String } + + +// Fact anchor: rust.dag declares surface spelling + coercion edge for i32. +data rust_r1_claim_surface_spelling_fact: Symbol = rust_surface_spelling_i32 +data rust_r1_claim_coercion_spelling_edge: Symbol = rust_coercion_field_i32_spelling + +// Fixture embeds the spelled type + literal suffix so rustc is the external authority. +data rust_r1_happy_fixture_source: String = "pub fn r1_test() -> i32 { 0i32 }\n" + +data rust_r1_falsification_fixture_source: String = "pub fn r1_test() -> i32 { \"string\" }\n" + + +fn rust_r1_happy_fixture() -> LeafModelRustFixture { + LeafModelRustFixture { + source: rust_r1_happy_fixture_source, + crate_type: leaf_model_rust_crate_type_lib + } +} + + +fn rust_r1_falsification_fixture() -> LeafModelRustFixture { + LeafModelRustFixture { + source: rust_r1_falsification_fixture_source, + crate_type: leaf_model_rust_crate_type_lib + } +} + + +fn rust_r1_fixture_pair() -> LeafModelFixturePair { + LeafModelFixturePair { + claim_id: leaf_model_claim_rust_r1_i32_surface_spelling, + surface_spelling_fact: rust_r1_claim_surface_spelling_fact, + coercion_spelling_fact: rust_r1_claim_coercion_spelling_edge, + happy: rust_r1_happy_fixture(), + expected_happy_verdict: TargetCompileAccepted, + falsification: LeafModelFalsificationCase { + fixture: rust_r1_falsification_fixture(), + expected_verdict: TargetCompileRejected { + diagnostic_code: target_diagnostic_e0308_type_mismatch + } + } + } +} + + +// Testgen port: `rust_r1_fixture` (docs/planning/v4-leaf-model-verification-2026-05-30.md §8). +fn rust_r1_fixture() -> LeafModelFixturePair { + rust_r1_fixture_pair() +} diff --git a/src/v4/std/leaf_model_verification.dag b/src/v4/std/leaf_model_verification.dag index 8ba703cccb0..07bed33d73c 100644 --- a/src/v4/std/leaf_model_verification.dag +++ b/src/v4/std/leaf_model_verification.dag @@ -3,6 +3,7 @@ // Status: Phase 1 substrate (docs/planning/v4-leaf-model-verification-2026-05-30.md §5). // Authority: leaf model owns FACTS (stable fact_id in extdeps); this module owns OBLIGA shape. // Co-authored with Modeling DFS (proud-pike-680) — consume Verdict from verdict.dag (PR #3961). +// R1 rustc slice: concrete fixture-pair + compile verdict carriers (PR #3972). module v4.std.leaf_model_verification @@ -10,7 +11,7 @@ import v4.std.collection { List } import v4.std.nat { Nat } import v4.std.node { Node, Symbol } import v4.std.text { String } -import v4.std.verdict { Verdict } +import v4.std.verdict { Verdict, verdict_combine } // Layer A boundary: OBLIGA rows reference model facts structurally (Node projection of declared bindings). type LeafModelClaim { @@ -22,7 +23,6 @@ type LeafModelClaim { } // REQUIRED paired probe — claim without falsification is not verifiable (planning doc §5). -// expected_failure_mode is Expectation-shaped per M=rust.dag instantiation (PR #3971 §5 sketches). type FalsificationCase { subject_variant: Subject expected_failure_mode: Expectation @@ -36,8 +36,8 @@ type TargetArtifact { } // 🟡 gated — feature:leaf-model-fixture-runner — bind TASKS.md T-19/T-22 follow-up — -// dissolve-on: TargetToolchain / TargetEdition / TargetBuildProfile / TargetOverflowDispositionField coproducts replace these Symbol scaffolds; forbidden: parallel invocation vocab outside this carrier. -// Edition, build profile, and OverflowDisposition field pin are independent coordinates (not a single edition_or_profile union). +// dissolve-on: TargetToolchain / TargetEdition / TargetBuildProfile / TargetOverflowDispositionField coproducts replace these Symbol scaffolds; +// forbidden: parallel invocation vocab outside this carrier. type TargetInvocation { toolchain: Symbol edition: Symbol @@ -60,7 +60,6 @@ type LeafModelClaimVerdictRow { falsification_verdict: Verdict } -// Populations are Nat so negative totals are unrepresentable (same discipline as verdict.dag VerdictTally). type LeafModelVerificationTotals { proven: Nat model_failed: Nat @@ -69,9 +68,74 @@ type LeafModelVerificationTotals { not_checked: Nat } -// Report rows are authoritative; LeafModelVerificationTotals is derived at runner emission only (not stored here). -// 🟡 gated — feature:leaf-model-verification-report — dissolve-on: runner returns (report, totals) where totals is a fold over report.claims with bucket classification; forbidden: parallel stored totals beside source rows. +// 🟡 gated — feature:leaf-model-verification-report — dissolve-on: runner fold over report.claims. type LeafModelVerificationReport { model: M claims: List } + +// --- PR #3972 R1 rustc compile slice (happy/falsification fixtures + boundary runner) --- + +// 🟢 coproduct dissolution — CP-LMV-TARGET-COMPILE-VERDICT-PHASE1 (Phase 1 R1 rustc gate; widen per target). +type TargetCompileVerdict + = TargetCompileAccepted + | TargetCompileRejected { diagnostic_code: Symbol } + +data target_diagnostic_e0308_type_mismatch: Symbol = target_diagnostic_e0308_type_mismatch + +type LeafModelClaimId = Symbol + +data leaf_model_claim_rust_r1_i32_surface_spelling: LeafModelClaimId = leaf_model_claim_rust_r1_i32_surface_spelling + +type LeafModelRustCrateType = Symbol + +data leaf_model_rust_crate_type_lib: LeafModelRustCrateType = leaf_model_rust_crate_type_lib + +// 🟡 gated — feature:leaf-model-r1-rustc-bridge — bind PR #3972 Phase 1 R1 — +// dissolve-on-arrival: fold into LeafModelFixture (TargetArtifact + TargetInvocation + Verdict); +// forbidden: parallel fixture vocabulary outside LeafModelFixture once Layer B generator lands +// (docs/planning/v4-leaf-model-verification-2026-05-30.md §9 DFS gate). +type LeafModelRustFixture { + source: String + crate_type: LeafModelRustCrateType +} + +// 🟡 gated — feature:leaf-model-r1-rustc-bridge — dissolve-on-arrival: nested under LeafModelFixture.falsification_artifact +type LeafModelFalsificationCase { + fixture: LeafModelRustFixture + expected_verdict: TargetCompileVerdict +} + +// 🟡 gated — feature:leaf-model-r1-rustc-bridge — dissolve-on-arrival: R1 row becomes LeafModelFixture> +type LeafModelFixturePair { + claim_id: LeafModelClaimId + surface_spelling_fact: Symbol + coercion_spelling_fact: Symbol + happy: LeafModelRustFixture + expected_happy_verdict: TargetCompileVerdict + falsification: LeafModelFalsificationCase +} + +type LeafModelVerificationRunReceipt { + claim_id: LeafModelClaimId + happy_verdict: Verdict + falsification_verdict: Verdict +} + +fn leaf_model_verification_claim_passes( + receipt: LeafModelVerificationRunReceipt +) -> Verdict { + verdict_combine(a: receipt.happy_verdict, b: receipt.falsification_verdict) +} + +fn leaf_model_verification_combine_runs( + runs: List +) -> Verdict { + fold( + runs, + init: Pass, + f: fn(acc, r) { + verdict_combine(a: acc, b: leaf_model_verification_claim_passes(receipt: r)) + } + ) +} diff --git a/src/v4/test/claim/language_model/rust_r1.dag b/src/v4/test/claim/language_model/rust_r1.dag new file mode 100644 index 00000000000..fefea2db167 --- /dev/null +++ b/src/v4/test/claim/language_model/rust_r1.dag @@ -0,0 +1,127 @@ +// src/v4/test/claim/language_model/rust_r1.dag +// Scope: Phase 1 R1 — rust.dag i32 surface spelling vs rustc (docs/planning/v4-leaf-model-verification-2026-05-30.md §7). +// Status: modeled claim + fixture pair; host runner scripts/v4-leaf-model-rust-r1-verify.sh exercises rustc. + +module v4.test.claim.language_model.rust_r1 + + +import v4.extdeps.languages.rust { + rust_coercion_field_i32_spelling, + rust_surface_spelling_i32 +} +import v4.lens.leaf_model_verification { + rust_r1_fixture, + rust_r1_falsification_fixture_source, + rust_r1_happy_fixture_source +} +import v4.std.diagnostic { + Diagnostic, + Textual, + Unavailable, + UserInputBoundary, + WholeFile, + outcome_rejected +} +import v4.std.leaf_model_verification { + LeafModelClaimId, + LeafModelVerificationRunReceipt, + leaf_model_claim_rust_r1_i32_surface_spelling, + TargetCompileRejected, + TargetCompileVerdict, + target_diagnostic_e0308_type_mismatch +} +import v4.std.logic { Bool } +import v4.std.node { Atom, Node, Symbol, TypeNode } +import v4.std.verdict { verdict_fail } +import v4.std.verification { + EqualsClaim, + ManualAnchorAbsent, + TestClaim, + TestClassification, + Tier1, + Boundary, + manual_claim_anchor +} + + +data rust_r1_claim_bool_true: Symbol = rust_r1_claim_bool_true +data rust_r1_claim_bool_false: Symbol = rust_r1_claim_bool_false + + +fn rust_r1_claim_bool_atom(b: Bool) -> Node { + match b { + true => Node { kind: TypeNode { connective: Atom { identity: rust_r1_claim_bool_true } }, children: [] } + false => Node { kind: TypeNode { connective: Atom { identity: rust_r1_claim_bool_false } }, children: [] } + } +} + + +data claim_rust_r1_fixture_pair_wired: TestClaim = EqualsClaim { + label: "language_model/rust_r1: fixture pair references rust_surface_spelling_i32 fact anchors", + anchor: manual_claim_anchor(anchor: ManualAnchorAbsent), + lhs: rust_r1_claim_bool_atom(b: true), + rhs: rust_r1_claim_bool_atom( + b: rust_r1_fixture().claim_id == leaf_model_claim_rust_r1_i32_surface_spelling + && rust_r1_fixture().surface_spelling_fact == rust_surface_spelling_i32 + && rust_r1_fixture().coercion_spelling_fact == rust_coercion_field_i32_spelling + && rust_r1_fixture().happy.source == rust_r1_happy_fixture_source + && rust_r1_fixture().falsification.fixture.source == rust_r1_falsification_fixture_source + ), + classification: TestClassification { tier: Tier1, layer: Boundary } +} + + +data rust_r1_pending_verification_reason: Symbol = rust_r1_pending_verification_reason + + +fn rust_r1_pending_verification_diagnostic() -> Diagnostic { + Diagnostic { + reason: rust_r1_pending_verification_reason, + at: Textual { file: rust_r1_pending_verification_reason, extent: WholeFile }, + correction: Unavailable { reason: UserInputBoundary } + } +} + + +// Receipt row default fail-closed until host runner overwrites (T-22 bridge follow-on). +data rust_r1_verification_run_receipt_default: LeafModelVerificationRunReceipt = LeafModelVerificationRunReceipt { + claim_id: leaf_model_claim_rust_r1_i32_surface_spelling, + happy_verdict: verdict_fail( + actual: outcome_rejected(d: rust_r1_pending_verification_diagnostic()) + ), + falsification_verdict: verdict_fail( + actual: outcome_rejected(d: rust_r1_pending_verification_diagnostic()) + ) +} + + +data claim_rust_r1_verification_receipt_shape: TestClaim = EqualsClaim { + label: "language_model/rust_r1: verification receipt carriers happy + falsification verdict slots", + anchor: manual_claim_anchor(anchor: ManualAnchorAbsent), + lhs: rust_r1_claim_bool_atom( + b: rust_r1_verification_run_receipt_default.claim_id == leaf_model_claim_rust_r1_i32_surface_spelling + ), + rhs: rust_r1_claim_bool_atom(b: true), + classification: TestClassification { tier: Tier1, layer: Boundary } +} + + +fn rust_r1_fixture_pair_carries_rust_dag_fact_anchors() -> Bool { + rust_r1_fixture().surface_spelling_fact == rust_surface_spelling_i32 + && rust_r1_fixture().coercion_spelling_fact == rust_coercion_field_i32_spelling +} + + +data claim_rust_r1_surface_spelling_fact_ids_stable: TestClaim = EqualsClaim { + label: "language_model/rust_r1: fixture pair carries rust.dag i32 surface-spelling fact anchors", + anchor: manual_claim_anchor(anchor: ManualAnchorAbsent), + lhs: rust_r1_claim_bool_atom(b: rust_r1_fixture_pair_carries_rust_dag_fact_anchors()), + rhs: rust_r1_claim_bool_atom(b: true), + classification: TestClassification { tier: Tier1, layer: Boundary } +} + + +// Modeled expectation for falsification probe (rustc E0308). +data rust_r1_modeled_falsification_expectation: TargetCompileVerdict = TargetCompileRejected { + diagnostic_code: target_diagnostic_e0308_type_mismatch +}