Accept bare dates in temporal prefixes; restrict arithmetic to linear forms

[rmichaelthomas]

Summary

Two independent fixes in the enforcement fragment, both verified against the live build at 92eb657 (PR #61 merge).

Fix A — temporal-prefix bare-date acceptance (bug fix)

reorder() guarded the starting/until temporal-prefix branch on TokenType.QUOTED_STRING only; the lexer emits TokenType.DATE for bare dates. The parser already handles both forms correctly, but every existing test called parse(tokenize(...)) directly and never exercised reorder() — so liminate.run(), the only route real callers (including seshat-app's check_action) use, silently rejected bare-date temporal windows with ERROR_PARSE.

Root cause: token-type guard mismatch between lexer output and reorderer expectation.

Not a regression — reorderer.py is byte-identical between parent commit c918fa0 (pre PR #60/#61) and 92eb657, confirmed via git diff.

Fix: both guards widened to accept QUOTED_STRING or DATE via one shared _TEMPORAL_DATE_TOKENS constant, so the two sites can't drift apart the same way again.

Fix B — arithmetic linearity restriction (Fable decidability condition (c))

A nonlinear expression (both operands of multiplied_by/divided_by runtime-resolved, e.g. beta multiplied by beta) parsed, analyzed, and executed inside forbid/require/permit/expect/choose conditions with no restriction — a precondition gap for the future Z3 satisfiability encoder (Fable Step 2, not built yet). plus/minus are linear and stay unrestricted in every operand combination; date arithmetic already rejects multiplied_by/divided_by at runtime and that message is untouched.

Scope note: the restriction is deliberately narrower than the original build prompt specified. An initial universal version — restricting nonlinearity everywhere _check_arithmetic is reached — broke 8 pre-existing tests that multiply two ordinary remembered values (price * quantity, rate * hours, etc.), because _check_arithmetic is shared by 6 call sites and only 2 of them are ever reachable from a deontic/choice condition. The restriction is scoped to exactly those 2 sites via a restrict_nonlinear flag threaded through _check_arithmetic/_check_arithmetic_operand, defaulting False, set True only at the _resolve_choose_operand call site (the value side of forbid/require/permit/expect/choose). All 1668 baseline tests pass unmodified.

Known gap, documented rather than fixed: the restriction only inspects a condition's own expression tree. remember a value called doubled from beta multiplied by beta followed by forbid alpha is above doubled currently passes analysis and evaluates, because the condition sees a bare NameRef, never the ArithmeticNode that produced it. This is not composition-specific — any remembered-value indirection reproduces it, and it is the common authoring form, not an edge case. Condition (c) is therefore syntactically enforced for direct condition arithmetic, but not fully closed — closing it requires value provenance (taint at store time, a definition-site walk, or resolving names to their defining expressions inside the future Z3 encoder), none of which exist yet. A dedicated test (test_KNOWN_GAP_value_indirection_bypasses_the_linearity_restriction) pins the current behavior so provenance work finds it immediately.

Files modified

• src/liminate/reorderer.py — Fix A
• src/liminate/analyzer.py — Fix B
• tests/test_reorderer.py — Fix A tests (8 new, through liminate.run())
• tests/test_arithmetic.py — Fix B tests (18 new, including the boundary pair and the documented known-gap test)

Invariants satisfied

• Vocabulary count unchanged at 61 (21 verbs, 22 connectives, 10 operators, 3 articles, 3 multi-word).
• PR fix: reject cyclic predicate definitions, guard evaluation depth #60/Reject self-referential predicate definitions #61 cycle/self-reference error messages byte-identical; all their tests pass unmodified.
• The two temporal token-type guards share one constant (Fix A).
• Linearity check fires after type checking (text-in-arithmetic, missing-symbol, non-numeric-field errors keep precedence) — verified with a dedicated test.
• plus/minus unrestricted in every operand combination.
• Date arithmetic messages unchanged — verified with a dedicated test.
• Zero baseline tests modified — git diff --stat on tests/ shows insertions only.

Suite count

• Baseline at main@92eb657 (measured via isolated worktree): 1668 passed / 0 failed / 0 skipped — the original build prompt's stated "1,666 passing + 2 skipped" was stale/inaccurate for this environment.
• After both fixes: 1694 passed / 0 failed / 0 skipped (1668 baseline + 8 Fix A tests + 18 Fix B tests).

Test plan

• python3 -m pytest -q — 1694 passed, 0 failed, 0 skipped
• All six temporal forms (bare/quoted × both/starting-only/until-only) pass through liminate.run()
• starting_date/until_date populate on the AST for bare dates; starting ... until ... inherited combination parses
• Fix B reject list (beta * beta, beta / beta, nested) rejects with ERROR_SEMANTIC inside forbid/require/permit/expect/choose
• Fix B pass list (literal × literal, fact × literal, literal × fact, plus/minus, all-literal nested) unchanged
• Boundary pair: same expression passes outside a condition, rejects inside one
• Type-check precedence and date-arithmetic message parity confirmed unchanged
• Known-gap test documents the value-indirection bypass

🤖 Generated with Claude Code