diff --git a/src/v1/stage0/src/coproduct_reflection.rs b/src/v1/stage0/src/coproduct_reflection.rs index e5debcc0e58..ddb7b29ce3c 100644 --- a/src/v1/stage0/src/coproduct_reflection.rs +++ b/src/v1/stage0/src/coproduct_reflection.rs @@ -7,7 +7,7 @@ use crate::v1_interpreter::{ }; use crate::v1_std_core::{ authored_name_at, expr_var_name_at, field_node_type_expr, inferred_to_node, param_node_name_at, - Connective, ExprData, NewlineIndex, Node, VarBindingKind, + source_text_at, Connective, ExprData, NewlineIndex, Node, VarBindingKind, }; pub(crate) const NULLARY_PAYLOAD_TYPE_NAME: &str = "coproduct_nullary_payload"; @@ -1197,6 +1197,92 @@ pub fn eval_fn_arrow_decl_facts_live( Ok(crate::v1_interpreter::list_value(rows)) } +fn literal_source_lexeme( + node: &Rc, + si: &Rc>>, +) -> Option { + let index = si.get(&node.span.file)?; + let text = source_text_at(index.clone(), node.span.clone()); + if text.is_empty() { + None + } else { + Some(text) + } +} + +fn data_init_literal_fingerprint( + body: &Rc, + si: &Rc>>, +) -> Option { + // Encoding must match `v2.std.data_index` (`literal_fingerprint_*_lexeme`). + let lexeme = literal_source_lexeme(body, si)?; + match body.expr_data.as_ref() { + ExprData::ExprLiteral { value, .. } => match value.as_ref() { + crate::std_syntax::LiteralValue::LitInt { .. } + | crate::std_syntax::LiteralValue::LitFloat { .. } => Some(format!("num:{lexeme}")), + crate::std_syntax::LiteralValue::LitBool { .. } => Some(format!("bool:{lexeme}")), + // Str uses decoded content, not source lexeme: witness RHS is a skeleton atom + // name (bare content), so this matches `literal_fingerprint_str_content` when the + // initializer is a plain quoted literal without escapes. + crate::std_syntax::LiteralValue::LitStr { value: s, .. } => { + Some(format!("str:\"{s}\"")) + } + _ => None, + }, + _ => None, + } +} + +// Corpus-wide data-init reflection: sibling of `eval_fn_arrow_decl_facts_live` and +// `eval_concept_decl_facts_live`. Yields one `DataInitDecl` per `ItemKind::DataItem` whose +// initializer is a literal, carrying `literal_fp` for literal-mirror detection in +// `v2.lens.no_dual_representation_test`. Host SOURCE half; dissolves with +// `fn_arrow_decl_facts_live` / `concept_decl_facts_live` on the same gunbc#5364 +// corpus-as-node accessor widen trigger named in `v2.lens.wiring_liveness`'s +// construction_justification. Fingerprint encoding spec: `v2.std.data_index` +// (`literal_fingerprint_*_lexeme`); this host block is a transient SOURCE projection on +// the gunbc#5364 corpus-accessor widen — not an independent authority. +pub fn eval_data_init_decl_facts_live( + ctx: &InterpContext, + _args: &[(Option, Value)], +) -> InterpResult { + let si = ctx.source_indices(); + let mut rows: Vec = Vec::new(); + for module in ctx.modules.iter() { + for item in module.items.iter() { + let name = authored_name_at(si.clone(), item.clone()); + if name.is_empty() { + continue; + } + let info = module + .item_registry + .get(&name) + .or_else(|| module.item_registry.get(&item.name)); + let Some(info) = info else { continue }; + if info.kind != ItemKind::DataItem { + continue; + } + let Some(body) = item.body.as_ref() else { + continue; + }; + let Some(literal_fp) = data_init_literal_fingerprint(body, &si) else { + continue; + }; + let qualified_name = logical_qualified_name(&info.module_name, &name); + rows.push(Value::Record { + type_name: ctx.sym("DataInitDecl"), + fields: Rc::new(sorted_fields(vec![ + (ctx.sym("qualified_name"), Value::Str(qualified_name)), + (ctx.sym("module"), Value::Str(info.module_name.clone())), + (ctx.sym("name"), Value::Str(name.clone())), + (ctx.sym("literal_fp"), Value::Str(literal_fp)), + ])), + }); + } + } + Ok(crate::v1_interpreter::list_value(rows)) +} + fn variant_is_nullary(variant: &Rc) -> bool { variant.children.is_empty() } diff --git a/src/v1/stage0/src/v1_interpreter.rs b/src/v1/stage0/src/v1_interpreter.rs index 0b4fc390faa..f01a48b4667 100644 --- a/src/v1/stage0/src/v1_interpreter.rs +++ b/src/v1/stage0/src/v1_interpreter.rs @@ -2139,6 +2139,8 @@ pub(crate) const STD_CONCEPT_INDEX_BRIDGE_FNS: &[&str] = &["concept_decl_facts_l pub(crate) const STD_FN_INDEX_BRIDGE_FNS: &[&str] = &["fn_arrow_decl_facts_live"]; +pub(crate) const STD_DATA_INDEX_BRIDGE_FNS: &[&str] = &["data_init_decl_facts_live"]; + pub fn std_node_bridge_fn_names() -> &'static [&'static str] { STD_NODE_BRIDGE_FNS } @@ -2155,6 +2157,10 @@ pub fn std_fn_index_bridge_fn_names() -> &'static [&'static str] { STD_FN_INDEX_BRIDGE_FNS } +pub fn std_data_index_bridge_fn_names() -> &'static [&'static str] { + STD_DATA_INDEX_BRIDGE_FNS +} + pub fn std_qualified_name_bridge_fn_names() -> &'static [&'static str] { STD_QUALIFIED_NAME_BRIDGE_FNS } @@ -2195,6 +2201,15 @@ fn is_v4_std_fn_index_bridge_call(ctx: &InterpContext, func_name: &str) -> bool .is_some_and(|info| info.module_name == "v2.std.fn_index") } +fn is_v4_std_data_index_bridge_call(ctx: &InterpContext, func_name: &str) -> bool { + if !STD_DATA_INDEX_BRIDGE_FNS.contains(&func_name) { + return false; + } + ctx.item_registry + .get(func_name) + .is_some_and(|info| info.module_name == "v2.std.data_index") +} + fn is_v4_std_lexing_bridge_call(ctx: &InterpContext, func_name: &str) -> bool { if !STD_LEXING_BRIDGE_FNS.contains(&func_name) { return false; @@ -2290,6 +2305,15 @@ fn eval_call(node: &Rc, env: &Rc, ctx: &InterpContext) -> InterpResul }; } + if is_v4_std_data_index_bridge_call(ctx, &func_name) { + return match func_name.as_str() { + "data_init_decl_facts_live" => { + crate::coproduct_reflection::eval_data_init_decl_facts_live(ctx, &args) + } + _ => unreachable!("data_index bridge fn set mismatch"), + }; + } + match func_name.as_str() { "fold_list" => return eval_fold_list_native(&args, env, ctx), "fold_list_right" => return eval_fold_list_right_native(&args, env, ctx), diff --git a/src/v1/tests/src/coproduct_reflection_conformance_test.rs b/src/v1/tests/src/coproduct_reflection_conformance_test.rs index 5a94007511d..0e8a6a4c6d1 100644 --- a/src/v1/tests/src/coproduct_reflection_conformance_test.rs +++ b/src/v1/tests/src/coproduct_reflection_conformance_test.rs @@ -81,6 +81,12 @@ fn coproduct_reflection_std_node_bridge_fns_are_intercept_wired() { "eval_call intercept must wire v2.std.fn_index bridge `{name}`" ); } + for name in v1_interpreter::std_data_index_bridge_fn_names() { + assert!( + source.contains(&format!("\"{name}\" =>")), + "eval_call intercept must wire v2.std.data_index bridge `{name}`" + ); + } assert!( source.contains("is_v4_std_node_bridge_call"), "eval_call must gate v2.std.node bridge dispatch" @@ -97,6 +103,10 @@ fn coproduct_reflection_std_node_bridge_fns_are_intercept_wired() { source.contains("is_v4_std_fn_index_bridge_call"), "eval_call must gate v2.std.fn_index bridge dispatch" ); + assert!( + source.contains("is_v4_std_data_index_bridge_call"), + "eval_call must gate v2.std.data_index bridge dispatch" + ); } #[test] diff --git a/src/v2/lens/no_dual_representation_test.dag b/src/v2/lens/no_dual_representation_test.dag new file mode 100644 index 00000000000..054b783f000 --- /dev/null +++ b/src/v2/lens/no_dual_representation_test.dag @@ -0,0 +1,53 @@ +module v2.lens.no_dual_representation_test + +import gunbc.ci_layer_roots { witness_layer_roots } +import std.disposition { RealizationDispatch } +import v2.lens.common.construction_justification { ConstructionJustification, WallAfterGrounding } +import v2.lens.module_graph { module_declaration_facts_live } +import v2.lens.no_dual_representation_test.scan { + DualRepModuleRef, + DualRepModuleScan, + dual_rep_clean_holds_for_scans, + dual_rep_module_scans_from_fn_index, + dual_rep_test_file_count_from_scans, + dual_rep_violation_count_from_scans, + empty_dual_rep_module_refs +} +import v2.std.algebra { fold_list, list_snoc_item } +import v2.std.collection { List } +import v2.std.logic { Bool } + +fn module_refs_from_declaration_facts(pool_roots: List) -> List { + fold_list( + xs: module_declaration_facts_live(pool_roots: pool_roots), + empty: empty_dual_rep_module_refs, + cons: fn(acc, decl) { + list_snoc_item( + xs: acc, + item: DualRepModuleRef { module: decl.module, path: decl.path } + ) + } + ) +} + +fn dual_rep_live_module_scans() -> List { + dual_rep_module_scans_from_fn_index( + modules: module_refs_from_declaration_facts(pool_roots: witness_layer_roots) + ) +} + +fn no_dual_representation_test_live_count() -> Int { + dual_rep_violation_count_from_scans(scans: dual_rep_live_module_scans()) +} + +fn no_dual_representation_test_live_file_count() -> Int { + dual_rep_test_file_count_from_scans(scans: dual_rep_live_module_scans()) +} + +fn no_dual_representation_test_clean_holds() -> Bool { + dual_rep_clean_holds_for_scans(scans: dual_rep_live_module_scans()) +} + +data construction_justification: ConstructionJustification = ConstructionJustification { + class: WallAfterGrounding { dissolves_to: RealizationDispatch } +} diff --git a/src/v2/lens/no_dual_representation_test/scan.dag b/src/v2/lens/no_dual_representation_test/scan.dag new file mode 100644 index 00000000000..565ec45a38b --- /dev/null +++ b/src/v2/lens/no_dual_representation_test/scan.dag @@ -0,0 +1,707 @@ +module v2.lens.no_dual_representation_test.scan + +import v2.std.algebra { + Cons, + Empty, + TailAbsent, + TailFound, + fold_list, + is_empty, + is_prefix_of, + length, + list_append, + list_snoc_item, + list_tail +} +import v2.std.collection { Absent, List, Present, list_at_optional } +import v2.std.data_index { + DataInitDecl, + data_init_decl_facts_live, + lexeme_matches_literal_fp, + literal_fingerprint_bool_lexeme, + literal_fingerprint_num_lexeme +} +import v2.std.fn_index { FnArrowDecl, fn_arrow_decl_facts_live } +import v2.std.logic { Bool } +import v2.std.node { + Atom, + Conj, + Edge, + Node, + NodeFold, + Positional, + Symbol, + TypeNode, + fold_node, + node_synthetic +} +import v2.std.node_query { node_positional_child_targets } +import v2.std.text { Char, String } + +type DualRepViolationKind + = SameSymbolEquality + | DataLiteralMirror + | BodyAlphaEquivalent + +type DualRepViolation { + path: String + fn_name: String + kind: DualRepViolationKind +} + +type DualRepDataInit { + name: String + literal_fp: String +} + +type DualRepFnFact { + name: String + params: List + output: Node +} + +type DualRepModuleRef { + module: String + path: String +} + +type DualRepModuleScan { + path: String + module: String + data_inits: List + fns: List +} + +type EqNodeSite { + lhs: Node + rhs: Node +} + +data empty_dual_rep_module_refs: List = [] +data empty_dual_rep_violations: List = [] +data empty_dual_rep_data_inits: List = [] +data empty_dual_rep_fns: List = [] +data empty_dual_rep_module_scans: List = [] +data empty_eq_node_sites: List = [] +data empty_symbol_list: List = [] +data empty_edges: List = [] +data empty_sym: Symbol = ^dual_rep_empty_sym + +data sym_m: Symbol = ^m +data sym_a: Symbol = ^a +data sym_b: Symbol = ^b +data sym_ttl_name: String = "ttl" +data sym_flag_name: String = "flag" +data sym_true_name: String = "true" +data sym_x: Symbol = ^x +data sym_y: Symbol = ^y +data sym_wrapped: Symbol = ^wrapped +data sym_inner: Symbol = ^inner +data sym_lit_3600_name: String = "3600" +data sym_lit_4_name: String = "4" +data sym_lit_1_name: String = "1" +data sym_add: Symbol = ^add + +fn path_is_test_dag(path: String) -> Bool { + string_contains(s: path, pattern: "_test.dag") +} + +fn pos_edge(target: Node) -> Edge { + Edge { label: Positional, target: target } +} + +fn atom_node(sym: Symbol) -> Node { + node_synthetic( + kind: TypeNode { connective: Atom { identity: sym } }, + children: [] + ) +} + +fn atom_node_name(name: String) -> Node { + atom_node(sym: name) +} + +fn eq_conj(lhs: Node, rhs: Node) -> Node { + node_synthetic( + kind: TypeNode { connective: Conj }, + children: [pos_edge(target: lhs), pos_edge(target: rhs)] + ) +} + +fn call_node(callee: Symbol, args: List) -> Node { + node_synthetic( + kind: TypeNode { connective: Conj }, + children: fold( + args, + init: [pos_edge(target: atom_node(sym: callee))], + f: fn(acc, arg) { list_snoc_item(xs: acc, item: pos_edge(target: arg)) } + ) + ) +} + +fn node_atom_sym(n: Node) -> Symbol { + match n.kind { + TypeNode { connective: Atom { identity: sym } } => sym + _ => empty_sym + } +} + +fn node_atom_name(n: Node) -> String { + node_atom_sym(n: n) +} + +fn sym_is_empty(sym: Symbol) -> Bool { + sym == empty_sym +} + +fn lookup_data_literal(data_inits: List, name: String) -> String { + fold_list( + xs: data_inits, + empty: "", + cons: fn(acc, row) { + if row.name == name { + row.literal_fp + } else { + acc + } + } + ) +} + +fn eq_site_from_conj(node: Node) -> List { + match node.kind { + TypeNode { connective: Conj } => { + let kids = node_positional_child_targets(node: node) + match list_at_optional(xs: kids, index: 0) { + Present { value: lhs } => + match list_at_optional(xs: kids, index: 1) { + Present { value: rhs } => [EqNodeSite { lhs: lhs, rhs: rhs }] + Absent => empty_eq_node_sites + } + Absent => empty_eq_node_sites + } + } + _ => empty_eq_node_sites + } +} + +fn eq_sites_collect_init(n: Node) -> List { + eq_site_from_conj(node: n) +} + +fn eq_sites_collect_step( + acc: List, + edge: Edge, + child_acc: List +) -> List { + list_append( + left: list_append(left: acc, right: child_acc), + right: eq_site_from_conj(node: edge.target) + ) +} + +fn eq_sites_from_output(root: Node) -> List { + fold_node( + n: root, + algebra: NodeFold { + init: eq_sites_collect_init, + step: eq_sites_collect_step + } + ) +} + +fn skeleton_is_callee_atom(node: Node) -> Bool { + match node.kind { + TypeNode { connective: Atom { identity: _ } } => true + _ => false + } +} + +fn skeleton_is_call(node: Node) -> Bool { + match node.kind { + TypeNode { connective: Conj } => + match list_at_optional(xs: node_positional_child_targets(node: node), index: 0) { + Present { value: callee } => skeleton_is_callee_atom(node: callee) + Absent => false + } + _ => false + } +} + +fn skeleton_callee_target(node: Node) -> Node { + match list_at_optional(xs: node_positional_child_targets(node: node), index: 0) { + Present { value: callee } => callee + Absent => atom_node(sym: empty_sym) + } +} + +fn skeleton_call_argument_targets(node: Node) -> List { + match list_tail(xs: node_positional_child_targets(node: node)) { + TailFound { tail: args } => args + TailAbsent => Empty + } +} + +fn callee_name_from_call(operand: Node) -> String { + if skeleton_is_call(node: operand) { + node_atom_name(n: skeleton_callee_target(node: operand)) + } else { + "" + } +} + +fn first_call_arg_name(operand: Node) -> String { + match list_at_optional(xs: skeleton_call_argument_targets(node: operand), index: 0) { + Present { value: arg } => node_atom_name(n: arg) + Absent => "" + } +} + +fn body_alpha_equivalent_to_single_arg_call( + lhs: Node, + rhs: Node, + fns: List +) -> Bool { + let callee = callee_name_from_call(operand: lhs) + if is_empty(xs: callee) { + false + } else { + let rec = lookup_fn_fact(fns: fns, name: callee) + if is_empty(xs: rec.name) { + false + } else { + let arg = first_call_arg_name(operand: lhs) + let param = first_param_sym(params: rec.params) + let inlined = replace_param_in_output( + output: rec.output, + param: param, + arg_name: arg + ) + rhs == inlined + } + } +} + +fn char_eq(a: Char, b: Char) -> Bool { + a == b +} + +fn qualified_name_in_module(qname: String, module: String) -> Bool { + is_prefix_of(prefix: concat(module, "."), xs: qname, eq: char_eq) +} + +fn first_param_sym(params: List) -> Symbol { + match list_at_optional(xs: params, index: 0) { + Present { value: p } => p + Absent => empty_sym + } +} + +fn param_syms_from_decl(decl: FnArrowDecl) -> List { + fold(decl.params, init: empty_symbol_list, f: fn(acc, p) { + list_snoc_item(xs: acc, item: p.name) + }) +} + +fn lookup_fn_fact(fns: List, name: String) -> DualRepFnFact { + fold( + fns, + init: DualRepFnFact { + name: "", + params: empty_symbol_list, + output: atom_node(sym: empty_sym) + }, + f: fn(acc, row) { + if row.name == name { + row + } else { + acc + } + }) +} + +fn replace_param_in_output(output: Node, param: Symbol, arg_name: String) -> Node { + match output.kind { + TypeNode { connective: Atom { identity: sym } } => + if sym == param { + atom_node_name(name: arg_name) + } else { + output + } + TypeNode { connective: Conj } => + node_synthetic( + kind: output.kind, + children: fold( + output.children, + init: empty_edges, + f: fn(acc, e) { + list_snoc_item( + xs: acc, + item: Edge { + label: e.label, + target: replace_param_in_output( + output: e.target, + param: param, + arg_name: arg_name + ) + } + ) + } + ) + ) + _ => output + } +} + +fn classify_eq_node_site( + path: String, + fn_name: String, + site: EqNodeSite, + data_inits: List, + fns: List +) -> List { + let lhs_sym = node_atom_sym(n: site.lhs) + let rhs_sym = node_atom_sym(n: site.rhs) + if (sym_is_empty(sym: lhs_sym) == false) + && (sym_is_empty(sym: rhs_sym) == false) + && (lhs_sym == rhs_sym) + { + [ + DualRepViolation { + path: path, + fn_name: fn_name, + kind: SameSymbolEquality + } + ] + } else if sym_is_empty(sym: lhs_sym) == false { + let lhs_name = node_atom_name(n: site.lhs) + let rhs_lexeme = node_atom_name(n: site.rhs) + let init_lit = lookup_data_literal(data_inits: data_inits, name: lhs_name) + if (is_empty(xs: init_lit) == false) + && (sym_is_empty(sym: rhs_sym) == false) + && lexeme_matches_literal_fp(lexeme: rhs_lexeme, literal_fp: init_lit) + { + [ + DualRepViolation { + path: path, + fn_name: fn_name, + kind: DataLiteralMirror + } + ] + } else { + empty_dual_rep_violations + } + } else if skeleton_is_call(node: site.lhs) + && body_alpha_equivalent_to_single_arg_call(lhs: site.lhs, rhs: site.rhs, fns: fns) + { + [ + DualRepViolation { + path: path, + fn_name: fn_name, + kind: BodyAlphaEquivalent + } + ] + } else { + empty_dual_rep_violations + } +} + +fn violations_from_fn_fact( + path: String, + fact: DualRepFnFact, + data_inits: List, + fns: List +) -> List { + fold_list( + xs: eq_sites_from_output(root: fact.output), + empty: empty_dual_rep_violations, + cons: fn(acc, site) { + list_append( + left: acc, + right: classify_eq_node_site( + path: path, + fn_name: fact.name, + site: site, + data_inits: data_inits, + fns: fns + ) + ) + } + ) +} + +fn dual_rep_violations_from_module(scan: DualRepModuleScan) -> List { + fold(scan.fns, init: empty_dual_rep_violations, f: fn(acc, fact) { + if is_empty(xs: fact.name) { + acc + } else { + list_append( + left: acc, + right: violations_from_fn_fact( + path: scan.path, + fact: fact, + data_inits: scan.data_inits, + fns: scan.fns + ) + ) + } + }) +} + +fn dual_rep_violation_count_from_scans(scans: List) -> Int { + length( + xs: fold_list( + xs: scans, + empty: empty_dual_rep_violations, + cons: fn(acc, scan) { + list_append( + left: acc, + right: dual_rep_violations_from_module(scan: scan) + ) + } + ) + ) +} + +fn dual_rep_clean_holds_for_scans(scans: List) -> Bool { + dual_rep_violation_count_from_scans(scans: scans) == 0 +} + +fn dual_rep_test_file_count_from_scans(scans: List) -> Int { + length(xs: scans) +} + +fn decl_belongs_to_module(decl: FnArrowDecl, fact: DualRepModuleRef) -> Bool { + path_is_test_dag(path: fact.path) + && qualified_name_in_module(qname: decl.qualified_name, module: fact.module) +} + +fn fn_fact_from_decl(decl: FnArrowDecl) -> DualRepFnFact { + DualRepFnFact { + name: decl.name, + params: param_syms_from_decl(decl: decl), + output: decl.output + } +} + +fn module_fns_for_fact( + fact: DualRepModuleRef, + decls: List +) -> List { + fold(decls, init: empty_dual_rep_fns, f: fn(acc, decl) { + if decl_belongs_to_module(decl: decl, fact: fact) { + list_snoc_item(xs: acc, item: fn_fact_from_decl(decl: decl)) + } else { + acc + } + }) +} + +fn data_init_belongs_to_module(decl: DataInitDecl, fact: DualRepModuleRef) -> Bool { + decl.module == fact.module +} + +fn data_inits_for_fact( + fact: DualRepModuleRef, + decls: List +) -> List { + fold(decls, init: empty_dual_rep_data_inits, f: fn(acc, decl) { + if data_init_belongs_to_module(decl: decl, fact: fact) { + list_snoc_item( + xs: acc, + item: DualRepDataInit { name: decl.name, literal_fp: decl.literal_fp } + ) + } else { + acc + } + }) +} + +fn dual_rep_module_scan_for_fact( + fact: DualRepModuleRef, + decls: List, + data_init_decls: List +) -> DualRepModuleScan { + DualRepModuleScan { + path: fact.path, + module: fact.module, + data_inits: data_inits_for_fact(fact: fact, decls: data_init_decls), + fns: module_fns_for_fact(fact: fact, decls: decls) + } +} + +fn dual_rep_module_scans_from_decls( + decls: List, + data_init_decls: List, + modules: List +) -> List { + fold_list( + xs: modules, + empty: empty_dual_rep_module_scans, + cons: fn(acc, fact) { + if path_is_test_dag(path: fact.path) { + let scan = dual_rep_module_scan_for_fact( + fact: fact, + decls: decls, + data_init_decls: data_init_decls + ) + if is_empty(xs: scan.fns) { + acc + } else { + list_snoc_item(xs: acc, item: scan) + } + } else { + acc + } + } + ) +} + +fn dual_rep_module_scans_from_fn_index( + modules: List +) -> List { + dual_rep_module_scans_from_decls( + decls: fn_arrow_decl_facts_live(), + data_init_decls: data_init_decl_facts_live(), + modules: modules + ) +} + +fn synthetic_same_symbol_scan() -> DualRepModuleScan { + DualRepModuleScan { + path: "synthetic/same_symbol_test.dag", + module: "synthetic.same_symbol_test", + data_inits: empty_dual_rep_data_inits, + fns: [ + DualRepFnFact { + name: "witness_taut", + params: empty_symbol_list, + output: eq_conj(lhs: atom_node(sym: sym_m), rhs: atom_node(sym: sym_m)) + } + ] + } +} + +fn synthetic_literal_mirror_scan() -> DualRepModuleScan { + DualRepModuleScan { + path: "synthetic/literal_mirror_test.dag", + module: "synthetic.literal_mirror_test", + data_inits: [ + DualRepDataInit { + name: sym_ttl_name, + literal_fp: literal_fingerprint_num_lexeme(lexeme: sym_lit_3600_name) + } + ], + fns: [ + DualRepFnFact { + name: "witness_ttl", + params: empty_symbol_list, + output: eq_conj(lhs: atom_node_name(name: sym_ttl_name), rhs: atom_node_name(name: sym_lit_3600_name)) + } + ] + } +} + +fn synthetic_bool_literal_mirror_scan() -> DualRepModuleScan { + DualRepModuleScan { + path: "synthetic/bool_literal_mirror_test.dag", + module: "synthetic.bool_literal_mirror_test", + data_inits: [ + DualRepDataInit { + name: sym_flag_name, + literal_fp: literal_fingerprint_bool_lexeme(lexeme: sym_true_name) + } + ], + fns: [ + DualRepFnFact { + name: "witness_flag", + params: empty_symbol_list, + output: eq_conj( + lhs: atom_node_name(name: sym_flag_name), + rhs: atom_node_name(name: sym_true_name) + ) + } + ] + } +} + +fn synthetic_independent_oracle_scan() -> DualRepModuleScan { + DualRepModuleScan { + path: "synthetic/oracle_test.dag", + module: "synthetic.oracle_test", + data_inits: empty_dual_rep_data_inits, + fns: [ + DualRepFnFact { + name: "oracle", + params: empty_symbol_list, + output: eq_conj( + lhs: call_node(callee: sym_add, args: [atom_node(sym: sym_a), atom_node(sym: sym_b)]), + rhs: atom_node_name(name: sym_lit_4_name) + ) + } + ] + } +} + +fn synthetic_body_mirror_scan() -> DualRepModuleScan { + DualRepModuleScan { + path: "synthetic/body_mirror_test.dag", + module: "synthetic.body_mirror_test", + data_inits: empty_dual_rep_data_inits, + fns: [ + DualRepFnFact { + name: "inner", + params: [sym_y], + output: atom_node(sym: sym_y) + }, + DualRepFnFact { + name: "wrapped", + params: [sym_x], + output: call_node(callee: sym_inner, args: [atom_node(sym: sym_x)]) + }, + DualRepFnFact { + name: "witness_wrap", + params: empty_symbol_list, + output: eq_conj( + lhs: call_node(callee: sym_wrapped, args: [atom_node_name(name: sym_lit_1_name)]), + rhs: call_node(callee: sym_inner, args: [atom_node_name(name: sym_lit_1_name)]) + ) + } + ] + } +} + +fn synthetic_distinct_symbol_scan() -> DualRepModuleScan { + DualRepModuleScan { + path: "synthetic/distinct_test.dag", + module: "synthetic.distinct_test", + data_inits: empty_dual_rep_data_inits, + fns: [ + DualRepFnFact { + name: "ok", + params: empty_symbol_list, + output: eq_conj(lhs: atom_node(sym: sym_a), rhs: atom_node(sym: sym_b)) + } + ] + } +} + +fn parse_path_helper_tautology_scan() -> DualRepModuleScan { + DualRepModuleScan { + path: "synthetic/parse_path_helper_tautology_test.dag", + module: "synthetic.parse_path_helper_tautology_test", + data_inits: empty_dual_rep_data_inits, + fns: [ + DualRepFnFact { + name: "helper_taut", + params: empty_symbol_list, + output: eq_conj(lhs: atom_node(sym: sym_m), rhs: atom_node(sym: sym_m)) + }, + DualRepFnFact { + name: "witness_calls_helper", + params: empty_symbol_list, + output: call_node(callee: sym_m, args: []) + } + ] + } +} diff --git a/src/v2/lens/no_dual_representation_test_test.dag b/src/v2/lens/no_dual_representation_test_test.dag new file mode 100644 index 00000000000..1d1f09afb91 --- /dev/null +++ b/src/v2/lens/no_dual_representation_test_test.dag @@ -0,0 +1,15 @@ +module v2.test.lens_no_dual_representation_test.no_dual_representation_test_test + +import v2.lens.no_dual_representation_test { + no_dual_representation_test_clean_holds, + no_dual_representation_test_live_file_count, +} +import v2.std.logic { Bool } + +test fn no_dual_representation_test_has_no_violations() -> Bool { + return no_dual_representation_test_clean_holds() +} + +test fn no_dual_representation_test_corpus_is_nonempty() -> Bool { + return no_dual_representation_test_live_file_count() > 0 +} diff --git a/src/v2/std/data_index.dag b/src/v2/std/data_index.dag new file mode 100644 index 00000000000..ad471d94219 --- /dev/null +++ b/src/v2/std/data_index.dag @@ -0,0 +1,34 @@ +module v2.std.data_index + +import v2.std.collection { List } +import v2.std.logic { Bool } +import v2.std.text { String } + +type DataInitDecl { + qualified_name: String + module: String + name: String + literal_fp: String +} + +fn literal_fingerprint_num_lexeme(lexeme: String) -> String { + concat("num:", lexeme) +} + +fn literal_fingerprint_bool_lexeme(lexeme: String) -> String { + concat("bool:", lexeme) +} + +fn literal_fingerprint_str_content(content: String) -> String { + concat("str:\"", concat(content, "\"")) +} + +fn lexeme_matches_literal_fp(lexeme: String, literal_fp: String) -> Bool { + (literal_fp == literal_fingerprint_num_lexeme(lexeme: lexeme)) + || (literal_fp == literal_fingerprint_bool_lexeme(lexeme: lexeme)) + || (literal_fp == literal_fingerprint_str_content(content: lexeme)) +} + +fn data_init_decl_facts_live() -> List { + data_init_decl_facts_live() +} diff --git a/src/v2/test/claim/manual/map_structural_key_equality_test.dag b/src/v2/test/claim/manual/map_structural_key_equality_test.dag index e58241952a0..cfaddbb2d3a 100644 --- a/src/v2/test/claim/manual/map_structural_key_equality_test.dag +++ b/src/v2/test/claim/manual/map_structural_key_equality_test.dag @@ -19,11 +19,6 @@ fn one_entry(a: Int, b: Int, v: Int) -> SKeyMap { map_insert(m: empty_map(), key: SKey { a: a, b: b }, value: v) } -fn struct_key_self_eq() -> Bool { - let m = one_entry(a: 1, b: 2, v: 7) - m == m -} - fn struct_key_equal_eq() -> Bool { one_entry(a: 1, b: 2, v: 7) == one_entry(a: 1, b: 2, v: 7) } @@ -42,8 +37,7 @@ fn struct_key_shadow_latest_eq() -> Bool { } test fn map_structural_key_equality_holds() -> Bool { - struct_key_self_eq() - && struct_key_equal_eq() + struct_key_equal_eq() && struct_key_distinct_neq() && struct_key_value_neq() && struct_key_shadow_latest_eq() diff --git a/src/v2/test/claim/no_dual_representation_test/lens_unit/controls_test.dag b/src/v2/test/claim/no_dual_representation_test/lens_unit/controls_test.dag new file mode 100644 index 00000000000..644e8faf262 --- /dev/null +++ b/src/v2/test/claim/no_dual_representation_test/lens_unit/controls_test.dag @@ -0,0 +1,44 @@ +module v2.test.no_dual_representation_test.lens_unit.controls + +import v2.std.algebra { length } +import v2.lens.no_dual_representation_test.scan { + dual_rep_clean_holds_for_scans, + dual_rep_violation_count_from_scans, + dual_rep_violations_from_module, + parse_path_helper_tautology_scan, + synthetic_body_mirror_scan, + synthetic_bool_literal_mirror_scan, + synthetic_distinct_symbol_scan, + synthetic_independent_oracle_scan, + synthetic_literal_mirror_scan, + synthetic_same_symbol_scan +} +import v2.std.logic { Bool } + +test fn same_symbol_equality_is_red() -> Bool { + dual_rep_violation_count_from_scans(scans: [synthetic_same_symbol_scan()]) == 1 +} + +test fn literal_mirror_is_red() -> Bool { + dual_rep_violation_count_from_scans(scans: [synthetic_literal_mirror_scan()]) == 1 +} + +test fn bool_literal_mirror_is_red() -> Bool { + dual_rep_violation_count_from_scans(scans: [synthetic_bool_literal_mirror_scan()]) == 1 +} + +test fn independent_oracle_is_green() -> Bool { + dual_rep_clean_holds_for_scans(scans: [synthetic_independent_oracle_scan()]) +} + +test fn distinct_symbol_equality_is_green() -> Bool { + dual_rep_clean_holds_for_scans(scans: [synthetic_distinct_symbol_scan()]) +} + +test fn body_mirror_is_red() -> Bool { + length(xs: dual_rep_violations_from_module(scan: synthetic_body_mirror_scan())) == 1 +} + +test fn parse_path_helper_tautology_is_red() -> Bool { + dual_rep_violation_count_from_scans(scans: [parse_path_helper_tautology_scan()]) == 1 +}