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
66 changes: 66 additions & 0 deletions dag/test/claim/transport_emission_not_modeled_witness_test.dag
Original file line number Diff line number Diff line change
@@ -0,0 +1,66 @@
module test.claim.transport_emission_not_modeled_witness

import gunbc.compile_diagnostic_census {
CompileDiagnosticCensus,
CensusObserved,
CensusNotRunnable,
census_blocking_rows,
census_rows_of_class,
census_total_count,
}
import v2.std.live_tree { LiveTreeDisposition, SubstrateInputsOnly }

data live_tree_disposition: LiveTreeDisposition = SubstrateInputsOnly

// Permanent regression control for the `transport file` emission refusal (DESIGN §4b(4): a climb
// deletes the production machinery it obsoletes, but the discriminating RED and its positive
// control STAY ENROLLED as the executing evidence that the higher rung is still real -- deleting
// the evidence with the machinery would recreate specification-without-execution one rung up).
//
// What the deleted machinery did: three per-target renderers each fabricated a read of
// `base_path + "/" + operation_name` for EVERY file operation, so a declared Write emitted a read
// of a path the declaration never named, dropped its `content` argument, and returned a String
// against a declared bool -- output that does not compile in Rust, Go or Python. The refusal that
// replaced it is minted once, before target-specific rendering, in emit_artifact.
//
// The two shell/rest rows are NOT decoration. Without them this file cannot distinguish "the file
// arm refuses" from "the transport dispatch is broken for everything", which is the failure mode
// that would make a green suite defend a total outage.
data transport_emission_not_modeled_witness_note: String = "Paired control for the file-transport emission refusal via compile_dag_diagnostic_census. A service whose operations declare `transport file` must refuse with exactly one counted TransportEmissionNotModeled per file operation; rest and shell operations must remain unaffected, both alone and when declared beside a file operation in the same module. The mixed row is the discriminator: it pins the refusal to the OPERATION rather than to the service or the module, so a wall that poisoned every sibling operation would go red here while the file-only row stayed green."

data file_transport_source: String = "module tfx_file\nservice Fs \{\n operation Write \{\n input \{ path: String, content: String \}\n output \{ success: Bool from \"write_success\" \}\n transport file \{ path: \"\{path\}\" \}\n \}\n operation Read \{\n input \{ path: String \}\n output \{ content: String from \"content\" \}\n readonly\n transport file \{ path: \"\{path\}\" \}\n \}\n operation Delete \{\n input \{ path: String \}\n output \{ success: Bool from \"write_success\" \}\n transport file \{ path: \"\{path\}\", verb: \"delete\" \}\n \}\n\}\n"

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 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"

fn not_modeled_blocking_count(source: String) -> Int {
match compile_dag_diagnostic_census(source) {
CensusObserved { rows: rows } =>
census_total_count(rows: census_blocking_rows(rows: census_rows_of_class(rows: rows, wanted: "TransportEmissionNotModeled")))
CensusNotRunnable { cause: _ } => -1
}
}

fn blocking_diagnostic_count(source: String) -> Int {
match compile_dag_diagnostic_census(source) {
CensusObserved { rows: rows } => census_total_count(rows: census_blocking_rows(rows: rows))
CensusNotRunnable { cause: _ } => -1
}
}

test fn w_file_transport_operations_each_refuse_emission() -> Bool {
not_modeled_blocking_count(source: file_transport_source) == 3
}

test fn w_rest_and_shell_transports_emit_without_refusal() -> Bool {
not_modeled_blocking_count(source: rest_and_shell_source) == 0
}

test fn w_rest_and_shell_transports_are_clean_of_all_blocking_diagnostics() -> Bool {
blocking_diagnostic_count(source: rest_and_shell_source) == 0
}

test fn w_only_the_file_operation_refuses_among_its_siblings() -> Bool {
not_modeled_blocking_count(source: mixed_transport_source) == 1
}
12 changes: 12 additions & 0 deletions src/v1/00_core.dag
Original file line number Diff line number Diff line change
Expand Up @@ -196,6 +196,15 @@ type CompilerDiagnostic
| CallNamedArgOnFunctionValue { callee: String, argument: String, span: SourceSpan }
| OccurrenceTransportViolation { refusal: OccurrenceTransportRefusal }
| ContainerSpellingUnrecognized { name: String, container_leaf: String, span: SourceSpan }
| TransportEmissionNotModeled {
transport_kind: String,
service: String,
operation: String,
declaring_module: String,
target: String,
missing_realization_fact: String,
span: SourceSpan
}

type ErrorNode {
diagnostic: CompilerDiagnostic
Expand Down Expand Up @@ -329,6 +338,7 @@ fn diagnostic_to_span(d: CompilerDiagnostic) -> SourceSpan {
Absent => no_span()
}
ContainerSpellingUnrecognized { name: _, container_leaf: _, span: s } => s
TransportEmissionNotModeled { transport_kind: _, service: _, operation: _, declaring_module: _, target: _, missing_realization_fact: _, span: s } => s
}
}

Expand Down Expand Up @@ -402,6 +412,8 @@ fn diagnostic_to_message(d: CompilerDiagnostic) -> String {
occurrence_transport_refusal_diagnostic_message(refusal: refusal)
ContainerSpellingUnrecognized { name: n, container_leaf: leaf, span: _ } =>
concat("unrecognized container spelling '", n, "': its last segment '", leaf, "' names a container, but no arity is declared for '", n, "' in std.types container_type_arity — declare the row or spell the container by a declared name")
TransportEmissionNotModeled { transport_kind: kind, service: svc, operation: op, declaring_module: m, target: tgt, missing_realization_fact: missing, span: _ } =>
concat("'", kind, "' transport emission is not modeled: operation '", svc, ".", op, "' declared in '", m, "' cannot be emitted for target '", tgt, "' -- ", missing, ". Bind a realization handler for the '", kind, "' transport (DESIGN §3: interface shape and transport are two facts); do not add a per-target renderer")
}
}

Expand Down
112 changes: 109 additions & 3 deletions src/v1/05_emit.dag
Original file line number Diff line number Diff line change
Expand Up @@ -2,7 +2,7 @@ module v1.compiler.emit

import std.syntax { LiteralValue, BinOp, AlgebraFieldKind }
import v1.std.core {
Node, ErrorNode, InferredNode, Resolved, CompilerError, TypeVariable, is_compiler_error,
Node, ErrorNode, make_error_node, TransportEmissionNotModeled, InferredNode, Resolved, CompilerError, TypeVariable, is_compiler_error,
module_imports, module_items, param_node_name_at, param_node_type_expr,
param_node_default_value, NewlineIndex, authored_name_at, empty_intern_table,
expr_var_name_at, expr_call_func_at, let_binding_name_at, field_access_field_at, ExprData,
Expand Down Expand Up @@ -936,12 +936,11 @@ fn emit_unified_transport_dispatch(
target: RenderTarget,
render_rest: fn(String, Node, Int, Map<String, NewlineIndex>) -> String,
render_shell: fn(String, Node, Int, Map<String, NewlineIndex>) -> String,
render_file: fn(String, Int) -> String,
render_local: fn(String, Int) -> String
) -> String {
if is_rest_transport(t: transport, source_indices: source_indices) { render_rest(op_name, transport, depth, source_indices) }
else if is_shell_transport(t: transport) { render_shell(op_name, transport, depth, source_indices) }
else if is_file_transport(t: transport, source_indices: source_indices) { render_file(op_name, depth) }
else if is_file_transport(t: transport, source_indices: source_indices) { emit_unmodeled_file_transport_refusal(op_name: op_name, target: target) }
else if is_local_transport(t: transport, source_indices: source_indices) { render_local(op_name, depth) }
else { emit_error_expr(message: "unrecognized transport kind", target: target) }
}
Expand Down Expand Up @@ -1738,6 +1737,113 @@ fn emit_error_expr(message: String, target: RenderTarget) -> String {
apply_type_template1(template: spec.error_expr_template, arg0: msg)
}

// `transport file` has no emitted realization. The defect this replaces was not a renderer bug
// and not primarily a binding gap: it is SEMANTIC INFORMATION LOSS AT THE DISPATCH BOUNDARY.
// The declaration carries a verb, a path template, input bindings and an output contract; this
// dispatch handed the renderer a name and an indent depth; the renderer could observe none of it.
// The three target renderers that stood here were therefore downstream of one defect rather than
// three peers, which is why all three are deleted rather than the Rust one repaired.
//
// What they did: Rust emit_file_call, Python emit_py_file_call and Go emit_go_file_call each
// fabricated `read(base_path + "/" + op_name)` for EVERY operation, so a declared Write emitted a
// read of a path the declaration never named, dropped its `content` argument, and returned a
// String against a declared bool. None of the three produced output that compiles. That is
// DESIGN §5's fabricated plausible output -- below the ladder, not a low rung on it -- so
// refusing is a climb and costs no capability: there was never a working file emission to remove.
//
// The refusal is minted ONCE, before any target-specific rendering, by
// unmodeled_file_transport_diagnostics via emit_artifact: a module declaring a file-transport
// operation emits NO file and yields a typed, located, counted TransportEmissionNotModeled.
// One refusal serves all targets rather than three saying the same thing. Counted is the point
// (DESIGN §5): a refusal whose frequency is observable is how we learn a real consumer arrived,
// and its absence is how this decayed unnoticed until someone happened to look.
//
// emit_unmodeled_file_transport_refusal below is the FLOOR beneath that wall, in the dispatch arm
// itself. It is unreachable while the wall stands and is still required: is_local_transport is
// DEFINED as "not rest, not shell, not file", so deleting the file arm would route a file
// transport into render_local and fabricate a direct function call by omission.
//
// NEXT-RUNG TRIGGER (DESIGN §4b(2) -- waiting on a named event, not stalled): this class climbs
// when a real consumer needs a file transport emitted. The repair is then the §3 one -- interface
// shape and transport are two facts, so the emitters bind a realization handler rather than each
// inlining one -- and NOT a fourth per-target renderer. THREADING THE PATH ALONE DOES NOT CLOSE
// IT, and the trigger says so in its own text because a narrow reading solves a third of the
// problem and looks finished: the deleted renderers also dropped `content` and returned a String
// against a declared bool, and neither is a path problem. The interface must carry the verb, the
// resolved path template, the operation input bindings, the payload/content input, the declared
// output type, and the failure/effect semantics.
//
// Deliberately unbuilt today (DESIGN §6 -- work is priced in displaced cost): six operations
// across two modules, no production consumer. Building the full binding for a surface nobody
// reaches is the purity trap the design document names.
//
// The interpreter realization (v1_interpreter dispatch_file) is unaffected and remains the
// working one: it reads the same declaration correctly, substituting the path template and
// dispatching on `verb`. Nothing here changes an interpreted effect.
fn render_target_name(target: RenderTarget) -> String {
match target {
Rust => "rust"
Python => "python"
Go => "go"
Dag => "dag"
}
}

// The semantic the dispatch could not supply. Stated as the work rather than as a shrug, so the
// person who eventually fires the trigger reads the shape of the job off the diagnostic itself.
data unmodeled_file_transport_missing_fact: String = "the file transport dispatch supplies only the operation name and an indent depth; emitting this operation requires the declared verb, the resolved path template, the operation input bindings, the payload/content input, the declared output type, and the failure/effect semantics"

// Mirrors emit_unified_transport_dispatch's precedence rather than testing is_file_transport
// alone: the dispatch tries rest, then shell, then file, so a transport carrying more than one key
// is emitted by the FIRST arm that claims it. Asking only "is it file?" would refuse an operation
// the dispatch would in fact have emitted as rest or shell -- two authorities for one ordering,
// agreeing today by coincidence rather than by construction (DESIGN §3).
fn is_file_transport_after_dispatch_precedence(t: Node, source_indices: Map<String, NewlineIndex>) -> Bool {
if is_rest_transport(t: t, source_indices: source_indices) { false }
else if is_shell_transport(t: t) { false }
else { is_file_transport(t: t, source_indices: source_indices) }
}

fn unmodeled_file_transport_operation_diagnostics(tm: TypedModule, item: Node, target: RenderTarget) -> List<ErrorNode> {
let env = tm.type_env
let si = env.source_indices
let module_name = authored_name(env: env, node: tm.module)
let service_name = authored_name(env: env, node: item)
let fallback = service_fallback_transport(item: item)
item.children |> flat_map(op_node => {
let t = effective_operation_transport(op_node: op_node, fallback: fallback)
if is_file_transport_after_dispatch_precedence(t: t, source_indices: si) {
[make_error_node(
diagnostic: TransportEmissionNotModeled {
transport_kind: "file",
service: service_name,
operation: authored_name(env: env, node: op_node),
declaring_module: module_name,
target: render_target_name(target: target),
missing_realization_fact: unmodeled_file_transport_missing_fact,
span: op_node.span
},
module_name: module_name)]
} else { [] }
})
}

fn unmodeled_file_transport_diagnostics(typed: ResolvedGraph, target: RenderTarget) -> List<ErrorNode> {
typed.modules |> flat_map(tm =>
tm.items
|> filter(item => is_service_item(item: item))
|> flat_map(item => unmodeled_file_transport_operation_diagnostics(tm: tm, item: item, target: target))
)
}

fn emit_unmodeled_file_transport_refusal(op_name: String, target: RenderTarget) -> String {
emit_error_expr(
message: concat(
"file transport emission is not modeled for operation '", op_name, "' (target ",
render_target_name(target: target), ") -- ", unmodeled_file_transport_missing_fact),
target: target)
}

fn emit_lambda_params(param_names: List<String>, target: RenderTarget) -> String {
let spec = language_spec(target: target)
let param_strs = param_names |> map(p =>
Expand Down
14 changes: 1 addition & 13 deletions src/v1/05_emit_go.dag
Original file line number Diff line number Diff line change
Expand Up @@ -20,8 +20,7 @@ import v1.std.core {
expr_method_call_semantics, record_lit_type_name_at, lambda_body, cast_expr, cast_target,
return_value, foreach_variable_at, foreach_collection, foreach_body, method_arg_nodes,
index_base, index_expr, slice_base, slice_start, slice_end, with_required_cardinality,
Connective, Conj, Disj, CardOptional, is_rest_transport, is_shell_transport,
is_file_transport
Connective, Conj, Disj, CardOptional, is_rest_transport, is_shell_transport
}

import v1.compiler.artifact { RenderTarget, Go }
Expand Down Expand Up @@ -441,7 +440,6 @@ fn emit_go_transport_body(transport: Node, op_name: String, source_indices: Map<
transport: transport, op_name: op_name, source_indices: source_indices, depth: depth, target: Go,
render_rest: (n, t, d, si) => emit_go_rest_call(op_name: n, transport: t, depth: d, source_indices: si),
render_shell: (n, t, d, si) => emit_go_shell_call(op_name: n, transport: t, depth: d, source_indices: si),
render_file: (n, d) => emit_go_file_call(op_name: n, depth: d),
render_local: (n, d) => emit_go_local_call(op_name: n, depth: d))
}

Expand Down Expand Up @@ -515,16 +513,6 @@ fn emit_go_shell_call(op_name: String, transport: Node, depth: Int, source_indic
all_lines |> join(separator: "\n")
}

fn emit_go_file_call(op_name: String, depth: Int) -> String {
let prefix = make_indent(level: depth)
concat(
prefix, "path := fmt.Sprintf(\"%s/", to_snake(name: op_name), "\", c.BasePath)\n",
"data, err := os.ReadFile(path)\n",
"if err != nil {\n\treturn \"\", fmt.Errorf(\"reading file: %w\", err)\n}\n",
"return string(data), nil"
)
}

fn emit_go_local_call(op_name: String, depth: Int) -> String {
let prefix = make_indent(level: depth)
concat(prefix, "// Local binding -- direct function call\n",
Expand Down
12 changes: 1 addition & 11 deletions src/v1/05_emit_python.dag
Original file line number Diff line number Diff line change
Expand Up @@ -20,7 +20,7 @@ import v1.std.core {
cast_expr, cast_target, return_value, foreach_variable_at, foreach_collection, foreach_body,
method_arg_nodes, index_base, index_expr, slice_base, slice_start, slice_end,
with_required_cardinality, Connective, Conj, Disj, CardOptional, is_rest_transport,
is_shell_transport, is_file_transport
is_shell_transport
}

import v1.compiler.artifact { RenderTarget, Python }
Expand Down Expand Up @@ -411,7 +411,6 @@ fn emit_py_transport_body(transport: Node, op_name: String, source_indices: Map<
transport: transport, op_name: op_name, source_indices: source_indices, depth: depth, target: Python,
render_rest: (n, t, d, si) => emit_py_rest_call(op_name: n, transport: t, source_indices: si),
render_shell: (n, t, d, si) => emit_py_shell_call(op_name: n, transport: t, source_indices: si),
render_file: (n, d) => emit_py_file_call(op_name: n),
render_local: (n, d) => emit_py_local_call(op_name: n))
}

Expand Down Expand Up @@ -487,15 +486,6 @@ fn emit_py_shell_call(op_name: String, transport: Node, source_indices: Map<Stri
)
}

fn emit_py_file_call(op_name: String) -> String {
let self_base_path = concat("{", "self.base_path", "}")
concat(
"path = f\"", self_base_path, "/", emit_ident(name: op_name, target: Python), "\"\n",
"with open(path) as f:\n",
" return f.read()"
)
}

fn emit_py_local_call(op_name: String) -> String {
concat("# Local binding -- direct function call\n",
"return ", emit_ident(name: op_name, target: Python), "()")
Expand Down
Loading