# ADR-005: OCTAVE v1.5 — Compiler Shift + Operator Evolution

## Status
PROPOSED

## Context

### The Problem
Agents naturally write rich OCTAVE expressions that the parser silently corrupts or rejects, forcing 3–4 iteration rounds per document. Issue #287's "Wind/Wall/Door" debate identified the root cause: we ask a probabilistic writer to produce deterministic data directly, with no compilation step. Separately, the emitter doesn't append a POSIX trailing newline (#284), breaking standard pre-commit hooks.

### The Opportunity
A 4-model cross-validation study (Claude Opus 4.6, Gemini 3.1 Pro Preview, ChatGPT 5.2, Claude Sonnet 4.6) validated three epistemic operators that fill genuine semantic gaps in OCTAVE — the ability to distinguish extracted facts from agent inferences, and to mark contradictions structurally rather than textually.

### Evidence Base
- **Cross-model study**: `docs/research/cross-model-operator-validation-study.md`
- **Round-trip fidelity**: `docs/research/compression-fidelity-round-trip-study.md`
- **Issues**: #284 (trailing newline), #287 (parser corruption P1–P4)

### Current Architecture
- **Lexer** (`src/octave_mcp/core/lexer.py`): 7 operators in `OPERATOR_CHARS` (line 121) + `ASCII_ALIASES` (line 97). `%` hits E005 catch-all at line 1125. No support for □/◇/⊥.
- **Parser** (`src/octave_mcp/core/parser.py`): `parse_value()` dispatches to `parse_flow_expression()` on seeing EXPRESSION_OPERATORS after an identifier. Operators within values terminate value assembly — everything after is orphaned (#287 P2). Constructor brackets `NAME[args]` converted to `NAME<args>` or stripped (#287 P4).
- **Emitter** (`src/octave_mcp/core/emitter.py`): `emit()` (lines 624–691) joins lines with `\n` and returns — no trailing newline (#284 root cause).
- **Write tool** (`src/octave_mcp/mcp/write.py`): `f.write(canonical_content)` at line 1520 writes whatever `emit()` returns.
- **Grammar** (`docs/grammar/octave-v1.0-grammar.ebnf`): 7 expression operators in Sections 7–8.

## Decision

### Architectural Principle: SOURCE → STRICT Compilation

OCTAVE adopts a compiler model. Agents write in a lenient superset (OCTAVE_SOURCE) which the toolchain compiles to canonical form (OCTAVE_STRICT). The compilation is deterministic, auditable, and teaches agents correct form by echoing what changed — rather than rejecting input.

This ADR introduces the embryo of this model: lenient-mode parsing in `octave_write` that preserves operator-rich values and special characters, with a confirmation echo showing the SOURCE → STRICT delta.

**Alignment with ADR-001**: This extends the "Spec-Static, Schema-Dynamic" principle. Core grammar remains static. What changes is the parser's *tolerance* of source-form input and its ability to compile rather than reject.

### Decision 1: Three New Operators — □ ◇ ⊥

**Add three operators to the OCTAVE language specification: two provenance markers and one contradiction operator.**

#### Critical Design Constraint: Provenance Markers, Not Modal Logic

□ and ◇ are **provenance markers** — they answer exactly one question: *"Did this data come from a source document, or did the agent generate it?"* They are NOT composable modal logic operators. OCTAVE redefines these symbols for structured provenance, just as it redefines → for flow rather than material implication.

**Empirical basis for this constraint:** Cross-model testing revealed that when □ wraps structured data (e.g. `□[Revenue=4.2B]`, `□[Intrusion_Success=∅{State: Exhausted}]`), LLMs read it pragmatically as a provenance/certainty marker. But when □ wraps natural language prose (e.g. `□["market failure is highly likely"]`), LLMs revert to formal modal logic interpretation ("necessarily true in all possible worlds"), which misrepresents the intended semantics. This divergence was confirmed across ChatGPT 5.2 and Claude Opus 4.6.

**Content rule:** □/◇ wrap structured OCTAVE values, not natural language prose. Compress meaning into structured form first, then mark provenance.

**Architectural distinction** (from Wind/Wall/Door debate review): □ and ◇ are **unary wrappers** (they wrap a single value), while ⊥ is a **binary relation operator** (it connects two contradictory claims). Treating all three as binary `EXPRESSION_OPERATORS` would break compound expressions like `□[Fact] → ◇[Inference]`.

**Provenance Wrappers (unary):**

| Symbol | Unicode | TokenType | Grammar Role | Meaning |
|--------|---------|-----------|--------------|--------|
| □ | U+25A1 | NECESSITY | EpistemicWrapper → EpistemicNode | Extracted from source document |
| ◇ | U+25C7 | POSSIBILITY | EpistemicWrapper → EpistemicNode | Generated by this agent (inference) |

**Relation Operator (binary):**

| Symbol | Unicode | TokenType | Grammar Role | Meaning |
|--------|---------|-----------|--------------|--------|
| ⊥ | U+22A5 | CONTRADICTION | EXPRESSION_OPERATORS (binary, lowest precedence) | Logical impossibility / cannot both be true |

**Rationale:**
1. **4-model zero-shot validation**: All four models resolved □/◇/⊥ correctly with zero OCTAVE context. ChatGPT identified □ as "strong claim / invariant" and ◇ as "tentative claim / uncertainty allowed" when given only `□[Revenue=4.2B]` vs `◇[Revenue≈4.2B]`.
2. **Strong corpus binding on structured data**: These symbols produce correct pragmatic readings when wrapping structured OCTAVE content. The THREAT::Ares example (`□[Intrusion_Success=∅{State: Exhausted}]`) was correctly reconstructed by ChatGPT 5.2 and Sonnet 4.6 with full semantic fidelity.
3. **Genuine semantic gap**: When an agent writes `Revenue::4.2B`, there is no way to distinguish whether the value was extracted from a source document or calculated by the agent. □/◇ makes this distinction structural.
4. **Operator minimalism preserved**: Adding 3 operators to the existing 7 yields 10 total — within the validated minimalism boundary where Gemini self-corrected from 15+ to agreement that 7+3 is better.

**What was rejected:**
- ⊙ for Zugzwang — failed cross-model validation (ChatGPT read as "focal evaluation state")
- Physics/calculus metaphors (∇, ∫, ∂, μ) — metaphorical repurposing of mathematical symbols creates ambiguity
- Chess notation (!!, !?) — untested for LLM-to-LLM fidelity
- ≅ (semantic congruence) — validated but lower priority, deferred to future ADR
- ▨ (entailment/attribution) — speech-act logic is out of scope for v1.5; attribution is handled by KEY placement

#### Epistemic Default

Unadorned values (e.g. `Revenue::4.2B` without □/◇) have **no epistemic status** — they are values, as they always have been. □/◇ are opt-in annotations. The spec documentation should recommend their use and note that unadorned values carry no provenance guarantee. This avoids retroactive semantic changes to existing OCTAVE documents.

#### Parser Guard: Nesting Ban (E_NESTED_CERTAINTY)

`□[◇[x]]` and all other wrapper nesting must be a parser error (`E_NESTED_CERTAINTY`).

**Rationale (empirically grounded):** When LLMs encounter nested □/◇ compositions, they revert to formal modal logic interpretation ("□[◇[x]]" = "necessarily possible"), losing the intended OCTAVE provenance semantics. This was directly falsified in testing: ChatGPT 5.2 interpreted `□[◇["Market_Failure"]]` as a modal logic construct, not as "it's a fact that the source asserts a possibility." The nesting ban exists because LLMs empirically misinterpret composition, not merely because it's logically redundant.

#### ⊥ Operator Precedence

⊥ (Contradiction) has the **lowest binding precedence** among all EXPRESSION_OPERATORS. It evaluates last, comparing fully resolved expressions on each side.

Example: `□[Feature_A] ∧ □[Feature_B] ⊥ □[Legacy_System]` parses as `(□[Feature_A] ∧ □[Feature_B]) ⊥ □[Legacy_System]`.

#### Calculus of Certainty (Provenance Propagation)

When agents combine values marked with □/◇, the resulting provenance follows these rules:

| Input A | Input B | Transformation | Result | Rationale |
|---------|---------|---------------|--------|-----------|
| □ (fact) | □ (fact) | Deterministic (math/logic) | □ (fact) | Derived fact — no agent judgment involved |
| □ (fact) | □ (fact) | Heuristic (LLM inference) | ◇ (inference) | Agent touched it — downgrades to inference |
| □ (fact) | ◇ (inference) | Any | ◇ (inference) | Contamination — weakest provenance wins |
| ◇ (inference) | ◇ (inference) | Any | ◇ (inference) | Stays uncertain |

This eliminates the need for a separate "derived" operator (△) — derivation is a state transition governed by the truth table, not a symbol.

#### Anti-Laundering Protocol (Multi-Agent Chains)

When Agent B consumes OCTAVE produced by Agent A:
- **Summarizing** Agent A's ◇ claim → keep ◇
- **Calculating** from Agent A's □ inputs deterministically → promote to □ (truth table row 1)
- **Repeating** a claim without verification → `Claim::□["Agent A said X"]` (quote the utterance, not the fact)

This prevents provenance laundering — an agent cannot upgrade ◇ to □ by simply repeating it.

#### Canonical Usage Patterns

**Correct — structured data with provenance:**
```
SEC_FILING_10K::
  Revenue::□[4.2B]
  Margins::□[12%]

AGENT_ANALYSIS::
  Risk_Score::◇[HIGH]
  Market_Outlook::◇[contraction∧DAMOCLEAN]
```

**Correct — the CEO problem (attribution in KEY, structured content, □ marks provenance):**
```
CEO_Statement::□[market_failure∧DAMOCLEAN]
```
Reads as: "I extracted from the source that the CEO frames market failure as a Damoclean threat."

**Wrong — natural language inside □ (triggers formal logic reversion):**
```
CEO_Statement::□["market failure is highly likely"]
```
LLMs interpret this as "it is necessarily true that market failure is highly likely" — not the intended provenance marking.

**Wrong — flow operator for attribution (misplaces modality):**
```
□[CEO_Statement] → ◇[Market_Failure]
```
Reads as "if CEO statement is necessarily true, then market failure is possible" — causality, not attribution.

**Changes required:**
- `lexer.py`: Add □, ◇, ⊥ to `OPERATOR_CHARS`; add `TokenType.NECESSITY`, `TokenType.POSSIBILITY`, `TokenType.CONTRADICTION`
- `parser.py`: Add ⊥ to `EXPRESSION_OPERATORS` frozenset (binary, lowest precedence). Add □/◇ as `EPISTEMIC_WRAPPERS` (new frozenset, unary). Handle wrappers in `parse_value()` producing `EpistemicNode`; handle ⊥ in `parse_flow_expression()`
- Grammar EBNF: Add epistemic wrapper production to Section 7; add ⊥ to Section 8 (operator terminals). Wrappers are prefix-unary: `□[value]`, `◇[value]`. ⊥ has lowest binding precedence.
- Spec documentation: New section explaining provenance markers — explicitly stating these are NOT formal modal logic operators, with correct/incorrect usage patterns and the Calculus of Certainty truth table

### Decision 2: Trailing Newline (#284)

**Ensure `emit()` always returns content ending with `\n`.**

File: `src/octave_mcp/core/emitter.py` — `emit()` function (line 691)

Change: `if not output.endswith('\n'): output += '\n'` before the return.

Rationale: POSIX standard for text files. Fixes pre-commit `end-of-file-fixer` failures. Zero risk — emitter is the single canonical output path.

### Decision 3: Lexer Accepts `%` in Values (#287 P1)

**Add `%` to the set of characters valid within value contexts.**

File: `src/octave_mcp/core/lexer.py` — before the E005 catch-all (line 1125)

Rationale: Percentages are extremely common in OCTAVE content (metrics, budgets, compression ratios). Currently `60%_burned` hits E005. When `%` is encountered in a value position, it should be treated as part of the current token.

**Binding constraint:** `%` is only valid when immediately preceded by an alphanumeric character (e.g. `60%`, `100%_complete`). A standalone `%` or prefix `%foo` must still raise E005. This prevents future ambiguity if `%` ever acquires operator semantics (e.g. modulo).

**Boundary rule:** The `%` token terminates immediately upon encountering an operator character. `60%→` must lex as two tokens: `60%` + `→`, not a single malformed token.

### Decision 4: Parser Preserves Operator-Rich Values (#287 P2)

**When an operator appears between constructors within a value, capture the entire expression as a single value string.**

Example: `CHRONOS::2024[x] → 2026[y]` — the `→` is semantic content, not a structural delimiter.

Approach: When `lenient=True` (default for `octave_write`), treat the entire post-`::` content as a string value if it contains operators between constructors. Log a `W_SOURCE_COMPILE` correction showing what was normalized. When `lenient=False` (strict mode), current behavior preserved.

This is the embryo of SOURCE → STRICT compilation. It does not change the canonical OCTAVE grammar — it changes how tolerantly the parser accepts input before normalizing.

### Decision 5: Block Parent Preservation (#287 P3)

**When a block key like `LOSS_PROFILE:` has indented children, ensure children remain associated with their parent during normalization.**

File: `src/octave_mcp/core/parser.py` — implicit dedent detection (~line 790)

The current bug promotes children to root level when inside META blocks.

### Decision 6: Confirmation Echo Pattern

**When SOURCE → STRICT compilation occurs, the write tool response includes a `compilations` field showing the delta.**

Example:
```json
{
  "compilations": [
    {"source": "budget::60%_burned", "strict": "budget::\"60%_burned\"", "rule": "special_char_wrap"}
  ]
}
```

This teaches agents correct form by showing the transformation rather than rejecting input. Replaces the current pattern of silent correction or opaque error.

**Token budget constraint:** Cap the `compilations` array at 5 entries. If more corrections occurred, append a summary: `"...and N other normalizations applied."` This prevents the echo from consuming excessive context window on heavily malformed input.

**Future optimization:** The JSON echo format is reliable but token-heavy. A future iteration may adopt OCTAVE-native echo format (e.g. `budget::60%_burned ↹ budget::"60%_burned" (special_char_wrap)`) for lower token cost in agent-to-agent contexts. Deferred to post-v1.5 — reliability over token savings at this scale.

### Decision 7: Literal Zone Documentation

**Include guidance about literal zones (fenced code blocks) in tool responses and error messages.**

Agents consistently try to encode code as OCTAVE strings because nothing teaches them that fenced code blocks are valid OCTAVE content. LLMs are heavily RLHF-tuned to output Markdown; without explicit guidance that Markdown code blocks are natively supported in OCTAVE, the default bias is to flatten code into escaped strings.

**Primary delivery point:** The `octave_write` and `octave_validate` tool descriptions themselves, not just standalone docs. Tool descriptions are where agents read first. Secondary: error messages when string-escaped code is detected.

## Implementation Order

1. Trailing newline (#284) — smallest, zero risk, unblocks pre-commit
2. Lexer `%` fix (#287 P1) — isolated lexer change
3. New operators □/◇/⊥ — lexer + parser + grammar (□/◇ as unary wrappers, ⊥ as binary operator)
4. Parser value preservation (#287 P2) — most complex, needs careful test coverage
5. Block parent fix (#287 P3) — parser indentation logic
6. Confirmation echo + literal zone docs — write tool response changes

## Testing Strategy

- TDD: each change gets tests before implementation (per quality gates)
- Round-trip tests: write OCTAVE_SOURCE → read back → verify no data loss
- Cross-operator tests: ensure new operators don't interfere with existing 7
- Wrapper composition tests: `□[x] → ◇[y]` parses correctly; `□[◇[x]]` raises `E_NESTED_CERTAINTY`
- Provenance propagation tests: `□[10] + □[20]` deterministic → `□[30]`; `□[x]` + heuristic → `◇[result]`
- ⊥ precedence tests: `A ∧ B ⊥ C` parses as `(A ∧ B) ⊥ C`
- Pre-commit integration test: verify `end-of-file-fixer` passes on emitted files
- Existing 2080+ test suite must remain green throughout

## Consequences

### Positive
1. **Reduced iteration cycles**: Agents can write naturally; the toolchain compiles rather than rejects
2. **Epistemic clarity**: □/◇ distinction makes fact vs inference structural, not ambiguous
3. **Cross-model fidelity**: New operators validated across 4 LLM architectures before adoption
4. **POSIX compliance**: Trailing newline fixes integration with standard tooling
5. **Teachable corrections**: Confirmation echo shows agents what changed and why

### Negative
1. **Operator count increases**: 7 → 10 operators, increasing spec surface area
2. **Lenient mode complexity**: Two parsing modes (lenient/strict) adds code paths to maintain
3. **Grammar evolution**: EBNF and spec documents need updating alongside code

### Risks
1. **Lenient mode drift**: If lenient tolerance expands unchecked, SOURCE and STRICT diverge too far. Mitigated by requiring every lenient acceptance to produce an auditable compilation log.
2. **Operator precedence interactions**: New operators must integrate cleanly with existing 7. Mitigated by TDD and round-trip testing.
3. **Wrapper/operator confusion**: If □/◇ are mistakenly added to `EXPRESSION_OPERATORS` (binary), compound expressions like `□[Fact] → ◇[Inference]` will misparse. Mitigated by the explicit wrapper/operator split and `E_NESTED_CERTAINTY` guard.
4. **Formal logic reversion**: Agents without OCTAVE context may interpret □/◇ as formal modal logic operators. Mitigated by: (a) content rule requiring structured data inside wrappers, (b) explicit "not modal logic" statement in spec docs and tool descriptions, (c) canonical usage patterns showing correct vs incorrect forms.
5. **Provenance laundering**: In multi-agent chains, an agent could upgrade ◇ to □ by simply repeating a claim. Mitigated by the anti-laundering protocol and truth table.

## Scope Boundary

**In scope:** Issues #284, #287 (P1–P4), new operators □/◇/⊥, confirmation echo, literal zone docs.

**Out of scope (future milestones):**
- Full OCTAVE_SOURCE grammar specification (formal superset)
- Residual compression / tier-on-demand
- Mythology formalization as first-class spec feature
- ≅ operator (semantic congruence) — validated but deferred
- ⊙ / chess notation — failed or unvalidated

## References

### Specifications
- `src/octave_mcp/resources/specs/octave-core-spec.oct.md` — Core grammar, operators
- `docs/grammar/octave-v1.0-grammar.ebnf` — Formal grammar definition

### Research
- `docs/research/cross-model-operator-validation-study.md` — 4-model validation evidence
- `docs/research/compression-fidelity-round-trip-study.md` — Round-trip fidelity data

### Issues
- #284 — Trailing newline missing from emitter output
- #287 — Parser corruption: %, operator-rich values, block parents

### Related ADRs
- ADR-001 — Configurability and Modularity Architecture ("Spec-Static, Schema-Dynamic")
- ADR-004 — Tool Consolidation Design (octave_write as unified entry point)
