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

src/liminate/analyzer.py

@@ -790,6 +790,8 @@ def _check_arithmetic(
     node: ArithmeticNode,
     symtab: dict[str, SymbolEntry],
     iterator: IteratorContext | None,
+    *,
+    restrict_nonlinear: bool = False,
 ) -> None:
     """Infrastructure Era — validate both operands of a binary
     arithmetic expression. Both must be numeric (or resolvable to a
@@ -798,15 +800,48 @@ def _check_arithmetic(
     a numeric field; BareWord operands defer to runtime (they may
     resolve via the iterator context). Nested ArithmeticNode operands
     recurse.
+
+    `restrict_nonlinear` — Fable decidability condition (c). Only the
+    value side of a deontic/choice condition (`forbid`/`require`/
+    `permit`/`expect`/`choose`, via `_resolve_choose_operand`) sets this;
+    it never enters the SMT encoder from `remember ... with/from`, list
+    items, or `add <expr> to <list>`, so those stay unrestricted.
     """
-    _check_arithmetic_operand(node.left, symtab, iterator)
-    _check_arithmetic_operand(node.right, symtab, iterator)
+    _check_arithmetic_operand(
+        node.left, symtab, iterator, restrict_nonlinear=restrict_nonlinear
+    )
+    _check_arithmetic_operand(
+        node.right, symtab, iterator, restrict_nonlinear=restrict_nonlinear
+    )
+
+    if restrict_nonlinear and node.op in ("multiplied_by", "divided_by"):
+        if not _is_literal_operand(node.left) and not _is_literal_operand(node.right):
+            raise _SemanticError(
+                f"Multiplication and division need at least one plain "
+                f"number. '{render(node.left)}' and '{render(node.right)}' "
+                f"are both values that vary at run time."
+            )
+
+
+def _is_literal_operand(node: ASTNode) -> bool:
+    """Fable decidability condition (c) — at most one operand of a
+    `multiplied_by`/`divided_by` node may be runtime-resolved. A node is
+    a compile-time literal iff it's a NumberLiteral/DateLiteral, or an
+    ArithmeticNode whose own operands are both literal.
+    """
+    if isinstance(node, (NumberLiteral, DateLiteral)):
+        return True
+    if isinstance(node, ArithmeticNode):
+        return _is_literal_operand(node.left) and _is_literal_operand(node.right)
+    return False
 
 
 def _check_arithmetic_operand(
     operand: ASTNode,
     symtab: dict[str, SymbolEntry],
     iterator: IteratorContext | None,
+    *,
+    restrict_nonlinear: bool = False,
 ) -> None:
     if isinstance(operand, NumberLiteral):
         return
@@ -821,7 +856,9 @@ def _check_arithmetic_operand(
             f"'{operand.content}' is text."
         )
     if isinstance(operand, ArithmeticNode):
-        _check_arithmetic(operand, symtab, iterator)
+        _check_arithmetic(
+            operand, symtab, iterator, restrict_nonlinear=restrict_nonlinear
+        )
         return
     if isinstance(operand, FieldAccessNode):
         _check_field_access(operand, symtab)
@@ -2559,7 +2596,10 @@ def _resolve_choose_operand(
     if isinstance(node, ArithmeticNode):
         # Infrastructure Era — arithmetic operands inside `choose` /
         # `require` / `expect` conditions resolve to numbers.
-        _check_arithmetic(node, symtab, iterator=None)
+        # Fable decidability condition (c) — this is the value side of a
+        # deontic/choice condition, the only place that reaches the SMT
+        # encoder, so it's the one call site that restricts nonlinearity.
+        _check_arithmetic(node, symtab, iterator=None, restrict_nonlinear=True)
         return "number", "arithmetic expression"
     raise _SemanticError("Unexpected operand in 'choose' condition.")
 

src/liminate/reorderer.py

@@ -33,6 +33,8 @@
 
 ReorderOutput = list[Token] | LiminateResult
 
+_TEMPORAL_DATE_TOKENS = (TokenType.QUOTED_STRING, TokenType.DATE)
+
 
 def reorder(tokens: list[Token]) -> ReorderOutput:
     """Reorder a token list into canonical form, or report an error."""
@@ -41,7 +43,7 @@ def reorder(tokens: list[Token]) -> ReorderOutput:
 
     # Temporal-Boundary Era: statement-initial `starting` and/or `until`
     # connectives are pass-through prefixes (same pattern as `inherited`).
-    # Each is followed by a QUOTED_STRING date token. Strip the temporal
+    # Each is followed by a quoted or bare date token. Strip the temporal
     # prefix, reorder the remainder, re-prepend. Placed BEFORE the
     # `inherited` check so the canonical order
     # `starting ... until ... inherited <verb> ...` is preserved.
@@ -51,7 +53,7 @@ def reorder(tokens: list[Token]) -> ReorderOutput:
         tokens[0].type is TokenType.CONNECTIVE
         and tokens[0].value == "starting"
         and len(tokens) > 1
-        and tokens[1].type is TokenType.QUOTED_STRING
+        and tokens[1].type in _TEMPORAL_DATE_TOKENS
     ):
         temporal_prefix.extend([tokens[0], tokens[1]])
         rest_start = 2
@@ -61,7 +63,7 @@ def reorder(tokens: list[Token]) -> ReorderOutput:
         and tokens[rest_start].type is TokenType.CONNECTIVE
         and tokens[rest_start].value == "until"
         and rest_start + 1 < len(tokens)
-        and tokens[rest_start + 1].type is TokenType.QUOTED_STRING
+        and tokens[rest_start + 1].type in _TEMPORAL_DATE_TOKENS
     ):
         temporal_prefix.extend([tokens[rest_start], tokens[rest_start + 1]])
         rest_start = rest_start + 2

tests/test_arithmetic.py

@@ -351,3 +351,244 @@ def test_list_of_negative_numbers_is_numeric():
     ])
     for r in results:
         assert r.status is ResultStatus.SUCCESS, r.message
+
+
+# ---------------------------------------------------------------------------
+# Arithmetic linearity restriction (Fable decidability condition (c)) —
+# `multiplied_by`/`divided_by` reject when both operands are runtime-
+# resolved, but ONLY as the value side of a deontic/choice condition
+# (forbid/require/permit/expect/choose). Outside a condition —
+# `remember ... with/from`, list items, `add <expr> to <list>` — nonlinear
+# arithmetic is unrestricted; it never reaches the Z3 satisfiability
+# encoder (Fable Step 2, not built yet).
+# ---------------------------------------------------------------------------
+
+
+def _semantic_message(results):
+    return results[-1].message or ""
+
+
+# ---------- reject: both operands runtime-resolved, inside a condition ----------
+
+
+def test_forbid_condition_rejects_fact_times_fact():
+    session, results = run_lines([
+        "remember a number called alpha with 10",
+        "remember a number called beta with 2",
+        "forbid alpha is above beta multiplied by beta",
+    ])
+    assert results[-1].status is ResultStatus.ERROR_SEMANTIC
+    msg = _semantic_message(results)
+    assert "at least one plain number" in msg
+    assert "'beta' and 'beta'" in msg
+
+
+def test_forbid_condition_rejects_fact_divided_by_fact():
+    session, results = run_lines([
+        "remember a number called alpha with 10",
+        "remember a number called beta with 2",
+        "forbid alpha is above beta divided by beta",
+    ])
+    assert results[-1].status is ResultStatus.ERROR_SEMANTIC
+    assert "at least one plain number" in _semantic_message(results)
+
+
+def test_forbid_condition_rejects_nested_fact_times_fact():
+    session, results = run_lines([
+        "remember a number called alpha with 10",
+        "remember a number called beta with 2",
+        "forbid alpha is above beta multiplied by beta multiplied by 2",
+    ])
+    assert results[-1].status is ResultStatus.ERROR_SEMANTIC
+    assert "at least one plain number" in _semantic_message(results)
+
+
+def test_require_condition_rejects_fact_times_fact():
+    session, results = run_lines([
+        "remember a number called alpha with 10",
+        "remember a number called beta with 2",
+        "require alpha is above beta multiplied by beta",
+    ])
+    assert results[-1].status is ResultStatus.ERROR_SEMANTIC
+    assert "at least one plain number" in _semantic_message(results)
+
+
+def test_permit_condition_rejects_fact_times_fact():
+    session, results = run_lines([
+        "remember a number called alpha with 10",
+        "remember a number called beta with 2",
+        "permit alpha is above beta multiplied by beta",
+    ])
+    assert results[-1].status is ResultStatus.ERROR_SEMANTIC
+    assert "at least one plain number" in _semantic_message(results)
+
+
+def test_expect_condition_rejects_fact_times_fact():
+    session, results = run_lines([
+        "remember a number called alpha with 10",
+        "remember a number called beta with 2",
+        "expect alpha is above beta multiplied by beta",
+    ])
+    assert results[-1].status is ResultStatus.ERROR_SEMANTIC
+    assert "at least one plain number" in _semantic_message(results)
+
+
+def test_choose_condition_rejects_fact_times_fact():
+    session, results = run_lines([
+        "remember a number called alpha with 10",
+        "remember a number called beta with 2",
+        'choose if alpha is above beta multiplied by beta: show "big" otherwise show "small"',
+    ])
+    assert results[-1].status is ResultStatus.ERROR_SEMANTIC
+    assert "at least one plain number" in _semantic_message(results)
+
+
+# ---------- pass: at least one literal operand, inside a condition (unchanged) ----------
+
+
+def test_forbid_condition_allows_literal_times_literal():
+    session, results = run_lines([
+        "remember a number called alpha with 10",
+        "forbid alpha is above 3 multiplied by 4",
+    ])
+    assert results[-1].status is ResultStatus.SUCCESS
+
+
+def test_forbid_condition_allows_fact_times_literal():
+    session, results = run_lines([
+        "remember a number called alpha with 10",
+        "remember a number called beta with 2",
+        "forbid alpha is above beta multiplied by 3",
+    ])
+    assert results[-1].status is ResultStatus.PROHIBITION_VIOLATED
+
+
+def test_forbid_condition_allows_literal_times_fact():
+    session, results = run_lines([
+        "remember a number called alpha with 10",
+        "remember a number called beta with 2",
+        "forbid alpha is above 3 multiplied by beta",
+    ])
+    assert results[-1].status is ResultStatus.PROHIBITION_VIOLATED
+
+
+def test_forbid_condition_allows_fact_plus_fact():
+    """`plus`/`minus` are linear — no restriction in any operand
+    combination."""
+    session, results = run_lines([
+        "remember a number called alpha with 10",
+        "remember a number called beta with 2",
+        "forbid alpha is above beta plus beta",
+    ])
+    assert results[-1].status is ResultStatus.PROHIBITION_VIOLATED
+
+
+def test_forbid_condition_allows_fact_minus_fact():
+    session, results = run_lines([
+        "remember a number called alpha with 10",
+        "remember a number called beta with 2",
+        "forbid alpha is above beta minus beta",
+    ])
+    assert results[-1].status is ResultStatus.PROHIBITION_VIOLATED
+
+
+def test_forbid_condition_allows_all_literal_nested():
+    session, results = run_lines([
+        "remember a number called alpha with 10",
+        "forbid alpha is above 2 multiplied by 3 multiplied by 4",
+    ])
+    assert results[-1].status is ResultStatus.SUCCESS
+
+
+# ---------- boundary pair: the restriction is condition-scoped, not global ----------
+#
+# These two tests document opposite sides of the same boundary and must be
+# read together: the identical `beta multiplied by beta` expression passes
+# outside a condition and rejects inside one. If a future change requires
+# editing either one, it is very likely re-widening (or narrowing) the
+# restriction's scope rather than fixing an unrelated bug — check the other
+# test in the pair before touching either.
+
+
+def test_fact_times_fact_passes_outside_a_condition():
+    """`remember ... with/from` arithmetic never reaches the Z3 encoder,
+    so it stays unrestricted — the non-deontic half of the boundary."""
+    session, results = run_lines([
+        "remember a number called beta with 2",
+        "remember a number called z with beta multiplied by beta",
+    ])
+    for r in results:
+        assert r.status is ResultStatus.SUCCESS, r.message
+
+
+def test_fact_times_fact_rejects_inside_a_condition():
+    """The same expression, as a condition value, rejects — the deontic
+    half of the boundary."""
+    session, results = run_lines([
+        "remember a number called alpha with 10",
+        "remember a number called beta with 2",
+        "forbid alpha is above beta multiplied by beta",
+    ])
+    assert results[-1].status is ResultStatus.ERROR_SEMANTIC
+
+
+# ---------- type-check precedence: linearity check fires last ----------
+
+
+def test_text_in_condition_arithmetic_still_gives_text_error_not_linearity_error():
+    session, results = run_lines([
+        "remember a number called alpha with 10",
+        "remember a number called beta with 2",
+        'forbid alpha is above "text" multiplied by beta',
+    ])
+    assert results[-1].status is ResultStatus.ERROR_SEMANTIC
+    msg = _semantic_message(results)
+    assert "text" in msg.lower()
+    assert "at least one plain number" not in msg
+
+
+# ---------- date arithmetic message parity (untouched) ----------
+
+
+def test_date_arithmetic_rejection_message_is_unchanged():
+    session, results = run_lines([
+        "remember a date called d1 with 2025-01-01",
+        "remember a number called z with d1 multiplied by 2",
+    ])
+    assert results[-1].status is ResultStatus.ERROR_SEMANTIC
+    assert "can't be multiplied or divided" in _semantic_message(results).lower()
+
+
+# ---------------------------------------------------------------------------
+# Known gap — Fable decidability condition (c) remains OPEN. See the PR
+# description / chain addendum for the full record. The restriction above
+# only inspects a condition's own expression tree: it catches
+# `beta multiplied by beta` written directly as a condition value, but not
+# the same nonlinearity introduced through value indirection. Any
+# remember-bound name whose value derives from fact × fact / fact ÷ fact
+# reads as a plain NameRef in the condition AST, so the check never sees
+# the ArithmeticNode. This is the common authoring form, not an edge case —
+# closing it requires value provenance (taint at store time, a definition-
+# site walk at analysis time, or resolving names to their defining
+# expressions inside the future Z3 encoder). None of those are built yet.
+# This test pins the CURRENT behaviour so it is impossible to miss when
+# provenance work lands and this test needs to invert.
+# ---------------------------------------------------------------------------
+
+
+def test_KNOWN_GAP_value_indirection_bypasses_the_linearity_restriction():
+    """Condition (c) is open, not closed. A nonlinear expression computed
+    into a named value and then referenced in a condition currently
+    PASSES analysis and evaluates — the restriction only sees the
+    condition's own AST, which contains a bare NameRef, never the
+    ArithmeticNode that produced it. See the addendum for the candidate
+    provenance approaches under consideration."""
+    session, results = run_lines([
+        "remember a number called alpha with 10",
+        "remember a number called beta with 2",
+        "remember a value called doubled from beta multiplied by beta",
+        "forbid alpha is above doubled",
+    ])
+    for r in results[:-1]:
+        assert r.status is ResultStatus.SUCCESS, r.message
+    assert results[-1].status is ResultStatus.PROHIBITION_VIOLATED