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
13 changes: 13 additions & 0 deletions dag/test/claim/transport_emission_not_modeled_witness_test.dag
Original file line number Diff line number Diff line change
Expand Up @@ -39,6 +39,8 @@ data file_transport_source: String = "module tfx_file\nservice Fs \{\n operatio

data rest_and_shell_source: String = "module tfx_ok\nservice Sh \{\n operation ListDirs \{\n input \{ path: String \}\n output \{ dirs: String from \"stdout_lines\" \}\n readonly\n transport shell \{ argv: [\"find\", \"\{path\}\", \"-type\", \"d\"] \}\n \}\n\}\n\nservice Net \{\n config \{\n endpoint: \"https://example.invalid\"\n \}\n operation Fetch \{\n input \{ id: String \}\n output \{ body: String from \"body\" \}\n readonly\n transport rest \{ method: GET, path: \"/things/\{id\}\" \}\n \}\n\}\n"

data pathless_transport_source: String = "module tfx_nopath\nservice Fs \{\n operation Write \{\n input \{ path: String, content: String \}\n output \{ success: Bool from \"write_success\" \}\n transport file \{ \}\n \}\n\}\n"

data mixed_transport_source: String = "module tfx_mixed\nservice Mixed \{\n config \{\n endpoint: \"https://example.invalid\"\n \}\n operation Fetch \{\n input \{ id: String \}\n output \{ body: String from \"body\" \}\n readonly\n transport rest \{ method: GET, path: \"/things/\{id\}\" \}\n \}\n operation ListDirs \{\n input \{ path: String \}\n output \{ dirs: String from \"stdout_lines\" \}\n readonly\n transport shell \{ argv: [\"find\", \"\{path\}\", \"-type\", \"d\"] \}\n \}\n operation Read \{\n input \{ path: String \}\n output \{ content: String from \"content\" \}\n readonly\n transport file \{ path: \"\{path\}\" \}\n \}\n\}\n"

// The three discriminating REDs, one per FileEmissionRefusal arm the rust handler can meet. Each
Expand Down Expand Up @@ -74,6 +76,17 @@ test fn w_fully_declared_file_transport_module_is_clean_of_all_blocking_diagnost
blocking_diagnostic_count(source: file_transport_source) == 0
}

// A `transport file` with no `path:` is refused at PARSE, so the state is unrepresentable rather
// than caught downstream. The row asserts a blocking diagnostic AND ZERO of the emission class --
// that pairing is what distinguishes "parse refused it" from "emission refused it", which a single
// count could not. Before this change the parser substituted an empty string literal, so
// `transport file \{ \}` and `transport file \{ path: "" \}` became the SAME node and both emitted a
// host write against the empty path with no diagnostic at all (measured, not inferred).
test fn w_pathless_file_transport_refuses_at_parse_not_emission() -> Bool {
blocking_diagnostic_count(source: pathless_transport_source) > 0
&& not_modeled_blocking_count(source: pathless_transport_source) == 0
}

test fn w_rest_and_shell_transports_emit_without_refusal() -> Bool {
not_modeled_blocking_count(source: rest_and_shell_source) == 0
}
Expand Down
18 changes: 14 additions & 4 deletions src/v1/02_parse.dag
Original file line number Diff line number Diff line change
Expand Up @@ -3022,16 +3022,26 @@ fn parse_file_binding_body(tokens: TokenStream, ctx: ParseContext) -> TransportR
parse_file_fields(tokens: tokens, ctx: ctx, base_path: none, verb: none)
}

// A `transport file` with no `path:` REFUSES rather than standing in an empty string literal.
// The substitution that stood here was a fabricated plausible value (DESIGN §5), and its cost
// was not merely a bad default: it collapsed two states into one node. "no path was declared"
// and "the path was declared as the empty string" became byte-identical downstream, so no
// consumer could tell them apart -- and both emitted a host write to "" with no diagnostic,
// measured, while the interpreter realization of the SAME declaration refuses an empty path at
// runtime ("file transport resolved to an empty path"). Refusing here makes the first state
// unrepresentable rather than merely detected. The second state stays authorable and keeps its
// existing answer: the rust handler emits the interpreter's own guard beside the path binding
// (v1.compiler.emit_rust file_empty_path_guard), so an authored empty path refuses at run time.
fn parse_file_fields(tokens: TokenStream, ctx: ParseContext, base_path: Node?, verb: Node?) -> TransportResult {
let tokens = skip_newlines(tokens: tokens)
let span = token_span(tok: token_stream_first(stream: tokens))
let dummy = local_transport_node(span: span)
if tok_is_rbrace(tok: token_stream_first(stream: tokens)) || tok_is_eof(tok: token_stream_first(stream: tokens)) {
let bp = match base_path {
Present { value: e } => e
Absent => make_expr_node(expr_data: ExprLiteral { value: LitStr { value: "" } }, children: [], inferred: none, span: no_span())
match base_path {
Absent => TransportResult { transport: dummy, tokens: tokens, ctx: ctx, err: Present { value: parse_error(msg: "`transport file` declares no `path:` -- a file transport names the path it acts on, and there is nothing to substitute for it", span: span) } }
Present { value: bp } =>
TransportResult { transport: file_transport_node(base_path: bp, verb: verb, span: span), tokens: tokens, ctx: ctx, err: none }
}
TransportResult { transport: file_transport_node(base_path: bp, verb: verb, span: span), tokens: tokens, ctx: ctx, err: none }
} else {
let r = expect_ident(tokens: tokens)
if has_err(err: r.err) { return TransportResult { transport: dummy, tokens: r.tokens, ctx: ctx, err: r.err } }
Expand Down
6 changes: 3 additions & 3 deletions src/v1/stage0/src/v1_compiler_emit_rust.rs
Original file line number Diff line number Diff line change
Expand Up @@ -30826,7 +30826,7 @@ pub fn emit_file_path_line(
});
let fmt_str = Rc::new({
let mut __result = Vec::new();
for p in parts.clone().iter().cloned() {
for p in parts.iter().cloned() {
__result.push(match (*p.clone()).clone() {
StringPart::Text { value: v, .. } => escape_rust_interp_text(v.clone()),
StringPart::Interpolation { expr: _, .. } => "{}".to_string(),
Expand All @@ -30837,7 +30837,7 @@ pub fn emit_file_path_line(
.join(&"".to_string());
let args = Rc::new({
let mut __result = Vec::new();
for p in parts.clone().iter().cloned() {
for p in parts.iter().cloned() {
__result.extend(
(*match (*p.clone()).clone() {
StringPart::Text { value: _, .. } => Rc::new(vec![]),
Expand Down Expand Up @@ -31043,7 +31043,7 @@ pub fn emit_file_return(
let fields = file_output_channel_fields(op_node.clone());
let field_exprs = Rc::new({
let mut __result = Vec::new();
for ch in fields.clone().iter().cloned() {
for ch in fields.iter().cloned() {
__result.push(emit_file_channel_expr(
file_output_channel_of_field(ch.clone(), source_indices.clone()),
(ch.return_cardinality.clone() == Cardinality::CardOptional),
Expand Down
37 changes: 18 additions & 19 deletions src/v1/stage0/src/v1_compiler_parse.rs
Original file line number Diff line number Diff line change
Expand Up @@ -8047,25 +8047,24 @@ pub fn parse_file_fields(
if (tok_is_rbrace(token_stream_first(tokens.clone()))
|| tok_is_eof(token_stream_first(tokens.clone())))
{
let bp = match base_path.clone() {
Some(e) => e.clone(),
None => make_expr_node(
Rc::new(ExprData::ExprLiteral {
value: Rc::new(LiteralValue::LitStr {
value: "".to_string(),
}),
}),
Rc::new(vec![]),
None,
no_span(),
),
};
break Rc::new(TransportResult {
transport: file_transport_node(bp.clone(), verb.clone(), span.clone()),
tokens: tokens.clone(),
ctx: ctx.clone(),
err: None,
});
match base_path.clone() {
None => {
break Rc::new(TransportResult {
transport: dummy.clone(),
tokens: tokens.clone(),
ctx: ctx.clone(),
err: Some(parse_error("`transport file` declares no `path:` -- a file transport names the path it acts on, and there is nothing to substitute for it".to_string(), span.clone())),
});
}
Some(bp) => {
break Rc::new(TransportResult {
transport: file_transport_node(bp.clone(), verb.clone(), span.clone()),
tokens: tokens.clone(),
ctx: ctx.clone(),
err: None,
});
}
}
} else {
let r = expect_ident(tokens.clone());
if has_err(r.err.clone()) {
Expand Down
Loading