Skip to content
Merged
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
88 changes: 88 additions & 0 deletions src/v1/compiler_tests_rust.dag
Original file line number Diff line number Diff line change
Expand Up @@ -2785,6 +2785,93 @@ fn ct_declared_type_conformance_witness_test() -> String {
" }\n\n")
}

fn ct_shell_service_output_projection_known_hole_probe_test() -> String {
concat(
" // KNOWN-HOLE PROBE (not a desired-behavior control), DESIGN section 4b(4).\n",
" //\n",
" // The shell service-emission path FABRICATES rather than refuses: every declared\n",
" // output field is bound to `stdout`, whatever source the declaration named, and the\n",
" // error arm returns a bare String against a declared Box<dyn std::error::Error>.\n",
" // Both produce Rust that does not compile, with ZERO diagnostics -- section 5's\n",
" // fabricated-plausible-output arm, in the emitter.\n",
" //\n",
" // The three-output fixture is load-bearing. The two-field case this was first seen\n",
" // on (an operation declaring `success: Bool from \"exit_success\"` beside\n",
" // `stdout: String from \"stdout\"`) cannot distinguish \"wrong tuple index\" from \"the\n",
" // declared source never arrived\": with two fields, \"always the first output\" and\n",
" // \"always stdout\" produce the same bytes. Three fields separate them, and the\n",
" // ABSENCE of the `let stderr = ...` prelude line is the positive evidence -- that\n",
" // line is emitted only when some field claims the stderr channel, so its absence\n",
" // proves the `from \"stderr\"` field was invisible to the renderer rather than\n",
" // mis-ordered. child_from_key returns Absent for all three.\n",
" //\n",
" // WHEN THE WALL LANDS THIS PROBE MUST FLIP and become a permanent regression\n",
" // control: the emitted body must bind each field to its named source, box the error\n",
" // arm, and REFUSE -- typed and located, naming the field and the unresolvable\n",
" // source -- for any source it cannot realize.\n",
" #[test]\n",
" fn shell_service_output_projection_fabricates_stdout_known_hole_probe() {\n",
" let result = std::thread::Builder::new()\n",
" .stack_size(32 * 1024 * 1024)\n",
" .spawn(|| {\n",
" let source = std::rc::Rc::new(crate::v1_compiler_compile::SourceFile {\n",
" path: \"probe.dag\".to_string(),\n",
" content: \"module probe\\nservice Probe {\\n operation Version {\\n input {}\\n output {\\n success: Bool from \\\"exit_success\\\"\\n out: String from \\\"stdout\\\"\\n err: String from \\\"stderr\\\"\\n }\\n transport shell { argv: [\\\"git\\\", \\\"--version\\\"] }\\n }\\n}\\n\".to_string(),\n",
" });\n",
" let r = crate::v1_compiler_compile::compile_sources(\n",
" std::rc::Rc::new(im::vector![source]),\n",
" crate::v1_compiler_artifact::RenderTarget::Rust,\n",
" );\n",
" let errors: Vec<_> = r\n",
" .diagnostics\n",
" .iter()\n",
" .filter(|d| crate::v1_std_core::is_error_diagnostic(d.diagnostic.clone()))\n",
" .collect();\n",
" assert!(\n",
" errors.is_empty(),\n",
" \"KNOWN HOLE today: the emitter does not refuse; it fabricates silently. \\\n",
" When the wall lands this becomes the refusal assertion. Got: {:?}\",\n",
" errors\n",
" );\n",
" let emitted = r\n",
" .files\n",
" .iter()\n",
" .find(|f| f.path == \"src/probe.rs\")\n",
" .map(|f| f.content.clone())\n",
" .expect(\"service module must emit src/probe.rs\");\n",
"\n",
" // The signature reads the declaration correctly...\n",
" assert!(\n",
" emitted.contains(\n",
" \"-> Result<(bool, String, String), Box<dyn std::error::Error>>\"\n",
" ),\n",
" \"signature must project the three declared output types, got:\\n{}\",\n",
" emitted\n",
" );\n",
" // ...and the body then ignores every declared source.\n",
" assert!(\n",
" emitted.contains(\"Ok((stdout.clone(), stdout.clone(), stdout.clone()))\"),\n",
" \"KNOWN HOLE: every output field is bound to stdout regardless of its \\\n",
" declared source. If this assertion fails the wall may have landed -- \\\n",
" flip this probe to assert the correct per-channel binding. Got:\\n{}\",\n",
" emitted\n",
" );\n",
" // The stderr prelude is the absence that proves the source was never read.\n",
" assert!(\n",
" !emitted.contains(\"String::from_utf8_lossy(&output.stderr)\"),\n",
" \"KNOWN HOLE: the `from \\\"stderr\\\"` field is invisible to the renderer, \\\n",
" so no stderr prelude line is emitted. Got:\\n{}\",\n",
" emitted\n",
" );\n",
" })\n",
" .expect(\"failed to spawn thread\")\n",
" .join();\n",
" result\n",
" .expect(\"shell_service_output_projection_fabricates_stdout_known_hole_probe panicked\");\n",
" }\n",
"\n")
}

fn compiler_tests_source() -> String {
concat(
ct_module_header(),
Expand All @@ -2800,6 +2887,7 @@ fn compiler_tests_source() -> String {
ct_call_shape_duplicate_wall_witness_test(),
ct_function_value_named_application_controls_witness_test(),
ct_function_value_field_method_known_hole_probe_test(),
ct_shell_service_output_projection_known_hole_probe_test(),
ct_method_existence_wall_witness_test(),
ct_declared_type_conformance_witness_test(),
ct_sole_constructor_test(),
Expand Down
83 changes: 83 additions & 0 deletions src/v1/stage0/src/compiler_tests.rs
Original file line number Diff line number Diff line change
Expand Up @@ -856,6 +856,89 @@ mod compiler_tests {
);
}

// KNOWN-HOLE PROBE (not a desired-behavior control), DESIGN section 4b(4).
//
// The shell service-emission path FABRICATES rather than refuses: every declared
// output field is bound to `stdout`, whatever source the declaration named, and the
// error arm returns a bare String against a declared Box<dyn std::error::Error>.
// Both produce Rust that does not compile, with ZERO diagnostics -- section 5's
// fabricated-plausible-output arm, in the emitter.
//
// The three-output fixture is load-bearing. The two-field case this was first seen
// on (an operation declaring `success: Bool from "exit_success"` beside
// `stdout: String from "stdout"`) cannot distinguish "wrong tuple index" from "the
// declared source never arrived": with two fields, "always the first output" and
// "always stdout" produce the same bytes. Three fields separate them, and the
// ABSENCE of the `let stderr = ...` prelude line is the positive evidence -- that
// line is emitted only when some field claims the stderr channel, so its absence
// proves the `from "stderr"` field was invisible to the renderer rather than
// mis-ordered. child_from_key returns Absent for all three.
//
// WHEN THE WALL LANDS THIS PROBE MUST FLIP and become a permanent regression
// control: the emitted body must bind each field to its named source, box the error
// arm, and REFUSE -- typed and located, naming the field and the unresolvable
// source -- for any source it cannot realize.
#[test]
fn shell_service_output_projection_fabricates_stdout_known_hole_probe() {
let result = std::thread::Builder::new()
.stack_size(32 * 1024 * 1024)
.spawn(|| {
let source = std::rc::Rc::new(crate::v1_compiler_compile::SourceFile {
path: "probe.dag".to_string(),
content: "module probe\nservice Probe {\n operation Version {\n input {}\n output {\n success: Bool from \"exit_success\"\n out: String from \"stdout\"\n err: String from \"stderr\"\n }\n transport shell { argv: [\"git\", \"--version\"] }\n }\n}\n".to_string(),
});
let r = crate::v1_compiler_compile::compile_sources(
std::rc::Rc::new(im::vector![source]),
crate::v1_compiler_artifact::RenderTarget::Rust,
);
let errors: Vec<_> = r
.diagnostics
.iter()
.filter(|d| crate::v1_std_core::is_error_diagnostic(d.diagnostic.clone()))
.collect();
assert!(
errors.is_empty(),
"KNOWN HOLE today: the emitter does not refuse; it fabricates silently. \
When the wall lands this becomes the refusal assertion. Got: {:?}",
errors
);
let emitted = r
.files
.iter()
.find(|f| f.path == "src/probe.rs")
.map(|f| f.content.clone())
.expect("service module must emit src/probe.rs");

// The signature reads the declaration correctly...
assert!(
emitted.contains(
"-> Result<(bool, String, String), Box<dyn std::error::Error>>"
),
"signature must project the three declared output types, got:\n{}",
emitted
);
// ...and the body then ignores every declared source.
assert!(
emitted.contains("Ok((stdout.clone(), stdout.clone(), stdout.clone()))"),
"KNOWN HOLE: every output field is bound to stdout regardless of its \
declared source. If this assertion fails the wall may have landed -- \
flip this probe to assert the correct per-channel binding. Got:\n{}",
emitted
);
// The stderr prelude is the absence that proves the source was never read.
assert!(
!emitted.contains("String::from_utf8_lossy(&output.stderr)"),
"KNOWN HOLE: the `from \"stderr\"` field is invisible to the renderer, \
so no stderr prelude line is emitted. Got:\n{}",
emitted
);
})
.expect("failed to spawn thread")
.join();
result
.expect("shell_service_output_projection_fabricates_stdout_known_hole_probe panicked");
}

#[test]
fn method_existence_wall_witness() {
// DISCRIMINATING RED for method_existence_wall_note. Before the wall an
Expand Down
Loading
Loading