Skip to content
Closed
Show file tree
Hide file tree
Changes from all commits
Commits
File filter

Filter by extension

Filter by extension

Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
19 changes: 17 additions & 2 deletions dsl/test/claim/dsl_compile_clean_witness_test.dag
Original file line number Diff line number Diff line change
@@ -1,6 +1,8 @@
// dsl/test/claim/dsl_compile_clean_witness.dag — by-execution +/- witness for dsl compile-clean.
//
// GREEN: run_clean_tree_compile() — gunbc compile over live dsl/ exits 0.
// GREEN: run_clean_tree_compile() — gunbc compile over live dsl/ (+ src/v2 pools) exits 0.
// GREEN: run_cross_tree_import_green_receipt() — planted dsl→v2 import resolves and compiles.
// GREEN: run_dsl_shell_primary_precedence_receipt() — dsl extdeps.shell (shell.Env) wins over v2 overlay.
// RED: run_perturb_optional_skew_red_receipt() — planted Some/None skew fails compile.
//
// Run: gunbc run --source-root dsl --entry <this> --function dsl_compile_clean_witnesses --claim-run
Expand All @@ -9,17 +11,30 @@ module test.claim.dsl_compile_clean_witness

import tools.dsl_compile_clean_transport {
run_clean_tree_compile,
run_cross_tree_import_green_receipt,
run_dsl_shell_primary_precedence_receipt,
run_perturb_optional_skew_red_receipt
}

fn witness_clean_tree_compile_holds() -> Bool {
run_clean_tree_compile()
}

fn witness_cross_tree_import_compiles_green() -> Bool {
run_cross_tree_import_green_receipt()
}

fn witness_dsl_shell_primary_precedence_holds() -> Bool {
run_dsl_shell_primary_precedence_receipt()
}

fn witness_perturb_optional_skew_goes_red() -> Bool {
run_perturb_optional_skew_red_receipt()
}

test fn dsl_compile_clean_witnesses() -> Bool {
witness_clean_tree_compile_holds() && witness_perturb_optional_skew_goes_red()
witness_clean_tree_compile_holds()
&& witness_cross_tree_import_compiles_green()
&& witness_dsl_shell_primary_precedence_holds()
&& witness_perturb_optional_skew_goes_red()
}
5 changes: 4 additions & 1 deletion dsl/tools/dsl_compile_clean_gate.dag
Original file line number Diff line number Diff line change
@@ -1,9 +1,12 @@
// tools/dsl_compile_clean_gate.dag — whole-tree dsl/ compile-clean gate, run by `gunbc`.
// tools/dsl_compile_clean_gate.dag — whole-tree dsl/ compile-clean gate (dual-root pools), run by `gunbc`.
//
// Run in CI:
// cargo run -p v1-compiler --release --bin gunbc -- run \
// --source-root dsl --entry dsl/tools/dsl_compile_clean_gate.dag --function main
//
// Transport compiles every .dag under dsl/ with witness_layer_roots (dsl + src/v2) as import
// pools — see tools.dsl_compile_clean_transport header for indexing semantics.
//
// SCAFFOLD — uses `--target rust` pending v1.compiler.dag_collect identity-key fix (180
// collisions on `--target dag` emit); flip to `--target dag` when that backend bug lands.
// Parse→resolve→typecheck front-end is identical; rust emit proves the tree is well-typed.
Expand Down
146 changes: 120 additions & 26 deletions dsl/tools/dsl_compile_clean_transport.dag
Original file line number Diff line number Diff line change
@@ -1,8 +1,16 @@
// tools/dsl_compile_clean_transport.dag — shell transport for whole-tree dsl/ compile-clean.
//
// Host runs `gunbc compile --source-root <dsl> --target rust` over the live tree (GREEN) and
// a perturb receipt (RED: planted fresh-name unimported module resolved against the live
// dsl/ index as dependency pool — no cp -r + cold whole-tree rebuild).
// Host runs `gunbc compile` over the live dsl/ tree (GREEN) with witness_layer_roots as the
// dependency pool (§3 single authority: dsl first, src/v2 second) and
// `--dependency-pool-index primary-precedence` (primary root authoritative; pool fills absent
// paths only — NOT global last-wins). gunbc indexes every .dag under all --source-root flags
// under all --source-root flags into the module pool, but only compiles entry modules from
// the FIRST root (load_sources / Compile in cli_run.rs); later roots are import pools only —
// adding src/v2 does NOT cold-compile the whole v2 tree, only modules pulled by dsl imports.
//
// Also runs:
// * perturb RED receipt — planted bad module fails typecheck against the live pools;
// * cross-tree GREEN receipt — planted dsl module importing v2.* resolves and compiles.
//
// Both transports are modeled off hand-written `let script = "..."` blobs onto structured
// `ShellProgram`s rendered by `serialize_bash` (extdeps.languages.bash.program). The shared
Expand All @@ -12,6 +20,7 @@
module tools.dsl_compile_clean_transport

import extdeps.shell
import gunbc.ci_layer_roots { witness_layer_roots }
import extdeps.languages.bash.program {
ShellProgram, ShellStmt, ShellWord,
Command, Assign, If, Subshell, AndOr, WithRedir, Heredoc, Exit,
Expand All @@ -21,21 +30,32 @@ import extdeps.languages.bash.program {
}
import tools.host_prelude { ensure_gunbc_built }

// set -e; <prelude>; OUT=$(mktemp -d); "$GUNBC" compile --source-root "$ROOT"/dsl ... ; rm -rf "$OUT"
// --source-root <r> for every witness_layer_root (§3 — same roots as the rest of CI).
fn dcc_source_root_flags() -> List<ShellWord> {
fold(witness_layer_roots, init: [], f: (acc, r) => concat(acc, [lit(text: "--source-root"), lit(text: r)]))
}

fn dcc_pool_index_flags() -> List<ShellWord> {
[lit(text: "--dependency-pool-index"), lit(text: "primary-precedence")]
}

// set -e; <prelude>; cd "$ROOT"; OUT=$(mktemp -d); "$GUNBC" compile <witness roots> ... ; rm -rf "$OUT"
fn clean_tree_compile_program() -> ShellProgram {
let root = var_ref(name: "ROOT")
let gunbc = var_ref(name: "GUNBC")
let out = var_ref(name: "OUT")
ShellProgram {
set_e: true,
statements: concat(ensure_gunbc_built(), [
command(words: [lit(text: "cd"), root]),
assign(name: "OUT", value: CmdSubst { body: command(words: [lit(text: "mktemp"), lit(text: "-d")]) }),
command(words: [
gunbc, lit(text: "compile"),
lit(text: "--source-root"), Concat { parts: [root, lit(text: "/dsl")] },
lit(text: "--output-dir"), out,
lit(text: "--target"), lit(text: "rust")
]),
command(words: concat(
[gunbc, lit(text: "compile")],
concat(dcc_source_root_flags(), concat(dcc_pool_index_flags(), [
lit(text: "--output-dir"), out,
lit(text: "--target"), lit(text: "rust")
]))
)),
command(words: [lit(text: "rm"), lit(text: "-rf"), out])
])
}
Expand All @@ -49,22 +69,24 @@ fn run_clean_tree_compile() -> Bool {
// The planted module whose legacy Some/None on a builtin T? must fail typecheck.
data perturb_module_source: String = "module test.perturb_compile_clean_red\nfn probe() -> String? {\n match Present { value: \"x\" } {\n Some { value: s } => Some { value: s }\n None => none\n }\n}"

// RED receipt: plant the fresh-name unimported bad module; resolve against the live dsl/
// index (second --source-root) as dependency pool — no cp -r + cold whole-tree rebuild.
// Compile MUST fail (if it succeeds → exit 1).
// set -e; <prelude>; TMP=$(mktemp -d)
// cat > "$TMP"/_perturb_compile_clean_red.dag <<'PERTURB' ... PERTURB
// if "$GUNBC" compile --source-root "$TMP" --source-root "$ROOT"/dsl \
// --output-dir "$TMP"/out --target rust >/dev/null 2>&1
// then rm -rf "$TMP"; exit 1; fi
// rm -rf "$TMP"; exit 0
// Planted dsl module that imports v2.* — must compile when pools include src/v2.
data cross_tree_green_module_source: String = "module test.perturb_compile_clean_cross_tree_green\nimport v2.std.logic { Bool }\nfn probe() -> Bool { True }"

// Discriminating primary-precedence receipt: shell.Env exists only in dsl extdeps.shell (~101 lines);
// v2 overlay (~34 lines) has shell.Exec only — last-wins would misresolve and fail typecheck.
data dsl_shell_primary_module_source: String = "module test.perturb_compile_clean_dsl_shell_primary\nimport extdeps.shell\nfn probe() -> String? {\n shell.Env.Get(name: \"PATH\")\n}"

// RED receipt: plant the fresh-name unimported bad module; resolve against witness_layer_roots
// as dependency pools — no cp -r + cold whole-tree rebuild. Compile MUST fail (if it succeeds
// → exit 1).
fn compile_clean_perturb_program() -> ShellProgram {
let root = var_ref(name: "ROOT")
let gunbc = var_ref(name: "GUNBC")
let tmp = var_ref(name: "TMP")
ShellProgram {
set_e: true,
statements: concat(ensure_gunbc_built(), [
command(words: [lit(text: "cd"), root]),
assign(name: "TMP", value: CmdSubst { body: command(words: [lit(text: "mktemp"), lit(text: "-d")]) }),
Heredoc {
path: Concat { parts: [tmp, lit(text: "/_perturb_compile_clean_red.dag")] },
Expand All @@ -73,13 +95,13 @@ fn compile_clean_perturb_program() -> ShellProgram {
},
If {
cond: WithRedir {
stmt: command(words: [
gunbc, lit(text: "compile"),
lit(text: "--source-root"), tmp,
lit(text: "--source-root"), Concat { parts: [root, lit(text: "/dsl")] },
lit(text: "--output-dir"), Concat { parts: [tmp, lit(text: "/out")] },
lit(text: "--target"), lit(text: "rust")
]),
stmt: command(words: concat(
[gunbc, lit(text: "compile"), lit(text: "--source-root"), tmp],
concat(dcc_source_root_flags(), concat(dcc_pool_index_flags(), [
lit(text: "--output-dir"), Concat { parts: [tmp, lit(text: "/out")] },
lit(text: "--target"), lit(text: "rust")
]))
)),
redir: StdoutAndStderrToNull
},
then: [
Expand All @@ -97,3 +119,75 @@ fn run_perturb_optional_skew_red_receipt() -> Bool {
let result = shell.Exec.Run(script: serialize_bash(p: compile_clean_perturb_program()))
result.success
}

// GREEN receipt: planted dsl module imports v2.std.logic; first --source-root is TMP (entry
// tree), witness_layer_roots are dependency pools — compile must succeed (set -e).
fn compile_cross_tree_green_program() -> ShellProgram {
let root = var_ref(name: "ROOT")
let gunbc = var_ref(name: "GUNBC")
let tmp = var_ref(name: "TMP")
let out = var_ref(name: "OUT")
ShellProgram {
set_e: true,
statements: concat(ensure_gunbc_built(), [
command(words: [lit(text: "cd"), root]),
assign(name: "TMP", value: CmdSubst { body: command(words: [lit(text: "mktemp"), lit(text: "-d")]) }),
Heredoc {
path: Concat { parts: [tmp, lit(text: "/_perturb_compile_clean_cross_tree_green.dag")] },
delimiter: "CROSS_TREE_GREEN",
body: cross_tree_green_module_source
},
assign(name: "OUT", value: CmdSubst { body: command(words: [lit(text: "mktemp"), lit(text: "-d")]) }),
command(words: concat(
[gunbc, lit(text: "compile"), lit(text: "--source-root"), tmp],
concat(dcc_source_root_flags(), concat(dcc_pool_index_flags(), [
lit(text: "--output-dir"), out,
lit(text: "--target"), lit(text: "rust")
]))
)),
command(words: [lit(text: "rm"), lit(text: "-rf"), out]),
command(words: [lit(text: "rm"), lit(text: "-rf"), tmp])
])
}
}

fn run_cross_tree_import_green_receipt() -> Bool {
let result = shell.Exec.Run(script: serialize_bash(p: compile_cross_tree_green_program()))
result.success
}

// GREEN receipt: primary root entry calls shell.Env (dsl-only service); pools supply v2 paths
// absent from dsl — extdeps.shell must stay on the dsl row, not the v2 overlay.
fn compile_dsl_shell_primary_precedence_program() -> ShellProgram {
let root = var_ref(name: "ROOT")
let gunbc = var_ref(name: "GUNBC")
let tmp = var_ref(name: "TMP")
let out = var_ref(name: "OUT")
ShellProgram {
set_e: true,
statements: concat(ensure_gunbc_built(), [
command(words: [lit(text: "cd"), root]),
assign(name: "TMP", value: CmdSubst { body: command(words: [lit(text: "mktemp"), lit(text: "-d")]) }),
Heredoc {
path: Concat { parts: [tmp, lit(text: "/_perturb_compile_clean_dsl_shell_primary.dag")] },
delimiter: "DSL_SHELL_PRIMARY",
body: dsl_shell_primary_module_source
},
assign(name: "OUT", value: CmdSubst { body: command(words: [lit(text: "mktemp"), lit(text: "-d")]) }),
command(words: concat(
[gunbc, lit(text: "compile"), lit(text: "--source-root"), tmp],
concat(dcc_source_root_flags(), concat(dcc_pool_index_flags(), [
lit(text: "--output-dir"), out,
lit(text: "--target"), lit(text: "rust")
]))
)),
command(words: [lit(text: "rm"), lit(text: "-rf"), out]),
command(words: [lit(text: "rm"), lit(text: "-rf"), tmp])
])
}
}

fn run_dsl_shell_primary_precedence_receipt() -> Bool {
let result = shell.Exec.Run(script: serialize_bash(p: compile_dsl_shell_primary_precedence_program()))
result.success
}
Loading
Loading