From 54983ee0046ca314d7b50d9d96e3c49d0abefc7d Mon Sep 17 00:00:00 2001 From: Mamdouh Aboammar Date: Sun, 1 Nov 2026 21:31:47 +0200 Subject: [PATCH] research: verify expression composition, module resolution and event playbook contracts --- DEBATES.md | 5 +++ DECISIONS.md | 5 +++ OUT_OF_THE_BOX.md | 5 +++ evals/phase-007g-reference.json | 13 ++++++++ evals/phase-007g-validation.md | 15 +++++++++ spec/grammar.ebnf | 14 +++++--- spec/phase-007g-composable-language-v1.md | 37 ++++++++++++++++++++++ tests/test_phase_007g_language_research.py | 29 +++++++++++++++++ 8 files changed, 118 insertions(+), 5 deletions(-) create mode 100644 evals/phase-007g-reference.json create mode 100644 evals/phase-007g-validation.md create mode 100644 spec/phase-007g-composable-language-v1.md create mode 100644 tests/test_phase_007g_language_research.py diff --git a/DEBATES.md b/DEBATES.md index 385eb95..b4ced75 100644 --- a/DEBATES.md +++ b/DEBATES.md @@ -1150,3 +1150,8 @@ Thesis: canonical SHA-256 evidence supports deterministic, portable post-restart ## Phase 007F — Commit acknowledgements and single-writer recovery versus physical guarantees Option A retained a caller-managed checkpoint but allowed accidental successful acknowledgements across ambiguous rename/fsync windows. Selected, without accepting an ADR: Option B, a narrow opt-in coordinator that validates a complete Phase 007E audit, publishes via the existing single-writer checkpoint writer, re-reads the evidence, and issues a checksum-bound receipt. Option C, consensus/database/broker infrastructure, remains unapproved. A failed directory fsync cannot authorize SUCCESS even if new content is visible. A stored checksum cannot authenticate its producer; without an externally trusted retained receipt it cannot reveal rollback to an older self-consistent image. Falsifiers and measured counterexamples: spec/financial-commit-recovery-007f.md and evals/financial-commit-recovery-007f.md. + + +## Phase 007G — Strict composability versus unconstrained scripting + +Selected: a bounded precedence-climbing expression tree, explicit named module exports, and file ingestion through the existing World event validation path. Rejected: arbitrary code evaluation, wildcard import merging, a package manager, a new event scheduler, implicit numeric widening or legacy/World engine unification. Falsifiers: incorrectly associated arithmetic, conflicting namespace bindings, invalid JSON acceptance, or altered seeded snapshot behavior. Research: spec/phase-007g-composable-language-v1.md. This is not an Accepted ADR. diff --git a/DECISIONS.md b/DECISIONS.md index 63ab68f..7691cda 100644 --- a/DECISIONS.md +++ b/DECISIONS.md @@ -556,3 +556,8 @@ Bounded implementation record only: opt-in canonical financial audit v1 with str ## Phase 007F — Implementation checkpoint; no accepted architecture decision 2026-11-01: Opt-in single-writer commit coordinator, versioned deterministic receipt and recovery validation added within the already approved domain boundary. A revalidated complete audit is required before publication; a changed checkpoint requires the previous trusted receipt; a successful acknowledgement requires publication plus revalidation; uncertain syscall outcomes raise an explicit recovery-required exception. Exactly-once network delivery, multi-writer serializability, producer authentication, crash-proof file hardware, and arbitrary valid rollback prevention are not accepted or demonstrated. Existing DEC-009 and Phase 007E contracts remain unchanged. See spec/financial-commit-recovery-007f.md. No new Accepted ADR. + + +## Phase 007G — Proposed language implementation checkpoint, not Accepted ADR + +Versioned additions introduce bounded typed arithmetic AST composition, deterministic explicit World declaration imports, and versioned strict event playbook input. Existing DEC-009 accounting boundaries, DEC-027 pre-event snapshot semantics and DEC-031 keyed RNG remain controlling. No legacy engine migration or empirical equivalence decision is made. Research: spec/phase-007g-composable-language-v1.md. diff --git a/OUT_OF_THE_BOX.md b/OUT_OF_THE_BOX.md index bd809ea..5adfd1b 100644 --- a/OUT_OF_THE_BOX.md +++ b/OUT_OF_THE_BOX.md @@ -548,3 +548,8 @@ Potential future externally anchored digest catalogs, HMAC with operator-owned k ## Phase 007F frontier — authenticated rollback fences and writer arbitration (unimplemented) Potential future research would specify operator-controlled immutable anchors, signature trust roots, durable fencing tokens, and a concrete multi-writer arbitration threat model. None is authorized by the present checksum-bound single-writer commit coordinator. A production durability promise additionally requires filesystem/hardware-specific power-loss experiments; an unanchored hash chain cannot independently prohibit older valid checkpoint substitution. + + +## Phase 007G frontier — Future module package system and engine equivalence (unimplemented) + +Potential future work could compare semantic traces for deliberately paired legacy and World models or test explicit module package manifests. Neither a package resolver nor a single merged simulation runtime is implemented or approved by Phase 007G. diff --git a/evals/phase-007g-reference.json b/evals/phase-007g-reference.json new file mode 100644 index 0000000..5d17a26 --- /dev/null +++ b/evals/phase-007g-reference.json @@ -0,0 +1,13 @@ +{ + "schema": "funnelscript-phase-007g-independent-example-v1", + "world": "Demo", + "seed": 42, + "inputs": [ + {"name": "Balance.Tick", "time": 1, "payload": {}}, + {"name": "Lead.Tick", "time": 0, "payload": {"increment": 3}} + ], + "expected": { + "processed_events": 2, + "state": {"Balance": {"count": 9}, "Lead": {"visits": 6}} + } +} diff --git a/evals/phase-007g-validation.md b/evals/phase-007g-validation.md new file mode 100644 index 0000000..e1cbe39 --- /dev/null +++ b/evals/phase-007g-validation.md @@ -0,0 +1,15 @@ +# Phase 007G — Evidence ledger and limitations + +- Three separately authored public tests were run before production edits with exit status 1: expression chain rejection (`Chained binary operators are not supported`), named-import brace rejection (`Expected token IDENTIFIER, found LBRACE`), and absent `events_file` parameter (`unexpected keyword argument`). The GREEN command `uv run pytest -q tests/test_composable_expressions_007g.py tests/test_named_exports_007g.py tests/test_event_playbooks_007g.py tests/test_world_modules.py` reported **26 passed** after implementations. Subsequent expanded feature tests reported **29 passed**; one test originally expected only ValueError for invalid priority, but the existing strict Event constructor correctly raises TypeError; the test expectation was expanded to include the established error class, without weakening behavior. +- Existing older tests that rejected formerly unsupported valid expressions were rewritten as positive numerical-value assertions; invalid operator endings and exact mixed-type failures remain negative tests. A full regression identified an older `payload.amount + 1` test that expected rejection. That check now expects acceptance, consistent with the new strictly typed grammar. Final full Python app test after this change initially reported **571 passed and 58 subtests**. Later full verification receipts must supersede these intermediate values if further changes are made. +- Independent language fixture reference is `evals/phase-007g-reference.json`: initial Count 1, transformed `(1+2)*3=9`; initial Visits 0, payload increment 3 and multiplier 2 yields 6; both events are processed, and event time order is 0 then 1. The fixture uses no production import and no claimed real-world causality. +- Security boundaries: local source-only named imports preserve path normalization, traversal and symlink confinement, and cycle rejection. A strict UTF-8 JSON playbook uses duplicate-key detection, exact schema, 1 MiB max file size, at most 10,000 events, original event type/priority validation, and rejects mixed inline/file modes. Expression depth limit 24, token window limit 256, exact primitive numeric type equality, controlled divide-by-zero and non-finite output. No filesystem write, eval, interpreter fusion or provider connection is introduced. +- Compatible concepts: typed states/events and deterministic schedules. Intentionally different semantics: legacy marketing strategy SimulationEngine and source World reducer, separate AST and trial APIs. Missing adapter and equivalence oracle: no migrated unified runtime. Neither empirical economics equivalence nor PR-independent approval is implied. + +## Final fresh verification and reviewer limitations (2026-11-01) + +Full application suites: `uv run pytest -q` and `uv run pytest -v` each returned exit code 0, **573 passed and 58 subtests passed**. `uv run python -m compileall -q src/funnelscript`, `uv build`, `bun install --frozen-lockfile`, `bun test` (1 passed), `bun run build`, `git diff --check` and an installed-wheel `funnelscript run-world` smoke using a real multi-export module and strict JSON playbook completed with exit code 0. The resulting oracle state was `Balance.count=9`, `Lead.visits=6`, 2 processed events. Original Phase 007A–007F regression tests are included in the full run. + +Research: `uv run --no-project --with pytest pytest -q` and `-v` each returned exit code 0, **57 passed and 149 subtests passed**. No production financial files, compiler-incompatible syntax in legacy StrategyAST, new dependency or new simulation engine was added. + +Manual non-Codex staged-diff/static review inspected parser disambiguation, explicit import alias binding, path confinement, bounded event-file decoding, no `eval()`/`exec()` use, exact numeric type preservation, and the existing copy-on-write rule evaluation. No external independent reviewer sign-off is claimed: the available A2M Code Review Graph tool does not authorize isolated `phase-007g` worktree roots, so independent graph review cannot be asserted. This limitation does not alter the evidence from executed tests. Unverified claims include statistical market calibration, legacy/World full semantic equivalence, distributed imports, general-purpose expression evaluation and real-world economic causality. diff --git a/spec/grammar.ebnf b/spec/grammar.ebnf index cf10be0..7fcab3b 100644 --- a/spec/grammar.ebnf +++ b/spec/grammar.ebnf @@ -8,7 +8,8 @@ ProgramFile ::= StrategyFile | WorldFile ; (* New declaration words are soft keywords in the reference lexer. *) WorldFile ::= "world" Identifier "{" WorldDeclaration* "}" ; WorldDeclaration ::= WorldEntityDeclaration | WorldAgentDeclaration | WorldImport ; -WorldImport ::= "import" StringLiteral "as" Identifier ";" ; +WorldImport ::= "import" StringLiteral ("as" Identifier | "{" NamedImport ("," NamedImport)* "}") ";" ; +NamedImport ::= Identifier ("as" Identifier)? ; WorldEntityDeclaration ::= "entity" Identifier "{" WorldMember* "}" ; WorldAgentDeclaration ::= "agent" Identifier "{" WorldMember* "}" ; WorldMember ::= StateField | EventDeclaration | RuleDeclaration ; @@ -21,17 +22,20 @@ GuardClause ::= "when" "(" Identifier GuardOp StateLiteral ")" ; GuardOp ::= "==" | "!=" | "<" | "<=" | ">" | ">=" ; RuleStatement ::= TransitionStatement | EmitStatement ; TransitionStatement ::= "transition" Identifier "=" TransitionExpression ";" ; -TransitionExpression ::= StateExpression | SampleExpression ; +TransitionExpression ::= StateExpression ; (* Lexer recognizes // comments before the single / division token. *) -BinaryOperator ::= "+" | "-" | "*" | "/" ; -BinaryRight ::= StateLiteral | PayloadReference | Identifier ; +AdditiveOperator ::= "+" | "-" ; +MultiplicativeOperator ::= "*" | "/" ; SampleExpression ::= "sample" ("bernoulli" "(" SampleArgument ")" | "uniform" "(" SampleArgument "," SampleArgument ")") ; SampleArgument ::= SignedNumber | PayloadReference | Identifier ; EmitStatement ::= "emit" Identifier ("(" EventArgList? ")")? "after" SignedNumber ";" ; EventArgList ::= EventArgument ("," EventArgument)* ; EventArgument ::= Identifier "=" StateExpression ; -StateExpression ::= StateLiteral | PayloadReference | Identifier (BinaryOperator BinaryRight)? ; +StateExpression ::= AdditiveExpression ; +AdditiveExpression ::= MultiplicativeExpression (AdditiveOperator MultiplicativeExpression)* ; +MultiplicativeExpression ::= PrimaryExpression (MultiplicativeOperator PrimaryExpression)* ; +PrimaryExpression ::= StateLiteral | PayloadReference | Identifier | "(" StateExpression ")" | SampleExpression ; PayloadReference ::= "payload" "." Identifier ; PrimitiveType ::= "int" | "float" | "bool" | "string" ; StateLiteral ::= SignedNumber | StringLiteral | BooleanLiteral ; diff --git a/spec/phase-007g-composable-language-v1.md b/spec/phase-007g-composable-language-v1.md new file mode 100644 index 0000000..68e5458 --- /dev/null +++ b/spec/phase-007g-composable-language-v1.md @@ -0,0 +1,37 @@ +# Phase 007G — Proposed composability contracts (not an Accepted ADR) + +Research anchor: Pratt/precedence-climbing expression parsing (Pratt 1973); compositional operational semantics (Plotkin 1981); deterministic discrete-event simulation (Law, Simulation Modeling and Analysis); explicit lexical symbol binding and dependency-cycle detection; RFC 8259 JSON interoperability. Implementation limits are independently falsifiable, not claims of compiler equivalence with a legacy engine. + +## H-EXPR — typed composable expressions + +Falsifier: parsing `a - b - c` as `a - (b - c)`, `a + b * c` as `(a + b) * c`, permitting mixed `int`/`float` without explicit conversion, or observing a partially mutated snapshot after arithmetic failure. + +Versioned grammar `world-expression-v1` (bounded by 24 AST levels, 256 tokens per expression): +```ebnf +expression = additive ; +additive = multiplicative , { ("+" | "-") , multiplicative } ; +multiplicative= primary , { ("*" | "/") , primary } ; +primary = number | string | boolean | state-reference + | "payload" , "." , identifier | "(" , expression , ")" + | stochastic-sample ; +state-reference = identifier ; +``` +All state/payload references are owner-local. Binary operands must have identical exact numeric types. Division yields float and must target float; typed literal divisor zero is rejected statically, dynamic divisor zero fails without committing any transition. No implicit int-to-float coercion, no side effects or evaluation of Python code; existing sample operator semantics and RNG ownership remain unchanged. Parsing consumes expression until statement delimiters. Left-associative tiers retain deterministic source-level ordering. + +## H-MODULE — named explicit exports + +Falsifier: importing an unknown name, duplicated local binding, path traversal, symlink escape or transitive cycle succeeds. Versioned extension `named-import-v1`: +```ebnf +import = "import" , string , ("as" , identifier + | "{" , selected , { "," , selected } , "}" ) , ";" ; +selected = identifier , [ "as" , identifier ] ; +``` +Legacy `import "single.fnl" as Alias;` retains the exact-one-declaration rule. Named imports select declared exports by source name from a multi-declaration World module, without wildcard/implicit namespace joins; aliasing changes the owner label only. Direct and transitive module paths remain constrained to importer directory or packaged `std:` root. Duplicate aliases are rejected by the existing World type checker. No network resolution or dynamic execution. + +## H-PLAYBOOK — reproducible files + +Falsifier: file-input and identical inline JSON events produce different deterministic World states, malformed typed payload is admitted, duplicate key is lost, or oversized input triggers unbounded decoding. Versioned `funnelscript-event-playbook-v1` is an exact object `{"schema":"funnelscript-event-playbook-v1","events":[...]}`, containing 0–10,000 records with strict event fields `name,time,payload,priority`. File UTF-8 size at most 1 MiB. JSON duplicate keys rejected at any depth. Each record is canonicalized through existing inline event parser and World execution; no parallel event semantics. `--event` and `--events-file` are mutually exclusive in v1. No network reads or external effects. + +## Compatibility and scientific boundary + +World keeps snapshot-atomic event transitions, seeded keyed RNG and per-owner events. The older marketing SimulationEngine is a separate algorithm and makes no bitwise equivalence claim. Canonical financial audit/receipts are unchanged; changes are limited to parser, type AST, World evaluation and CLI ingestion. No Accepted ADR authorized. Evidence requires RED before each production change; full legacy, financial, packaging and frontend regression before GitHub delivery. diff --git a/tests/test_phase_007g_language_research.py b/tests/test_phase_007g_language_research.py new file mode 100644 index 0000000..ac93123 --- /dev/null +++ b/tests/test_phase_007g_language_research.py @@ -0,0 +1,29 @@ +"""Independent Phase 007G grammar and hand-calculated event oracle checks.""" +import json +from pathlib import Path + +ROOT = Path(__file__).resolve().parents[1] + + +def test_grammar_is_closed_for_new_expression_and_module_nonterminals(): + grammar = (ROOT / 'spec/grammar.ebnf').read_text() + assert 'WorldImport ::= "import" StringLiteral' in grammar + assert 'NamedImport ::= Identifier ("as" Identifier)?' in grammar + assert 'AdditiveExpression ::= MultiplicativeExpression' in grammar + assert 'MultiplicativeExpression ::= PrimaryExpression' in grammar + assert 'PrimaryExpression ::= StateLiteral | PayloadReference | Identifier' in grammar + assert 'BinaryRight ::=' not in grammar + spec = (ROOT / 'spec/phase-007g-composable-language-v1.md').read_text() + for name in ('H-EXPR', 'H-MODULE', 'H-PLAYBOOK', 'snapshot', '1 MiB', '10,000'): + assert name in spec + + +def test_oracle_is_independent_of_production_engine(): + receipt = json.loads((ROOT / 'evals/phase-007g-reference.json').read_text()) + assert receipt['schema'] == 'funnelscript-phase-007g-independent-example-v1' + assert receipt['seed'] == 42 + assert {event['name'] for event in receipt['inputs']} == {'Balance.Tick', 'Lead.Tick'} + initial_balance, initial_visits = 1, 0 + assert receipt['expected']['state']['Balance']['count'] == (initial_balance + 2) * 3 + assert receipt['expected']['state']['Lead']['visits'] == initial_visits + 3 * 2 + assert receipt['expected']['processed_events'] == 2