Repository navigation
Phase 1 dispatch (PR #3959 §11.4 step 4): R1 fixture generator + runner against rustc for rust.dag per merged leaf-model verification doc. Phase 1 scope: R1 (i32 surface spelling) — emit Rust source 'pub fn r1_test() -> i32 { 0i32 }' as fixture; invoke rustc; capture verdict; falsification probe = e #3972
New issue
Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.
By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.
Already on GitHub? Sign in to your account
Merged
Merged
Changes from 4 commits
Commits
Show all changes
33 commits
Select commit
Hold shift + click to select a range
7cbdfdf
WIP: Phase 1 dispatch (PR #3959 §11.4 step 4): R1 fixture generator +…
briansrls 16ecaf8
WIP: Phase 1 dispatch (PR #3959 §11.4 step 4): R1 fixture generator +…
briansrls 1cec310
WIP: Phase 1 dispatch (PR #3959 §11.4 step 4): R1 fixture generator +…
briansrls 0359f83
fix(ci): apply cargo fmt for R1 leaf-model boundary test
briansrls 669ee5f
WIP: Phase 1 dispatch (PR #3959 §11.4 step 4): R1 fixture generator +…
briansrls 84b107e
WIP: Phase 1 dispatch (PR #3959 §11.4 step 4): R1 fixture generator +…
briansrls 4b62822
fix(review): address openai-pro coproduct dispositions + host-runner …
briansrls fd91932
fix(ci): add SG-0 PR-body append for leaf-model R1 census +1
briansrls 88c0cf5
fix(ci): raise v4 bootstrap/testclaim compile timeouts (exit 143)
briansrls c96fc11
Merge remote-tracking branch 'origin/main' into session/quick-lark-396
briansrls 816a836
merge(main): pick up ci_int_offset bounded peel (SG-7 / v4 bootstrap)
briansrls b39d09b
fix(v4): use Symbol anchors for single-variant leaf-model IDs
briansrls 5b5212a
fix(v4): single-line Symbol data binding (parse error after newline)
briansrls 3823b20
fix(v4): annotate falsification expectation as TargetCompileVerdict
briansrls 10308dd
fix(review): carry rust.dag fact anchors in LeafModelFixturePair
briansrls 4f3549d
merge(main): resolve timeout conflict; keep 420s testclaim CI default
briansrls 802e1d7
WIP: Phase 1 dispatch (PR #3959 §11.4 step 4): R1 fixture generator +…
briansrls 41665fe
merge(main): unify leaf_model_verification substrate + CI 480s timeouts
briansrls 774c42e
WIP: Phase 1 dispatch (PR #3959 §11.4 step 4): R1 fixture generator +…
briansrls 7d7a795
WIP: Phase 1 dispatch (PR #3959 §11.4 step 4): R1 fixture generator +…
briansrls 84dae9d
fix(ci): scope phase1/nat_semiring rung gate to fixture-touched PR paths
briansrls 649ee25
Merge remote-tracking branch 'origin/main' into session/quick-lark-396
briansrls dbdcbd4
WIP: Phase 1 dispatch (PR #3959 §11.4 step 4): R1 fixture generator +…
briansrls 5ab802e
fix(ci,substrate): address api-review on gate scope + fixture vocabulary
briansrls 4b3faca
fix(ci): move nat_semiring gate scope detector out of workflow YAML
briansrls ec57ad9
fix(ci): nat_semiring scope detector self-validates gate wiring edits
briansrls 4cddd83
WIP: Phase 1 dispatch (PR #3959 §11.4 step 4): R1 fixture generator +…
briansrls ee7c49b
fix(ci): split nat_semiring full gate vs workflow-policy ratchet
briansrls 45af5ba
WIP: Phase 1 dispatch (PR #3959 §11.4 step 4): R1 fixture generator +…
briansrls cb54615
WIP: Phase 1 dispatch (PR #3959 §11.4 step 4): R1 fixture generator +…
briansrls 07ac0d9
WIP: Phase 1 dispatch (PR #3959 §11.4 step 4): R1 fixture generator +…
briansrls 1b88cb0
merge: resolve main into session/quick-lark-396
briansrls dead3f8
merge: keep 480s corpus-gate timeout comment with main
briansrls File filter
Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
There are no files selected for viewing
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| Original file line number | Diff line number | Diff line change |
|---|---|---|
| @@ -0,0 +1,166 @@ | ||
| #!/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. | ||
|
|
||
| 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" |
110 changes: 110 additions & 0 deletions
110
src/v3/compiler/tests/boundary/v4_leaf_model_rust_r1_rustc_test.rs
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| Original file line number | Diff line number | Diff line change |
|---|---|---|
| @@ -0,0 +1,110 @@ | ||
| //! **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`. | ||
| //! | ||
| //! **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<String> { | ||
| 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}" | ||
| ); | ||
| } | ||
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| Original file line number | Diff line number | Diff line change |
|---|---|---|
| @@ -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, | ||
| RustCrateTypeLib, | ||
| RustR1I32SurfaceSpelling, | ||
| TargetCompileAccepted, | ||
| TargetCompileRejected, | ||
| target_diagnostic_e0308_type_mismatch | ||
| } | ||
| 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 | ||
|
Contributor
Author
There was a problem hiding this comment. Choose a reason for hiding this commentThe reason will be displayed to describe this comment to others. Learn more. BLOCKING: Symbol is used without importing v4.std.node.Symbol, so the new lens module cannot resolve its fact anchors and fails the v4 parse/resolve gate. |
||
| 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 { | ||
| claim_id: RustR1I32SurfaceSpelling, | ||
| source: rust_r1_happy_fixture_source, | ||
| crate_type: RustCrateTypeLib | ||
| } | ||
| } | ||
|
|
||
|
|
||
| fn rust_r1_falsification_fixture() -> LeafModelRustFixture { | ||
| LeafModelRustFixture { | ||
| claim_id: RustR1I32SurfaceSpelling, | ||
| source: rust_r1_falsification_fixture_source, | ||
| crate_type: RustCrateTypeLib | ||
| } | ||
| } | ||
|
|
||
|
|
||
| fn rust_r1_fixture_pair() -> LeafModelFixturePair { | ||
| LeafModelFixturePair { | ||
| claim_id: RustR1I32SurfaceSpelling, | ||
| happy: rust_r1_happy_fixture(), | ||
| expected_happy_verdict: TargetCompileAccepted, | ||
| falsification: LeafModelFalsificationCase { | ||
| claim_id: RustR1I32SurfaceSpelling, | ||
| 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() | ||
| } | ||
Oops, something went wrong.
Oops, something went wrong.
Add this suggestion to a batch that can be applied as a single commit.
This suggestion is invalid because no changes were made to the code.
Suggestions cannot be applied while the pull request is closed.
Suggestions cannot be applied while viewing a subset of changes.
Only one suggestion per line can be applied in a batch.
Add this suggestion to a batch that can be applied as a single commit.
Applying suggestions on deleted lines is not supported.
You must change the existing code in this line in order to create a valid suggestion.
Outdated suggestions cannot be applied.
This suggestion has been applied or marked resolved.
Suggestions cannot be applied from pending reviews.
Suggestions cannot be applied on multi-line comments.
Suggestions cannot be applied while the pull request is queued to merge.
Suggestion cannot be applied right now. Please check back later.
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
BLOCKING: This new hand-authored Rust test bridge lacks the required same-PR SG-0 EXPECTED_HAND_AUTHORED_TEST/INVARIANTS receipt or concrete ROADMAP-row deferral, violating INVARIANTS P5 for src/v3 Rust tests.