diff --git a/scripts/v4-leaf-model-python-cross-runtime-drift-verify.sh b/scripts/v4-leaf-model-python-cross-runtime-drift-verify.sh new file mode 100755 index 00000000000..897cabb5484 --- /dev/null +++ b/scripts/v4-leaf-model-python-cross-runtime-drift-verify.sh @@ -0,0 +1,174 @@ +#!/usr/bin/env bash +# scripts/v4-leaf-model-python-cross-runtime-drift-verify.sh +# +# PY-L2-CROSS-RUNTIME-DRIFT — positive cross-runtime DIVERGENCE receipt. This is the +# complement of the L2 cross-target PARITY lane: where parity proves runtime-value EQUALITY +# on the common domain, this runner proves that the SAME modeled program (exact integer add +# at the fixed-width boundary, MAX + 1) DIVERGES across runtimes. Python realizes Int as +# arbitrary precision (exact sum); Rust i64 / Go int64 realize it as fixed-width +# two's-complement (defined wraparound). The receipt asserts the drift POSITIVELY so the +# verification system demonstrably DETECTS drift rather than treating wraparound as parity. +# +# Authority: src/v4/lens/leaf_model_verification.dag (python_cross_runtime_drift_*); the +# expected divergence is the modeled ValueDiff (expected = arbitrary-precision value, +# actual = fixed-width wrapped value) consumed from the lens, never re-authored here. +# +# Tool policy: python3 + rustc are MANDATORY (they form the arbitrary-precision-vs-fixed-width +# drift pair the claim is about). Go is a CORROBORATING fixed-width witness (rust == go) and is +# asserted only when the `go` toolchain is present; an offline runner without Go still produces +# an honest receipt that proves the Python-vs-Rust drift. + +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 +for tool in python3 rustc; do + if ! command -v "$tool" >/dev/null 2>&1; then + echo "error: $tool not on PATH (mandatory for the cross-runtime drift pair)" >&2 + exit 1 + fi +done + +go_available=false +command -v go >/dev/null 2>&1 && go_available=true + +eval "$(python3 - "$fixture_dag" <<'PY' +from __future__ import annotations + +import re, shlex, sys +from pathlib import Path + +text = Path(sys.argv[1]).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: {sys.argv[1]}: missing data {name}: String = ...") + +for name, var in [ + ("python_cross_runtime_drift_python_source", "python_source"), + ("python_cross_runtime_drift_rust_source", "rust_source"), + ("python_cross_runtime_drift_go_source", "go_source"), + ("python_cross_runtime_drift_arbitrary_precision_value", "expected_python_value"), + ("python_cross_runtime_drift_fixed_width_value", "expected_fixed_width_value"), +]: + print(f"{var}={shlex.quote(extract(name))}") +PY +)" + +run_suffix="${GITHUB_RUN_ID:-local}-${GITHUB_RUN_ATTEMPT:-$$}" +scratch="${RUNNER_TEMP:-/tmp}/v4-leaf-model-python-cross-runtime-drift-${run_suffix}" +rm -rf "$scratch" +mkdir -p "$scratch" + +printf '%s' "$python_source" >"${scratch}/fixture.py" +printf '%s' "$rust_source" >"${scratch}/fixture.rs" +printf '%s' "$go_source" >"${scratch}/fixture.go" + +# --- Python: arbitrary precision --- +python3 -m py_compile "${scratch}/fixture.py" +python_value="$(python3 "${scratch}/fixture.py")" + +# --- Rust: fixed-width wrapping_add --- +rustc -O "${scratch}/fixture.rs" -o "${scratch}/fixture_rs" >/dev/null +rust_value="$("${scratch}/fixture_rs")" + +# --- Go: corroborating fixed-width witness (optional) --- +go_value="" +if [[ "$go_available" == true ]]; then + ( cd "$scratch" && GOFLAGS= GOCACHE="${scratch}/.gocache" go build -o fixture_go fixture.go ) >/dev/null 2>&1 + go_value="$("${scratch}/fixture_go")" +fi + +# --- drift relation --- +python_matches=false +rust_matches=false +go_matches=true +drift_python_vs_rust=false +drift_python_vs_go=true +fixed_width_agree=true + +[[ "$python_value" == "$expected_python_value" ]] && python_matches=true +[[ "$rust_value" == "$expected_fixed_width_value" ]] && rust_matches=true +[[ "$python_value" != "$rust_value" ]] && drift_python_vs_rust=true + +if [[ "$go_available" == true ]]; then + go_matches=false + fixed_width_agree=false + drift_python_vs_go=false + [[ "$go_value" == "$expected_fixed_width_value" ]] && go_matches=true + [[ "$python_value" != "$go_value" ]] && drift_python_vs_go=true + [[ "$rust_value" == "$go_value" ]] && fixed_width_agree=true +fi + +drift_detected=false +if [[ "$python_matches" == true && "$rust_matches" == true \ + && "$drift_python_vs_rust" == true \ + && "$go_matches" == true && "$drift_python_vs_go" == true \ + && "$fixed_width_agree" == true ]]; then + drift_detected=true +fi + +export V4_DRIFT_PYTHON_VALUE="$python_value" +export V4_DRIFT_RUST_VALUE="$rust_value" +export V4_DRIFT_GO_VALUE="$go_value" +export V4_DRIFT_GO_AVAILABLE="$go_available" +export V4_DRIFT_EXPECTED_PYTHON="$expected_python_value" +export V4_DRIFT_EXPECTED_FIXED="$expected_fixed_width_value" +export V4_DRIFT_PYTHON_MATCHES="$python_matches" +export V4_DRIFT_RUST_MATCHES="$rust_matches" +export V4_DRIFT_GO_MATCHES="$go_matches" +export V4_DRIFT_PVR="$drift_python_vs_rust" +export V4_DRIFT_PVG="$drift_python_vs_go" +export V4_DRIFT_FIXED_AGREE="$fixed_width_agree" +export V4_DRIFT_DETECTED="$drift_detected" + +python3 - <<'PY' +import json, os + +def b(name): return os.environ[name] == "true" + +go_available = b("V4_DRIFT_GO_AVAILABLE") +print(json.dumps({ + "schema": "scripts/v4-leaf-model-python-cross-runtime-drift-verify.sh::drift_receipt_v1", + "claim_id": "PythonCrossRuntimeDriftArbitraryPrecision", + "kind": "positive-divergence (complement of L2 parity)", + "modeled_divergence": { + "expected_arbitrary_precision_value": os.environ["V4_DRIFT_EXPECTED_PYTHON"], + "expected_fixed_width_value": os.environ["V4_DRIFT_EXPECTED_FIXED"], + "carrier": "ValueDiff (src/v4/std/host_run.dag) via python_cross_runtime_drift_probe", + }, + "observed": { + "python": {"value": os.environ["V4_DRIFT_PYTHON_VALUE"], "matches_expected": b("V4_DRIFT_PYTHON_MATCHES")}, + "rust": {"value": os.environ["V4_DRIFT_RUST_VALUE"], "matches_expected": b("V4_DRIFT_RUST_MATCHES")}, + "go": ({"value": os.environ["V4_DRIFT_GO_VALUE"], "matches_expected": b("V4_DRIFT_GO_MATCHES")} + if go_available else {"value": None, "matches_expected": "deferred(go-unavailable)"}), + }, + "drift_relation": { + "python_vs_rust_diverges": b("V4_DRIFT_PVR"), + "python_vs_go_diverges": (b("V4_DRIFT_PVG") if go_available else "deferred(go-unavailable)"), + "rust_vs_go_agree": (b("V4_DRIFT_FIXED_AGREE") if go_available else "deferred(go-unavailable)"), + }, + "drift_detected": b("V4_DRIFT_DETECTED"), +}, indent=2)) +PY + +if [[ "$drift_detected" != true ]]; then + echo "error: leaf-model python cross-runtime drift NOT positively detected (python=${python_value}, rust=${rust_value}, go=${go_value:-})" >&2 + exit 1 +fi + +if [[ "$go_available" == true ]]; then + echo "leaf-model python cross-runtime drift DETECTED (python ${python_value} != fixed-width ${rust_value}; rust == go)" +else + echo "leaf-model python cross-runtime drift DETECTED (python ${python_value} != rust ${rust_value}; go corroboration deferred — toolchain unavailable)" +fi diff --git a/src/v3/compiler/tests/boundary/v4_leaf_model_python_cross_runtime_drift_test.rs b/src/v3/compiler/tests/boundary/v4_leaf_model_python_cross_runtime_drift_test.rs new file mode 100644 index 00000000000..d0a72392575 --- /dev/null +++ b/src/v3/compiler/tests/boundary/v4_leaf_model_python_cross_runtime_drift_test.rs @@ -0,0 +1,199 @@ +//! **Layer:** boundary — cross-runtime drift detection for v4 leaf-model python. +//! +//! PY-L2-CROSS-RUNTIME-DRIFT — the positive-divergence complement of the L2 cross-target +//! parity lane. The SAME modeled program (exact integer add at the fixed-width boundary, +//! `MAX + 1`) realized in each target's native integer DIVERGES: Python's `int` is arbitrary +//! precision (exact sum `9223372036854775808`), while Rust `i64` / Go `int64` are fixed-width +//! two's-complement (defined wraparound to `-9223372036854775808`). This receipt asserts the +//! drift POSITIVELY, so the verification system demonstrably DETECTS drift rather than treating +//! wraparound as parity. +//! +//! Authority: `src/v4/lens/leaf_model_verification.dag` (`python_cross_runtime_drift_*`); +//! carrier `LeafModelCrossRuntimeDriftProbe` + `ValueDiff` in +//! `src/v4/std/leaf_model_verification.dag`; claim wiring in `python_cross_runtime_drift.dag`; +//! host runner `scripts/v4-leaf-model-python-cross-runtime-drift-verify.sh`. + +use std::io::Write; +use std::process::Command; + +const LENS_DAG: &str = include_str!("../../../../v4/lens/leaf_model_verification.dag"); +const LENS_DAG_PATH: &str = "src/v4/lens/leaf_model_verification.dag"; +const STD_DAG: &str = include_str!("../../../../v4/std/leaf_model_verification.dag"); +const STD_DAG_PATH: &str = "src/v4/std/leaf_model_verification.dag"; +const CLAIM_DAG: &str = + include_str!("../../../../v4/test/claim/language_model/python_cross_runtime_drift.dag"); +const CLAIM_DAG_PATH: &str = "src/v4/test/claim/language_model/python_cross_runtime_drift.dag"; + +const PYTHON_SOURCE: &str = + "def add_exact(a: int, b: int) -> int:\n return a + b\n\nif __name__ == \"__main__\":\n print(add_exact((2 ** 63) - 1, 1))\n"; +const RUST_SOURCE: &str = "fn add_exact(a: i64, b: i64) -> i64 { a.wrapping_add(b) }\nfn main() {\n println!(\"{}\", add_exact(i64::MAX, 1));\n}\n"; + +const EXPECTED_ARBITRARY_PRECISION: &str = "9223372036854775808"; +const EXPECTED_FIXED_WIDTH: &str = "-9223372036854775808"; + +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('t') => out.push('\t'), + 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)) +} + +/// Per-call-unique scratch dir. Rust tests run in parallel within one process and several tests +/// call `run_python` with the same label, so a pid+label path would race (one test's +/// `remove_dir_all` deletes another's fixture). A process-wide atomic counter makes every +/// invocation's directory unique — hermetic per TESTING.md. +fn scratch_dir(label: &str) -> std::path::PathBuf { + use std::sync::atomic::{AtomicU64, Ordering}; + static COUNTER: AtomicU64 = AtomicU64::new(0); + let pid = std::process::id(); + let seq = COUNTER.fetch_add(1, Ordering::Relaxed); + std::env::temp_dir().join(format!("v4_leaf_model_python_drift_{label}_{pid}_{seq}")) +} + +/// Tokenize + parse a single `.dag` (full multi-module `compile_to_dag` is not hermetic per-file; +/// this catches surface/syntax regressions in the new drift carriers — same compromise as +/// `v4_bin_main_dag_smoke_test`). +fn tokenize_and_parse(dag_text: &str, dag_path: &str) { + let tokens = v3_compiler::tokenize_for_test(dag_text, dag_path) + .unwrap_or_else(|e| panic!("{dag_path}: tokenize: {e:?}")); + let _module = v3_compiler::parse_for_test(&tokens, dag_path) + .unwrap_or_else(|e| panic!("{dag_path}: parse: {e:?}")); +} + +#[test] +fn v4_leaf_model_python_drift_dags_tokenize_and_parse() { + tokenize_and_parse(STD_DAG, STD_DAG_PATH); + tokenize_and_parse(LENS_DAG, LENS_DAG_PATH); + tokenize_and_parse(CLAIM_DAG, CLAIM_DAG_PATH); +} + +#[test] +fn v4_leaf_model_python_drift_fixture_strings_match_dag_authority() { + let py = extract_fixture_source(LENS_DAG, "python_cross_runtime_drift_python_source").unwrap(); + let rs = extract_fixture_source(LENS_DAG, "python_cross_runtime_drift_rust_source").unwrap(); + let py_val = extract_fixture_source( + LENS_DAG, + "python_cross_runtime_drift_arbitrary_precision_value", + ) + .unwrap(); + let fw_val = + extract_fixture_source(LENS_DAG, "python_cross_runtime_drift_fixed_width_value").unwrap(); + assert_eq!(py, PYTHON_SOURCE); + assert_eq!(rs, RUST_SOURCE); + assert_eq!(py_val, EXPECTED_ARBITRARY_PRECISION); + assert_eq!(fw_val, EXPECTED_FIXED_WIDTH); +} + +/// The modeled divergence is positive: the two `ValueDiff` arms differ. +#[test] +fn v4_leaf_model_python_drift_modeled_divergence_is_positive() { + assert_ne!( + EXPECTED_ARBITRARY_PRECISION, EXPECTED_FIXED_WIDTH, + "drift receipt requires arbitrary-precision value != fixed-width value" + ); +} + +fn run_python(source: &str) -> String { + let tmp_dir = scratch_dir("py"); + let _ = std::fs::remove_dir_all(&tmp_dir); + std::fs::create_dir_all(&tmp_dir).expect("create scratch dir"); + let src_path = tmp_dir.join("fixture.py"); + std::fs::File::create(&src_path) + .and_then(|mut f| f.write_all(source.as_bytes())) + .expect("write python fixture"); + let out = Command::new("python3") + .arg(&src_path) + .output() + .expect("invoke python3"); + let _ = std::fs::remove_dir_all(&tmp_dir); + assert!( + out.status.success(), + "python fixture must run clean; stderr:\n{}", + String::from_utf8_lossy(&out.stderr) + ); + String::from_utf8_lossy(&out.stdout).trim().to_string() +} + +/// rustc is MANDATORY (fail-closed): the cross-runtime drift claim *is* Python arbitrary +/// precision vs Rust fixed-width, and the host runner treats rustc as required for the same +/// reason. The repo's other rust boundary tests (`v4_leaf_model_rust_*`) likewise invoke rustc +/// unconditionally — it is the bootstrap toolchain, always present in a test environment. +/// Skipping the assertion when rustc is absent would let a green receipt never exercise the +/// drift pair, so we panic instead. +fn run_rust(source: &str) -> String { + Command::new("rustc") + .arg("--version") + .output() + .expect("rustc must be available (mandatory for the Python-vs-Rust drift pair)"); + let tmp_dir = scratch_dir("rs"); + let _ = std::fs::remove_dir_all(&tmp_dir); + std::fs::create_dir_all(&tmp_dir).expect("create scratch dir"); + let src_path = tmp_dir.join("fixture.rs"); + let bin_path = tmp_dir.join("fixture_rs"); + std::fs::File::create(&src_path) + .and_then(|mut f| f.write_all(source.as_bytes())) + .expect("write rust fixture"); + let compile = Command::new("rustc") + .env_remove("RUSTC_BOOTSTRAP") + .arg("--edition=2021") + .arg("-O") + .arg(&src_path) + .arg("-o") + .arg(&bin_path) + .output() + .expect("invoke rustc"); + assert!( + compile.status.success(), + "rustc must accept the drift fixture; stderr:\n{}", + String::from_utf8_lossy(&compile.stderr) + ); + let run = Command::new(&bin_path).output().expect("run rust binary"); + let _ = std::fs::remove_dir_all(&tmp_dir); + String::from_utf8_lossy(&run.stdout).trim().to_string() +} + +#[test] +fn v4_leaf_model_python_drift_python_realizes_arbitrary_precision() { + let value = run_python(PYTHON_SOURCE); + assert_eq!( + value, EXPECTED_ARBITRARY_PRECISION, + "Python int must realize the exact arbitrary-precision sum" + ); +} + +#[test] +fn v4_leaf_model_python_drift_python_vs_rust_diverges() { + let python_value = run_python(PYTHON_SOURCE); + let rust_value = run_rust(RUST_SOURCE); + assert_eq!( + rust_value, EXPECTED_FIXED_WIDTH, + "Rust i64 must wrap to i64::MIN at the fixed-width boundary" + ); + assert_ne!( + python_value, rust_value, + "cross-runtime DRIFT: Python arbitrary precision must diverge from Rust fixed-width" + ); +} diff --git a/src/v3/compiler/tests/integration.rs b/src/v3/compiler/tests/integration.rs index 0d83c13f1df..c87258907b9 100644 --- a/src/v3/compiler/tests/integration.rs +++ b/src/v3/compiler/tests/integration.rs @@ -301,6 +301,8 @@ mod v4_extdeps_formatters_black_dag_smoke_test; mod v4_extdeps_react_dag_smoke_test; #[path = "boundary/v4_leaf_model_go_r1_r2_r3_external_test.rs"] mod v4_leaf_model_go_r1_r2_r3_external_test; +#[path = "boundary/v4_leaf_model_python_cross_runtime_drift_test.rs"] +mod v4_leaf_model_python_cross_runtime_drift_test; #[path = "boundary/v4_leaf_model_python_r1_test.rs"] mod v4_leaf_model_python_r1_test; #[path = "boundary/v4_leaf_model_python_r2_r3_external_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 e057224347a..44299c73ea8 100644 --- a/src/v3/compiler/tests/integration/sg0_census_test.rs +++ b/src/v3/compiler/tests/integration/sg0_census_test.rs @@ -413,6 +413,22 @@ const EXPECTED_HAND_AUTHORED_TEST: &[&str] = &[ // verdicts; P5 deferral to ROADMAP.md `PB-Runtime-External-Toolchain-TestClaims`. // Interim host runners: scripts/v4-leaf-model-go-r{1,2a,2b,3-external}-verify.sh. "src/v3/compiler/tests/boundary/v4_leaf_model_go_r1_r2_r3_external_test.rs", + // Phase 1 leaf-model python cross-runtime DRIFT (Worksheet C): boundary tokenize/parse smoke + // of the drift std/lens/claim dags + runtime divergence exercise for + // `python_cross_runtime_drift_*` (Python arbitrary precision vs Rust/Go fixed-width wrap); + // host runner `scripts/v4-leaf-model-python-cross-runtime-drift-verify.sh`. + // + // **P5 receipt (INVARIANTS.md §P5 — SG-0 `EXPECTED_HAND_AUTHORED_TEST`):** the checkable + // receipt is this registration itself (per-PR mechanism (b)) — the `EXPECTED_HAND_AUTHORED_TEST` + // census moves by exactly +1 now and must shrink by 1 at dissolution; the sorted/unique and + // disk-vs-list census tests in this file mechanically enforce it. Deferral lane — + // **ROADMAP.md** "What v4 is building toward" rows "Tests as `.dag` `TestClaim` data" + // (`src/v4/test/claim/`) and "Pure bootstrap / self-host" (trajectory to zero hand-maintained + // Rust; `self_host.dag` ratchet). Concrete dissolution trigger: delete this hand-Rust test when + // the modeled `TestClaim` runner exercises + // `src/v4/test/claim/language_model/python_cross_runtime_drift.dag` directly, so the boundary + // host-process bridge is no longer the only exerciser of the drift claim. + "src/v3/compiler/tests/boundary/v4_leaf_model_python_cross_runtime_drift_test.rs", // Phase 1 leaf-model python R1 (W2.6 / PR #3938 §11.4): boundary CPython exercise for // `src/v4/lens/leaf_model_verification.dag` python fixtures until T-22 modeled // `run_target_verification` owns target verdicts; interim host runner diff --git a/src/v4/lens/leaf_model_verification.dag b/src/v4/lens/leaf_model_verification.dag index 989466b7baa..89286a74aaf 100644 --- a/src/v4/lens/leaf_model_verification.dag +++ b/src/v4/lens/leaf_model_verification.dag @@ -14,12 +14,14 @@ import v4.extdeps.languages.go { go_facts_int64, go_integer_algebra_inhabitance, go_integer_facts_node, + go_repr_twos_complement_integer, go_surface_spelling_int } import v4.extdeps.languages.python { python_atom_realization_symbol, python_facts_field_encoding, python_integer_algebra_inhabitance_python_facts_int, + python_repr_int_arbitrary_precision, python_surface_spelling_int } import v4.extdeps.typecheckers.pyright { @@ -37,6 +39,7 @@ import v4.extdeps.languages.rust { rust_coercion_field_i32_spelling, rust_integer_algebra_inhabitance_rust_facts_i32, rust_mvp1_target_model_staging, + rust_repr_integer_twos_complement, rust_surface_spelling_i32, rust_target_atom_realization_symbol, rust_target_atom_type_form @@ -44,6 +47,7 @@ import v4.extdeps.languages.rust { import v4.std.algebra { algebra_inhabitance_node } import v4.std.collection { optional_absent } import v4.std.diagnostic { Accepted, Rejected } +import v4.std.host_run { ValueDiff } import v4.std.logic { Bool } import v4.std.target_model { TargetAtomRealization, @@ -75,6 +79,8 @@ import v4.std.leaf_model_verification { LeafModelTypeScriptRuntimeFixture, LeafModelTypeScriptRuntimeFixturePair, LeafModelRustFixture, + LeafModelCrossRuntimeDriftProbe, + leaf_model_claim_python_cross_runtime_drift_arbitrary_precision, leaf_model_claim_go_r1_int_surface_spelling, leaf_model_claim_go_r2a_int_algebra_operations, leaf_model_claim_go_r2b_int64_silent_overflow_truncates, @@ -271,6 +277,42 @@ fn python_r2b_fixture() -> LeafModelPythonFixturePair { python_r2b_fixture_pair() } +// --- PY-L2-CROSS-RUNTIME-DRIFT — positive cross-runtime divergence receipt --- +// The same modeled program — exact integer add at the fixed-width boundary, `MAX + 1` — realized +// in each target's native integer. Python's Int is arbitrary precision, so it prints the exact sum +// (9223372036854775808). Rust `i64` and Go `int64` are fixed-width two's-complement, so the same add +// wraps to i64::MIN (-9223372036854775808). The runner asserts the drift POSITIVELY: python_value != +// rust_value (and != go_value when Go is present), while rust_value == go_value (cross-runtime +// fixed-width agreement). Rust uses `wrapping_add` so the boundary is defined behavior (no debug +// overflow panic); Go signed overflow is defined to wrap by the language spec. Complement of the L2 +// parity lane (PR #4154), which asserts EQUALITY on the common domain. +data python_cross_runtime_drift_python_source: String = "def add_exact(a: int, b: int) -> int:\n return a + b\n\nif __name__ == \"__main__\":\n print(add_exact((2 ** 63) - 1, 1))\n" + +data python_cross_runtime_drift_rust_source: String = "fn add_exact(a: i64, b: i64) -> i64 { a.wrapping_add(b) }\nfn main() {\n println!(\"{}\", add_exact(i64::MAX, 1));\n}\n" + +data python_cross_runtime_drift_go_source: String = "package main\n\nimport (\n\t\"fmt\"\n\t\"math\"\n)\n\nfunc addExact(a int64, b int64) int64 { return a + b }\n\nfunc main() {\n\tfmt.Println(addExact(math.MaxInt64, 1))\n}\n" + +// Arbitrary-precision (Python) value vs fixed-width wrapped (Rust/Go) value — the modeled divergence. +data python_cross_runtime_drift_arbitrary_precision_value: String = "9223372036854775808" + +data python_cross_runtime_drift_fixed_width_value: String = "-9223372036854775808" + +fn python_cross_runtime_drift_probe() -> LeafModelCrossRuntimeDriftProbe { + LeafModelCrossRuntimeDriftProbe { + claim_id: leaf_model_claim_python_cross_runtime_drift_arbitrary_precision, + arbitrary_precision_fact: python_repr_int_arbitrary_precision, + fixed_width_rust_fact: rust_repr_integer_twos_complement, + fixed_width_go_fact: go_repr_twos_complement_integer, + arbitrary_precision_source: python_cross_runtime_drift_python_source, + fixed_width_rust_source: python_cross_runtime_drift_rust_source, + fixed_width_go_source: python_cross_runtime_drift_go_source, + expected_divergence: ValueDiff { + expected: python_cross_runtime_drift_arbitrary_precision_value, + actual: python_cross_runtime_drift_fixed_width_value + } + } +} + // R3-external — Symbol atom realization: nominal class (happy) vs ctor arity mismatch (falsification). data python_r3_external_claim_atom_realization_fact: Symbol = python_atom_realization_symbol diff --git a/src/v4/std/leaf_model_verification.dag b/src/v4/std/leaf_model_verification.dag index 1e7a1eb7b12..f52527f0df8 100644 --- a/src/v4/std/leaf_model_verification.dag +++ b/src/v4/std/leaf_model_verification.dag @@ -9,6 +9,7 @@ module v4.std.leaf_model_verification import v4.std.collection { List } +import v4.std.host_run { ValueDiff } import v4.std.nat { Nat } import v4.std.node { Node, Symbol } import v4.std.text { String } @@ -165,6 +166,47 @@ data leaf_model_claim_go_r1_int_surface_spelling: LeafModelClaimId = leaf_model_ data leaf_model_claim_go_r2a_int_algebra_operations: LeafModelClaimId = leaf_model_claim_go_r2a_int_algebra_operations data leaf_model_claim_go_r2b_int64_silent_overflow_truncates: LeafModelClaimId = leaf_model_claim_go_r2b_int64_silent_overflow_truncates data leaf_model_claim_go_r3_external_symbol_projection: LeafModelClaimId = leaf_model_claim_go_r3_external_symbol_projection +data leaf_model_claim_python_cross_runtime_drift_arbitrary_precision: LeafModelClaimId = leaf_model_claim_python_cross_runtime_drift_arbitrary_precision + +// --- PY-L2-CROSS-RUNTIME-DRIFT: positive cross-runtime divergence receipt --- +// Complement of the L2 cross-target PARITY lane (PR #4154, +// `run_cross_target_mvp2_python_parity_transport`), which proves runtime-value EQUALITY on the +// common domain (R2a add/order, R3 symbol projection). This carrier proves the COMPLEMENT +// obligation named in the Python RCA worksheet (Worksheet C): the SAME modeled program — exact +// integer add at the fixed-width boundary — DIVERGES across runtimes. Python realizes Int as +// arbitrary precision (the correct sum); Rust `i64` / Go `int64` realize it as fixed-width +// two's-complement with defined wraparound. That divergence is a MODELED fact, not a bug: the +// receipt asserts it POSITIVELY, so the verification system demonstrably DETECTS drift instead of +// silently treating fixed-width wraparound as parity. The expected divergence is anchored to +// `ValueDiff` (the host_run divergence carrier) — `expected` is the arbitrary-precision +// value, `actual` is the fixed-width wrapped value — so the receipt references a modeled value +// pair, never a script-local literal. Go is a corroborating fixed-width witness (rust == go); +// the runner asserts it only when the Go toolchain is present. +// +// FACTS FLOW FORWARD (INVARIANTS P1/P2): the drift is not asserted as a bare value pair — the +// MODELED CAUSE travels with it. The three `*_fact` fields anchor the divergence to the extdeps +// language representation facts that JUSTIFY it: Python int is `python_repr_int_arbitrary_precision` +// (so the sum is exact) while Rust and Go integers are `rust_repr_integer_twos_complement` / +// `go_repr_twos_complement_integer` (so the same add wraps at the fixed-width boundary). The +// `TestClaim` asserts these anchors, so the receipt carries the reason for the drift, not just its +// observed values — that is what makes this carrier reusable authority rather than a literal pair. +// +// 🟡 gated — feature:leaf-model-cross-runtime-drift — dissolve-on: the modeled `TestClaim` runner +// exercises `src/v4/test/claim/language_model/python_cross_runtime_drift.dag` directly (retiring the +// boundary host-process bridge `scripts/v4-leaf-model-python-cross-runtime-drift-verify.sh` + +// `v4_leaf_model_python_cross_runtime_drift_test.rs`, shrinking `EXPECTED_HAND_AUTHORED_TEST` by 1); +// forbidden: a parallel drift-probe vocabulary outside this carrier — extend it, don't fork it. +type LeafModelCrossRuntimeDriftProbe { + claim_id: LeafModelClaimId + // Modeled cause of the divergence (extdeps representation facts) — Facts Flow Forward. + arbitrary_precision_fact: Symbol + fixed_width_rust_fact: Symbol + fixed_width_go_fact: Symbol + arbitrary_precision_source: String + fixed_width_rust_source: String + fixed_width_go_source: String + expected_divergence: ValueDiff +} type LeafModelRustCrateType = Symbol diff --git a/src/v4/test/claim/language_model/python_cross_runtime_drift.dag b/src/v4/test/claim/language_model/python_cross_runtime_drift.dag new file mode 100644 index 00000000000..c36b9167ef1 --- /dev/null +++ b/src/v4/test/claim/language_model/python_cross_runtime_drift.dag @@ -0,0 +1,88 @@ +// src/v4/test/claim/language_model/python_cross_runtime_drift.dag +// Scope: PY-L2-CROSS-RUNTIME-DRIFT — positive cross-runtime divergence receipt (complement of +// the L2 cross-target parity lane). The same modeled program (exact integer add at the +// fixed-width boundary) diverges: Python arbitrary precision vs Rust i64 / Go int64 wraparound. +// Status: modeled claim + drift probe row; host runner +// scripts/v4-leaf-model-python-cross-runtime-drift-verify.sh. + +module v4.test.claim.language_model.python_cross_runtime_drift + +import v4.extdeps.languages.python { python_repr_int_arbitrary_precision } +import v4.extdeps.languages.rust { rust_repr_integer_twos_complement } +import v4.extdeps.languages.go { go_repr_twos_complement_integer } +import v4.lens.leaf_model_verification { + python_cross_runtime_drift_probe, + python_cross_runtime_drift_python_source, + python_cross_runtime_drift_rust_source, + python_cross_runtime_drift_go_source, + python_cross_runtime_drift_arbitrary_precision_value, + python_cross_runtime_drift_fixed_width_value +} +import v4.std.leaf_model_verification { + LeafModelCrossRuntimeDriftProbe, + leaf_model_claim_python_cross_runtime_drift_arbitrary_precision +} +import v4.std.logic { Bool } +import v4.std.node { Atom, Node, Symbol, TypeNode } +import v4.std.verification { + EqualsClaim, + ManualAnchorAbsent, + TestClaim, + TestClassification, + Tier1, + Boundary, + manual_claim_anchor +} + +data python_cross_runtime_drift_claim_bool_true: Symbol = python_cross_runtime_drift_claim_bool_true +data python_cross_runtime_drift_claim_bool_false: Symbol = python_cross_runtime_drift_claim_bool_false + +fn python_cross_runtime_drift_claim_bool_atom(b: Bool) -> Node { + match b { + true => Node { kind: TypeNode { connective: Atom { identity: python_cross_runtime_drift_claim_bool_true } }, children: [] } + false => Node { kind: TypeNode { connective: Atom { identity: python_cross_runtime_drift_claim_bool_false } }, children: [] } + } +} + +// Field access is taken on a bound probe PARAMETER (the v4 surface parser supports `p.field` +// chains on an identifier, not postfix `.field` on a call result), so the wiring/divergence +// predicates live in helper fns that receive the probe. +fn python_cross_runtime_drift_probe_is_wired(p: LeafModelCrossRuntimeDriftProbe) -> Bool { + p.claim_id == leaf_model_claim_python_cross_runtime_drift_arbitrary_precision + && p.arbitrary_precision_fact == python_repr_int_arbitrary_precision + && p.fixed_width_rust_fact == rust_repr_integer_twos_complement + && p.fixed_width_go_fact == go_repr_twos_complement_integer + && p.arbitrary_precision_source == python_cross_runtime_drift_python_source + && p.fixed_width_rust_source == python_cross_runtime_drift_rust_source + && p.fixed_width_go_source == python_cross_runtime_drift_go_source + && p.expected_divergence.expected == python_cross_runtime_drift_arbitrary_precision_value + && p.expected_divergence.actual == python_cross_runtime_drift_fixed_width_value +} + +fn python_cross_runtime_drift_probe_diverges(p: LeafModelCrossRuntimeDriftProbe) -> Bool { + p.expected_divergence.expected != p.expected_divergence.actual +} + +// The drift probe wires the modeled claim id to the three target sources, and anchors the expected +// divergence to ValueDiff (expected = arbitrary-precision value, actual = fixed-width value). +data claim_python_cross_runtime_drift_probe_wired: TestClaim = EqualsClaim { + label: "language_model/python_cross_runtime_drift: probe wires drift claim id + per-target sources + ValueDiff divergence anchor", + anchor: manual_claim_anchor(anchor: ManualAnchorAbsent), + lhs: python_cross_runtime_drift_claim_bool_atom(b: true), + rhs: python_cross_runtime_drift_claim_bool_atom( + b: python_cross_runtime_drift_probe_is_wired(p: python_cross_runtime_drift_probe()) + ), + classification: TestClassification { tier: Tier1, layer: Boundary } +} + +// The divergence is POSITIVE: the arbitrary-precision value and the fixed-width value differ. A +// receipt that found them equal would mean the verifier failed to detect drift (false parity). +data claim_python_cross_runtime_drift_is_positive_divergence: TestClaim = EqualsClaim { + label: "language_model/python_cross_runtime_drift: arbitrary-precision value diverges from fixed-width value (drift is real)", + anchor: manual_claim_anchor(anchor: ManualAnchorAbsent), + lhs: python_cross_runtime_drift_claim_bool_atom(b: true), + rhs: python_cross_runtime_drift_claim_bool_atom( + b: python_cross_runtime_drift_probe_diverges(p: python_cross_runtime_drift_probe()) + ), + classification: TestClassification { tier: Tier1, layer: Boundary } +}