Skip to content
Closed
4 changes: 2 additions & 2 deletions dag/gunbc/auth/approval_store_receipt.dag
Original file line number Diff line number Diff line change
Expand Up @@ -2,7 +2,7 @@ module gunbc.auth.approval_store_receipt

import std.logic { Bool }
import std.types { NonEmptyStr, Timestamp, String, Int, List }
import v2.std.algebra { skip }
import v2.std.algebra { skip, length }
import std.optional { Present, Absent }
import std.scoped_authorization { AttemptIdentity }
import std.durable_compare_and_set { cas_generation_first }
Expand Down Expand Up @@ -249,7 +249,7 @@ fn receipt_line_at(lines: List<String>, i: Int) -> String {

fn request_field(line: String, key: String) -> String {
let prefix = join([key, "="], "")
if starts_with(s: line, prefix: prefix) { substring(s: line, start: string_length(s: prefix), end: string_length(s: line)) } else { "" }
if starts_with(s: line, prefix: prefix) { substring(s: line, start: length(xs: prefix), end: length(xs: line)) } else { "" }
}

// THE WIRE A RECEIPT TRAVELS AS: its signing input, then its tag, one line each. The signing input
Expand Down
23 changes: 21 additions & 2 deletions dag/gunbc/instruments/native_emission_controls.dag
Original file line number Diff line number Diff line change
@@ -1,7 +1,7 @@
module gunbc.instruments.native_emission_controls

import std.types { Bool, Int, List, NonEmptyStr, Set, String }
import v2.std.algebra { filter }
import v2.std.algebra { filter, length }
import std.list { duplicated_by_key }
import gunbc.instruments.native_emission_controls_homonym { ControlBoxed, narrow_slot_value, narrow_slots_equal }
import std.resource_contract { Observation, Read }
Expand Down Expand Up @@ -481,6 +481,22 @@ fn control_outcome_is_bad(o: ControlOutcome<Int, String>) -> Bool {
}
}

// RULE: `v2.std.algebra` `length` over HOST text (kernel `String`) lowers to
// `v1_rt::string_length`. Corpus `v2.std.text.String` is structural FreeMonoid and keeps the
// generic body. Without the host arm, kernel `String` at `request_field` is E0308; with a
// leaf-name arm, structural text at `string_split_step` is E0308 the other way.
fn control_algebra_length_of_string(s: String) -> Int {
length(xs: s)
}

fn algebra_length_on_string_cases() -> List<NativeEmissionCase> {
[
NativeEmissionCase { identity: "algebra_length_of_a_string_counts_scalars", held: control_algebra_length_of_string(s: "abc") == 3 },
NativeEmissionCase { identity: "algebra_length_of_a_string_red_is_not_another_count", held: control_algebra_length_of_string(s: "abc") != 4 },
NativeEmissionCase { identity: "algebra_length_of_a_list_is_unchanged", held: length(xs: ["a", "b"]) == 2 }
]
}

fn fold_accumulator_formals_cases() -> List<NativeEmissionCase> {
[
NativeEmissionCase { identity: "fold_constructor_init_sums_all_nonnegative", held: control_outcome_good_value(o: control_sum_until_negative(xs: [1, 2, 3])) == 6 },
Expand Down Expand Up @@ -526,6 +542,9 @@ data native_emission_expected_identities: List<String> = [
"effectful_fold_step_red_empty_keeps_init",
"capability_alias_output_octet_in_range",
"capability_alias_output_red_octet_out_of_range",
"algebra_length_of_a_string_counts_scalars",
"algebra_length_of_a_string_red_is_not_another_count",
"algebra_length_of_a_list_is_unchanged",
"fold_constructor_init_sums_all_nonnegative",
"fold_constructor_init_red_negative_switches_arm",
"fold_constructor_init_red_empty_keeps_init",
Expand All @@ -543,7 +562,7 @@ data native_emission_expected_identities: List<String> = [
]

fn native_emission_cases() -> List<NativeEmissionCase> {
concat(concat(concat(concat(concat(same_leaf_declaration_cases(), concat(concat(concat(concat(concat(concat(header_bound_cases(), fn_value_bound_cases()), filter_in_branch_condition_cases()), claim_driver_filesystem_cases()), effectful_fold_step_cases()), capability_alias_output_cases()), fold_accumulator_formals_cases())), list_index_cases()), effectful_generic_return_cases()), generic_empty_map_turbofish_cases()), data_literal_tree_cases())
concat(concat(concat(concat(concat(concat(same_leaf_declaration_cases(), concat(concat(concat(concat(concat(concat(header_bound_cases(), fn_value_bound_cases()), filter_in_branch_condition_cases()), claim_driver_filesystem_cases()), effectful_fold_step_cases()), capability_alias_output_cases()), fold_accumulator_formals_cases())), list_index_cases()), effectful_generic_return_cases()), generic_empty_map_turbofish_cases()), data_literal_tree_cases()), algebra_length_on_string_cases())
}

fn case_row(c: NativeEmissionCase) -> String {
Expand Down
52 changes: 52 additions & 0 deletions dag/test/claim/infer_algebra_length_homonym_witness_test.dag
Original file line number Diff line number Diff line change
@@ -0,0 +1,52 @@
module test.claim.infer_algebra_length_homonym_witness

import extdeps.filesystem.filesystem_io
import std.types { Bool, String }
import v2.std.live_tree { LiveTreeDisposition, ReadsLiveTree }

data live_tree_disposition: LiveTreeDisposition = ReadsLiveTree

// THE SAME-LEAF CONTROL THE ACCEPTED CORPUS CANNOT CARRY. A second `fn length` under dag/ or
// src/v2 makes every bare `length` an unimported two-declarer (floor). The specimen is therefore
// a fixture outside those roots, compiled here through compile_dag_rust_emit_check — the same
// isolated nested-compile shape #13459 used for a kernel-name collision that must not be
// ingestible. The file is the authority; this module reads it.
//
// WHAT WOULD GO RED UNDER THE OLD LEAF PREDICATE. That predicate rewrote any host-String call
// whose callee *leaf* was `length` to `v1_rt::string_length`. This fixture's `probe` calls a
// `length` whose decl_name is `length` and whose owner is `algebra_length_homonym_probe`. The
// identity gate leaves the constant body; the leaf predicate would emit `v1_rt::string_length`
// and this exclude-list would fail.

data algebra_length_homonym_probe_path: String = "fixtures/algebra_length_homonym/probe.dag"

fn algebra_length_homonym_probe_source() -> String {
filesystem_read(path: algebra_length_homonym_probe_path).content
}

test fn a_user_length_on_host_string_is_not_emitted_as_string_length() -> Bool {
compile_dag_rust_emit_check(
algebra_length_homonym_probe_source(),
"src/algebra_length_homonym_probe.rs",
["99"],
["v1_rt::string_length"]
)
}

test fn algebra_length_on_host_string_still_lowers_to_string_length() -> Bool {
compile_dag_rust_emit_check(
"module algebra_length_host_probe\nimport std.types { String, Int }\nimport v2.std.algebra { length }\nfn probe(s: String) -> Int { length(xs: s) }\n",
"src/algebra_length_host_probe.rs",
["v1_rt::string_length(&"],
["v2_std_algebra::length("]
)
}

test fn host_text_receiver_length_lowers_to_string_length() -> Bool {
compile_dag_rust_emit_check(
"module host_text_length_method_probe\nimport std.types { String, Int }\nfn probe(s: String) -> Int { s.length() }\n",
"src/host_text_length_method_probe.rs",
["string_length"],
[]
)
}
13 changes: 13 additions & 0 deletions fixtures/algebra_length_homonym/probe.dag
Original file line number Diff line number Diff line change
@@ -0,0 +1,13 @@
module algebra_length_homonym_probe

import std.types { String, Int }

// A user `length` whose leaf is the algebra op's leaf and whose owner is not v2.std.algebra.
// Lives under fixtures/ so the accepted corpus (dag + src/v2) never grows a second `fn length`
// (floor: every bare `length` would then be an unimported two-declarer). Compiled only by
// test.claim.infer_algebra_length_homonym_witness.
fn length(xs: String) -> Int { 99 }

fn probe() -> Int {
length(xs: "abc")
}
62 changes: 61 additions & 1 deletion src/v1/05_emit_rust.dag
Original file line number Diff line number Diff line change
Expand Up @@ -12629,6 +12629,52 @@ fn lambda_argument_scope(arg: Node, scope: InferScope) -> InferScope {
// emit_func_def names the declaration it renders on the body scope (caller_decl_name) so that read
// has a subject.

// ONE HOST-TEXT DISCRIMINATOR FOR BOTH SPELLINGS. AlgebraMethodSemantics remaps `.length` on a
// host-string receiver to `string_length`; the function form `v2.std.algebra` `length` over
// `FreeMonoid<Char>` is that operation spelled as a call. Kernel `String` inhabits the monoid, so
// `length(xs: s)` is legal source. Emitting it as the generic FreeMonoid body (`Rc<Vec<T>>`) is
// E0308 against the host `String` at `request_field`. `v2.std.text.String` is the other carrier:
// the structural alias `FreeMonoid<Char>` (`Rc<Vec<i64>>` here). Rewriting THAT call (or
// `.length` on it) to `v1_rt::string_length` is E0308 the other way (self-host `v2_std_text.rs`
// `string_split_step`). Both arms ask `is_host_text_typed_expr` — leaf name `String` is not enough.
// THE CALLEE IS THE DECLARATION, NOT THE LEAF. A call spelled `length` that resolves to another
// module's function (or a local) must emit that function; rewriting by the authored name would
// replace a byte-count or a constant with a scalar count and answer wrongly in silence.
fn rust_call_target_is_v2_algebra_length(target: CallTargetIdentity) -> Bool {
match rust_call_target_declared_length(target: target) {
Absent => false
Present { value: id } =>
id.decl_name == "length" && id.owner_module_path == "v2.std.algebra"
}
}

fn rust_call_target_declared_length(target: CallTargetIdentity) -> DeclaredCallableIdentity? {
match target {
SourceDeclarationCall { owner_module_path: owner, decl_name: decl } =>
Present { value: DeclaredCallableIdentity { owner_module_path: owner, decl_name: decl } }
RuntimePrimitiveCall { primitive_name: _, projected_from: projected } => projected
LocallyBoundCall { name: _ } => none
CallableTargetUndetermined => none
}
}

fn rust_emit_length_on_host_string(call_target: CallTargetIdentity, func: String, args: List<Node>, call_semantics: CallSemantics?, registry: Map<String, ItemInfo>, scope: InferScope, depth: Int, shared_types: Set<String>, emit_info: EmitGraphInfo) -> String? {
if rust_call_target_is_v2_algebra_length(target: call_target) == false { none } else {
let length_args = order_typed_call_args_from_semantics(args: args, func: func, call_semantics: call_semantics, scope: scope)
match length_args |> first {
Absent => none
Present { value: xs_arg } =>
if is_host_text_typed_expr(e: arg_value(n: xs_arg), source_indices: scope.type_env.source_indices) {
Present { value: concat(
"v1_rt::string_length(&",
emit_typed_expr_base(texpr: arg_value(n: xs_arg), registry: registry, scope: scope, depth: depth, shared_types: shared_types, emit_info: emit_info),
")"
) }
} else { none }
}
}
}

fn emit_typed_call(func: String, args: List<Node>, inferred: InferredNode?, call_semantics: CallSemantics?, callee_is_function_value: Bool, call_target: CallTargetIdentity, registry: Map<String, ItemInfo>, scope: InferScope, depth: Int, shared_types: Set<String>, emit_info: EmitGraphInfo) -> String {
if callee_is_function_value {
return emit_typed_function_value_call(func: func, args: args, registry: registry, scope: scope, depth: depth, shared_types: shared_types, emit_info: emit_info)
Expand Down Expand Up @@ -12709,6 +12755,10 @@ fn emit_typed_call(func: String, args: List<Node>, inferred: InferredNode?, call
}
return disc_result
}
match rust_emit_length_on_host_string(call_target: call_target, func: func, args: args, call_semantics: call_semantics, registry: registry, scope: scope, depth: depth, shared_types: shared_types, emit_info: emit_info) {
Present { value: lowered } => return lowered
Absent => {}
}
let ordered_args = order_typed_call_args_from_semantics(args: args, func: func, call_semantics: call_semantics, scope: scope)
let application_plan = call_semantics_supplied_application_plan(cs: call_semantics)
let callee = match call_target {
Expand Down Expand Up @@ -13695,7 +13745,7 @@ fn emit_typed_method_call(method_call_node: Node, receiver: Node, method: String

let method_name_raw = authored_name_at(source_indices: scope.type_env.source_indices, node: method_def)
let method_name = if method_name_raw == "length" {
if is_string_typed_expr(e: receiver, source_indices: scope.type_env.source_indices) { "string_length" } else { "count" }
if is_host_text_typed_expr(e: receiver, source_indices: scope.type_env.source_indices) { "string_length" } else { "count" }
} else { method_name_raw }
let algebra_field_call = rust_callable_field_method_call(method_name: method_name, receiver: receiver, args: args, registry: registry, scope: scope, depth: depth, shared_types: shared_types, emit_info: emit_info)
if algebra_field_call != none {
Expand Down Expand Up @@ -15774,6 +15824,16 @@ fn is_string_typed_expr(e: Node, source_indices: Map<String, NewlineIndex>) -> B
}
}

fn is_host_text_typed_expr(e: Node, source_indices: Map<String, NewlineIndex>) -> Bool {
match e.inferred {
Present { value: Resolved { node: rt } } =>
let is_optional = rt.return_cardinality == CardOptional
let inner = if is_optional { with_required_cardinality(n: rt) } else { rt }
is_host_text_carrier_type(n: inner, source_indices: source_indices)
_ => false
}
}

fn emit_typed_string_interp(parts: List<StringPart>, registry: Map<String, ItemInfo>, scope: InferScope, depth: Int, shared_types: Set<String>, emit_info: EmitGraphInfo) -> String {
let has_interpolations = parts |> any(p => match p { Interpolation { expr: _ } => true _ => false })
let fmt_parts = parts |> map(p => typed_interp_format_part(part: p, registry: registry, scope: scope, depth: depth, shared_types: shared_types, emit_info: emit_info, has_interpolations: has_interpolations))
Expand Down
116 changes: 115 additions & 1 deletion src/v1/stage0/src/v1_compiler_emit_rust.rs
Original file line number Diff line number Diff line change
Expand Up @@ -26715,6 +26715,88 @@ pub fn lambda_argument_scope(arg: Rc<Node>, scope: Rc<InferScope>) -> Rc<InferSc
}
}

pub fn rust_call_target_is_v2_algebra_length(target: Rc<CallTargetIdentity>) -> bool {
match rust_call_target_declared_length(target.clone()) {
std::option::Option::None => false,
Some(id) => {
((id.decl_name.clone() == "length".to_string())
&& (id.owner_module_path.clone() == "v2.std.algebra".to_string()))
}
}
}

pub fn rust_call_target_declared_length(
target: Rc<CallTargetIdentity>,
) -> Option<Rc<DeclaredCallableIdentity>> {
match (*target.clone()).clone() {
CallTargetIdentity::SourceDeclarationCall {
owner_module_path: owner,
decl_name: decl,
..
} => Some(Rc::new(DeclaredCallableIdentity {
owner_module_path: owner.clone(),
decl_name: decl.clone(),
})),
CallTargetIdentity::RuntimePrimitiveCall {
projected_from: projected,
..
} => projected.clone(),
CallTargetIdentity::LocallyBoundCall { name: _, .. } => std::option::Option::None,
CallTargetIdentity::CallableTargetUndetermined => std::option::Option::None,
}
}

pub fn rust_emit_length_on_host_string(
call_target: Rc<CallTargetIdentity>,
func: String,
args: Rc<Vec<Rc<Node>>>,
call_semantics: Option<Rc<CallSemantics>>,
registry: Rc<HashMap<String, Rc<ItemInfo>>>,
scope: Rc<InferScope>,
depth: i64,
shared_types: Rc<BTreeSet<String>>,
emit_info: Rc<EmitGraphInfo>,
) -> Option<String> {
if (rust_call_target_is_v2_algebra_length(call_target.clone()) == false) {
std::option::Option::None
} else {
{
let length_args = crate::v1_compiler_emit::order_typed_call_args_from_semantics(
args.clone(),
func.clone(),
call_semantics.clone(),
scope.clone(),
);
match length_args.clone().first().cloned() {
std::option::Option::None => std::option::Option::None,
Some(xs_arg) => {
if is_host_text_typed_expr(
crate::v1_std_core::arg_value(xs_arg.clone()),
scope.type_env.clone().source_indices.clone(),
) {
Some(v1_rt::concat(
v1_rt::concat(
"v1_rt::string_length(&".to_string(),
emit_typed_expr_base(
crate::v1_std_core::arg_value(xs_arg.clone()),
registry.clone(),
scope.clone(),
depth.clone(),
shared_types.clone(),
emit_info.clone(),
),
),
")".to_string(),
))
} else {
std::option::Option::None
}
}
}
}
}
}

pub fn emit_typed_call(
func: String,
args: Rc<Vec<Rc<Node>>>,
Expand Down Expand Up @@ -26994,6 +27076,20 @@ pub fn emit_typed_call(
return disc_result;
}
}
match rust_emit_length_on_host_string(
call_target.clone(),
func.clone(),
args.clone(),
call_semantics.clone(),
registry.clone(),
scope.clone(),
depth.clone(),
shared_types.clone(),
emit_info.clone(),
) {
Some(lowered) => return lowered.clone(),
std::option::Option::None => {}
}
let ordered_args = crate::v1_compiler_emit::order_typed_call_args_from_semantics(
args.clone(),
func.clone(),
Expand Down Expand Up @@ -30044,7 +30140,7 @@ pub fn emit_typed_method_call(
method_def.clone(),
);
let method_name = if (method_name_raw.clone() == "length".to_string()) {
if is_string_typed_expr(
if is_host_text_typed_expr(
receiver.clone(),
scope.type_env.clone().source_indices.clone(),
) {
Expand Down Expand Up @@ -35283,6 +35379,24 @@ pub fn is_string_typed_expr(
}
}

pub fn is_host_text_typed_expr(
e: Rc<Node>,
source_indices: Rc<HashMap<String, Rc<NewlineIndex>>>,
) -> bool {
match e.inferred.clone().as_deref().cloned() {
Some(InferredNode::Resolved { node: rt, .. }) => {
let is_optional = (rt.return_cardinality.clone() == Cardinality::CardOptional);
let inner = if is_optional.clone() {
crate::v1_std_core::with_required_cardinality(rt.clone())
} else {
rt.clone()
};
is_host_text_carrier_type(inner.clone(), source_indices.clone())
}
_ => false,
}
}

pub fn emit_typed_string_interp(
parts: Rc<Vec<Rc<StringPart>>>,
registry: Rc<HashMap<String, Rc<ItemInfo>>>,
Expand Down
Loading