diff --git a/dag/gunbc/non_fold_residue.dag b/dag/gunbc/non_fold_residue.dag index 8db4eec35f4..425277234fd 100644 --- a/dag/gunbc/non_fold_residue.dag +++ b/dag/gunbc/non_fold_residue.dag @@ -71,6 +71,8 @@ data nfr_reason_cost_loop_zero_body_fold: String = "C1 zero-body summation fold data nfr_reason_cost_expr_zero_absorbing_compose: String = "zero-absorbing CostExpr composition (zero-valued CostConst is the identity for sequential add and parallel max; nested wildcard arms are the non-degenerate CostAdd/CostMax construction path, not anonymous recursion) — landed with v2.lens.cost.expr cost_expr_seq/cost_expr_par for C2 ComplexitySummary composition; surfaced by whole-corpus nfr receipt on first CI run" +data nfr_reason_cost_valuation_zero_annihilator: String = "Zero-annihilator discrimination in the C1 exact evaluator: the arms separate an ExactCost carrying Zero from every other CostEvaluation on BOTH operands, so the wildcard is a nested-VALUE discrimination and not a variant sweep — CostEvaluation has exactly two variants and the other two matches in this module were made exhaustive rather than rostered when this row was written. Enumerating it would mean writing the residual combine_evaluation call once per surviving shape, which is the redundancy DESIGN §2 forbids rather than the totality DESIGN §4 asks for, and it would put a duplicated expression underneath an arm ORDER that multiply_evaluations_zero_note declares load-bearing: the annihilator is checked before refusal-dominance, so refusal times zero answers exact zero. A later tidy that flattens these arms silently restores the defect the function exists to fix. Declared at landing with the two-sided annihilator fix, not surfaced by a later cold sweep, so the ratchet arms with the code." + data nfr_reason_provider_terminal_absorb: String = "terminal-state absorption over the provider/worker observation coproducts: the arm names each TERMINAL variant (ProviderCompleted / ProviderFailed / ProviderEventsRefused, or WorkerProcessRunning) and gives every non-terminal variant one shared arm, because those variants reduce to the identical behaviour — enumerating them would clone the arm per variant, which is the redundancy DESIGN §2 forbids rather than the totality DESIGN §4 asks for. Landed with the Codex dispatch and recursive workflow evidence slice; declared at landing (not surfaced by a later cold sweep) so the ratchet arms with the code." data nfr_dissolve_provider_terminal_absorb: String = "ProviderExecutionState and WorkerProcessEvidence carry a DERIVED terminality projection from inhabitance (dag/std/algebra, DESIGN §3/§4 — the same move as derived equality), so these folds match on the partition rather than on the variant list, the shared arm becomes a named case instead of a wildcard, and the rows delete." @@ -709,6 +711,11 @@ data non_fold_residue_frontier: List = [ reason: nfr_reason_cost_expr_zero_absorbing_compose, trigger: TriggerProse { text: nfr_dissolve_wildcard_total }, }, + FrontierRow { + subject: PathSubject { path: "src/v2/lens/cost/valuation.dag::multiply_evaluations" }, + reason: nfr_reason_cost_valuation_zero_annihilator, + trigger: TriggerProse { text: nfr_dissolve_wildcard_total }, + }, FrontierRow { subject: PathSubject { path: "src/v2/lens/fact_density.dag::connective_is_kernel_ambient_atom" }, reason: nfr_reason_mint_era, diff --git a/dag/std/algebra.dag b/dag/std/algebra.dag index 87ec9ecad05..4a3dcbd215f 100644 --- a/dag/std/algebra.dag +++ b/dag/std/algebra.dag @@ -122,6 +122,11 @@ type FreeMonoid = Empty | Cons { head: T, tail: FreeMonoid } +type FreeSemigroup { + head: T + tail: FreeMonoid +} + type PartialFunction { lookup: fn(K) -> V? empty: PartialFunction diff --git a/dag/test/claim/realization_schedule_critical_path_test.dag b/dag/test/claim/realization_schedule_critical_path_test.dag index 44cd42f63fa..cf1d2fc083a 100644 --- a/dag/test/claim/realization_schedule_critical_path_test.dag +++ b/dag/test/claim/realization_schedule_critical_path_test.dag @@ -42,7 +42,7 @@ test fn witness_measured_total_uses_critical_path_basis() -> Bool { test fn witness_nat_ordering_supports_max() -> Bool { match std.nat.nat_compare(a: 7, b: 3) { - Greater => nat_max(a: 7, b: 3) == 7 + Greater => std.nat.nat_max(a: 7, b: 3) == 7 _ => false } } diff --git a/src/v1/stage0/src/std_algebra.rs b/src/v1/stage0/src/std_algebra.rs index 55a401b98a5..80453d9a965 100644 --- a/src/v1/stage0/src/std_algebra.rs +++ b/src/v1/stage0/src/std_algebra.rs @@ -228,6 +228,13 @@ pub struct PointwisePower { pub type FreeMonoid = Vec; +#[derive(Debug, Clone, PartialEq, serde::Serialize, serde::Deserialize)] +pub struct FreeSemigroup { + pub head: T, + pub tail: Rc>, + pub _phantom: std::marker::PhantomData, +} + #[derive(Clone)] pub struct PartialFunction { pub lookup: Rc Option>, diff --git a/src/v2/compiler/self_host/frontier_probe_types.dag b/src/v2/compiler/self_host/frontier_probe_types.dag index 7ada0eed0d3..b4e6e0a81c0 100644 --- a/src/v2/compiler/self_host/frontier_probe_types.dag +++ b/src/v2/compiler/self_host/frontier_probe_types.dag @@ -42,9 +42,9 @@ import v2.std.optional { Absent, Optional, Present } import v2.std.qualified_name { QualifiedName } import v2.std.text { String } -data frontier_nonempty_carrier_pattern_note: String = "NonEmptySymbolChain and NonEmptyGrammarChoiceAmbiguityRows join NonEmptyDiagnostics and NonEmptyProcessNodeIds as hand-rolled nonempty carriers beside the generic NonEmptyList refinement (fixture-only today). Counted here so the pattern is visible rather than silently repeated. Dissolve triggers: non_empty_symbol_chain_dissolve_trigger (this module); NonEmptyGrammarChoiceAmbiguityRows trigger on v2.std.grammar_choice_ambiguity." +data frontier_nonempty_carrier_pattern_note: String = "NonEmptySymbolChain and NonEmptyGrammarChoiceAmbiguityRows join NonEmptyDiagnostics, NonEmptyProcessNodeIds and v2.std.collection FiniteSet as hand-rolled nonempty carriers. The generic carrier is NO LONGER fixture-only: std.algebra FreeSemigroup is a real construction wall in the tree, so this count is now migration debt with a reachable destination rather than a pattern with nowhere to go. Counted here so the pattern is visible rather than silently repeated. Dissolve triggers: non_empty_symbol_chain_dissolve_trigger (this module); NonEmptyGrammarChoiceAmbiguityRows trigger on v2.std.grammar_choice_ambiguity. NonEmptyDiagnostics, NonEmptyProcessNodeIds and FiniteSet carry NO trigger and are untracked stalls owed one - see std.algebra free_semigroup_grounding_note, which names them at the grain a grep decides." -data non_empty_symbol_chain_dissolve_trigger: String = "migrate_when_nonempty_list_refinement_promoted — NonEmptySymbolChain dissolves into NonEmptyList when the refinement is promoted from v2.test.claim.manual.refinement_nonempty_list to std." +data non_empty_symbol_chain_dissolve_trigger: String = "migrate_when_free_semigroup_available — NonEmptySymbolChain dissolves into std.algebra FreeSemigroup. RETARGETED: this trigger previously named the promotion of the manual Refined> fixture to std, and the generic carrier that landed is a record with a head field rather than that refinement, with the NonEmptyList alias deliberately withheld while the fixture lives - so the event as previously spelled will not occur and this row would have stalled untracked. The construction wall is now available; see std.algebra free_semigroup_grounding_note." data frontier_fixture_cemented_producer_note: String = "FixtureCemented is forward-declared for the fixture-free self-host bar; inhabited by the behavioral-equivalence probe when it detects injected fixtures cementing greens (e.g. add_arrow_eval_allocate_literal, pick-lit hardcoding) — not by frontier_classify_rejection_reason (assemble/emit stage only)." diff --git a/src/v2/lens/cost.dag b/src/v2/lens/cost.dag index 27d9bf2d7b5..e6dcec86200 100644 --- a/src/v2/lens/cost.dag +++ b/src/v2/lens/cost.dag @@ -233,17 +233,25 @@ fn symbolic_sequential(a: SymbolicCost, b: SymbolicCost) -> SymbolicCost { } } +data symbolic_product_zero_absorption_note: String = "Zero is checked on BOTH operands before anything else, and the order is the whole point. An earlier revision matched a's arms first - including UnknownCost - and only then inspected b, so zero times unknown absorbed to zero while unknown times ZERO returned unknown. Multiplication is commutative, so an operand order that changes the answer is a defect on its face, not a stylistic asymmetry: the authority absorbed zero only when zero happened to be written on the left. Found by comparing this authority against v2.lens.cost.valuation, whose exact evaluator has the same obligation - a zero multiplicity means the other factor is never executed, so its work is zero whatever that factor is and however little is known about it. Both paths now answer zero for both orders, so the two agree completely rather than agreeing in one direction and diverging in the other. The scope of that claim is CLASSIFICATION, not provenance, and saying so here is what stops a later reader from concluding the function is symmetric in every respect and then being surprised. One asymmetry survives deliberately: unknown times unknown returns the LEFT operand's diagnostic, so the reverse order returns the right one and the other is dropped. That is a lesser class than what this change fixed - before it, the operand order changed the KIND of the answer, and now it changes only which of two equally valid diagnostics is carried - and it is not introduced here: symbolic_sequential carries the identical left-biased drop, so it is a module-wide pattern of UnknownCost holding exactly one diagnostic. Closing it means widening UnknownCost to carry several, which is a real change with its own witnesses and does not belong on the annihilator fix." + fn symbolic_product(a: SymbolicCost, b: SymbolicCost) -> SymbolicCost { match a { ConstantCost { value: Zero } => zero_cost() - ConstantCost { value: Succ { prev: Zero } } => b - UnknownCost { diagnostic: _ } => a _ => match b { ConstantCost { value: Zero } => zero_cost() - ConstantCost { value: Succ { prev: Zero } } => a - UnknownCost { diagnostic: _ } => b - _ => ProductCost { lhs: a, rhs: b } + _ => + match a { + ConstantCost { value: Succ { prev: Zero } } => b + UnknownCost { diagnostic: _ } => a + _ => + match b { + ConstantCost { value: Succ { prev: Zero } } => a + UnknownCost { diagnostic: _ } => b + _ => ProductCost { lhs: a, rhs: b } + } + } } } } diff --git a/src/v2/lens/cost/valuation.dag b/src/v2/lens/cost/valuation.dag new file mode 100644 index 00000000000..0d680b89c8c --- /dev/null +++ b/src/v2/lens/cost/valuation.dag @@ -0,0 +1,378 @@ +module v2.lens.cost.valuation + +import std.algebra { Cons, Empty, FreeSemigroup } +import std.decl_ref { DeclarationRef } +import v2.lens.cost { SizeVariable } +import v2.lens.cost.expr { + CostAdd, + CostConst, + CostEffect, + CostExpr, + CostExprRefusalCause, + CostLog, + CostMax, + CostMul, + CostRefused, + CostSum, + InvalidLogBase, + SizeAdd, + SizeConst, + SizeExpr, + SizeLength, + SizeMax, + SizeOf +} +import v2.std.algebra { fold_list, non_empty_append, non_empty_singleton } +import v2.std.collection { List } +import v2.std.diagnostic { Locus, textual_whole_file_locus } +import v2.std.logic { Bool } +import v2.std.nat { Nat, Succ, Zero, nat_add, nat_cata, nat_lte, nat_mul } +import v2.std.optional { Absent, Optional, Present, optional_present } + +data cost_valuation_subject_note: String = "The subject of this module is SEMANTIC work, not hardware time: a CostExpr together with a COMPLETE valuation of its size variables yields how much modelled work the expression denotes. Cycles, nanoseconds and machine calibration belong to the parity plan's C5 realization bridge and are deliberately absent here, so nothing in this module may acquire a duration, a rate or a calibration constant." + +data cost_valuation_exact_core_scope_note: String = "SCOPED TO THE EXACT CORE BY OPERATOR RULING, and the two things held back are SEQUENCED rather than rejected. What is here: exact valuation at a complete binding set, CostSum binder scoping and shadowing, duplicate-binding refusal, effect refusal, logarithm refusal, and the earned-zero versus fabricated-zero distinction. What is held on branch session/deep-owl-215-partial-bounded-hold: PARTIAL evaluation - an unresolved state for a caller who never claimed completeness - and BOUNDED evaluation - a ceiling-valued binding and the interval arithmetic over it. The reason is that the program is converging on one end-to-end result, exact work and span as literal numbers for a real DAG section, and the exact core is all that milestone needs. Two constraints ride with the held work so that returning it cannot quietly undo decisions already taken. FIRST, complete and partial evaluation stay TWO ENTRY POINTS over one fold; that they are separate modes is sound and must not be collapsed back into a single evaluator, because a caller who swaps one for the other to make a refusal go away is running the author-side absorbing fallback and a single entry point would make that invisible. SECOND, the unresolved state must carry the residual COST EXPRESSION and not merely the names of the free variables: the held revision carried names only, so 3 + x lost the 3, lost the addition, and lost the shape, leaving a result no consumer could complete, lower-bound, render, or check for conservation of work. The residual must be the rich CostExpr rather than a normalized SymbolicCost, because normalization is precisely the step that discards the CostSum binder - see projection_path_binder_discard_debt_note." + +type CostValuationBinding { + variable: SizeVariable + value: Nat +} + +type CostEvaluationRefusal + = MissingSizeBinding { variable: SizeVariable, at: Locus } + | DuplicateSizeBinding { variable: SizeVariable, at: Locus } + | UnmodeledEffectCost { operation: DeclarationRef, at: Locus } + | IntegerLogarithmUnavailable { base: Nat, argument: SizeExpr, at: Locus } + | ExpressionRefused { cause: CostExprRefusalCause, at: Locus } + +data cost_evaluation_nonempty_note: String = "The nonempty carrier (std.algebra FreeSemigroup) in the refused arm is load-bearing, not decoration: a refusal carrying no cause is a nonsense state, and the free-semigroup head field makes it unwritable rather than merely unlikely - construction over validation, DESIGN section 5. Do not weaken the field to List." + +type CostEvaluation + = ExactCost { value: Nat } + | CostEvaluationRefused { causes: FreeSemigroup } + +data cost_evaluation_two_state_note: String = "Two states, because at the exact core there are exactly two honest answers: the work is this number, or here is why it cannot be. The four-state shape the design carries - adding a partial and a bounded state - is not abandoned; it returns with the work held on session/deep-owl-215-partial-bounded-hold, where each of those states will have a producer AND will carry what its consumer needs: a residual expression for the partial state, an input envelope for the bounded one. Declaring either arm here with no producer would have been rung inflation, a state named for a capability the module does not have, and the bounded arm in particular was carried through an earlier revision of this module while its arithmetic silently collapsed a two-endpoint envelope to its own ceiling." + +type CostValuationEnv { + bindings: List +} + +type BindingScan { + seen: List + duplicates: List +} + +fn cost_valuation_authority_locus() -> Locus { + textual_whole_file_locus(file: ^cost_valuation_authority_virtual_file) +} + +fn size_variable_eq(a: SizeVariable, b: SizeVariable) -> Bool { + a.source == b.source +} + +fn size_variable_in(xs: List, wanted: SizeVariable) -> Bool { + fold_list( + xs: xs, + empty: false, + cons: fn(acc, item) { acc || size_variable_eq(a: item, b: wanted) } + ) +} + +fn refuse(cause: CostEvaluationRefusal) -> CostEvaluation { + CostEvaluationRefused { causes: non_empty_singleton(item: cause) } +} + +data env_scoping_note: String = "env_bind PREPENDS and lookup_bindings answers the HEAD-most match, so a CostSum binder shadows an outer binding of the same identity for the extent of the body and only for that extent. Removal on exit is structural rather than an unbind step: the extended environment is a local value, so the environment the caller holds is the one that was never modified. That is the scoping obligation discharged by construction rather than by remembering to undo something. The lookup is written as explicit head-first recursion instead of a fold precisely because the ANSWER DEPENDS ON DIRECTION, and a fold's direction is a property of fold_list rather than of this module." + +fn env_bind(env: CostValuationEnv, binding: CostValuationBinding) -> CostValuationEnv { + CostValuationEnv { + bindings: Cons { head: binding, tail: env.bindings } + } +} + +fn lookup_bindings( + bindings: List, + variable: SizeVariable +) -> Optional { + match bindings { + Empty => Absent + Cons { head: h, tail: t } => + if size_variable_eq(a: h.variable, b: variable) { + optional_present(value: h.value) + } else { + lookup_bindings(bindings: t, variable: variable) + } + } +} + +fn env_lookup(env: CostValuationEnv, variable: SizeVariable) -> Optional { + lookup_bindings(bindings: env.bindings, variable: variable) +} + +data unbound_size_refusal_note: String = "At the exact core the caller has ASSERTED a complete valuation, so a variable with no binding is a caller defect and refuses with the variable NAMED. It may never answer zero: that is the fabricated-plausible-output class DESIGN section 5 forbids outright, and zero is exactly the value that reads as harmless in a cost report. The partial-valuation mode - for a caller who never claimed completeness, and for whom an unbound variable is an honest state rather than a defect - is held on session/deep-owl-215-partial-bounded-hold and returns as a SECOND ENTRY POINT over this same fold, never as a widening of this one." + +fn unbound_size(variable: SizeVariable) -> CostEvaluation { + refuse( + cause: MissingSizeBinding { + variable: variable, + at: cost_valuation_authority_locus() + } + ) +} + +data combine_evaluation_order_note: String = "A refusal dominates a known magnitude, which is forced rather than chosen: a refusal means the derivation is WRONG to continue, so it may not be masked by a sibling that happened to resolve. Causes ACCUMULATE when both sides refuse, because DESIGN section 5 requires each deficit's frequency to be countable and a discarded second cause is a deficit that never ranks for fixing. The op argument must be monotone for the arithmetic to be meaningful; add, mul and max are, and nothing else is passed." + +fn combine_evaluation( + a: CostEvaluation, + b: CostEvaluation, + op: fn(Nat, Nat) -> Nat +) -> CostEvaluation { + match a { + CostEvaluationRefused { causes: ca } => + match b { + CostEvaluationRefused { causes: cb } => + CostEvaluationRefused { causes: non_empty_append(left: ca, right: cb) } + ExactCost { value: vb } => CostEvaluationRefused { causes: ca } + } + ExactCost { value: va } => + match b { + CostEvaluationRefused { causes: cb } => CostEvaluationRefused { causes: cb } + ExactCost { value: vb } => ExactCost { value: op(va, vb) } + } + } +} + +data multiply_evaluations_zero_note: String = "A zero factor gives exact zero on EITHER side, and it overrides the refusal dominance that governs every other combination. That is not the absorbing fallback DESIGN section 5 forbids, and the distinction is worth stating precisely because the shapes look alike. An absorbing fallback answers when it CANNOT compute - substituting a superset or a plausible number for an unknown. This answers because it CAN: a zero multiplicity means the other factor is executed zero times, so the work it denotes is zero regardless of what that factor is and regardless of how little is modelled about it. Refusing here would be the did-no-work versus could-not-model conflation that the earned-zero controls exist to prevent, one level out - zero times an unmodelled effect is not an unknown quantity, it is no work. The third discriminator is what keeps this from being a blanket zero: ONE times an unmodelled effect still refuses, because that factor IS executed. Symmetric by construction rather than by convention, since multiplication is commutative and an operand order that changed the answer would be a defect - the same one that was found and fixed in v2.lens.cost symbolic_product while landing this. THE ORDER OF THE ARMS IS LOAD-BEARING AND THIS PARAGRAPH IS WHAT PROTECTS IT: the annihilator is checked BEFORE any refusal handling, so a REFUSAL times zero answers ExactCost zero rather than refusing. The annihilator deliberately BEATS refusal-dominance, which governs every other combination in this module. Reordering these arms to check refusals first - which reads like tightening a fail-closed path and is therefore the tempting edit - silently restores the defect this function exists to fix, and it would do so while every other witness in the file stays green. Only zero_times_an_unmodelled_effect_is_exactly_zero and an_unmodelled_effect_times_zero_is_exactly_zero would red, and they are enrolled for exactly that reason. The delegation is also deliberate: the residual after annihilator handling is EXACTLY refusal-dominance - exact times exact multiplies, anything carrying a refusal refuses, causes accumulate - so it calls combine_evaluation rather than restating it. What must never move into that generic combiner is the annihilator itself, because addition and max do not have one." + +fn multiply_evaluations(a: CostEvaluation, b: CostEvaluation) -> CostEvaluation { + match a { + ExactCost { value: Zero } => ExactCost { value: Zero } + _ => + match b { + ExactCost { value: Zero } => ExactCost { value: Zero } + _ => combine_evaluation(a: a, b: b, op: nat_mul) + } + } +} + +fn evaluate_size_expr(size: SizeExpr, env: CostValuationEnv) -> CostEvaluation { + match size { + SizeConst { value: v } => ExactCost { value: v } + SizeOf { variable: v } => + match env_lookup(env: env, variable: v) { + Present { value: n } => ExactCost { value: n } + Absent => unbound_size(variable: v) + } + SizeLength { of: v } => + match env_lookup(env: env, variable: v) { + Present { value: n } => ExactCost { value: n } + Absent => unbound_size(variable: v) + } + SizeAdd { left: l, right: r } => + combine_evaluation( + a: evaluate_size_expr(size: l, env: env), + b: evaluate_size_expr(size: r, env: env), + op: nat_add + ) + SizeMax { left: l, right: r } => + combine_evaluation( + a: evaluate_size_expr(size: l, env: env), + b: evaluate_size_expr(size: r, env: env), + op: v2.std.nat.nat_max + ) + } +} + +type SummationState { + index: Nat + accumulated: CostEvaluation +} + +data summation_semantics_note: String = "CostSum with binder i, upper u and body b denotes the sum of b evaluated at i = 0, 1, .. u-1: u iterations with the binder taking a distinct value in each. It is therefore evaluated by ITERATING the body under an extended environment, never by multiplying one body evaluation by the iteration count - the latter is correct only when the body is invariant in the binder, and silently wrong when it is not. Zero iterations produce exact zero, which is the empty sum and the one place a zero here is earned; it is paired with the missing-binding refusal so that a zero in a cost report is never ambiguous between nothing to do and nothing modelled." + +data summation_settled_disposition_note: String = "Once the accumulator has refused, later iterations do not evaluate the body. This is a COST fix with a soundness argument, not an optimisation, and both halves matter. The cost: non_empty_append is linear in its left argument because list_append folds the left side, so accumulating one cause per iteration is quadratic in the iteration count - and CostEffect refuses unconditionally in this slice, so any loop containing an effect reaches it, at whatever size the bound happens to be. The standing bare-minimum-cost rule fixes a proven quadratic fold regardless of the realized n, because n is not a time-stable fact. The signal: those causes are IDENTICAL - the body expression is fixed across iterations and only the binder VALUE changes - so accumulating them amplified one deficit u times rather than counting u deficits, degrading the very countability the accumulate rule exists to protect. The soundness argument for skipping, stated so it can be re-checked rather than trusted: a refusal here is a property of the body EXPRESSION, not of the binder's value - unboundness, an unmodelled effect, an invalid log base and an unavailable integer logarithm are all value-independent - so a body that refuses at one iteration refuses at every one. Dissolve-on: the first value-DEPENDENT refusal cause, at which point this skip becomes unsound and the fix becomes cause-identity dedup instead." + +fn evaluate_summation( + binder: SizeVariable, + iterations: Nat, + env: CostValuationEnv, + evaluate_body: fn(CostValuationEnv) -> CostEvaluation +) -> CostEvaluation { + nat_cata( + n: iterations, + zero: SummationState { index: Zero, accumulated: ExactCost { value: Zero } }, + succ: fn(state) { + SummationState { + index: Succ { prev: state.index }, + accumulated: match state.accumulated { + CostEvaluationRefused { causes: c } => CostEvaluationRefused { causes: c } + ExactCost { value: acc } => combine_evaluation( + a: state.accumulated, + b: evaluate_body( + env_bind( + env: env, + binding: CostValuationBinding { variable: binder, value: state.index } + ) + ), + op: nat_add + ) + } + } + } + ).accumulated +} + +data cost_log_evaluation_note: String = "THREE distinct facts, reported as three distinct causes, because a logarithm can fail in three unrelated ways and collapsing them misdirects every reader of the diagnostic. An earlier revision of this arm ignored the base entirely and answered UngroundedLogArgument for every non-refusing case, which reported base 0 as an ARGUMENT problem and called a fully grounded argument UNGROUNDED - two paths disagreeing about one fact, while v2.lens.cost.expr's normalizer right beside this one already checked the base against its own InvalidLogBase vocabulary. (1) An INVALID BASE, 0 or 1, where no logarithm is defined, refuses through that expression authority's InvalidLogBase - the single authority for that fact, cited rather than re-minted. (2) An UNBOUND ARGUMENT refuses as MissingSizeBinding like any other unbound size, because the argument is an ordinary SizeExpr and nothing about a logarithm changes that. (3) A VALID base with an EXACT argument is a well-posed question this module cannot yet answer: an exact Nat-valued logarithm needs a floor-log authority std does not carry, and minting one inside a lens module would be the re-invention DESIGN section 2 calls a failed decomposition - so it refuses as IntegerLogarithmUnavailable, a cause that names the real gap and is countable against it. Dissolve-on: a cited integer-logarithm authority on std.nat, at which point case 3 answers ExactCost and IntegerLogarithmUnavailable is deleted with it." + +fn evaluate_cost_log( + base: Nat, + argument: SizeExpr, + env: CostValuationEnv +) -> CostEvaluation { + if nat_lte(a: base, b: Succ { prev: Zero }) { + refuse( + cause: ExpressionRefused { + cause: InvalidLogBase { + base: base, + at: cost_valuation_authority_locus() + }, + at: cost_valuation_authority_locus() + } + ) + } else { + match evaluate_size_expr(size: argument, env: env) { + CostEvaluationRefused { causes: c } => CostEvaluationRefused { causes: c } + ExactCost { value: _ } => + refuse( + cause: IntegerLogarithmUnavailable { + base: base, + argument: argument, + at: cost_valuation_authority_locus() + } + ) + } + } +} + +fn evaluate_cost_expr_in_env(expr: CostExpr, env: CostValuationEnv) -> CostEvaluation { + match expr { + CostConst { value: v } => ExactCost { value: v } + CostAdd { left: l, right: r } => + combine_evaluation( + a: evaluate_cost_expr_in_env(expr: l, env: env), + b: evaluate_cost_expr_in_env(expr: r, env: env), + op: nat_add + ) + CostMul { left: l, right: r } => + multiply_evaluations( + a: evaluate_cost_expr_in_env(expr: l, env: env), + b: evaluate_cost_expr_in_env(expr: r, env: env) + ) + CostMax { left: l, right: r } => + combine_evaluation( + a: evaluate_cost_expr_in_env(expr: l, env: env), + b: evaluate_cost_expr_in_env(expr: r, env: env), + op: v2.std.nat.nat_max + ) + CostSum { binder: bi, upper: u, body: bd } => + match evaluate_size_expr(size: u, env: env) { + ExactCost { value: n } => + evaluate_summation( + binder: bi, + iterations: n, + env: env, + evaluate_body: fn(inner) { + evaluate_cost_expr_in_env(expr: bd, env: inner) + } + ) + CostEvaluationRefused { causes: c } => CostEvaluationRefused { causes: c } + } + CostLog { base: b, argument: a } => + evaluate_cost_log(base: b, argument: a, env: env) + CostEffect { operation: op } => + refuse( + cause: UnmodeledEffectCost { + operation: op, + at: cost_valuation_authority_locus() + } + ) + CostRefused { cause: c } => + refuse( + cause: ExpressionRefused { + cause: c, + at: cost_valuation_authority_locus() + } + ) + } +} + +fn scan_bindings(bindings: List) -> BindingScan { + fold_list( + xs: bindings, + empty: BindingScan { seen: [], duplicates: [] }, + cons: fn(acc, item) { + if size_variable_in(xs: acc.seen, wanted: item.variable) { + BindingScan { + seen: acc.seen, + duplicates: Cons { head: item.variable, tail: acc.duplicates } + } + } else { + BindingScan { + seen: Cons { head: item.variable, tail: acc.seen }, + duplicates: acc.duplicates + } + } + } + ) +} + +data duplicate_binding_note: String = "A duplicate binding for one variable is refused rather than resolved by a first-wins or last-wins rule, because both rules answer a number for a question the caller asked two ways. Note the scope precisely: this checks the CALLER-supplied valuation only. A CostSum binder that shadows an outer binding of the same identity is not a duplicate - it is correct lexical scoping - and the two are kept apart by scanning the supplied list ONCE at entry, before any binder extends the environment." + +fn refuse_duplicate(variable: SizeVariable) -> CostEvaluation { + refuse( + cause: DuplicateSizeBinding { + variable: variable, + at: cost_valuation_authority_locus() + } + ) +} + +fn duplicate_binding_refusal( + duplicates: List +) -> Optional { + fold_list( + xs: duplicates, + empty: Absent, + cons: fn(acc, item) { + match acc { + Absent => Present { value: refuse_duplicate(variable: item) } + Present { value: v } => + Present { + value: combine_evaluation( + a: v, + b: refuse_duplicate(variable: item), + op: nat_add + ) + } + } + } + ) +} + +data projection_path_binder_discard_debt_note: String = "TRACKED DEBT, on a path this module does not use. v2.lens.cost.expr normalize_cost_expr_to_symbolic matches CostSum with the binder DISCARDED, so a binder-dependent body projects a SymbolicCost naming a variable that is bound inside the sum; the magnitude may survive but the variable identity does not, and a consumer comparing on identity gets a well-formed wrong answer. It is reachable through a body of CostLog whose argument is SizeOf of the binder. This module's evaluator does not inherit the defect - it binds the binder and shadows lexically - so the two paths now disagree, which is why the defect is named HERE rather than left for the next reader to rediscover from the divergence. It is deliberately not fixed by the change that landed this evaluator: the projection feeds the enrolled Blocking cost wall and has its own consumers, so it is a separate subject with its own regression surface. It is also why the held partial-evaluation work must carry a rich CostExpr residual rather than a normalized SymbolicCost - normalization is exactly the lossy step. Trigger: fix normalize_cost_expr_to_symbolic to carry the binder, with a discriminating witness whose binder and bound variable are DISTINCT, since the existing bounded_summation fixture uses the same variable for both and therefore cannot see this class. This row dissolves when that witness is green." + +fn evaluate_cost_expr( + expr: CostExpr, + bindings: List +) -> CostEvaluation { + match duplicate_binding_refusal( + duplicates: scan_bindings(bindings: bindings).duplicates + ) { + Present { value: refusal } => refusal + Absent => + evaluate_cost_expr_in_env( + expr: expr, + env: CostValuationEnv { bindings: bindings } + ) + } +} diff --git a/src/v2/lens/cost/valuation_test.dag b/src/v2/lens/cost/valuation_test.dag new file mode 100644 index 00000000000..8c81c514974 --- /dev/null +++ b/src/v2/lens/cost/valuation_test.dag @@ -0,0 +1,471 @@ +module v2.test.lens_cost.valuation + +import std.algebra { Empty } +import std.decl_ref { DeclarationRef, WholeDeclaration } +import v2.lens.cost { ConstantCost, SizeVariable, SymbolicCost, UnknownCost, symbolic_product, unit_cost, zero_cost } +import v2.lens.cost.expr { + CostAdd, + CostConst, + CostEffect, + CostExpr, + CostLog, + CostMul, + CostSum, + InvalidLogBase, + SizeConst, + normalize_cost_expr_to_symbolic, + size_of +} +import v2.lens.cost.valuation { + CostEvaluation, + CostEvaluationRefused, + CostValuationBinding, + DuplicateSizeBinding, + ExactCost, + ExpressionRefused, + IntegerLogarithmUnavailable, + MissingSizeBinding, + UnmodeledEffectCost, + evaluate_cost_expr +} +import v2.std.live_tree { LiveTreeDisposition, SubstrateInputsOnly } +import v2.std.logic { Bool } +import v2.std.nat { Nat, Succ, Zero } +import v2.std.node { + Atom, + Node, + Symbol, + SyntheticOccurrence, + TypeNode +} +import v2.std.verification { + EqualsClaim, + ManualAnchorAbsent, + TestClaim, + TestClassification, + Tier1, + Unit, + manual_claim_anchor +} + +data live_tree_disposition: LiveTreeDisposition = SubstrateInputsOnly + +data nat_1: Nat = Succ { prev: Zero } +data nat_2: Nat = Succ { prev: nat_1 } +data nat_3: Nat = Succ { prev: nat_2 } +data nat_4: Nat = Succ { prev: nat_3 } +data nat_5: Nat = Succ { prev: nat_4 } +data nat_6: Nat = Succ { prev: nat_5 } +data nat_7: Nat = Succ { prev: nat_6 } +data nat_8: Nat = Succ { prev: nat_7 } +data nat_9: Nat = Succ { prev: nat_8 } +data nat_10: Nat = Succ { prev: nat_9 } + +fn synthetic_leaf(identity: Symbol) -> Node { + Node { + kind: TypeNode { connective: Atom { identity: identity } }, + children: [], + occurrence_id: SyntheticOccurrence + } +} + +data outer_leaf: Node = synthetic_leaf(identity: ^valuation_outer_size_atom) +data inner_leaf: Node = synthetic_leaf(identity: ^valuation_inner_size_atom) + +data outer_variable: SizeVariable = SizeVariable { source: outer_leaf } +data inner_variable: SizeVariable = SizeVariable { source: inner_leaf } + +fn bind(variable: SizeVariable, value: Nat) -> CostValuationBinding { + CostValuationBinding { variable: variable, value: value } +} + +fn unit_loop_over(variable: SizeVariable) -> CostExpr { + CostSum { + binder: inner_variable, + upper: size_of(variable: variable), + body: CostConst { value: nat_1 } + } +} + +fn is_exact(evaluation: CostEvaluation, expected: Nat) -> Bool { + match evaluation { + ExactCost { value: v } => v == expected + _ => false + } +} + +test fn unit_body_over_size_five_evaluates_to_five() -> Bool { + is_exact( + evaluation: evaluate_cost_expr( + expr: unit_loop_over(variable: outer_variable), + bindings: [bind(variable: outer_variable, value: nat_5)] + ), + expected: nat_5 + ) +} + +test fn changing_the_bound_size_changes_the_derived_work() -> Bool { + is_exact( + evaluation: evaluate_cost_expr( + expr: unit_loop_over(variable: outer_variable), + bindings: [bind(variable: outer_variable, value: nat_10)] + ), + expected: nat_10 + ) && !is_exact( + evaluation: evaluate_cost_expr( + expr: unit_loop_over(variable: outer_variable), + bindings: [bind(variable: outer_variable, value: nat_10)] + ), + expected: nat_5 + ) +} + +fn binder_dependent_loop() -> CostExpr { + CostSum { + binder: outer_variable, + upper: size_of(variable: outer_variable), + body: CostSum { + binder: inner_variable, + upper: size_of(variable: outer_variable), + body: CostConst { value: nat_1 } + } + } +} + +test fn binder_dependent_body_is_summed_not_treated_as_invariant() -> Bool { + is_exact( + evaluation: evaluate_cost_expr( + expr: binder_dependent_loop(), + bindings: [bind(variable: outer_variable, value: nat_5)] + ), + expected: nat_10 + ) +} + +test fn invariant_body_control_does_not_produce_the_summed_answer() -> Bool { + is_exact( + evaluation: evaluate_cost_expr( + expr: CostSum { + binder: outer_variable, + upper: size_of(variable: outer_variable), + body: CostConst { value: nat_1 } + }, + bindings: [bind(variable: outer_variable, value: nat_5)] + ), + expected: nat_5 + ) +} + +test fn missing_binding_refuses_and_never_becomes_zero() -> Bool { + match evaluate_cost_expr( + expr: unit_loop_over(variable: outer_variable), + bindings: [] + ) { + CostEvaluationRefused { causes: c } => + match c.head { + MissingSizeBinding { variable: v, at: _ } => v.source == outer_leaf + _ => false + } + ExactCost { value: _ } => false + } +} + +test fn duplicate_bindings_refuse() -> Bool { + match evaluate_cost_expr( + expr: unit_loop_over(variable: outer_variable), + bindings: [ + bind(variable: outer_variable, value: nat_5), + bind(variable: outer_variable, value: nat_10) + ] + ) { + CostEvaluationRefused { causes: c } => + match c.head { + DuplicateSizeBinding { variable: v, at: _ } => v.source == outer_leaf + _ => false + } + _ => false + } +} + +test fn distinct_bindings_control_does_not_refuse() -> Bool { + is_exact( + evaluation: evaluate_cost_expr( + expr: unit_loop_over(variable: outer_variable), + bindings: [ + bind(variable: outer_variable, value: nat_5), + bind(variable: inner_variable, value: nat_10) + ] + ), + expected: nat_5 + ) +} + +fn shadowing_expr() -> CostExpr { + CostAdd { + left: CostSum { + binder: outer_variable, + upper: SizeConst { value: nat_2 }, + body: unit_loop_over(variable: outer_variable) + }, + right: unit_loop_over(variable: outer_variable) + } +} + +test fn binder_shadowing_is_scoped_and_removed_on_exit() -> Bool { + is_exact( + evaluation: evaluate_cost_expr( + expr: shadowing_expr(), + bindings: [bind(variable: outer_variable, value: nat_3)] + ), + expected: nat_4 + ) +} + +test fn shadowing_control_rejects_the_unshadowed_reading() -> Bool { + !is_exact( + evaluation: evaluate_cost_expr( + expr: shadowing_expr(), + bindings: [bind(variable: outer_variable, value: nat_3)] + ), + expected: nat_9 + ) +} + +test fn zero_iterations_produce_exact_zero() -> Bool { + is_exact( + evaluation: evaluate_cost_expr( + expr: CostSum { + binder: inner_variable, + upper: SizeConst { value: Zero }, + body: CostConst { value: nat_1 } + }, + bindings: [] + ), + expected: Zero + ) +} + +data effect_operation: DeclarationRef = DeclarationRef { + module_path: "v2.test.lens_cost.valuation", + decl_name: "unmodelled_effect_specimen", + field: WholeDeclaration +} + +test fn cost_effect_refuses_until_an_effect_model_exists() -> Bool { + match evaluate_cost_expr( + expr: CostEffect { operation: effect_operation }, + bindings: [] + ) { + CostEvaluationRefused { causes: c } => + match c.head { + UnmodeledEffectCost { operation: _, at: _ } => true + _ => false + } + ExactCost { value: _ } => false + } +} + +data log_cause_separation_note: String = "Four witnesses for one construct, because a logarithm fails in three unrelated ways and an earlier revision of the evaluator reported every non-refusing case as UngroundedLogArgument - ignoring the base entirely, so base 0 read as an ARGUMENT problem and a fully grounded argument was called UNGROUNDED. Each witness pins one cause. The discriminating pair is base-zero against grounded-argument: under the earlier arm both answered the same cause, so either one alone would have passed while the arm was wrong, and only asserting that they differ catches it." + +test fn log_base_zero_refuses_as_an_invalid_base() -> Bool { + match evaluate_cost_expr( + expr: CostLog { base: Zero, argument: size_of(variable: outer_variable) }, + bindings: [bind(variable: outer_variable, value: nat_8)] + ) { + CostEvaluationRefused { causes: c } => + match c.head { + ExpressionRefused { cause: inner, at: _ } => + match inner { + InvalidLogBase { base: b, at: _ } => b == Zero + _ => false + } + _ => false + } + _ => false + } +} + +test fn log_base_one_refuses_as_an_invalid_base() -> Bool { + match evaluate_cost_expr( + expr: CostLog { base: nat_1, argument: size_of(variable: outer_variable) }, + bindings: [bind(variable: outer_variable, value: nat_8)] + ) { + CostEvaluationRefused { causes: c } => + match c.head { + ExpressionRefused { cause: inner, at: _ } => + match inner { + InvalidLogBase { base: b, at: _ } => b == nat_1 + _ => false + } + _ => false + } + _ => false + } +} + +test fn log_of_a_grounded_argument_names_the_missing_authority_not_the_argument() -> Bool { + match evaluate_cost_expr( + expr: CostLog { base: nat_2, argument: size_of(variable: outer_variable) }, + bindings: [bind(variable: outer_variable, value: nat_8)] + ) { + CostEvaluationRefused { causes: c } => + match c.head { + IntegerLogarithmUnavailable { base: b, argument: _, at: _ } => b == nat_2 + _ => false + } + _ => false + } +} + +test fn log_of_an_unbound_argument_refuses_as_a_missing_binding() -> Bool { + match evaluate_cost_expr( + expr: CostLog { base: nat_2, argument: size_of(variable: outer_variable) }, + bindings: [] + ) { + CostEvaluationRefused { causes: c } => + match c.head { + MissingSizeBinding { variable: v, at: _ } => v.source == outer_leaf + _ => false + } + _ => false + } +} + +data refusing_body_cause_count_note: String = "Ten iterations of a body that refuses unconditionally yield ONE cause, not ten. Both halves of that are the subject: ten identical causes would amplify a single deficit tenfold, degrading the countability the accumulate rule exists to protect, and building them costs quadratic time because non_empty_append is linear in its left argument. This witness reds if the settled-disposition skip in evaluate_summation is removed, which is what makes it a regression control rather than a description." + +test fn refusing_body_under_a_bound_yields_exactly_one_cause() -> Bool { + match evaluate_cost_expr( + expr: CostSum { + binder: inner_variable, + upper: size_of(variable: outer_variable), + body: CostEffect { operation: effect_operation } + }, + bindings: [bind(variable: outer_variable, value: nat_10)] + ) { + CostEvaluationRefused { causes: c } => + match c.tail { + Empty => true + _ => false + } + _ => false + } +} + +data zero_multiplicity_note: String = "Three discriminators, and the third is what keeps the first two from being a blanket zero. A zero factor means the other factor is executed ZERO times, so its work is zero whatever it is - refusing there would conflate did-no-work with could-not-model, which is the earned-zero distinction one level out. Both operand orders are asserted because multiplication is commutative and an order-sensitive answer is a defect; that exact defect existed in v2.lens.cost symbolic_product, which matched UnknownCost on the left operand before ever inspecting the right, and is fixed with this change. ONE times an unmodelled effect still REFUSES, because that factor is executed." + +test fn zero_times_an_unmodelled_effect_is_exactly_zero() -> Bool { + is_exact( + evaluation: evaluate_cost_expr( + expr: CostMul { + left: CostConst { value: Zero }, + right: CostEffect { operation: effect_operation } + }, + bindings: [] + ), + expected: Zero + ) +} + +test fn an_unmodelled_effect_times_zero_is_exactly_zero() -> Bool { + is_exact( + evaluation: evaluate_cost_expr( + expr: CostMul { + left: CostEffect { operation: effect_operation }, + right: CostConst { value: Zero } + }, + bindings: [] + ), + expected: Zero + ) +} + +test fn one_times_an_unmodelled_effect_still_refuses() -> Bool { + match evaluate_cost_expr( + expr: CostMul { + left: CostConst { value: nat_1 }, + right: CostEffect { operation: effect_operation } + }, + bindings: [] + ) { + CostEvaluationRefused { causes: c } => + match c.head { + UnmodeledEffectCost { operation: _, at: _ } => true + _ => false + } + ExactCost { value: _ } => false + } +} + +data symbolic_product_commutativity_note: String = "Every arm is asserted in BOTH operand orders - the zero absorption AND the one-times-unknown non-absorption - because the defect being fixed was precisely that operand order changed the answer, so a one-sided assertion is the shape that missed it in the first place. The projection authority is asserted in both orders, because it previously answered zero in one and unknown in the other. The unknown-times-zero direction is the one that was wrong and is the regression control for the reorder; the zero-times-unknown direction must keep working and is the control that the reorder did not simply swap the bug to the other side." + +fn unknown_symbolic_cost() -> SymbolicCost { + normalize_cost_expr_to_symbolic(expr: CostEffect { operation: effect_operation }) +} + +test fn symbolic_product_absorbs_zero_from_the_left() -> Bool { + match symbolic_product(a: zero_cost(), b: unknown_symbolic_cost()) { + ConstantCost { value: Zero } => true + _ => false + } +} + +test fn symbolic_product_absorbs_zero_from_the_right() -> Bool { + match symbolic_product(a: unknown_symbolic_cost(), b: zero_cost()) { + ConstantCost { value: Zero } => true + _ => false + } +} + +test fn symbolic_product_still_returns_unknown_without_a_zero_factor() -> Bool { + match symbolic_product(a: unknown_symbolic_cost(), b: unit_cost()) { + UnknownCost { diagnostic: _ } => true + _ => false + } +} + +test fn symbolic_product_one_times_unknown_stays_unknown() -> Bool { + match symbolic_product(a: unit_cost(), b: unknown_symbolic_cost()) { + UnknownCost { diagnostic: _ } => true + _ => false + } +} + +data claim_conjunction_totality_note: String = "The conjunction enumerates EVERY other test fn in this file, and that totality is the point rather than a convenience. It is itself a `test fn` rather than a plain helper, which the corpus naming-hygiene walk requires and which is not a formality here: reached only from the claim `data` it would have been unreachable from every `test fn`, i.e. silently de-enrolled - the conjunction added to close a specification-without-execution finding, not executing. An earlier revision listed three of them while the claim label asserted refusal and scoping behaviour the others established, so the claim could have gone green with its own label false - specification-without-execution at the claim seam, caught by review 49620. The rule this file now follows: a claim label may assert only what its conjunction executes, so adding a test fn without adding it here is the defect to watch for." + +test fn every_valuation_witness_holds() -> Bool { + unit_body_over_size_five_evaluates_to_five() + && changing_the_bound_size_changes_the_derived_work() + && binder_dependent_body_is_summed_not_treated_as_invariant() + && invariant_body_control_does_not_produce_the_summed_answer() + && missing_binding_refuses_and_never_becomes_zero() + && duplicate_bindings_refuse() + && distinct_bindings_control_does_not_refuse() + && binder_shadowing_is_scoped_and_removed_on_exit() + && shadowing_control_rejects_the_unshadowed_reading() + && zero_iterations_produce_exact_zero() + && cost_effect_refuses_until_an_effect_model_exists() + && log_base_zero_refuses_as_an_invalid_base() + && log_base_one_refuses_as_an_invalid_base() + && log_of_a_grounded_argument_names_the_missing_authority_not_the_argument() + && log_of_an_unbound_argument_refuses_as_a_missing_binding() + && refusing_body_under_a_bound_yields_exactly_one_cause() + && zero_times_an_unmodelled_effect_is_exactly_zero() + && an_unmodelled_effect_times_zero_is_exactly_zero() + && one_times_an_unmodelled_effect_still_refuses() + && symbolic_product_absorbs_zero_from_the_left() + && symbolic_product_absorbs_zero_from_the_right() + && symbolic_product_still_returns_unknown_without_a_zero_factor() + && symbolic_product_one_times_unknown_stays_unknown() +} + +data claim_cost_valuation: TestClaim = EqualsClaim { + label: "lens_cost/valuation: CostExpr evaluated at a complete SizeVariable valuation yields exact semantic work, refuses a missing or duplicated binding rather than answering zero, scopes a CostSum binder to its body, and separates the three ways a logarithm fails - every leaf witness in this file enrolled in the conjunction", + anchor: manual_claim_anchor(anchor: ManualAnchorAbsent), + lhs: outer_leaf, + rhs: if every_valuation_witness_holds() { + outer_leaf + } else { + synthetic_leaf(identity: ^valuation_claim_failed) + }, + classification: TestClassification { tier: Tier1, layer: Unit } +} diff --git a/src/v2/lens/inert_carrier.dag b/src/v2/lens/inert_carrier.dag index 668c24b2cc4..1c32ca65422 100644 --- a/src/v2/lens/inert_carrier.dag +++ b/src/v2/lens/inert_carrier.dag @@ -23,9 +23,10 @@ data inert_carrier_roster: List = [ inert_row(unit: "GitCliReportedVersion", reason: "modeled git-cli extdeps carrier with no live consumer yet"), inert_row(unit: "GitPushRequest", reason: "modeled git publication-transport carrier (extdeps.git.publication_transport slice 1): witness-tested in publication_publisher_witness_test with no non-test consumer yet; live transport binding awaits tools.publication_publisher slice"), inert_row(unit: "LocalAlias", reason: "inert G1 fixture type in qualified_module_projection_stripped_fixture.dag (see inert_carrier_local_alias_roster_note)"), - inert_row(unit: "ProcMeminfo", reason: "modeled machine-facts carrier with no live consumer yet"), inert_row(unit: "ReactHookSite", reason: "modeled typescript extdeps carrier with no live consumer yet"), - inert_row(unit: "SystemdUnitStatus", reason: "modeled systemd extdeps carrier with no live consumer yet") + inert_row(unit: "SystemdUnitStatus", reason: "modeled systemd extdeps carrier with no live consumer yet"), + inert_row(unit: "TerminatingOneShotFrontier", reason: "modeled std.witness_purpose frontier coproduct from #7965 (Slice C-a): its variants name the two substrate absences that block a terminating one-shot classification, and only its own test file references it, so it is inert by the seed rule until the classifier consumes it"), + inert_row(unit: "WitnessPurpose", reason: "modeled std.witness_purpose taxonomy from #7965 (Slice C-a): the stable purpose coproduct a witness declares, landed ahead of the consumer that derives witness size from it, with no non-test reference yet") ] fn inert_carrier_rostered_names() -> List { diff --git a/src/v2/std/algebra.dag b/src/v2/std/algebra.dag index d4e79c2668b..797098e592a 100644 --- a/src/v2/std/algebra.dag +++ b/src/v2/std/algebra.dag @@ -12,6 +12,7 @@ import std.algebra { Equal, Field, FreeMonoid, + FreeSemigroup, Greater, Group, Lattice, @@ -692,6 +693,26 @@ fn list_snoc_item(xs: FreeMonoid, item: T) -> FreeMonoid { list_append(left: xs, right: Cons { head: item, tail: Empty }) } +data free_semigroup_grounding_note: String = "FreeSemigroup is the free SEMIGROUP over T exactly as FreeMonoid is the free MONOID over T, so the pair is one algebraic axis read at two identities rather than a second sequence vocabulary (DESIGN section 2). The head field is the construction wall: an empty inhabitant has no representation, so a nonempty-by-obligation collection is UNWRITABLE empty rather than validated nonempty - the structurally-impossible rung of DESIGN section 4b rather than the mechanically-preventable one. This is deliberately NOT the Refined> spelling the manual fixture v2.test.claim.manual.refinement_nonempty_list carries: a refinement predicate is a validation that concedes the empty state is writable, and the NonEmptyList ALIAS is withheld while that fixture lives so one name never resolves to two declarations. CONVERGENCE DEBT, stated at the grain grep decides rather than at the grain that reads well. FIVE carriers in the tree are this same shape monomorphised: v2.std.diagnostic NonEmptyDiagnostics, v2.std.collection FiniteSet, gunbc.process_algebra NonEmptyProcessNodeIds, v2.compiler.self_host.frontier_probe_types NonEmptySymbolChain, and v2.std.grammar_choice_ambiguity NonEmptyGrammarChoiceAmbiguityRows. Only the last TWO carry a dissolution trigger today - non_empty_symbol_chain_dissolve_trigger and non_empty_grammar_choice_ambiguity_rows_dissolve_trigger, both retargeted onto this declaration by the change that landed it. The first three carry NO trigger and are therefore untracked stalls owed a follow-up row; an earlier revision of this note asserted all four of the carriers it named already carried one, which was false of two of them and is the cited-symbol class DESIGN section 3 names, sitting in the note that argues for single authority. The retarget was not tidying: both surviving triggers named the event as promoting the manual REFINEMENT to std, and the change that landed this declaration decided that promotion is not the mechanism, so those two carriers would otherwise have been left waiting on an event that cannot occur as spelled - an untracked stall wearing a tracked one's clothes. The migrations themselves are deliberately not carried by the lane that landed this authority, because a corpus-wide de-fork is not a consequence of the authority existing." + +fn non_empty_singleton(item: T) -> FreeSemigroup { + FreeSemigroup { head: item, tail: Empty } +} + +fn non_empty_append(left: FreeSemigroup, right: FreeSemigroup) -> FreeSemigroup { + FreeSemigroup { + head: left.head, + tail: list_append( + left: list_snoc_item(xs: left.tail, item: right.head), + right: right.tail + ) + } +} + +fn non_empty_to_list(xs: FreeSemigroup) -> FreeMonoid { + Cons { head: xs.head, tail: xs.tail } +} + fn list_init(xs: FreeMonoid) -> FreeMonoid { match xs { Empty => Empty diff --git a/src/v2/std/grammar_choice_ambiguity.dag b/src/v2/std/grammar_choice_ambiguity.dag index 681e9c734e3..c6d29bf6035 100644 --- a/src/v2/std/grammar_choice_ambiguity.dag +++ b/src/v2/std/grammar_choice_ambiguity.dag @@ -19,4 +19,4 @@ type NonEmptyGrammarChoiceAmbiguityRows { tail: FreeMonoid } -data non_empty_grammar_choice_ambiguity_rows_dissolve_trigger: String = "migrate_when_nonempty_list_refinement_promoted — NonEmptyGrammarChoiceAmbiguityRows dissolves into NonEmptyList when the manual NonEmptyList refinement is promoted from v2.test.claim.manual.refinement_nonempty_list to std." +data non_empty_grammar_choice_ambiguity_rows_dissolve_trigger: String = "migrate_when_free_semigroup_available — NonEmptyGrammarChoiceAmbiguityRows dissolves into std.algebra FreeSemigroup. RETARGETED: this trigger previously named the promotion of the manual Refined> fixture to std, and the generic carrier that landed is a record with a head field rather than that refinement, with the NonEmptyList alias deliberately withheld while the fixture lives - so the event as previously spelled will not occur and this row would have stalled untracked. The construction wall is now available; see std.algebra free_semigroup_grounding_note." diff --git a/src/v2/std/nat.dag b/src/v2/std/nat.dag index 172be1c9fea..70218c5b9e4 100644 --- a/src/v2/std/nat.dag +++ b/src/v2/std/nat.dag @@ -53,6 +53,16 @@ fn nat_lte(a: Nat, b: Nat) -> Bool { } } +data nat_max_two_nat_authorities_note: String = "This is NOT a duplicate of std.nat nat_max, and the distinction is worth stating because the name alone suggests otherwise. std.nat Nat is CommutativeSemiring - an algebra alias whose max is written with the host comparison operators - while v2.std.nat Nat is the Peano coproduct Zero | Succ, and the two are different types that no single function can serve. So this sits beside nat_add and nat_mul, which are forked for exactly the same reason and were not remarked on. What IS a real defect is that two Nat authorities exist at all; it predates this declaration and is the numeric-tower grounding thread's subject, not something a max function can close. Because v1-seed function names are not module-scoped, a bare nat_max reference in any closure containing both modules is ambiguous and must be qualified - v2.lens.cost.valuation does exactly that. Dissolve-on: one Nat authority, at which point one of the two nat_max declarations goes with it." + +fn nat_max(a: Nat, b: Nat) -> Nat { + match nat_compare(a: a, b: b) { + Less => b + Equal => a + Greater => a + } +} + fn nat_gte(a: Nat, b: Nat) -> Bool { match nat_compare(a: a, b: b) { Less => false diff --git a/src/v2/test/lens_mock_totality/git_mock_totality_test.dag b/src/v2/test/lens_mock_totality/git_mock_totality_test.dag index 66549033fe1..81a3d0392bc 100644 --- a/src/v2/test/lens_mock_totality/git_mock_totality_test.dag +++ b/src/v2/test/lens_mock_totality/git_mock_totality_test.dag @@ -22,6 +22,10 @@ fn materialize_git_mock(case: PublishedMockCase) -> Outcome outcome_accepted(value: MaterializedGitMock { tag: ^materialized_merge_base }) } else if case.operation_key == "git.Inspect.ListTreePathsAtRevision" { outcome_accepted(value: MaterializedGitMock { tag: ^materialized_list_tree_paths_at_revision }) + } else if case.operation_key == "git.Inspect.WorkingTreeStatus" { + outcome_accepted(value: MaterializedGitMock { tag: ^materialized_working_tree_status }) + } else if case.operation_key == "git.Inspect.IgnoredFiles" { + outcome_accepted(value: MaterializedGitMock { tag: ^materialized_ignored_files }) } else if case.operation_key == "git.Core.LsFiles" { outcome_accepted(value: MaterializedGitMock { tag: ^materialized_ls_files }) } else if case.operation_key == "git.Core.Diff" {