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
22 changes: 12 additions & 10 deletions src/v2/compiler/06_translate.dag
Original file line number Diff line number Diff line change
Expand Up @@ -275,36 +275,38 @@ type TokenSequenceItemKind
= TokenSequenceConcreteToken
| TokenSequenceNonterminal

data translate_grounding_gate_absent_facts_note: String = "Refuse only recorded GroundingNotDerived on the Holds arm, routing that variant through canonical_grounding_from_inferred_facts so the typed ^infer_grounding_not_derived diagnostic propagates (review 46789). DerivedGrounding on Holds accepts without re-running canonical admission. infer_facts_lookup_miss (Violates) is the compatibility class for trees with no infer judgment at a node: emit_orchestration's synthetic InferredTree (`orch_emit_facts_lookup`) and test-only shape-frontier carriers carry an empty facts map by construction, so lookup miss means no infer judgment exists — not an underived one recorded and erased (review 47246). Production paths (`cross_language_compile`, canonical infer→emit) pass infer's facts map facts-flow-forward. Eval refuses lookup miss because eval never runs on synthetic trees; translate is also consumed by emit, so absence is a named compatibility frontier until v2-inferred-tree-completeness splits the carrier. translate() opens with translate_grounding_derived_gate_subtree so mixed derived-root/underived-child trees cannot bypass fold attach or bodied-arrow shortcuts. translate_grounding_derived_gate_at_producer is the producer-entry call site for that same gate. translate_derived_parent_underived_child_gate refuses a recorded underived child under a derived parent during fold; translate_grounding_derived_gate_subtree covers bodied-arrow and import-carrier shortcuts that preserve producer IR without fold_node (review 46681). TranslateFoldAcc retains the source parent/child nodes because fold init rebuilds with empty children and facts.lookup keys on structural node equality."
type GroundingGatePassed {}

fn translate_grounding_derived_gate(tree: InferredTree, node: Node) -> Outcome<Empty> {
data translate_grounding_gate_absent_facts_note: String = "Refuse only recorded GroundingNotDerived on the Holds arm, routing that variant through canonical_grounding_from_inferred_facts so the typed ^infer_grounding_not_derived diagnostic propagates (review 46789). DerivedGrounding on Holds accepts without re-running canonical admission. infer_facts_lookup_miss (Violates) is the compatibility class for trees with no infer judgment at a node: emit_orchestration's synthetic InferredTree (`orch_emit_facts_lookup`) and test-only shape-frontier carriers carry an empty facts map by construction, so lookup miss means no infer judgment exists — not an underived one recorded and erased (review 47246). Production paths (`cross_language_compile`, canonical infer→emit) pass infer's facts map facts-flow-forward. Eval refuses lookup miss because eval never runs on synthetic trees; translate is also consumed by emit, so absence is a named compatibility frontier until v2-inferred-tree-completeness splits the carrier. translate() opens with translate_grounding_derived_gate_subtree so mixed derived-root/underived-child trees cannot bypass fold attach or bodied-arrow shortcuts. translate_grounding_derived_gate_at_producer is the producer-entry call site for that same gate. translate_derived_parent_underived_child_gate refuses a recorded underived child under a derived parent during fold; translate_grounding_derived_gate_subtree covers bodied-arrow and import-carrier shortcuts that preserve producer IR without fold_node (review 46681). TranslateFoldAcc retains the source parent/child nodes because fold init rebuilds with empty children and facts.lookup keys on structural node equality. The four translate_grounding_*_gate* fns return Outcome<GroundingGatePassed>: a zero-information accept carrier (same wire-schema gate pattern as target_model.dag CtorTemplateUnit), not Outcome<Bool> — Bool would admit a meaningful false the gate never produces. Empty is a FreeMonoid variant, not a unit type, so Outcome<Empty> is an unresolved compile error. Callers bind with bind_outcome(fn(_) => ...) and never read the payload; the signal is Accepted vs Rejected disposition only."

fn translate_grounding_derived_gate(tree: InferredTree, node: Node) -> Outcome<GroundingGatePassed> {
match inferred_facts_witness_for_node(tree: tree, node: node) {
Holds { value: facts } =>
match facts.grounding {
GroundingNotDerived { node: _ } =>
match canonical_grounding_from_inferred_facts(node: node, facts: facts) {
Accepted { value: _, diagnostics: _ } => outcome_accepted(Empty)
Accepted { value: _, diagnostics: _ } => outcome_accepted(GroundingGatePassed {})
Rejected { diagnostics: r } => Rejected { diagnostics: r }
}
DerivedGrounding { grounding: _ } =>
outcome_accepted(Empty)
outcome_accepted(GroundingGatePassed {})
}
Violates { diagnostic: _ } =>
outcome_accepted(Empty)
outcome_accepted(GroundingGatePassed {})
}
}

fn translate_derived_parent_underived_child_gate(
tree: InferredTree,
parent: Node,
child: Node
) -> Outcome<Empty> {
) -> Outcome<GroundingGatePassed> {
match inferred_facts_witness_for_node(tree: tree, node: parent) {
Holds { value: parent_facts } =>
if inferred_facts_grounding_derived(facts: parent_facts) {
translate_grounding_derived_gate(tree: tree, node: child)
} else {
outcome_accepted(Empty)
outcome_accepted(GroundingGatePassed {})
}
Violates { diagnostic: _ } =>
translate_grounding_derived_gate(tree: tree, node: child)
Expand All @@ -314,10 +316,10 @@ fn translate_derived_parent_underived_child_gate(
fn translate_grounding_derived_gate_subtree(
tree: InferredTree,
root: Node
) -> Outcome<Empty> {
) -> Outcome<GroundingGatePassed> {
fold_list(
xs: node_subtree_nodes(root: root),
empty: outcome_accepted(Empty),
empty: outcome_accepted(GroundingGatePassed {}),
cons: fn(acc, n) {
bind_outcome(
o: acc,
Expand Down Expand Up @@ -368,7 +370,7 @@ fn translate_import_shortcut_after_subtree_gate(
fn translate_grounding_derived_gate_at_producer(
tree: InferredTree,
node: Node
) -> Outcome<Empty> {
) -> Outcome<GroundingGatePassed> {
translate_grounding_derived_gate(tree: tree, node: node)
}

Expand Down
2 changes: 2 additions & 0 deletions src/v2/extdeps/languages/rust_test_fixtures.dag
Original file line number Diff line number Diff line change
@@ -1,5 +1,7 @@
module v2.extdeps.languages.rust_test

import std.algebra { Cons, Empty }

import v2.extdeps.languages.rust {
rust_add_declared_inhabitants_root,
rust_binding_spellings,
Expand Down
55 changes: 54 additions & 1 deletion src/v2/lens/complexity.dag
Original file line number Diff line number Diff line change
@@ -1,5 +1,58 @@
module v2.lens.complexity

import v2.lens.common.construction_justification { ConstructionJustification, RatchetForever }

import v2.lens.cost {
AsymptoticClass,
ClassConstant,
ClassExponential,
ClassFactorial,
ClassLinearithmic,
ClassLinear,
ClassLog,
ClassPolyLog,
ClassPolynomial,
ClassUnknown,
ConstantCost,
ExponentialCost,
FactorialCost,
LinearCost,
LogCost,
PolynomialCost,
PolyLogCost,
ProductCost,
SumCost,
UnknownCost,
PolyLogExponent,
PolynomialDegree,
SymbolicCost,
SizeVariable,
asymptotic_class_dominates,
asymptotic_class_of_cost,
cost_lens
}
import std.algebra { Empty }
import v2.std.collection { List }
import v2.std.diagnostic {
Accepted,
AmbiguousIntent,
Diagnostic,
Locus,
Rejected,
Textual,
WholeFile,
Unavailable
}
import v2.std.node { Node, Symbol }
import v2.std.refinement {
Refined,
VacuousValidation,
vacuous_admits_marker,
Validation,
refine,
refined_base,
refined_vacuous_stub_pack
}
import v2.std.witness { Holds, Violates, Witness }

fn complexity_variables_admits(xs: List<SizeVariable>) -> Bool {
true
Expand Down
24 changes: 24 additions & 0 deletions src/v2/lens/enforcement/receipts.dag
Original file line number Diff line number Diff line change
@@ -1,5 +1,29 @@
module v2.lens.enforcement.receipts

import std.algebra { Cons, Empty }
import v2.std.algebra { any, contains }
import v2.std.collection { List }
import v2.std.integer { Int }
import v2.std.logic { Bool }
import v2.std.text { String }
import v2.std.node { Atom, ComputationNode, Edge, Loop, Named, Node, Positional, SyntheticOccurrence, TypeNode }
import v2.std.witness { Holds, Violates, Witness }
import v2.std.decl_index { DeclFact, decl_facts_is_fn_like }
import v2.std.qualified_name { QualifiedName, qualified_name_from_dotted_string }
import v2.lens.cost { SymbolicCost, cost_lens }
import v2.lens.enforcement.vocab {
SubjectRoster, ScopeRoster, scope_roster_covers,
ConsumerKind, EnrolledInFloorRoster, PrePushHook, WitnessOnly, NoConsumer,
ConsumerWitnessBinding, BoundConsumerWitness, NoConsumerWitness,
ScopeSatisfaction, ScopeCovers, ScopeNarrowed, ScopeMissing,
NarrowingReason, TypeReflectionUnavailable,
RedControlStatus, RedControlPassed, RedControlAbsent, RedControlFailedToFlip,
SelfApplicationStatus, LensModuleFunctionObserved, SelfApplicationAbsent,
ReceiptRef, HasReceiptRef, NoReceiptRef,
consumer_kind_eq
}
import v2.lens.enforcement.contract { LensContract, EnrollmentDiscoveryReceipt, Cost, lens_id_v0_eq }
import std.realization_schedule { ScheduleWitnessEntry, schedule_witness_entry_eq }

type SubjectJudgment
= BodyJudged { verdict: Witness<SymbolicCost> }
Expand Down
2 changes: 2 additions & 0 deletions src/v2/lens/module_graph.dag
Original file line number Diff line number Diff line change
Expand Up @@ -43,6 +43,8 @@ type ModuleDependencyEdge {

data dependency_edge_source_migration_note: String = "EDGE SOURCE, isolated as the single swappable fact producer (operator constraint, 2026-07-10, on the entry_file_touched reground): today dependency_resolution_facts_live unions import_resolution_facts_live with strict-tier reference_resolution_facts_live (host twin selection_adjacency in cli_run.rs). The namespace-only resolution thread (operator-signed 2026-07-06) deletes the import grammar at its terminal step and derives dependencies from container.member references instead — when that lands, dependency_resolution_facts_live swaps to reference_derived_resolution_facts_flagged_pending_reference_producer and nothing above it changes: dependency_closure, import_closure, touched_path_in_closure, entry_affected_by_touched_paths, and every consumer of the closure query are edge-source-agnostic by construction (they read ModuleDependencyEdge rows as data, never import syntax). Do not add a second edge producer beside dependency_resolution_facts_live; the swap replaces its body."

data namespace_wave_import_strip_specimens_note: String = "Namespace-lane handoff specimens from gunbc#7908 (operator ruling 2026-08-06, msg_8e1c9e9d): three closure-binding failures from #6848 import stripping that whole-tree compile-clean repaired with explicit imports — NOT held for namespace-derived closure; main needed exact imports today, namespace program owns making this class unwritable later. (1) v2.lens.complexity: direct imports from v2.lens.cost stripped (PolynomialDegree, PolyLogExponent, SizeVariable, SymbolicCost, asymptotic_class_*); module referenced cost symbols with zero import lines. (2) v2.lens.enforcement.receipts: direct imports stripped from v2.lens.cost and v2.lens.enforcement.vocab (SymbolicCost, EnrolledInFloorRoster, EnrollmentDiscoveryReceipt, LensModuleFunctionObserved, etc.). (3) v2.extdeps.languages.rust_test_fixtures: missing std.algebra { Cons, Empty } bindings (#7772 partial un-strip; see rust_test_fixtures_rust_import_unstrip_note). Dissolve-on: bare-reference closure binding is construction-backed repo-wide so stripped modules cannot compile only by pool-membership coincidence."

data reference_derived_edge_source_disposition: Disposition = Scaffold {
dissolves_to: SingleAuthority,
bind: DeclarationRef {
Expand Down
Loading