diff --git a/dag/extdeps/filesystem/filesystem_io.dag b/dag/extdeps/filesystem/filesystem_io.dag index b17c0373e10..e132823804c 100644 --- a/dag/extdeps/filesystem/filesystem_io.dag +++ b/dag/extdeps/filesystem/filesystem_io.dag @@ -41,7 +41,7 @@ service Filesystem { input { path: String } output { content: String from "content" - success: Bool from "write_success" + success: Bool from "read_success" error: String from "error" } readonly @@ -51,7 +51,7 @@ service Filesystem { operation Delete { input { path: String } output { - success: Bool from "write_success" + success: Bool from "delete_success" error: String from "error" } transport file { path: "{path}", verb: "delete" } @@ -60,8 +60,8 @@ service Filesystem { operation List { input { path: String } output { - entries: String from "content" - success: Bool from "write_success" + entries: String from "entries" + success: Bool from "list_success" error: String from "error" } readonly diff --git a/dag/test/claim/transport_emission_not_modeled_witness_test.dag b/dag/test/claim/transport_emission_not_modeled_witness_test.dag index 82a2f0d68a5..eda001fe7e8 100644 --- a/dag/test/claim/transport_emission_not_modeled_witness_test.dag +++ b/dag/test/claim/transport_emission_not_modeled_witness_test.dag @@ -35,7 +35,7 @@ data live_tree_disposition: LiveTreeDisposition = SubstrateInputsOnly // 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 wall via compile_dag_diagnostic_census (rust target). A service whose operations declare `transport file` with a modeled verb, a renderable path and modeled output channels must now EMIT with zero TransportEmissionNotModeled rows; an operation declaring an unmodeled verb, an unmodeled output channel, or a payload verb with no `content` input must refuse with exactly one counted row. The mixed row is the discriminator: it pins both the emission and the refusal to the OPERATION rather than to the service or the module, so a wall that poisoned every sibling operation -- or a handler that emitted every sibling regardless of its declaration -- would go red here while the single-operation rows 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 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\", success: Bool from \"read_success\" \}\n readonly\n transport file \{ path: \"\{path\}\" \}\n \}\n operation Delete \{\n input \{ path: String \}\n output \{ success: Bool from \"delete_success\" \}\n transport file \{ path: \"\{path\}\", verb: \"delete\" \}\n \}\n operation List \{\n input \{ path: String \}\n output \{ entries: String from \"entries\", success: Bool from \"list_success\" \}\n readonly\n transport file \{ path: \"\{path\}\", verb: \"list\" \}\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" diff --git a/src/v1/05_emit.dag b/src/v1/05_emit.dag index 00ed20913fa..74743d64093 100644 --- a/src/v1/05_emit.dag +++ b/src/v1/05_emit.dag @@ -1049,11 +1049,11 @@ fn transport_binding_refusal_fact(cause: TransportBindingRefusal) -> String { // The single authority for which declared output keys the file realization can // answer. `is_modeled_file_output_channel` is derived from it. fn file_result_channel_of_key(key: String) -> FileResultChannel? { - if key == "write_success" || key == "success" { Present { value: FileChanSuccess } } + if key == "write_success" || key == "read_success" || key == "delete_success" || key == "list_success" || key == "success" { Present { value: FileChanSuccess } } else if key == "bytes_written" || key == "bytes" || key == "byte_count" { Present { value: FileChanByteCount } } else if key == "path" { Present { value: FileChanPath } } else if key == "error" { Present { value: FileChanError } } - else if key == "content" { Present { value: FileChanContent } } + else if key == "content" || key == "entries" { Present { value: FileChanContent } } else { none } } @@ -2108,7 +2108,7 @@ fn file_emission_refusal_fact(refusal: FileEmissionRefusal) -> String { "' writes a payload, and the operation declares no `content` input to write -- the payload is an input to the operation, never a value the emitter may invent") FileOutputKeyNotModeled { key: k } => concat("file transport output key '", k, - "' has no modeled channel -- the modeled channels are write_success, success, bytes_written, bytes, byte_count, path, error and content") + "' has no modeled channel -- the modeled channels are write_success, read_success, delete_success, list_success, success, bytes_written, bytes, byte_count, path, error, content and entries") FileOutputShapeNotModeled => "the file transport operation's declared output must be a product of named fields; the emitted realization answers per FIELD, so a return shape with no fields to answer for has no rendering" } diff --git a/src/v1/05_emit_rust.dag b/src/v1/05_emit_rust.dag index e4fcf1eea64..8b3361565fc 100644 --- a/src/v1/05_emit_rust.dag +++ b/src/v1/05_emit_rust.dag @@ -12012,7 +12012,7 @@ fn emit_file_channel_expr(channel: FileResultChannel, is_optional: Bool) -> Stri // one-tuple. The `from` key was read off the FIELD at binding time WITHOUT // unwrapping the product -- unwrapping collapses a one-field product to the // field's own type and loses the key, which would answer a declared -// `success: Bool from "write_success"` with the content channel and emit a String +// `success: Bool from "read_success"` with the content channel and emit a String // against a bool. fn emit_file_return(result_fields: List) -> String { let field_exprs = result_fields |> map(f => emit_file_channel_expr(channel: f.channel, is_optional: f.optional)) diff --git a/src/v1/stage0/src/v1_compiler_emit.rs b/src/v1/stage0/src/v1_compiler_emit.rs index ecb4562cdeb..bff8c8b48ff 100644 --- a/src/v1/stage0/src/v1_compiler_emit.rs +++ b/src/v1/stage0/src/v1_compiler_emit.rs @@ -2294,7 +2294,12 @@ pub fn transport_binding_refusal_fact(cause: Rc) -> Str } pub fn file_result_channel_of_key(key: String) -> Option { - if ((key.clone() == "write_success".to_string()) || (key.clone() == "success".to_string())) { + if (((((key.clone() == "write_success".to_string()) + || (key.clone() == "read_success".to_string())) + || (key.clone() == "delete_success".to_string())) + || (key.clone() == "list_success".to_string())) + || (key.clone() == "success".to_string())) + { Some(FileResultChannel::FileChanSuccess) } else { if (((key.clone() == "bytes_written".to_string()) || (key.clone() == "bytes".to_string())) @@ -2308,7 +2313,9 @@ pub fn file_result_channel_of_key(key: String) -> Option { if (key.clone() == "error".to_string()) { Some(FileResultChannel::FileChanError) } else { - if (key.clone() == "content".to_string()) { + if ((key.clone() == "content".to_string()) + || (key.clone() == "entries".to_string())) + { Some(FileResultChannel::FileChanContent) } else { None @@ -4521,7 +4528,7 @@ pub fn file_emission_refusal_fact(refusal: Rc) -> String { FileEmissionRefusal::FileVerbNotModeled { verb: v, .. } => v1_rt::concat(v1_rt::concat("file transport verb '".to_string(), v.clone()), "' is not a modeled action -- the modeled verbs are delete, list and write_owner_only, and an absent verb means write when the operation declares a `content` input and read otherwise".to_string()), FileEmissionRefusal::FilePathNotStaticallyRenderable => "the file transport `path:` must be a string literal or a string interpolation over the operation inputs; no other expression shape has a rendering".to_string(), FileEmissionRefusal::FileWriteMissingContentInput { verb: v, .. } => v1_rt::concat(v1_rt::concat("file transport verb '".to_string(), v.clone()), "' writes a payload, and the operation declares no `content` input to write -- the payload is an input to the operation, never a value the emitter may invent".to_string()), - FileEmissionRefusal::FileOutputKeyNotModeled { key: k, .. } => v1_rt::concat(v1_rt::concat("file transport output key '".to_string(), k.clone()), "' has no modeled channel -- the modeled channels are write_success, success, bytes_written, bytes, byte_count, path, error and content".to_string()), + FileEmissionRefusal::FileOutputKeyNotModeled { key: k, .. } => v1_rt::concat(v1_rt::concat("file transport output key '".to_string(), k.clone()), "' has no modeled channel -- the modeled channels are write_success, read_success, delete_success, list_success, success, bytes_written, bytes, byte_count, path, error, content and entries".to_string()), FileEmissionRefusal::FileOutputShapeNotModeled => "the file transport operation's declared output must be a product of named fields; the emitted realization answers per FIELD, so a return shape with no fields to answer for has no rendering".to_string(), } } diff --git a/src/v1/stage0/src/v1_interpreter.rs b/src/v1/stage0/src/v1_interpreter.rs index fca0df4f594..b53462d276a 100644 --- a/src/v1/stage0/src/v1_interpreter.rs +++ b/src/v1/stage0/src/v1_interpreter.rs @@ -10144,11 +10144,13 @@ fn map_file_outputs( let from_key = extract_from_key(child, ctx); let key = from_key.as_deref().unwrap_or(field_name.as_str()); let value = match key { - "write_success" | "success" => Value::Bool(result.success), + "write_success" | "read_success" | "delete_success" | "list_success" | "success" => { + Value::Bool(result.success) + } "bytes_written" | "bytes" | "byte_count" => Value::Int(result.byte_count), "path" => str_value(result.path.clone()), "error" => str_value(result.error.clone()), - "content" => str_value(result.content.clone()), + "content" | "entries" => str_value(result.content.clone()), _ => Value::Null, }; fields.push((ctx.sym(&field_name), value));