0bdb3a441c
ADR-0175 Phase 3 splits wrong=0-first: build the gate (3a) and PROVE invariant #2 before the bounded search (3b) that could exploit gaps. generate/derivation/: - model.py: Quantity / Step / GroundedDerivation. A derivation is a left-fold over text-sourced quantities; each Step carries its licensing cue (the lexeme the search claims licenses the op). - verify.py: self_verifies() — grounded operands ∧ grounded operation cues ∧ unit consistency ∧ no divide-by-zero. Grounding REUSES the canonical primitives from math_roundtrip (_tokens/_token_in/_value_grounds) so the gate cannot drift from the round-trip contract. select_self_verified() adds the uniqueness rule: unique self-verifying answer resolves; zero or disagreeing refuse (wrong=0). INVARIANT #2 proven (TestInvariant2_NoSpuriousSelfVerification): the gate refuses to self-verify a derivation that is not grounded+unit-consistent+unique even when its value coincides with gold — the 20/5==4 class: - invented operand not in text -> refused - operation cue not in text -> refused (division not licensed by any present cue) - value coincidence (20/5=4) with ungrounded op -> still refused - add across units (pounds + reps) -> refused - divide-by-zero -> refused Plus uniqueness: disagreeing grounded derivations -> refuse; agreeing -> resolve. Phase 3a is inert (nothing wires generate.derivation into serving). 3b is the bounded search that produces derivations for this gate + measures the flip-curve in the practice lane under perturbation. Verified: 16/16; ruff clean; smoke 67/67; no serving import.
72 lines
2.4 KiB
Python
72 lines
2.4 KiB
Python
"""ADR-0175 Phase 3a — grounded-derivation value model.
|
|
|
|
A derivation is a left-fold over text-sourced quantities: a ``start`` quantity
|
|
followed by ordered ``Step``s. Each step names the operation, its operand, and
|
|
the **licensing cue** — the surface lexeme the search claims licenses that
|
|
operation. The cue is verified against the problem text by the gate
|
|
(:mod:`generate.derivation.verify`); the model itself only computes the value.
|
|
"""
|
|
|
|
from __future__ import annotations
|
|
|
|
from dataclasses import dataclass
|
|
from typing import Final
|
|
|
|
VALID_OPS: Final[frozenset[str]] = frozenset({"multiply", "divide", "add", "subtract"})
|
|
|
|
|
|
@dataclass(frozen=True, slots=True)
|
|
class Quantity:
|
|
"""A quantity drawn from the problem. ``source_token`` is the surface token
|
|
as it appears in the text (used by the gate to prove the value is grounded)."""
|
|
|
|
value: float
|
|
unit: str
|
|
source_token: str
|
|
|
|
|
|
@dataclass(frozen=True, slots=True)
|
|
class Step:
|
|
"""One operation applied to the running value.
|
|
|
|
``cue`` is the surface lexeme the search asserts licenses ``op`` here; the
|
|
gate refuses to self-verify unless ``cue`` actually appears in the text.
|
|
"""
|
|
|
|
op: str
|
|
operand: Quantity
|
|
cue: str
|
|
|
|
def __post_init__(self) -> None:
|
|
if self.op not in VALID_OPS:
|
|
raise ValueError(f"op must be one of {sorted(VALID_OPS)}, got {self.op!r}")
|
|
|
|
|
|
@dataclass(frozen=True, slots=True)
|
|
class GroundedDerivation:
|
|
start: Quantity
|
|
steps: tuple[Step, ...]
|
|
|
|
@property
|
|
def answer(self) -> float:
|
|
"""Left-fold the steps over ``start``. Raises on divide-by-zero (the gate
|
|
rejects such derivations before this is relied upon)."""
|
|
value = self.start.value
|
|
for step in self.steps:
|
|
operand = step.operand.value
|
|
if step.op == "multiply":
|
|
value = value * operand
|
|
elif step.op == "divide":
|
|
value = value / operand # ZeroDivisionError surfaces; gate guards
|
|
elif step.op == "add":
|
|
value = value + operand
|
|
else: # subtract
|
|
value = value - operand
|
|
return value
|
|
|
|
@property
|
|
def answer_unit(self) -> str:
|
|
"""The aggregate keeps the primary (``start``) unit. Multiply/divide
|
|
compose across units onto the primary; add/subtract require (and the gate
|
|
enforces) a shared unit, so the primary is correct in every admitted case."""
|
|
return self.start.unit
|