Commit graph

1326 commits

Author SHA1 Message Date
Shay
32385d954c feat(runtime): read-only proposal-review sub-pass in idle_tick (IT-b)
core/config.py: review_pending_proposals: bool = False (opt-in, mirrors consolidate_determinations). chat/runtime.py: IdleTickResult gains an additive optional proposal_review field; idle_tick runs a READ-ONLY sub-pass (after consolidation, gated) that surfaces core.proposal_review.idle_summary(). It does NOT set did_work / checkpoint / mutate / ratify / mount / modify readers; a reporter exception is CAPTURED (safe=False, errors=('proposal_review_failed:<type>',)), never propagated.

docs/runtime_contracts.md documents the sub-pass + field (required for runtime-surface changes). Contract tests: default-off -> proposal_review None (existing shape preserved); enabled -> summary surfaced; exception captured not propagated; read-only review never checkpoints; other passes unperturbed. 91-test smoke green incl. architectural invariants + both existing idle contract suites. Existing idle_tick remains the only idle_tick; NOT L10 always-on.
2026-06-07 22:32:20 -07:00
Shay
65c8587207 feat(proposal-review): pure idle_summary function (IT-a)
core/proposal_review/summary.py: idle_summary(root=None) -> ProposalReviewIdleSummary composes the landed scan/build_report/dry_check into one JSON-safe primitives-only value (safe, total, review_needed, malformed, by_family tuple-of-pairs, errors). Pure read — no mutation, no clock, no runtime touch. errors carries the dry-check violations (why not safe); IT-b reuses it for a captured reporter exception. 7 tests incl. read-only + deterministic + json-serializable.
2026-06-07 22:25:00 -07:00
Shay
3ec5e91433
Merge pull request #636 from AssetOverflow/feat/proposal-review-d
feat(proposal-review): RPT-d — boundary ledger [merge LAST]
2026-06-07 22:22:25 -07:00
Shay
b53f728ee9
Merge pull request #635 from AssetOverflow/feat/proposal-review-c
feat(proposal-review): RPT-c — safety dry-check + read-only CLI [merge after B]
2026-06-07 22:22:22 -07:00
Shay
4049681b85
Merge pull request #634 from AssetOverflow/feat/proposal-review-b
feat(proposal-review): RPT-b — deterministic review report [merge after A]
2026-06-07 22:22:19 -07:00
Shay
eb675064ce
Merge pull request #633 from AssetOverflow/feat/proposal-review-a
feat(proposal-review): RPT-a — read-only scanner over the proposal sink [merge 1st]
2026-06-07 22:22:16 -07:00
Shay
48386f3237 docs(proposal-review): boundary ledger — read-only reporter, not idle_tick, not L10 (RPT-d)
Documents the boundary: observes + reports + verifies; never advances teaching / ratifies / mounts / modifies readers / affects serving. ChatRuntime.idle_tick remains the only idle_tick (different stream, different verb). A future PR may call this reporter from idle_tick as a read-only sub-pass. L10-adjacent, NOT L10; the always-on heartbeat remains separate/unbuilt and is not claimed here.
2026-06-07 21:44:07 -07:00
Shay
cc3003f425 feat(proposal-review): safety dry-check + read-only CLI (RPT-c)
core/proposal_review/safety.py: dry_check INDEPENDENTLY verifies (without trusting the emitter) that every artifact is inert — status==proposal_only, mounted==false, requires_review==true, content-address consistent (filename == sha256(family:problem_text_sha256)), path under the sink, no malformed (unverifiable) file — and that no serving-path module reads the sink. Any failure is a violation.

__main__.py: python -m core.proposal_review [comprehension-failures] [--json] [--root] — read-only report + dry-check; exit 0 iff safe. Mutates nothing. 8 tests, each safety assertion proven meaningful-fail; serving-unconsumed verified on the real tree.
2026-06-07 21:43:18 -07:00
Shay
3fc73eb14b feat(proposal-review): deterministic review report (RPT-b)
core/proposal_review/report.py: build_report projects scan results into a deterministic summary — total pending, counts by failure_family + by status (sorted), malformed count, review-needed list (sorted by content hash). report_json (sort_keys) + report_text. Deterministic given sink contents; no clock.

Time-based oldest/newest is intentionally OMITTED: the artifacts are content-addressed with no timestamp (the emitter is clock-free for idempotence), so an honest temporal order isn't in the data — only non-deterministic filesystem mtime, which would break report determinism. 5 tests.
2026-06-07 21:40:35 -07:00
Shay
3c6f820b54 feat(proposal-review): read-only scanner over the comprehension-failure sink (RPT-a)
core/proposal_review/{model,scan}.py: scan reads teaching/proposals/comprehension_failures/*.json into typed PendingProposal records (path, content_hash, failure_family, status, mounted, requires_review, problem_text_sha256, observed_attempts); any unparseable file becomes a MalformedArtifact (never silently dropped). Pure read — never writes/moves/deletes; deterministic (sorted by path); missing sink -> empty. The sink path is computed independently of the emitter (the reporter verifies the contract, doesn't import the writer).

Read-only reporter, NOT an idle_tick (ChatRuntime.idle_tick stays the only one), NOT L10. 4 tests incl. read-only invariant + malformed flagging.
2026-06-07 21:39:03 -07:00
Shay
31a984e69b
Merge pull request #632 from AssetOverflow/feat/contemplation-pack-e 2026-06-07 12:57:58 -07:00
Shay
1bc7f1ae26
Merge pull request #631 from AssetOverflow/feat/contemplation-pack-d 2026-06-07 12:56:19 -07:00
Shay
cfa8bdd5fa
Merge pull request #630 from AssetOverflow/feat/contemplation-pack-c 2026-06-07 12:55:17 -07:00
Shay
787aa833fd
Merge pull request #629 from AssetOverflow/feat/contemplation-pack-b 2026-06-07 12:53:40 -07:00
Shay
b37794814d
Merge pull request #628 from AssetOverflow/feat/contemplation-pack-a 2026-06-07 12:53:19 -07:00
Shay
1adf4f5de5 feat(contemplation): contemplation v0 pass manager (N6) + boundary-first growth fix
generate/contemplation/{findings,pass_manager}.py: a single bounded pass — route (N3) -> classify+enrich (N4) -> terminal -> maybe emit proposal-only (N5). No loops/daemon/L10. Seven terminals: SOLVED_VERIFIED / REFUSED_KNOWN_BOUNDARY / REFUSED_UNSUPPORTED_FAMILY / CONTRADICTION_DETECTED / PROPOSAL_EMITTED / AMBIGUOUS_ORGAN / NO_PROGRESS. R2 solved+verified end-to-end; R1 routed setup is SOLVED_VERIFIED (numeric answer stays the eval lane in v0).

Hazard found+fixed: N6 exposed that category_pair_not_found fires on ANY non-R2 text, so mapping it to a growth surface made gibberish falsely PROPOSAL_EMITTED. Reclassified it to input_shape and made missing_category_pair reserved — only the PRECISE missing_total_count/missing_weighted_total remain reachable growth surfaces. Classification is boundary-first (input_shape non-blocking), so a problem one organ recognizes as a substantive boundary never proposes against the other's broad refusal.

Acceptance proven: known correct refusal -> no proposal; unsupported gap -> proposal-only artifact (exactly the 2 missing_* gaps over the gold); answer-key contradiction -> CONTRADICTION_DETECTED; organ conflict -> AMBIGUOUS_ORGAN. 188 tests green incl. architectural invariants; R1 7/0/3 + R2 reader 10/0/0 unchanged; off-serving.
2026-06-07 08:59:47 -07:00
Shay
5903cba08a feat(teaching): proposal-only failure-artifact emitter (N5)
core/comprehension_attempt/proposal.py: emit_proposal writes a content-addressed teaching/proposals/comprehension_failures/<hash>.json ONLY for growth-surface families (proposal_allowed). Deliberately toothless: status always proposal_only, mounted always false, requires_review always true (enforced in __post_init__); the problem text is hashed (sha256), never stored; filename = sha256(family:text_sha) so the same failure is idempotent.

No proposal for a correct wrong=0 boundary. Serving never reads the sink (scanned: generate/stream, field/propagate, vault/store, generate/derivation, core/reliability_gate). Routes through the existing proposal-only flywheel (ADR-0055/0056/0057), never a parallel correction path. README pins the contract. 6 tests.
2026-06-07 08:48:45 -07:00
Shay
c1ad5b8142 feat(comprehension): failure-family registry (N4)
core/comprehension_attempt/failure_family.py: partitions every reachable organ refusal reason (R1 reader/admissibility, R2 reader/solver/answer-choice) into a named FailureFamily declaring owner / must_remain_refused / proposal_allowed / safe_next_action / proposal_target. family_for_reason is total + unambiguous (partition asserted by test); enrich_family resolves an attempt's family.

Only THREE families are growth surfaces (proposal_allowed=True): the R2 missing_category_pair / missing_total_count / missing_weighted_total gaps. All other reasons are correct wrong=0 boundaries (refuse, no proposal) — correct refusal != missing capability. answer_key_contradiction is a report verdict (no reason). Reserved R3 families forward-declared. 9 tests incl. whole-surface coverage + partition.
2026-06-07 08:46:07 -07:00
Shay
5ae516f4a2 feat(comprehension): deterministic multi-organ setup router (N3)
core/comprehension_attempt/router.py: route_setup tries R1 then R2, collects both attempts, and selects a setup ONLY when exactly one organ admits one. Zero->all_refused; >=2 with differing signatures->ambiguous (refuse, never pick); cross-organ signatures never coincide so two admitting organs always resolve to ambiguous. No scoring, no solving.

wrong=0 invariant asserted: every routed R2 setup is byte-equal to the independent gold signature. Each gold problem routes to exactly its owning organ (R2 well-formed->r2; R1 admitted->r1; refused->all_refused); none is ambiguous. 4 router tests.
2026-06-07 08:42:35 -07:00
Shay
67c54d6813 feat(comprehension): shared ComprehensionAttempt model + classify (N2)
core/comprehension_attempt/{model,classify}.py: a small frozen ComprehensionAttempt (organ, outcome, case_id, refusal_reason, family, setup_signature, answer, evidence) and classify_r1/classify_r2 that normalize each organ's heterogeneous output (typed setup | Refusal) into a uniform produce-mode setup outcome — setup_refused (with the organ's reason) or setup_correct (with a deterministic inline signature).

No solving, no gold comparison, no evals import (signatures computed inline) — runtime never depends on the harness. Ties to both gold corpora: R2 solved/solver_refuses->setup_correct, reader_refuses->setup_refused with the gold reason; R1 7 admitted / 3 refused. family left None (resolved by the N4 registry). 6 tests.
2026-06-07 08:40:53 -07:00
Shay
0b191055a8 docs(analysis): comprehension capability ledger — R1/R2 baseline + refusal taxonomy (N1)
Post-merge baseline for the contemplation batch: R1 7/0/3, R2 reader 10/0/0, gold 13/13, serving unchanged. Enumerates the full typed refusal surface across both organs (R1 reader/admissibility, R2 reader/solver/answer-choice) and a first-pass cross-organ failure-family taxonomy with must_remain_refused / proposal_allowed / owner — the table N4 will make executable. Repeats the load-bearing distinction: correct refusal != missing capability.
2026-06-07 08:36:22 -07:00
Shay
51b4a6e37d
Merge pull request #627 from AssetOverflow/feat/r2-reader
feat(constraint): R2 Pack C — two-category reader (the capability) + ledger
2026-06-07 08:32:11 -07:00
Shay
9337223733
Merge pull request #626 from AssetOverflow/feat/r2-solver-verifier
feat(constraint): R2 Pack B — exact integer solver + answer-choice verifier
2026-06-07 08:28:12 -07:00
Shay
ae16c0cae7
Merge pull request #625 from AssetOverflow/feat/r2-ruler
feat(constraint): R2 Pack A — constraint IR + setup oracle + gold + ADR-0211 (the ruler)
2026-06-07 08:19:31 -07:00
Shay
8d2c270144
Merge pull request #624 from AssetOverflow/feat/r1-inverse-frame
feat(comprehension): R1 inverse reader frame — close R1 at 7/0/3 (PR-7b)
2026-06-07 08:04:23 -07:00
Shay
a3a26b8fc5 test(constraint): pin the three Pack-C review hazards as regression tests
Per review: (H1) exactly-two-category binding already has its meaningful-fail twin; (H2) a weighted total whose unit does not match the coefficient unit refuses missing_weighted_total (never a cross-unit sum); (H3) answer-choice ties EXACTLY or refuses no_matching_option (never nearest). All three were already handled by construction; these pin them so they stay handled.
2026-06-07 07:49:10 -07:00
Shay
faecb21c37 docs(analysis): R2 inventory ledger — reader 10/0/0, 6 families read+solved+verified (R2 C9)
Records the final R2 v1 state: reader setup_correct 10 / setup_wrong 0 + 3 correct reader-refusals; 7 solved answers + 3 solver-refused + 3 reader-refused; gold 13/13. Per-fixture table, the four wrong=0 gates, the reader-vs-solver division of labor (equal coefficients are a solver refusal, not a reader one), covered families, and R3 deferrals. R1 7/0/3 and 15-case 15/0/0 unchanged.
2026-06-07 07:36:17 -07:00
Shay
4ddaef4d00 feat(constraint): two-category reader — prose to ConstraintProblem (R2 C5-C9)
generate/constraint_comprehension/reader.py: read_constraint_problem comprehends two-category constraint prose into a typed ConstraintProblem via five recognizers — C5 category-pair (from coefficient clauses; >2 -> too_many_categories), C6 coefficient (Each <cat> holds/has/costs/is-worth <N> <unit>; shared measured unit), C7 total-count (collective-unit sentence -> x+y=N; absent -> missing_total_count), C8 weighted-total (measured-unit sentence -> ax+by=T; absent -> missing_weighted_total), C9 query-target (How many <cat> -> the asked unknown). Refuses, never mis-assembles.

Reconciles the sketch's 'no equal coefficients' note: equal coefficients are a SOLVER refusal (indistinguishable_weights), not a reader one — the reader reads r2-010 setup_correct and the solver refuses it. run_reader lane + 'reader' CLI subcommand. R2 reader: setup_correct 10 / setup_wrong 0 / refused_correct 3; R1 7/0/3 and 15-case 15/0/0 unchanged. Off-serving. 8 reader tests incl. full read->solve->verify chain + meaningful-fail guards.
2026-06-07 07:34:55 -07:00
Shay
121362c52a feat(answer-choices): multiple-choice verifier with contradiction flag (R2 C4)
generate/answer_choices/{parse,verify}.py: parse_options normalizes {label:value} to {label:int} (int or single-integer string; ambiguous/empty refuse). verify_answer_choice ties a PROVEN value to exactly one option -> ChoiceVerdict(consistent); a disagreeing key -> ChoiceVerdict(contradiction) naming both the consistent answer and the wrong key (truth discipline, not a refusal). Refuses no_matching_option / ambiguous_options / unknown_provided_label.

End-to-end with C2 gold + C3 solver: every solved fixture solves, ties to its labeled answer, confirms consistent. Off-serving. 9 tests incl. contradiction-flag meaningful-fail.
2026-06-07 07:26:00 -07:00
Shay
babcf2fdb2 feat(constraint): exact integer 2-var solver — Cramer's rule, refusal-first (R2 C3)
generate/constraint_comprehension/solver.py: solve_two_var_linear (order-independent 2x2 integer Cramer's rule over typed constraints), the solve_two_var_count_weight specialization, and solve/answer_constraint_problem driving it from a ConstraintProblem. Four typed refusals: indistinguishable_weights (det==0), non_integer_solution (numer%det!=0, never rounds), negative_solution, verification_failed (identity backstop).

Ties to the C2 gold: solves all 7 solved fixtures to their gold value and refuses all 3 solver_refuses fixtures with EXACTLY the gold-claimed reason (the gold's reason is now solver-verified, not just annotation). Per-refusal meaningful-fail + positive re-substitution. Off-serving. 9 tests.
2026-06-07 07:23:23 -07:00
Shay
a098519bc1 feat(constraint): R2 setup oracle + gold + ADR-0211 — the ruler (R2 C2)
evals/constraint_oracle: span-free canonical setup signature (unknowns/facts/constraints/query; terms merged+sorted, lhs constant folded into rhs), a 13-fixture gold (7 solved / 3 solver_refuses / 3 reader_refuses) with a closed expect+refusal taxonomy, and a gold-validation runner. No reader yet — this proves the ruler is coherent (13/13 valid), not capability.

ADR-0211 ratifies the R2 finite-integer two-category constraint compiler: the IR, the canonical signature, the closed taxonomy, the four wrong=0 gates (setup oracle / reader refusal / exact solver / answer-choice contradiction flag), off-serving disjointness, and the C1-C9 ladder. Cross-refs ADR-0207/0175/0083/0055-0057; reuses the R1 setup_oracle pattern. Off-serving (no generate.derivation / reliability_gate). 13 oracle tests incl. per-branch meaningful-fail.
2026-06-07 07:19:29 -07:00
Shay
e71531c0c9 feat(constraint): R2 linear-constraint IR — typed problem model (R2 C1)
generate/constraint_comprehension/{expr,model}.py: frozen, slots'd dataclasses, no behavior. expr = LinearExpr (sum(coeff*symbol)+constant) + LinearConstraint (lhs eq rhs, optional source_span). model = Unknown (symbol/entity/unit/finite-integer domain), AttributeFact (per-category coefficient provenance), ConstraintQuery (symbol+unit), ConstraintProblem (unknowns/facts/constraints/query).

Terms pinned as (symbol, coefficient) to match the gold serialization. Query is a minimal dedicated type, not R1's BoundUnknown (no degenerate fit). Off-serving package; no generate.derivation / reliability_gate import. 9 IR tests (shape + frozen + defaults).
2026-06-07 07:10:20 -07:00
Shay
60b40d3e3a feat(comprehension): inverse reader frame — base of a more/fewer-than (PR-7b / R2 C0)
r1-07 now reads setup-correct and answers 6 — 'Nia has 9 more beads than Omar. Nia has 15. -> Omar = 6'. The reader binds the unknown base's unit FROM the relation when its subject is a known fact and its referent is the otherwise-ungrounded query target, so the equation is admissible; the answer oracle reverse-solves it (PR-7a). Bounded: single base == query target (no chains), known subject value, base not otherwise grounded, <=1 inverse (multiple_inverse_bases else), never over times/divide.

R1 setup 6/0/4 -> 7/0/3; R1 answers -> 7 correct / 0 wrong; 15-case 15/0/0; setup_wrong stays 0. Off-serving. Refreshes the R1 ledger to 7/0/3 (R1 closed; the 3 remaining refusals are wrong=0 boundaries).
2026-06-07 07:06:26 -07:00
Shay
0e6a7f9ac0
Merge pull request #619 from AssetOverflow/feat/inverse-solve-contract
feat: narrow reverse-solve oracle contract (PR-7a, contract only)
2026-06-07 06:44:07 -07:00
Shay
036ed8c659 feat(oracle): narrow reverse-solve contract — base of one more/fewer_than (PR-7a)
Pin the EXACT reverse-solve semantics in the independent answer oracle before the
reader learns the inverse frame (PR-7b). A single more_than/fewer_than whose entity
is grounded and whose ref is the (otherwise ungrounded) query target inverts to the
base: base = entity -/+ delta (always integer-exact for +/-).

Refuses everything wider (each a meaningful-fail oracle test): more than one inverse
constraint, an inverse base that is not the query target (a chain), an already-grounded
base, a negative count result, or an inverse over times/divide. The duplicate-definition
guard moved into the per-kind branches so a grounded entity on a more/fewer_than is read
as an inverse constraint, not a redefinition; forward more/fewer/times/divide/sum paths
are unchanged (regression-guarded).

Contract only — the reader is NOT touched: r1-07 still refuses (admissibility_refused),
so R1 stays 6 / 0 / 4 and 15-case 15 / 0 / 0. r1-07 gold drops the non-consumed ask_base
(aligning with the reader's future projection) and gains gold=6, dormant until PR-7b.

Off-serving (only evals/tests import the oracle). SHA gate 8/9 (public_demo env flake).
2026-06-07 06:22:36 -07:00
Shay
a8707d3bac
Merge pull request #618 from AssetOverflow/feat/aggregate-query-variants
feat: additive aggregate query variants — 'altogether' / 'in total'
2026-06-07 05:59:16 -07:00
Shay
ef06923866 feat(comprehension): additive aggregate query variants — 'altogether' / 'in total'
Widen the aggregate-query recognizer so a multi-part total may be asked with a
trailing qualifier after 'have': 'How many X do A and B have altogether?' and
'... in total?'. The qualifier is stripped and honored ONLY for the multi-part
(sumquery) form — a single-entity query carrying it refuses, guarded by
'not aggregate'.

Phrasing-only: no new arithmetic, no new relation kind, no inverse solving, no
distractor/pronoun handling. The parts still flow through the existing sum_of;
an ungrounded part (unit unbound) or a unit-incompatible part (unit mismatch) is
refused downstream by the REAL admissibility check, so the recognizer cannot
over-read. Off-serving organ only (no generate.derivation / reliability_gate).

Flips r1-03 (more+altogether -> 25) and r1-04 (fewer+in total -> 34):
  R1 setup   6 / 0 / 4    R1 answers 6 / 0 / 4  (setup_wrong 0, gold_error 0)
  15-case 15 / 0 / 0      29 quant tests, 102 affected-file tests green

Tests are meaningful-fail: the single-entity-qualifier, ungrounded-part, and
unit-incompatible-part refusals each fail loudly if their guard is removed.
2026-06-07 05:49:28 -07:00
Shay
82b14065f2
Merge pull request #617 from AssetOverflow/docs/r1-inventory-ledger
docs: R1 comprehension inventory ledger (4/0/6 baseline)
2026-06-07 05:49:12 -07:00
Shay
261c0e4c2d docs(analysis): R1 comprehension inventory ledger
Baseline decision artifact at main@5ada1392 (post-#616). Records the R1
4/0/6 state per-fixture: the 4 admitted semantic families and the invariant
protecting each, and a classification of the 6 refusals — 2 pure phrasing
gaps (r1-03/r1-04 aggregate-query), 1 real reverse-solve capability (r1-07),
and 3 correct wrong=0 boundaries that must stay refused (r1-08/09/10).

Source-verified against the merged reader (refusal codes + line refs) and
the live lanes (setup 4/0/6, answers 4/0/6 setup_wrong/gold_error 0,
15-case 15/0/0). Docs-only; no code, no serving lane, no SHA-lane content.
2026-06-07 05:30:14 -07:00
Shay
5ada1392a5
Merge pull request #616 from AssetOverflow/feat/partition-aggregate-divide
feat(comprehension): aggregate-then-divide partition frame — "split equally into N boxes" (PR-6d)
2026-06-07 05:24:50 -07:00
Shay
f9ef9e56a4 feat(comprehension): aggregate-then-divide partition frame — "split equally into N boxes" (PR-6d)
PR-6d adds the partition frame: combine all parts into a total, then split that
total equally into N containers. r1-06-subtotal-reused moves refused → correct —
the FIRST case where the divisor applies to a DERIVED symbol (the total), not a
directly given fact. That is real progress toward GSM8K setup comprehension,
where intermediate quantities are the norm.

Scope (kept narrow on purpose):
  No new relation kind.
  No new arithmetic operation.
  No rational support.
  No rounding/flooring.
  No serving path touched.

The frame reuses the already-ratified pieces — SumOf(parts) + Div(Symbol(total),
Literal(N)) → divide_by — so this PR is reader-only (no IR / admissibility /
oracle / signature change).

Frame grammar:
  "They combine their <unit> and split them equally into N <containers>."
  + "How many <unit> are in each <container>?"
  -> total = sum(all facts); per_<container> = total / N; ask per_<container>.

wrong=0 boundaries:
- Exact-divisibility still gates the ANSWER, now over a derived total: 5+6=11,
  11/3 is non-exact -> the setup reads correctly but the answer REFUSES (never
  floors). Setup comprehension and answer exactness are cleanly separated.
- Partition/query coherence: a partition is read ONLY together with its
  "in each <container>" query (and vice versa); container mismatch (box vs jar)
  refuses. Prevents over-reading a story detail into an unused derived value.
  Meaningful-fail verified: disabling the guard makes a dangling partition
  wrongly comprehend.

Gates:
  R1 setup:   4 correct / 0 wrong / 6 refused
  R1 answers: 4 correct / 0 wrong / 6 refused / setup_wrong 0 / gold_error 0
  15-case setup: 15 / 0 / 0
  97 PR-6d tests + 99 relational/invariant tests green. Reader is off-serving
  (no generate.derivation / core.reliability_gate import).
2026-06-06 21:07:19 -07:00
Shay
409615fcef
Merge pull request #615 from AssetOverflow/feat/half-as-many-divide
feat(comprehension): the divisive comparative frame — "half as many" as exact integer division (PR-6c)
2026-06-06 20:44:52 -07:00
Shay
0951d80e04 feat(comprehension): the divisive comparative frame — "half as many" as exact integer division (PR-6c)
PR-6c adds the divisive comparative frame: "half as many" read as EXACT INTEGER
DIVISION. It is the divisor twin of PR-5c's multiplicative frame, and moves the
independent R1 gold's r1-02-half from refused → correct.

No serving path touched. No rational/fractional answer support added. Non-exact
division refuses.

Design (ADR-0134 amended — divide made symmetric with multiply):
- `_check_divide` now admits a SINGLE-DEP divide-by-dimensionless-literal
  (item / dimensionless = item), the exact twin of single-dep multiply. The
  2-dep rate-divide path is untouched. This keeps the IR's "literal operands
  are not deps" invariant (proven in PR-6a) uniform across Mul AND Div, so the
  reader builds both without a per-op special case and WITHOUT synthesizing a
  divisor symbol that would pollute the setup-oracle's unit signature.
- `Div(Symbol, Literal)` IR node: "ref / divisor", operation_kind "divide",
  projects to `divide_by`. Divisor-only contract mirrors the scalar-only one.
- Reader: `_DIVISOR_WORDS={half:2}` slots into the same 8-token "<WORD> as many"
  template as the factor words; graph carries only the two entities.
- Gold reconciliation: r1-02 placeholder `times_as_many factor 0.5` → exact
  `divide_by divisor 2` (gold 4). Makes the INDEPENDENT gold integer-faithful.

The wrong=0 boundary — exact divisibility:
  the oracle admits `divide_by` only when `base % divisor == 0`. An odd base
  halved REFUSES (gold_error), never floors to a wrong integer. Divisor must be
  a nonzero int (0, 0.5, 1.5, bool all refuse); divisor=1 is intentionally the
  identity (pinned). admissibility proves DIMENSION; the oracle proves EXACT VALUE.

Meaningful-fail (CLAUDE.md Schema-Defined Proof Obligations), both verified red:
- drop the `% divisor` guard → test_oracle_refuses_non_exact_division fails (returns 3).
- disable the single-dep divide branch → the admissibility test AND the reader's
  `half` test fail (admissibility refuses → reader refuses → half stays refused).

Gates:
  R1 setup:   3 correct / 0 wrong / 7 refused
  R1 answers: 3 correct / 0 wrong / 7 refused / setup_wrong 0 / gold_error 0
  15-case setup: 15 / 0 / 0
  91 PR-6c tests + 60 relational lanes + 56 architectural invariants + 502
  binding-graph/proof-chain/adapter tests green. All 8 SHA-content lanes match
  (serving unmoved; admissibility has no generate.derivation/reliability_gate consumer).
2026-06-06 20:18:39 -07:00
Shay
5ac1526536
Merge pull request #614 from AssetOverflow/pr-6b-r1-answer-oracle-followup
test(comprehension): prove R1 times-as-many answer oracle (PR-6b follow-up)
2026-06-06 19:35:57 -07:00
Shay
f4cf490e8d test(comprehension): prove R1 answer-oracle lane 2026-06-06 18:32:21 -07:00
Shay
15b0b583aa test(comprehension): expose R1 answer lane CLI 2026-06-06 18:31:41 -07:00
Shay
56260629b8 test(comprehension): add answer gold for setup-correct R1 cases 2026-06-06 18:31:12 -07:00
Shay
88d8950d3e test(comprehension): expose R1 answer lane 2026-06-06 18:28:49 -07:00
Shay
c364d434da feat(comprehension): add R1 answer-oracle lane 2026-06-06 18:26:30 -07:00
Shay
ce8897e84f feat(comprehension): add off-serving times_as_many answer oracle 2026-06-06 18:20:23 -07:00