diff --git a/tools/semi_naive/.gitignore b/tools/semi_naive/.gitignore new file mode 100644 index 00000000..c18dd8d8 --- /dev/null +++ b/tools/semi_naive/.gitignore @@ -0,0 +1 @@ +__pycache__/ diff --git a/tools/semi_naive/NOTES.md b/tools/semi_naive/NOTES.md new file mode 100644 index 00000000..9a86809c --- /dev/null +++ b/tools/semi_naive/NOTES.md @@ -0,0 +1,191 @@ +# MM2 semi-naive encoding notes + +Every semantic decision in the transform is pinned by an executable probe in +`corpus/i0/` and `corpus/i4/`, run against the release binary built from this +tree with `cargo +nightly build --release -p mork --bin mork`. `./target/release/mork test` +exited 0 before the probes ran. Each command below used `--instrumentation 0` and wrote +the final space under `target/semi_naive/`. The checked result for each probe is stored +under `expected/i0/` and `expected/i4/`. + +## Removal and addition sinks + +Command: + +```text +./target/release/mork run tools/semi_naive/corpus/i0/remove_sink.mm2 --instrumentation 0 target/semi_naive/i0/remove_sink.space +``` + +Exact stdout: + +```text +loaded "tools/semi_naive/corpus/i0/remove_sink.mm2" ; running and outputing to Some("target/semi_naive/i0/remove_sink.space") +executing 1 steps took 0 ms (unifications 1, writes 2, transitions 4, max unify 2) +``` + +Exact final space: + +```text +(removed a) +(survivor b) +``` + +Decision: inside an `O` template, `(- pattern)` removes the instantiated pattern and `(+ pattern)` adds it. The transform uses these sinks for destructive bookkeeping transitions. + +## Bare whole-fact match + +Command: + +```text +./target/release/mork run tools/semi_naive/corpus/i0/bare_whole_fact.mm2 --instrumentation 0 target/semi_naive/i0/bare_whole_fact.space +``` + +Exact stdout: + +```text +loaded "tools/semi_naive/corpus/i0/bare_whole_fact.mm2" ; running and outputing to Some("target/semi_naive/i0/bare_whole_fact.space") +executing 1 steps took 0 ms (unifications 1, writes 2, transitions 14, max unify 3) +``` + +Exact final space: + +```text +(cand (fact absent)) +(fact present) +(bare-hit (fact present)) +``` + +The bound bare conjunct `$x` matched the complete `(fact present)` value and did not match the absent value. + +## Wrapped whole-fact match + +Command: + +```text +./target/release/mork run tools/semi_naive/corpus/i0/wrapped_whole_fact.mm2 --instrumentation 0 target/semi_naive/i0/wrapped_whole_fact.space +``` + +Exact stdout: + +```text +loaded "tools/semi_naive/corpus/i0/wrapped_whole_fact.mm2" ; running and outputing to Some("target/semi_naive/i0/wrapped_whole_fact.space") +executing 1 steps took 0 ms (unifications 1, writes 2, transitions 18, max unify 4) +``` + +Exact final space: + +```text +(f (fact present)) +(cand (fact absent)) +(wrapped-hit (fact present)) +``` + +Decision: both tested forms work, but the transform uses `(f fact)` for every source fact and `(f $x)` for existence checks. The fixed outer relation gives every whole-fact query a non-variable prefix and makes projection explicit. + +## Priority order + +Command: + +```text +./target/release/mork run tools/semi_naive/corpus/i0/priority_order.mm2 --instrumentation 0 target/semi_naive/i0/priority_order.space +``` + +Exact stdout: + +```text +loaded "tools/semi_naive/corpus/i0/priority_order.mm2" ; running and outputing to Some("target/semi_naive/i0/priority_order.space") +executing 2 steps took 0 ms (unifications 1, writes 2, transitions 4, max unify 1) +``` + +Exact final space: + +```text +(fired priority-0) +``` + +Decision: priority `0` fires before priority `1`. Priority 0 removed the shared token, so priority 1 observed no match. The phase encoding uses a common structured prefix followed by ordered numeric phase fields. + +## Conditional respawn and quiescence + +Command: + +```text +./target/release/mork run tools/semi_naive/corpus/i0/conditional_respawn.mm2 --instrumentation 0 target/semi_naive/i0/conditional_respawn.space +``` + +Exact stdout: + +```text +loaded "tools/semi_naive/corpus/i0/conditional_respawn.mm2" ; running and outputing to Some("target/semi_naive/i0/conditional_respawn.space") +executing 3 steps took 0 ms (unifications 2, writes 4, transitions 56, max unify 8) +``` + +Exact final space: + +```text +(cleared item) +(worker (, (dc $a)) (O (- (dc $a)) (+ (cleared $a)))) +(controller (, (dc $a) (worker $b $c) (controller $d $e)) (, (exec 0 $b $c) (exec 1 $d $e))) +``` + +The initial controller emitted a priority-0 worker and a priority-1 copy of itself. The worker removed the only `dc` fact. The copied controller was then consumed, found no `dc`, emitted nothing, and execution stopped after three steps. + +Decision: controller and worker definitions remain ordinary facts. A controller matches the current delta before it emits the next phase execs and its own replacement. An empty current delta therefore consumes the last controller without respawning it. + +## Direct phase emission + +The transform embeds every phase `exec` directly in the controller template instead of storing phase definitions as facts. Stored `(phase ...)` definition facts would make the controller match once per phase in every round. The probe deliberately reuses `$x` across two embedded phase statements. Command: + +```text +./target/release/mork run tools/semi_naive/corpus/i4/direct_controller.mm2 --instrumentation 0 target/semi_naive/i4/direct_controller.space +``` + +Exact stdout: + +```text +loaded "tools/semi_naive/corpus/i4/direct_controller.mm2" ; running and outputing to Some("target/semi_naive/i4/direct_controller.space") +executing 5 steps took 0 ms (unifications 4, writes 7, transitions 73, max unify 4) +``` + +Exact final space: + +```text +(left a) +(seed a) +(right a) +``` + +Decision: embed phase statements directly. The probe shows that the two emitted statements remain independently matchable even when their schematic variables originated under one controller template. MORK normalizes each emitted `exec` as an independent fact. The transform canonicalizes each embedded phase into one reusable variable namespace, leaving four variables for the controller's parity, body, and template bindings. A source rule needing more than 60 variables therefore hard-errors as `CONTROLLER_VARIABLE_LIMIT` before the complete controller could exceed MORK's 64-variable form limit. + +## Alternating delta buffers + +Datalog engines implement the semi-naive table update as merge `new` into the full relation, swap `delta` and `new`, and clear `new`; the relevant Soufflé sequence is in [`UnitTranslator.cpp`](https://github.com/souffle-lang/souffle/blob/a1303be3c0166400dee3d1f36f0d96abe03e6901/src/ast2ram/seminaive/UnitTranslator.cpp#L514-L532). MM2 has no constant-time relation swap, so the transform alternates the roles of two delta relations instead. + +The transform wraps full facts as `(f fact)`, seeds `(d0 fact)`, and starts with `(t d0 d1)`. The controller binds the current and next delta relation names from `t`. Each derive variant reads one factor from the bound current relation and its remaining factors from `f`. Difference removes `(c fact)` values already present in `f`. The clear phase removes the current delta and `t`. Promotion writes each surviving candidate directly to `f` and the bound next relation, emits `(t NEXT CURRENT)`, and removes the candidate. A round without a promoted candidate leaves no `t`, so the replacement controller quiesces. + +The tags are `f`, `d0`, `d1`, `c`, `t`, and priority prefix `s`. An earlier encoding kept fixed `dc`/`dn` relations and an advance phase that removed every `dn` fact and reinserted it as `dc`; the role swap deletes that phase, one executed step per round, and two writes per promoted delta fact. Under the fixed-role encoding the transformed 320 + 320 process-calculus run took 8,659 steps, 6,732 unifications, and 19,872 writes; the alternating encoding takes 7,697 steps, 5,451 unifications, and 16,348 writes on identical projections. No counter increased on any measured workload. + +Source priorities remain the second field in derive priorities, so source rule order is preserved inside the derive phase, and a monotonically assigned variant number breaks ties across rules. MORK's set insertion makes duplicate candidates idempotent, while the explicit difference phase determines newness before promotion. + +## Oracle source model + +`driver.py` treats the source `exec` statements as persistent Datalog rules. A pilot reinserts the original rules until two consecutive sorted spaces match. The measured source arm then materializes that many rounds with ordered `(naive round source-priority rule-index)` priorities and runs the materialized program once. Pilot counters are discarded. The reported source counters therefore come from one native `mork run`, as do the transformed counters. + +An exactly self-respawning source rule (one body `exec` handle matching the live rule, one identical emitted handle) instead runs naturally for the step bound recorded in its manifest row, and its comparison projection drops only the remaining live `exec`. A changed self handle refuses as `SELF_MODIFYING_RULE`; a distinct emitted rule refuses as `FOREIGN_EXEC_TEMPLATE`. + +The driver refuses a transformed program containing a bare top-level variable fact with `BARE_TOP_LEVEL_VARIABLE_FACT`, and a unit test regenerates every checked transform and requires exact byte equality with the checked artifact plus the absence of that divergence-class form. + +## Combined ProductZipper and leapfrog oracle + +`driver.py` accepts one or two `--binary` options under `--all`. One option runs the complete oracle through the selected executable. Two options run every case through both executables, compare each source and transformed projection across engines, and require equal steps, unifications, writes, and source rounds. Transitions and engine milliseconds are reported but are not compared, and the leapfrog output's trailing `max unify` counter is accepted without changing the five canonical metrics. ProductZipper source transitions are nonzero while leapfrog source transitions are zero, which confirms that transitions describe the selected engine rather than a cross-engine semantic invariant. + +The one repository case with an engine-specific unification counter is `programs/lens_aunt`: its nine-factor join routes to the leapfrog join under the `leapfrog` feature, so the number of unification attempts is a property of the engine, not the program. Steps, writes, and projections still agree across engines, and each engine's counters are deterministic across repeats. + +## Four-quadrant benchmark runner + +`bench.py` measures the Cartesian product of the naive repeated-evaluation protocol and the transformed single run with ProductZipper and leapfrog. Its default cases are process-calculus 80+80, 160+160, 320+320, and 480+480, plus transitive chains 64, 128, 256, and 384. + +For every repeat, the naive cell starts from the source program, runs one external `mork` process per round, appends the original persistent rules to the preceding output space, and stops when two consecutive sorted projections match. Its engine milliseconds and counters are sums over those processes. Its wall timer includes spawning, loading, dumping, projecting, and re-appending. The transformed cell is one `mork run` to quiescence. + +The four cells rotate their starting position across three interleaved repeats. Steps, unifications, writes, transitions, and rounds must match exactly across repeats. Source/transformed and ProductZipper/leapfrog projections must be byte-identical. Steps, unifications, writes, and rounds must also match across engines; transitions remain engine-specific. The table reports the minimum engine milliseconds and minimum end-to-end protocol wall independently, while the JSON retains every raw repeat and records which repeat supplied each minimum. + +A naive repeat has a 900-second deadline covering the complete external protocol. If it expires, the runner prints `SKIP` with the workload, cell, repeat, deadline, and reason, then records that cell as skipped. Other failures hard-error with a named reason and do not publish a JSON artifact. Each completed JSON records the exact commit, binary paths and SHA-256 hashes, host facts, method, raw samples, selected minima, exact counters, rounds, and projection hashes. diff --git a/tools/semi_naive/README.md b/tools/semi_naive/README.md new file mode 100644 index 00000000..a180eb1d --- /dev/null +++ b/tools/semi_naive/README.md @@ -0,0 +1,206 @@ +# MM2-native semi-naive evaluation + +A source-to-source transform that turns add-only MM2 rule programs into +MM2-native semi-naive loops, plus the oracle, corpus, generators, and +benchmarks that prove the transformed program equivalent and measure what the +transform saves. No engine code changes: everything here is Python over the +`mork` CLI, standard library only. + +Naive repeated evaluation re-derives the whole closure every round. Semi-naive +evaluation restricts each rule application to the facts derived in the previous +round, so every derivation is touched once. The transform expresses that +discipline entirely with existing MM2 machinery: wrapper relations, `O` sinks +for removal, priorities for phase order, and a self-respawning controller for +round choreography. `SPEC.md` is the normative specification of the lowering: +the accepted fragment, the exact emitted statements, and the equivalence +theorem with its conditions. `NOTES.md` holds the executable probes that pin +each piece of kernel semantics the encoding relies on, and the design +decisions built on them. + +## Running it + +```sh +# transform one program +python3 tools/semi_naive/transform.py source.mm2 transformed.mm2 + +# build both engines and put them where the tools look by default +cargo build --release -p mork && cp target/release/mork target/semi_naive/bin-pz +cargo build --release -p mork --features leapfrog && cp target/release/mork target/semi_naive/bin-lf + +# the complete oracle: checked corpus + generated workloads + repository +# programs, each run as source and as transform under both engines +python3 tools/semi_naive/driver.py --all --generate \ + --suite existing --suite repository \ + --binary target/semi_naive/bin-pz --binary target/semi_naive/bin-lf + +# unit tests (transform, driver, generators, bench, analyzer, acceptance sweep) +python3 -m unittest discover -s tools/semi_naive +``` + +With one `--binary`, the driver checks every case against its checked +expectations on that engine alone. With two, it additionally requires +byte-identical projections and equal steps, unifications, writes, and source +rounds across engines. The current gate is `40 cases, 0 failed`: 17 corpus and +generated cases plus the 23 repository programs the transform accepts. + +`bench.py` measures the four-quadrant Cartesian product of protocol and engine, +`repository_bench.py` measures the accepted repository programs, and +`analyze.py` validates a complete benchmark matrix before fitting scaling +exponents. Each records exact counters and rejects any cross-repeat or +cross-engine drift in them. + +## The encoding + +For source facts `fact` and add-only rules `(exec p (, B1 ... Bk) (, H1 ... Hm))`: + +1. Seed `(f fact)` and `(d0 fact)` for every source fact, then add `(t d0 d1)`. +2. The controller binds `CURRENT` and `NEXT` from `t` and emits one derive + variant per body factor of every rule. Exactly one factor reads + `(CURRENT fact)`; the others read `f`. Heads become candidates `(c H)`. +3. Difference: remove `(c fact)` whenever `(f fact)` already exists. +4. Clear: remove the old `CURRENT` facts and the round's `t` marker. +5. Promote: write each surviving candidate to `f` and `NEXT`, emit + `(t NEXT CURRENT)`, and remove the candidate. +6. The controller respawns only when promotion restored `t`, so a round that + promotes nothing quiesces. + +The alternating `d0`/`d1` role swap is the MM2 rendering of the semi-naive +table update in Datalog engines (merge new into full, swap delta and new, +clear new; see Soufflé's +[`UnitTranslator.cpp`](https://github.com/souffle-lang/souffle/blob/a1303be3c0166400dee3d1f36f0d96abe03e6901/src/ast2ram/seminaive/UnitTranslator.cpp#L514-L532)). +MM2 has no constant-time relation swap, so the roles alternate instead. + +Projection erases the bookkeeping (`f`, `d0`, `d1`, `c`, `t`, controller and +phase execs) and recovers the source space. The oracle sorts both spaces and +compares bytes. + +The oracle models source `exec` statements as persistent rules evaluated to a +fixed point, which is the repeated-evaluation discipline the transform targets; +it is not upstream's one-shot `exec` consumption. An exactly self-respawning +rule (its own `exec` handle in body and template, unchanged) is accepted by +stripping the handle; the generated controller supplies the repetition. + +## What it refuses + +The transform either emits the complete supported translation or exits 2 with +`REFUSE REASON`, never a partial output. The boundary, each row covered by a +checked refusal case: + +| Reason | Rejected input | +| :--- | :--- | +| `REMOVAL_TEMPLATE` | Source `O` template containing `(- ...)` | +| `IO_SOURCE` | `I` rule body | +| `IO_SINK` | Source `O` template without a removal | +| `COUNTED_EXEC_HEAD` | `exec` with an extra count or template field | +| `MALFORMED_EXEC` | `exec` missing priority, body, or head | +| `UNCLASSIFIABLE_PATTERN` | Non-list body factor, unsupported variable-headed relation, or reserved relation | +| `UNCLASSIFIABLE_TEMPLATE` | Non-list, dynamic, or reserved head relation | +| `SELF_MODIFYING_RULE` | A self-respawn changes its priority, pattern, or template | +| `FOREIGN_EXEC_TEMPLATE` | A template emits an `exec` other than its exact self-respawn handle | +| `VARIABLE_SOURCE_PRIORITY` | Source priority containing a variable | +| `EMPTY_RULE_BODY` | Comma body without factors | +| `EMPTY_RULE_HEAD` | Comma head without templates | +| `UNBOUND_HEAD_VARIABLE` | Head variable absent from the rule body | +| `TOO_MANY_VARIABLES` | Fact or rule exceeding MORK's 64-variable form limit | +| `CONTROLLER_VARIABLE_LIMIT` | Rule needing more than 60 source variables plus the controller's four bindings | +| `UNCLASSIFIABLE_FACT` | Top-level source value that is not a fixed-head relation | +| `RESERVED_SOURCE_FORM` | Top-level `exec`, `I`, or `O` used as data | +| `NO_RULES` | Program without a transformable rule | +| `PARSE_ERROR` | Malformed S-expression input | + +Sweeping `kernel/resources/*.mm2` and `differential/corpus/**/*.mm2` (103 +programs) accepts 23: `string_convert`, `transitive`, `cross_join_dict`, +`cross_join_tuple`, `lens_aunt`, `lens_composition`, `pattern_mining`, +`stv_roman`, `coref_absorbed_by_data_varref`, `func_type_unification`, +`two_bipolar_equal_crossed`, and twelve of the wiki examples: `mm2_basics_02`, +`mm2_basics_05`, and the reachability programs `p1_13`, `p2_06`, `p2_07`, +`p2_08`, `p3_03`, `p3_04`, `p3_09`, `p3_12`, `p3_18`, and `p4_03`. +`test_acceptance_sweep.py` pins the exact classification of all 103. The +refusals are dominated by rules that respawn modified copies of themselves or +emit other rules, which is control transfer the round controller cannot +absorb yet. Several accepted wiki snippets carry rules without data, so their +persistent fixpoint is empty; they still gate bookkeeping erasure and +first-round quiescence, an edge class the corpus previously lacked. + +## What it saves, measured + +All comparisons are deterministic engine counters from `mork run`; both arms +produce byte-identical sorted projections at every size, and process-calculus +cases additionally pin the required `(petri (! result ...))` fact. The source +arm is the materialized repeated-evaluation schedule; the transformed arm is +one run to quiescence. + +Process calculus (the shape of MORK's process-calculus benchmark, with the +same rule and data shape as persistent rules): + +| Operands | Naive unifications | Transformed unifications | Reduction | +| :--- | ---: | ---: | ---: | +| 80 + 80 | 23,002 | 1,371 | 16.8x | +| 160 + 160 | 90,802 | 2,731 | 33.2x | +| 320 + 320 | 360,802 | 5,451 | 66.2x | +| 480 + 480 | 810,002 | 8,171 | 99.1x | + +Transitive closure over chain graphs: + +| Edges | Naive unifications | Transformed unifications | Reduction | +| ---: | ---: | ---: | ---: | +| 64 | 93,591 | 57,329 | 1.63x | +| 128 | 748,919 | 435,763 | 1.72x | +| 256 | 5,991,735 | 3,392,053 | 1.77x | +| 384 | 24,166,967 | 11,203,319 | 2.16x | + +The reduction grows with size on both families because the naive protocol +re-derives every earlier round's results each round. The savings are +shape-dependent: repository programs that reach their fixed point in one +productive round have nothing for semi-naive evaluation to remove, and the +generated controller adds counters instead (`repository_bench.py` labels +twenty-one of the twenty-three accepted programs neutral-short, the small +transitive resource an overhead case, and the step-bounded `lens_aunt` a +bounded-source case). The transform pays on multi-round recursive workloads. + +### Four-quadrant timing + +Engine milliseconds are the minimum of three interleaved repeats, secondary to +the counters above. Naive cells sum one external process per round, so their +protocol wall also carries process spawn and file round-tripping; transformed +cells are one process. Measured on one shared machine: + +| Instance | Naive PZ | Naive LF | Transformed PZ | Transformed LF | +| :--- | ---: | ---: | ---: | ---: | +| PC 80+80 | 1,432 | 538 | 380 | 68 | +| PC 160+160 | 11,262 | 4,224 | 2,667 | 221 | +| PC 320+320 | 88,800 | 32,601 | 19,590 | 836 | +| PC 480+480 | 303,952 | 109,279 | 66,132 | 1,872 | +| Transitive 64 | 60 | 30 | 46 | 27 | +| Transitive 128 | 499 | 240 | 347 | 180 | +| Transitive 256 | 3,721 | 1,726 | 2,432 | 1,260 | +| Transitive 384 | 15,136 | 7,355 | 8,129 | 4,332 | + +The two optimizations act on separate costs and compose: semi-naive evaluation +removes cross-round re-derivation, and the leapfrog join removes per-candidate +byte re-walks inside each round's phase joins. At 320 + 320 the composed path +(naive ProductZipper to transformed leapfrog) is 88.8 s to 0.84 s on engine +timers; the transform alone on ProductZipper is 4.5x, and the transform alone +on leapfrog is 39.0x. At 480 + 480 the composed path is 304.0 s to 1.87 s. + +Over the full 80-to-480 matrix, transformed leapfrog transitions fit a log-log +exponent of 1.985 (R^2 0.999997) against a projection-byte exponent of 1.985: +the combined evaluator's work grows at the same rate as the serialized output +it must produce, which has an n^2 floor because the result holds order-n facts +whose Peano terms are order-n bytes. Transformed ProductZipper transitions fit +exponent 2.914 on the same runs. On the transitive family the leapfrog +exponent is 2.023 against a byte exponent of 1.993. `analyze.py` recomputes +these fits from the benchmark JSON artifacts and revalidates every projection +before fitting. + +## Notes for the engine + +Two engine-side observations from building this, recorded here because the +transform deliberately changes no engine code: + +- An insertion sink that reports whether it added a new fact would delete the + entire difference phase: newness is the only thing the `(c fact)` round-trip + computes. +- `transform_multi_multi_o` reserves a `1 << 32` byte buffer for each `O` + firing (`kernel/src/space.rs`), which bounds how cheap a bookkeeping-only + firing can be. diff --git a/tools/semi_naive/SPEC.md b/tools/semi_naive/SPEC.md new file mode 100644 index 00000000..55fd0a50 --- /dev/null +++ b/tools/semi_naive/SPEC.md @@ -0,0 +1,198 @@ +# Specification: lowering add-only MM2 rules into semi-naive rounds + +This document defines the lowering precisely: the accepted input fragment, the +exact statements the lowering emits, the round semantics they implement, the +equivalence theorem that justifies the whole construction, and the conditions +that theorem needs. `transform.py` is the reference implementation of this +specification; `driver.py` is its executable acceptance gate. The +specification is implementation-agnostic: a sink or a compiler pass emitting +the same statements satisfies it identically, and the oracle gates it +unchanged. + +## 1. Accepted fragment + +A source program is a sequence of top-level expressions, each either a fact or +a rule. + +A fact is a list expression whose head is a fixed atom that is not one of the +reserved atoms below. Non-list facts, facts headed by a variable, and facts +headed by a reserved atom are refused. + +A rule is a four-field exec statement + +``` +(exec p (, B1 ... Bk) (, H1 ... Hm)) k >= 1, m >= 1 +``` + +where `p` is a variable-free priority expression, every body factor `Bi` and +every head `Hj` is a list expression headed by a fixed, non-reserved atom, and +every variable occurring in a head also occurs in the body. A rule may +additionally be an exact self-respawn: one body factor is an exec handle that +matches the rule itself, and exactly one emitted head is that same handle, +unchanged. The lowering strips the pair and treats the remainder as the rule; +the generated controller supplies the repetition the self-respawn expressed. A +self-respawn that alters its priority, pattern, or template is refused +(`SELF_MODIFYING_RULE`), and a template emitting any other exec is refused +(`FOREIGN_EXEC_TEMPLATE`). + +Reserved atoms: `f`, `d0`, `d1`, `c`, `t`, `s` as relation heads, and `exec`, +`I`, `O` as top-level data. Programs using them where the lowering needs them +fresh are refused. The complete refusal table in README.md is the normative +applicability boundary; everything not accepted by this section is refused +with a named reason and no output. + +The source semantics this lowering targets is repeated evaluation: the rules +are treated as persistent and applied to a fixed point, as in Datalog. It does +not model one-shot exec consumption; a rule that should fire once is outside +the fragment. + +## 2. The emitted program + +Write CUR and NXT for the two delta-parity variables. The lowering emits, in +order: + +1. For every source fact `a`: `(f a)`. +2. For every source fact `a`: `(d0 a)`. +3. The initial turn marker: `(t d0 d1)`. +4. One controller statement, defined in section 4, whose template embeds the + phase statements of section 3. + +Phase priorities share the fixed shape `(s PHASE SRC UNIQ)`. `PHASE` is the +round phase, `0` through `4`. `SRC` is the source rule's priority expression, +preserved verbatim, in derive priorities and `0` elsewhere. `UNIQ` is a +tie-breaking atom (the reference implementation uses rule index times 10^6 +plus variant index); its only obligation is uniqueness. The encoding relies on +exactly one ordering property: the engine fires all pending phase-`i` execs +before any phase-`j` exec with `i < j`. Order inside one phase is immaterial +to the result, because within a phase all effects are insertions into or +removals from disjoint fact sets (section 5, C4). + +## 3. Phase statements + +For source rule `r` with priority `p`, factors `B1 ... Bk`, heads +`H1 ... Hm`, and for each variant `j` in `1..k`: + +``` +(exec (s 0 p UNIQ) (, (f B1) ... (CUR Bj) ... (f Bk)) (, (c H1) ... (c Hm))) +``` + +Factor order is preserved; factor `j` reads the current delta, every other +factor reads `f`. These are the derive variants: their union over `j` derives +every consequence with at least one premise in the current delta. + +The bookkeeping phases, with `$x` a fresh variable: + +``` +difference (exec (s 1 0 0) (, (c $x) (f $x)) (O (- (c $x)))) +clear delta (exec (s 2 0 0) (, (CUR $x)) (O (- (CUR $x)))) +clear turn (exec (s 2 0 1) (, (t CUR NXT)) (O (- (t CUR NXT)))) +promote (exec (s 3 0 0) (, (c $x)) + (O (+ (f $x)) (+ (NXT $x)) (+ (t NXT CUR)) (- (c $x)))) +``` + +Difference removes every candidate already known. Promotion moves each +survivor into `f` and into the next delta, re-creates the turn marker with the +parities swapped, and consumes the candidate. Set semantics makes the repeated +`(t NXT CUR)` insertions one fact. + +## 4. The controller + +Every phase statement above is embedded literally in the controller's +template, with its variables canonicalized into one shared namespace in which +CUR and NXT are the two distinguished parity variables. The controller is + +``` +(exec (s 4 0 0) + (, (t CUR NXT) (exec (s 4 0 0) $pat $tpl)) + (, PHASE1 ... PHASEn (exec (s 4 0 0) $pat $tpl))) +``` + +Its body binds the parities from the live turn marker and binds its own +statement through the generic handle `(exec (s 4 0 0) $pat $tpl)`. Firing it +therefore instantiates and emits every phase exec for one round with the +current parity assignment, plus its own replacement. The replacement fires +after the round's phases. If promotion restored a turn marker, the next round +begins with the parities swapped; if no candidate survived, no turn marker +exists, the replacement matches nothing, is consumed, and the program +quiesces. + +Emitted execs are independent facts, so one round's phase statements do not +interfere with the next round's. The canonicalized controller must stay within +MORK's 64-variable form limit; the reference implementation reserves four +variables (two parities, pattern, template) and refuses a source rule needing +more than 60 (`CONTROLLER_VARIABLE_LIMIT`). + +## 5. Round semantics and the equivalence theorem + +Let `S0` be the source fact set and `T` the immediate-consequence operator of +the rules: `T(S)` is the set of instantiated heads over bindings whose every +factor matches in `S`. The two evaluations are + +``` +naive F(0) = S0 F(n+1) = F(n) ∪ T(F(n)) +semi-naive G(0) = S0, D(0) = S0 + C(n+1) = TD(G(n), D(n)) candidates, phase 0 + D(n+1) = C(n+1) \ G(n) difference, phase 1 + G(n+1) = G(n) ∪ D(n+1) promotion, phase 3 +``` + +where `TD(S, D)` is the union over variants `j` of derivations reading factor +`j` from `D` and every other factor from `S`. + +Theorem 1 (round equivalence). For every `n`, `G(n) = F(n)`. + +Theorem 2 (quiescence). If `D(n+1)` is empty then `T(F(n)) ⊆ F(n)`: the naive +fixed point is reached, and the controller's stop is exact. + +The proof of Theorem 1 is the classical semi-naive argument (Bancilhon 1986; +Bancilhon-Maier-Sagiv-Ullman, PODS 1986) by induction with the invariant that +round `n+1` captures every immediate consequence of `F(n)`. The inclusion +`G(n+1) ⊆ F(n+1)` holds because every delta-restricted derivation is a +derivation. For the converse, take any derivation from `F(n) = G(n) = +G(n-1) ∪ D(n)`. Either every premise lies in `G(n-1)`, in which case the fact +was already captured at round `n`, or some premise lies in `D(n)`, in which +case the variant restricting that factor derives it into `C(n+1)`, and the +difference and promotion phases place it in `G(n+1)` whether or not it was +already known. The base round uses `D(0) = G(0)`, which covers every +derivation only because every rule has at least one body factor; `k >= 1` is +the `EMPTY_RULE_BODY` refusal, not a convention. + +The theorem transfers to the emitted program under four conditions, each +pinned by the encoding: + +- C1, set semantics: insertion is idempotent, so duplicate candidates and the + repeated turn-marker insertions collapse. This is MORK's native space + semantics. +- C2, add-only: no source rule removes facts, so `T` is monotone and the + accumulation never retracts. Removal templates are refused. +- C3, phase separation: all candidates of a round exist before difference + runs, difference completes before promotion, and the old delta is cleared + before the swapped marker exists. The `PHASE` field's dominance in priority + order is exactly this condition. +- C4, within-phase order freedom: derive variants only insert candidates, + difference only removes candidates present in `f`, promotion handles each + candidate independently. All are set operations whose result is independent + of firing order inside the phase, so the `SRC` and `UNIQ` fields never + affect the final space. + +## 6. Projection and the acceptance gate + +The projection of a transformed space is the set of `x` with `(f x)` in the +space; every `d0`, `d1`, `c`, `t` fact and every `(exec (s ...) ...)` +statement is bookkeeping and is erased. Correctness of an implementation of +this specification means: for every accepted program, the sorted projection of +the transformed run at quiescence is byte-identical to the sorted final space +of the source's repeated evaluation, with equal step, unification, and write +counters across engines where those are engine-invariant. `driver.py --all` +checks precisely this over the corpus, the generated workload families, and +the accepted repository programs, under both join engines. + +## 7. Non-goals + +The lowering does not implement newness detection inside the engine (the +difference phase exists only because insertion does not report it), does not +cover I/O, removal, or counted exec forms, and does not choose whether a +workload benefits: programs reaching their fixed point in one productive +round pay the controller overhead for no saving, as the repository +measurements in README.md show. Those boundaries are deliberate scope, stated +so that an engine-side implementation can widen them knowingly. diff --git a/tools/semi_naive/analyze.py b/tools/semi_naive/analyze.py new file mode 100755 index 00000000..ce9f04f3 --- /dev/null +++ b/tools/semi_naive/analyze.py @@ -0,0 +1,416 @@ +#!/usr/bin/env python3 +"""Validate and analyze the complete semi-naive four-quadrant benchmark.""" + +import argparse +import json +import math +import os +import statistics +import sys +import tempfile + +import bench + + +EXPECTED_CASES = { + (workload, size) + for workload, sizes in bench.WORKLOAD_SIZES.items() + for size in sizes +} +EXPECTED_CELLS = { + (workload, size, protocol, engine) + for workload, size in EXPECTED_CASES + for protocol in bench.PROTOCOL_ORDER + for engine in bench.ENGINE_ORDER +} +ROW_COUNTER_FIELDS = bench.COUNTER_FIELDS + ("rounds",) + + +class AnalysisRefusal(ValueError): + pass + + +def refuse(reason, detail=None): + if detail is None: + raise AnalysisRefusal(reason) + raise AnalysisRefusal("%s: %s" % (reason, detail)) + + +def read_artifact(path): + try: + with open(path, "r", encoding="utf-8") as stream: + value = json.load(stream) + except (OSError, json.JSONDecodeError) as error: + refuse("ARTIFACT_READ_FAILED", "%s: %s" % (path, error)) + if not isinstance(value, dict): + refuse("ARTIFACT_NOT_OBJECT", path) + return value + + +def binary_hashes(artifact, path): + binaries = artifact.get("binaries") + if not isinstance(binaries, dict) or set(binaries) != set(bench.ENGINE_ORDER): + refuse("ARTIFACT_REQUIRES_BOTH_ENGINES", path) + hashes = {} + for engine in bench.ENGINE_ORDER: + metadata = binaries.get(engine) + digest = metadata.get("sha256") if isinstance(metadata, dict) else None + if not isinstance(digest, str) or len(digest) != 64: + refuse("INVALID_BINARY_SHA256", "%s %s" % (path, engine)) + hashes[engine] = digest + if hashes["pz"] == hashes["lf"]: + refuse("ENGINE_BINARIES_IDENTICAL", path) + return hashes + + +def validate_sample(row, sample, expected_repeat, context): + if not isinstance(sample, dict): + refuse("INVALID_SAMPLE", context) + if sample.get("repeat") != expected_repeat: + refuse("INVALID_REPEAT_INDEX", context) + for field in ROW_COUNTER_FIELDS: + if sample.get(field) != row.get(field): + refuse( + "NONDETERMINISTIC_COUNTERS", + "%s %s sample=%r row=%r" + % (context, field, sample.get(field), row.get(field)), + ) + for field in ("engine_ms", "wall_ns"): + value = sample.get(field) + if not isinstance(value, int) or value < 0: + refuse("INVALID_SAMPLE_TIMER", "%s %s" % (context, field)) + + +def validate_row(row, repeats, context): + if not isinstance(row, dict): + refuse("INVALID_RESULT_ROW", context) + if row.get("status") != "measured": + refuse( + "UNMEASURED_CELL", + "%s: %s" % (context, row.get("reason", row.get("status"))), + ) + key = tuple(row.get(field) for field in ("workload", "size", "protocol", "engine")) + if key not in EXPECTED_CELLS: + refuse("UNEXPECTED_CELL", "%s: %r" % (context, key)) + if row.get("protocol_label") != bench.protocol_label(row["protocol"]): + refuse("INVALID_PROTOCOL_LABEL", context) + for field in ROW_COUNTER_FIELDS: + value = row.get(field) + if not isinstance(value, int) or value < 0: + refuse("INVALID_COUNTER", "%s %s" % (context, field)) + for field in ("projection_bytes", "projection_lines"): + value = row.get(field) + if not isinstance(value, int) or value <= 0: + refuse("INVALID_PROJECTION_SIZE", "%s %s" % (context, field)) + projection_hash = row.get("projection_sha256") + if not isinstance(projection_hash, str) or len(projection_hash) != 64: + refuse("INVALID_PROJECTION_SHA256", context) + + samples = row.get("samples") + if not isinstance(samples, list) or len(samples) != repeats: + refuse( + "INCOMPLETE_REPEATS", + "%s: %r != %d" + % (context, len(samples) if isinstance(samples, list) else None, repeats), + ) + for repeat, sample in enumerate(samples, 1): + validate_sample(row, sample, repeat, context) + if row.get("engine_ms") != min(sample["engine_ms"] for sample in samples): + refuse("ENGINE_MS_NOT_MINIMUM", context) + if row.get("wall_ns") != min(sample["wall_ns"] for sample in samples): + refuse("WALL_NOT_MINIMUM", context) + if not math.isclose( + row.get("wall_ms", math.nan), + row["wall_ns"] / 1_000_000, + rel_tol=0, + abs_tol=1e-9, + ): + refuse("WALL_MS_MISMATCH", context) + return key + + +def load_and_validate(paths): + if not paths: + refuse("NO_ARTIFACTS") + rows = {} + expected_hashes = None + sources = [] + for path in paths: + absolute = os.path.abspath(path) + artifact = read_artifact(absolute) + if artifact.get("schema") != 1: + refuse("UNSUPPORTED_BENCHMARK_SCHEMA", absolute) + if artifact.get("resolved") is not True: + refuse("UNRESOLVED_BENCHMARK", absolute) + if artifact.get("all_measured") is not True: + refuse("BENCHMARK_HAS_SKIPS", absolute) + methodology = artifact.get("methodology") + if not isinstance(methodology, dict) or methodology.get("repeats") != 3: + refuse("BENCHMARK_REQUIRES_MIN_OF_3", absolute) + hashes = binary_hashes(artifact, absolute) + if expected_hashes is None: + expected_hashes = hashes + elif hashes != expected_hashes: + refuse("MIXED_BINARY_HASHES", absolute) + artifact_rows = artifact.get("results") + if not isinstance(artifact_rows, list): + refuse("INVALID_RESULTS", absolute) + for index, row in enumerate(artifact_rows): + context = "%s result %d" % (absolute, index + 1) + key = validate_row(row, 3, context) + if key in rows: + refuse("DUPLICATE_CELL", "%r" % (key,)) + rows[key] = row + sources.append( + { + "path": absolute, + "sha256": bench.sha256_file(absolute), + "git_head": artifact.get("git_head"), + } + ) + + observed = set(rows) + if observed != EXPECTED_CELLS: + missing = sorted(EXPECTED_CELLS - observed) + extra = sorted(observed - EXPECTED_CELLS) + refuse("INCOMPLETE_MATRIX", "missing=%r extra=%r" % (missing, extra)) + validate_case_agreement(rows) + return rows, expected_hashes, sources + + +def validate_case_agreement(rows): + for workload, size in sorted(EXPECTED_CASES): + case_rows = [ + rows[(workload, size, protocol, engine)] + for protocol in bench.PROTOCOL_ORDER + for engine in bench.ENGINE_ORDER + ] + projection = { + (row["projection_sha256"], row["projection_bytes"], row["projection_lines"]) + for row in case_rows + } + if len(projection) != 1: + refuse("CROSS_CELL_PROJECTION_MISMATCH", "%s %d" % (workload, size)) + for protocol in bench.PROTOCOL_ORDER: + left = rows[(workload, size, protocol, "pz")] + right = rows[(workload, size, protocol, "lf")] + for field in bench.CROSS_ENGINE_FIELDS: + if left[field] != right[field]: + refuse( + "CROSS_ENGINE_COUNTER_MISMATCH", + "%s %d %s %s" % (workload, size, protocol, field), + ) + + +def power_fit(points): + if len(points) < 2 or any(x <= 0 or y <= 0 for x, y in points): + refuse("POWER_FIT_REQUIRES_POSITIVE_POINTS", repr(points)) + xs = [math.log(x) for x, _ in points] + ys = [math.log(y) for _, y in points] + fit = statistics.linear_regression(xs, ys) + correlation = statistics.correlation(xs, ys) + return { + "exponent": fit.slope, + "coefficient": math.exp(fit.intercept), + "r_squared": correlation * correlation, + } + + +def adjacent_growth(points): + growth = [] + for (left_size, left_value), (right_size, right_value) in zip(points, points[1:]): + raw = right_value / left_value + size_ratio = right_size / left_size + growth.append( + { + "from_size": left_size, + "to_size": right_size, + "size_ratio": size_ratio, + "raw_ratio": raw, + "per_doubling": raw ** (math.log(2) / math.log(size_ratio)), + } + ) + return growth + + +def ratio(numerator, denominator, label): + if denominator <= 0: + refuse("NONPOSITIVE_RATIO_DENOMINATOR", label) + return numerator / denominator + + +def analyze(rows, binary_hashes, sources): + scaling = {} + projection_scaling = {} + for workload in bench.WORKLOAD_ORDER: + sizes = bench.WORKLOAD_SIZES[workload] + scaling[workload] = {} + for engine in bench.ENGINE_ORDER: + points = [ + ( + size, + rows[(workload, size, "transformed", engine)]["transitions"], + ) + for size in sizes + ] + scaling[workload][engine] = { + "points": [ + {"size": size, "transitions": transitions} + for size, transitions in points + ], + "fit": power_fit(points), + "adjacent_growth": adjacent_growth(points), + } + projection_points = [ + ( + size, + rows[(workload, size, "transformed", "pz")]["projection_bytes"], + ) + for size in sizes + ] + projection_scaling[workload] = { + "points": [ + {"size": size, "bytes": projection_bytes} + for size, projection_bytes in projection_points + ], + "fit": power_fit(projection_points), + } + + case = "process_calculus", 320 + naive_pz = rows[case + ("naive", "pz")]["engine_ms"] + naive_lf = rows[case + ("naive", "lf")]["engine_ms"] + transformed_pz = rows[case + ("transformed", "pz")]["engine_ms"] + transformed_lf = rows[case + ("transformed", "lf")]["engine_ms"] + composition = { + "workload": case[0], + "size": case[1], + "engine_ms": { + "naive_pz": naive_pz, + "naive_lf": naive_lf, + "transformed_pz": transformed_pz, + "transformed_lf": transformed_lf, + }, + "ratios": { + "stock_to_combined": ratio(naive_pz, transformed_lf, "stock_to_combined"), + "same_lf_naive_to_transformed": ratio( + naive_lf, transformed_lf, "same_lf_naive_to_transformed" + ), + "same_pz_naive_to_transformed": ratio( + naive_pz, transformed_pz, "same_pz_naive_to_transformed" + ), + "transformed_pz_to_lf": ratio( + transformed_pz, transformed_lf, "transformed_pz_to_lf" + ), + }, + } + return { + "schema": 1, + "benchmark_sources": sources, + "binary_sha256": binary_hashes, + "validation": { + "cells": len(rows), + "cases": len(EXPECTED_CASES), + "all_measured": True, + "cross_cell_projection_agreement": True, + "cross_engine_counter_agreement": [ + "steps", + "unifications", + "writes", + "rounds", + ], + }, + "scaling": scaling, + "projection_scaling": projection_scaling, + "composition_at_process_calculus_320": composition, + } + + +def render_analysis(analysis): + lines = [ + "VALIDATED %d cells across %d cases; all projections agree" + % ( + analysis["validation"]["cells"], + analysis["validation"]["cases"], + ) + ] + for workload in bench.WORKLOAD_ORDER: + for engine in bench.ENGINE_ORDER: + data = analysis["scaling"][workload][engine] + growth = ", ".join( + "%d->%d %.6fx" + % (item["from_size"], item["to_size"], item["per_doubling"]) + for item in data["adjacent_growth"] + ) + lines.append( + "%s transformed %s transitions: exponent=%.6f R^2=%.9f; " + "per-doubling=%s" + % ( + workload, + engine.upper(), + data["fit"]["exponent"], + data["fit"]["r_squared"], + growth, + ) + ) + projection = analysis["projection_scaling"][workload]["fit"] + lines.append( + "%s projection bytes: exponent=%.6f R^2=%.9f" + % (workload, projection["exponent"], projection["r_squared"]) + ) + composition = analysis["composition_at_process_calculus_320"] + lines.append( + "process_calculus 320+320 engine-ms ratios: stock-to-combined=%.6fx; " + "same-LF-naive-to-transformed=%.6fx; same-PZ-naive-to-transformed=%.6fx; " + "transformed-PZ-to-LF=%.6fx" + % ( + composition["ratios"]["stock_to_combined"], + composition["ratios"]["same_lf_naive_to_transformed"], + composition["ratios"]["same_pz_naive_to_transformed"], + composition["ratios"]["transformed_pz_to_lf"], + ) + ) + return "\n".join(lines) + "\n" + + +def atomic_write_text(path, content): + directory = os.path.dirname(os.path.abspath(path)) + os.makedirs(directory, exist_ok=True) + descriptor, temporary = tempfile.mkstemp( + prefix=".semi-naive-analysis-", suffix=".txt", dir=directory + ) + try: + with os.fdopen(descriptor, "w", encoding="utf-8", newline="\n") as stream: + stream.write(content) + os.replace(temporary, path) + except BaseException: + try: + os.unlink(temporary) + except FileNotFoundError: + pass + raise + + +def main(): + parser = argparse.ArgumentParser(description=__doc__) + parser.add_argument("artifacts", nargs="+") + parser.add_argument("--json", dest="json_path") + parser.add_argument("--text", dest="text_path") + args = parser.parse_args() + + try: + rows, hashes, sources = load_and_validate(args.artifacts) + analysis = analyze(rows, hashes, sources) + rendered = render_analysis(analysis) + if args.json_path: + bench.atomic_write_json(args.json_path, analysis) + if args.text_path: + atomic_write_text(args.text_path, rendered) + sys.stdout.write(rendered) + except (AnalysisRefusal, RuntimeError) as error: + print("ERROR: %s" % error, file=sys.stderr) + return 2 + return 0 + + +if __name__ == "__main__": + raise SystemExit(main()) diff --git a/tools/semi_naive/bench.py b/tools/semi_naive/bench.py new file mode 100755 index 00000000..b7dfc1a4 --- /dev/null +++ b/tools/semi_naive/bench.py @@ -0,0 +1,640 @@ +#!/usr/bin/env python3 +"""Benchmark naive and transformed MM2 under ProductZipper and leapfrog.""" + +import argparse +import datetime +import hashlib +import json +import math +import os +import platform +import subprocess +import sys +import tempfile +import time + + +HERE = os.path.dirname(os.path.abspath(__file__)) +REPO = os.path.dirname(os.path.dirname(HERE)) +sys.path.insert(0, HERE) +import driver # noqa: E402 + +gen_process_calculus = driver.gen_process_calculus +gen_transitive = driver.gen_transitive + + +DEFAULT_PZ_BINARY = os.path.join(REPO, "target", "semi_naive", "bin-pz") +DEFAULT_LF_BINARY = os.path.join(REPO, "target", "semi_naive", "bin-lf") +DEFAULT_JSON = os.path.join(REPO, "target", "semi_naive", "semi-naive-four-quadrant.json") +DEFAULT_REPEATS = 3 +DEFAULT_NAIVE_TIMEOUT_SECONDS = 15 * 60 +DEFAULT_MAX_SOURCE_ROUNDS = 2048 + +WORKLOAD_SIZES = { + "process_calculus": (80, 160, 320, 480), + "transitive": (64, 128, 256, 384), +} +WORKLOAD_ORDER = tuple(WORKLOAD_SIZES) +PROTOCOL_ORDER = ("naive", "transformed") +ENGINE_ORDER = ("pz", "lf") +COUNTER_FIELDS = ("steps", "unifications", "writes", "transitions") +CROSS_ENGINE_FIELDS = ("steps", "unifications", "writes", "rounds") + + +class BenchmarkRefusal(ValueError): + pass + + +def positive_integer(value): + parsed = int(value) + if parsed <= 0: + raise argparse.ArgumentTypeError("value must be positive") + return parsed + + +def positive_float(value): + parsed = float(value) + if not math.isfinite(parsed) or parsed <= 0: + raise argparse.ArgumentTypeError("value must be positive") + return parsed + + +def unique(values, reason): + if len(values) != len(set(values)): + raise BenchmarkRefusal(reason) + return values + + +def case_specs(workloads, sizes): + workloads = unique(list(workloads or WORKLOAD_ORDER), "DUPLICATE_WORKLOAD") + if sizes is not None: + sizes = unique(list(sizes), "DUPLICATE_SIZE") + if len(workloads) != 1: + raise BenchmarkRefusal("SIZES_REQUIRE_ONE_WORKLOAD") + return [(workloads[0], size) for size in sizes] + return [ + (workload, size) + for workload in workloads + for size in WORKLOAD_SIZES[workload] + ] + + +def cell_specs(protocols, engines): + protocols = unique(list(protocols or PROTOCOL_ORDER), "DUPLICATE_PROTOCOL") + engines = unique(list(engines or ENGINE_ORDER), "DUPLICATE_ENGINE") + return [ + (protocol, engine) + for protocol in PROTOCOL_ORDER + if protocol in protocols + for engine in ENGINE_ORDER + if engine in engines + ] + + +def interleaved_schedule(cells, repeats): + if not cells: + raise BenchmarkRefusal("NO_BENCHMARK_CELLS") + for repeat in range(repeats): + offset = repeat % len(cells) + for index in range(len(cells)): + yield repeat, cells[(offset + index) % len(cells)] + + +def sha256_file(path): + digest = hashlib.sha256() + with open(path, "rb") as stream: + while True: + chunk = stream.read(1024 * 1024) + if not chunk: + return digest.hexdigest() + digest.update(chunk) + + +def validate_binaries(binaries, engines): + selected = {engine: os.path.abspath(binaries[engine]) for engine in engines} + for engine, binary in selected.items(): + if not os.access(binary, os.X_OK): + raise BenchmarkRefusal( + "BINARY_NOT_EXECUTABLE: %s=%s" % (engine, binary) + ) + if set(selected) == set(ENGINE_ORDER): + if os.path.samefile(selected["pz"], selected["lf"]): + raise BenchmarkRefusal("ENGINE_BINARIES_SAME_FILE") + if sha256_file(selected["pz"]) == sha256_file(selected["lf"]): + raise BenchmarkRefusal("ENGINE_BINARIES_IDENTICAL") + return selected + + +def generate_case(root, workload, size): + source_root = os.path.join(root, "source") + if workload == "process_calculus": + source = gen_process_calculus.generate(source_root, ((size, size),))[0] + instance = "%d+%d" % (size, size) + required = source[: -len(".source.mm2")] + ".required" + elif workload == "transitive": + source = gen_transitive.generate(source_root, (size,))[0] + instance = str(size) + required = None + else: + raise BenchmarkRefusal("UNSUPPORTED_WORKLOAD: %s" % workload) + + transformed = os.path.join(root, "transformed.mm2") + driver.transform_program(source, transformed) + driver.assert_no_bare_top_level_variable_facts(transformed) + return { + "workload": workload, + "size": size, + "instance": instance, + "source": source, + "transformed": transformed, + "required": required, + } + + +def sample_from_result(result, projection, wall_ns, rounds): + sample = {field: result[field] for field in COUNTER_FIELDS} + sample.update( + { + "engine_ms": result["milliseconds"], + "wall_ns": wall_ns, + "rounds": rounds, + "projection": projection, + } + ) + return sample + + +def run_naive_once(binary, case, workdir, steps, max_rounds, timeout_seconds): + started = time.perf_counter_ns() + deadline_ns = started + int(timeout_seconds * 1_000_000_000) + result = driver.run_source_protocol( + binary, + case["source"], + workdir, + steps, + max_rounds, + deadline_ns=deadline_ns, + ) + wall_ns = time.perf_counter_ns() - started + if wall_ns > int(timeout_seconds * 1_000_000_000): + raise subprocess.TimeoutExpired("repeated-evaluation protocol", timeout_seconds) + return sample_from_result( + result, + result["projection"], + wall_ns, + result["rounds"], + ) + + +def run_transformed_once(binary, case, workdir, steps): + started = time.perf_counter_ns() + result = driver.run_program( + binary, + case["transformed"], + os.path.join(workdir, "transformed.space"), + steps, + ) + wall_ns = time.perf_counter_ns() - started + projection = driver.sorted_projection(result["dump"], transformed=True) + return sample_from_result(result, projection, wall_ns, 1) + + +def run_cell_once( + protocol, + binary, + case, + workdir, + steps, + max_rounds, + naive_timeout_seconds, +): + if protocol == "naive": + return run_naive_once( + binary, + case, + workdir, + steps, + max_rounds, + naive_timeout_seconds, + ) + if protocol == "transformed": + return run_transformed_once(binary, case, workdir, steps) + raise BenchmarkRefusal("UNSUPPORTED_PROTOCOL: %s" % protocol) + + +def counter_bytes(sample): + fields = COUNTER_FIELDS + ("rounds",) + return "\n".join( + "%s=%d" % (field, sample[field]) for field in fields + ).encode("ascii") + + +def verify_projection(case, reference, sample, context): + projection = sample["projection"] + if case["required"] is not None: + with open(case["required"], "rb") as stream: + required = set(stream.read().splitlines()) + missing = sorted(required - set(projection.splitlines())) + if missing: + raise RuntimeError( + "REQUIRED_PROJECTION_MISSING: %s: %r" % (context, missing[0]) + ) + if reference is None: + return projection + if projection != reference: + line, expected, actual = driver.first_difference(reference, projection) + raise RuntimeError( + "CROSS_CELL_PROJECTION_MISMATCH: %s line %d: %r != %r" + % (context, line, expected, actual) + ) + return reference + + +def verify_counter_repeat(samples, sample, context): + if samples and counter_bytes(samples[0]) != counter_bytes(sample): + raise RuntimeError( + "NONDETERMINISTIC_COUNTERS: %s: %r != %r" + % (context, counter_bytes(samples[0]), counter_bytes(sample)) + ) + + +def public_sample(sample, repeat): + return { + "repeat": repeat + 1, + **{field: sample[field] for field in COUNTER_FIELDS}, + "rounds": sample["rounds"], + "engine_ms": sample["engine_ms"], + "wall_ns": sample["wall_ns"], + "wall_ms": sample["wall_ns"] / 1_000_000, + } + + +def completed_row(case, protocol, engine, samples, repeats): + if len(samples) != repeats: + raise RuntimeError( + "INCOMPLETE_REPEATS: %s %s %s: %d != %d" + % (case["workload"], case["instance"], protocol, len(samples), repeats) + ) + first = samples[0] + wall_index = min( + range(len(samples)), key=lambda index: samples[index]["wall_ns"] + ) + engine_index = min( + range(len(samples)), key=lambda index: samples[index]["engine_ms"] + ) + return { + "workload": case["workload"], + "size": case["size"], + "instance": case["instance"], + "protocol": protocol, + "protocol_label": protocol_label(protocol), + "engine": engine, + "status": "measured", + **{field: first[field] for field in COUNTER_FIELDS}, + "rounds": first["rounds"], + "engine_ms": samples[engine_index]["engine_ms"], + "wall_ns": samples[wall_index]["wall_ns"], + "wall_ms": samples[wall_index]["wall_ns"] / 1_000_000, + "selected_engine_repeat": engine_index + 1, + "selected_wall_repeat": wall_index + 1, + "projection_bytes": len(first["projection"]), + "projection_lines": first["projection"].count(b"\n"), + "projection_sha256": hashlib.sha256(first["projection"]).hexdigest(), + "samples": [ + public_sample(sample, repeat) + for repeat, sample in enumerate(samples) + ], + } + + +def skipped_row(case, protocol, engine, reason): + return { + "workload": case["workload"], + "size": case["size"], + "instance": case["instance"], + "protocol": protocol, + "protocol_label": protocol_label(protocol), + "engine": engine, + "status": "skipped", + "reason": reason, + "samples": [], + } + + +def verify_cross_engine_counters(rows): + by_cell = {(row["protocol"], row["engine"]): row for row in rows} + for protocol in PROTOCOL_ORDER: + left = by_cell.get((protocol, "pz")) + right = by_cell.get((protocol, "lf")) + if left is None or right is None: + continue + if left["status"] != "measured" or right["status"] != "measured": + continue + for field in CROSS_ENGINE_FIELDS: + if left[field] != right[field]: + raise RuntimeError( + "CROSS_ENGINE_COUNTER_MISMATCH: %s %s: pz %s=%d, lf %s=%d" + % ( + left["workload"], + left["instance"], + field, + left[field], + field, + right[field], + ) + ) + + +def benchmark_case( + case, + cells, + binaries, + repeats, + steps, + max_rounds, + naive_timeout_seconds, + work_root, +): + samples = {cell: [] for cell in cells} + skipped = {} + projection = None + for repeat, (protocol, engine) in interleaved_schedule(cells, repeats): + cell = (protocol, engine) + if cell in skipped: + continue + context = "%s %s %s %s repeat %d" % ( + case["workload"], + case["instance"], + protocol_label(protocol), + engine.upper(), + repeat + 1, + ) + print("RUN %s" % context, flush=True) + with tempfile.TemporaryDirectory( + prefix="%s-%s-%02d-" % (protocol, engine, repeat + 1), + dir=work_root, + ) as workdir: + try: + sample = run_cell_once( + protocol, + binaries[engine], + case, + workdir, + steps, + max_rounds, + naive_timeout_seconds, + ) + except subprocess.TimeoutExpired: + if protocol != "naive": + raise + reason = ( + "repeated-evaluation protocol exceeded %g seconds in repeat %d" + % (naive_timeout_seconds, repeat + 1) + ) + samples[cell] = [] + skipped[cell] = reason + print("SKIP %s: %s" % (context, reason), flush=True) + continue + + projection = verify_projection(case, projection, sample, context) + verify_counter_repeat(samples[cell], sample, context) + samples[cell].append(sample) + print( + "OK %s steps=%d unifications=%d writes=%d transitions=%d " + "engine_ms=%d wall_ms=%.3f rounds=%d" + % ( + context, + sample["steps"], + sample["unifications"], + sample["writes"], + sample["transitions"], + sample["engine_ms"], + sample["wall_ns"] / 1_000_000, + sample["rounds"], + ), + flush=True, + ) + + rows = [] + for protocol, engine in cells: + cell = (protocol, engine) + if cell in skipped: + rows.append(skipped_row(case, protocol, engine, skipped[cell])) + else: + rows.append( + completed_row(case, protocol, engine, samples[cell], repeats) + ) + verify_cross_engine_counters(rows) + return rows + + +def protocol_label(protocol): + if protocol == "naive": + return "naive repeated-evaluation protocol" + if protocol == "transformed": + return "transformed single run" + raise BenchmarkRefusal("UNSUPPORTED_PROTOCOL: %s" % protocol) + + +def format_integer(value): + return "-" if value is None else format(value, ",d") + + +def render_table(rows, repeats): + lines = [ + "| Workload | Instance | Protocol | Engine | Rounds | Steps | " + "Unifications | Writes | Transitions | Engine ms min-of-%d | " + "Protocol wall ms min-of-%d |" % (repeats, repeats), + "| :--- | :--- | :--- | :--- | ---: | ---: | ---: | ---: | ---: | ---: | ---: |", + ] + for row in rows: + if row["status"] == "skipped": + values = ["-"] * 7 + protocol = "%s; SKIPPED: %s" % ( + row["protocol_label"], + row["reason"], + ) + else: + values = [ + format_integer(row["rounds"]), + format_integer(row["steps"]), + format_integer(row["unifications"]), + format_integer(row["writes"]), + format_integer(row["transitions"]), + format_integer(row["engine_ms"]), + "%.3f" % row["wall_ms"], + ] + protocol = row["protocol_label"] + lines.append( + "| %s | %s | %s | %s | %s |" + % ( + row["workload"], + row["instance"], + protocol, + row["engine"].upper(), + " | ".join(values), + ) + ) + return "\n".join(lines) + "\n" + + +def atomic_write_json(path, value): + directory = os.path.dirname(os.path.abspath(path)) + os.makedirs(directory, exist_ok=True) + descriptor, temporary = tempfile.mkstemp( + prefix=".semi-naive-bench-", suffix=".json", dir=directory + ) + try: + with os.fdopen(descriptor, "w", encoding="utf-8", newline="\n") as stream: + json.dump(value, stream, indent=2, sort_keys=True) + stream.write("\n") + os.replace(temporary, path) + except BaseException: + try: + os.unlink(temporary) + except FileNotFoundError: + pass + raise + + +def git_head(): + completed = subprocess.run( + ["git", "rev-parse", "HEAD"], + cwd=REPO, + stdout=subprocess.PIPE, + stderr=subprocess.PIPE, + check=False, + text=True, + ) + if completed.returncode != 0: + raise RuntimeError( + "GIT_HEAD_UNAVAILABLE: %s" % completed.stderr.strip() + ) + return completed.stdout.strip() + + +def artifact(rows, binaries, repeats, timeout_seconds, max_rounds, steps): + all_measured = all(row["status"] == "measured" for row in rows) + return { + "schema": 1, + "resolved": True, + "all_measured": all_measured, + "generated_at_utc": datetime.datetime.now( + datetime.timezone.utc + ).isoformat(), + "git_head": git_head(), + "host": { + "platform": platform.platform(), + "machine": platform.machine(), + "python": platform.python_version(), + "logical_cpus": os.cpu_count(), + "load_average_at_write": os.getloadavg(), + }, + "binaries": { + engine: { + "path": binary, + "sha256": sha256_file(binary), + } + for engine, binary in binaries.items() + }, + "methodology": { + "repeats": repeats, + "schedule": "rotated interleaving by repeat within each case", + "wall_estimator": "minimum end-to-end wall across repeats", + "engine_ms": "minimum engine timer across repeats", + "counters": "steps, unifications, writes, and transitions must be byte-stable across repeats", + "naive": "external repeated-evaluation fixed-point protocol; engine_ms is summed across rounds", + "transformed": "one mork run to quiescence per repeat", + "naive_timeout_seconds_per_repeat": timeout_seconds, + "max_source_rounds": max_rounds, + "step_limit_per_mork_run": steps, + "binary_build": "RUSTFLAGS='-C target-cpu=native -Awarnings -C link-arg=-fuse-ld=mold' cargo +nightly build --release -p mork --bin mork", + }, + "results": rows, + } + + +def main(): + parser = argparse.ArgumentParser(description=__doc__) + parser.add_argument("--pz-binary", default=DEFAULT_PZ_BINARY) + parser.add_argument("--lf-binary", default=DEFAULT_LF_BINARY) + parser.add_argument( + "--workload", action="append", choices=WORKLOAD_ORDER, dest="workloads" + ) + parser.add_argument("--size", action="append", type=positive_integer, dest="sizes") + parser.add_argument( + "--protocol", action="append", choices=PROTOCOL_ORDER, dest="protocols" + ) + parser.add_argument( + "--engine", action="append", choices=ENGINE_ORDER, dest="engines" + ) + parser.add_argument("--repeats", type=positive_integer, default=DEFAULT_REPEATS) + parser.add_argument( + "--naive-timeout-seconds", + type=positive_float, + default=DEFAULT_NAIVE_TIMEOUT_SECONDS, + ) + parser.add_argument( + "--max-source-rounds", + type=positive_integer, + default=DEFAULT_MAX_SOURCE_ROUNDS, + ) + parser.add_argument("--steps", type=positive_integer, default=driver.DEFAULT_STEPS) + parser.add_argument("--json", default=DEFAULT_JSON) + args = parser.parse_args() + + try: + specs = case_specs(args.workloads, args.sizes) + cells = cell_specs(args.protocols, args.engines) + selected_engines = unique( + [engine for engine in ENGINE_ORDER if any(cell[1] == engine for cell in cells)], + "DUPLICATE_ENGINE", + ) + binaries = validate_binaries( + {"pz": args.pz_binary, "lf": args.lf_binary}, selected_engines + ) + + temp_root = os.path.join(REPO, "target", "semi_naive") + os.makedirs(temp_root, exist_ok=True) + rows = [] + with tempfile.TemporaryDirectory( + prefix="semi-naive-bench-", dir=temp_root + ) as benchmark_root: + for workload, size in specs: + case_root = os.path.join( + benchmark_root, "%s-%d" % (workload, size) + ) + os.makedirs(case_root) + case = generate_case(case_root, workload, size) + rows.extend( + benchmark_case( + case, + cells, + binaries, + args.repeats, + args.steps, + args.max_source_rounds, + args.naive_timeout_seconds, + case_root, + ) + ) + + result = artifact( + rows, + binaries, + args.repeats, + args.naive_timeout_seconds, + args.max_source_rounds, + args.steps, + ) + atomic_write_json(args.json, result) + print(render_table(rows, args.repeats), end="") + print("WROTE %s" % os.path.relpath(args.json, REPO)) + return 0 + except (BenchmarkRefusal, OSError, RuntimeError, subprocess.SubprocessError) as error: + print("ERROR: %s" % error, file=sys.stderr) + return 2 + + +if __name__ == "__main__": + sys.exit(main()) diff --git a/tools/semi_naive/corpus/i0/bare_whole_fact.mm2 b/tools/semi_naive/corpus/i0/bare_whole_fact.mm2 new file mode 100644 index 00000000..6fcb4cc8 --- /dev/null +++ b/tools/semi_naive/corpus/i0/bare_whole_fact.mm2 @@ -0,0 +1,10 @@ +; Test a bound bare variable as a whole-fact conjunct. + +(fact present) +(cand (fact present)) +(cand (fact absent)) + +(exec 0 + (, (cand $x) $x) + (O (- (cand $x)) + (+ (bare-hit $x)))) diff --git a/tools/semi_naive/corpus/i0/conditional_respawn.mm2 b/tools/semi_naive/corpus/i0/conditional_respawn.mm2 new file mode 100644 index 00000000..7124b7d1 --- /dev/null +++ b/tools/semi_naive/corpus/i0/conditional_respawn.mm2 @@ -0,0 +1,20 @@ +; A controller respawns only while `dc` exists. Its worker clears `dc`. + +(dc item) + +(worker + (, (dc $x)) + (O (- (dc $x)) + (+ (cleared $x)))) + +(controller + (, (dc $any) (worker $worker-pattern $worker-template) + (controller $controller-pattern $controller-template)) + (, (exec 0 $worker-pattern $worker-template) + (exec 1 $controller-pattern $controller-template))) + +(exec 1 + (, (dc $any) (worker $worker-pattern $worker-template) + (controller $controller-pattern $controller-template)) + (, (exec 0 $worker-pattern $worker-template) + (exec 1 $controller-pattern $controller-template))) diff --git a/tools/semi_naive/corpus/i0/priority_order.mm2 b/tools/semi_naive/corpus/i0/priority_order.mm2 new file mode 100644 index 00000000..029df80c --- /dev/null +++ b/tools/semi_naive/corpus/i0/priority_order.mm2 @@ -0,0 +1,12 @@ +; Priority 0 must consume the token before priority 1 can observe it. + +(token) + +(exec 0 + (, (token)) + (O (- (token)) + (+ (fired priority-0)))) + +(exec 1 + (, (token)) + (, (fired priority-1))) diff --git a/tools/semi_naive/corpus/i0/remove_sink.mm2 b/tools/semi_naive/corpus/i0/remove_sink.mm2 new file mode 100644 index 00000000..b79f9358 --- /dev/null +++ b/tools/semi_naive/corpus/i0/remove_sink.mm2 @@ -0,0 +1,9 @@ +; Pin `O` removal and addition dispatch. + +(victim a) +(survivor b) + +(exec 0 + (, (victim $x)) + (O (- (victim $x)) + (+ (removed $x)))) diff --git a/tools/semi_naive/corpus/i0/wrapped_whole_fact.mm2 b/tools/semi_naive/corpus/i0/wrapped_whole_fact.mm2 new file mode 100644 index 00000000..e7f3583e --- /dev/null +++ b/tools/semi_naive/corpus/i0/wrapped_whole_fact.mm2 @@ -0,0 +1,10 @@ +; Test a bound payload inside a fixed whole-fact wrapper. + +(f (fact present)) +(cand (fact present)) +(cand (fact absent)) + +(exec 0 + (, (cand $x) (f $x)) + (O (- (cand $x)) + (+ (wrapped-hit $x)))) diff --git a/tools/semi_naive/corpus/i1/transitive_chain_004.source.mm2 b/tools/semi_naive/corpus/i1/transitive_chain_004.source.mm2 new file mode 100644 index 00000000..d877f1dc --- /dev/null +++ b/tools/semi_naive/corpus/i1/transitive_chain_004.source.mm2 @@ -0,0 +1,10 @@ +; Four-edge chain and one two-factor transitive-closure rule. + +(edge n000 n001) +(edge n001 n002) +(edge n002 n003) +(edge n003 n004) + +(exec 0 + (, (edge $x $y) (edge $y $z)) + (, (edge $x $z))) diff --git a/tools/semi_naive/corpus/i1/transitive_chain_004.transformed.mm2 b/tools/semi_naive/corpus/i1/transitive_chain_004.transformed.mm2 new file mode 100644 index 00000000..983b26fe --- /dev/null +++ b/tools/semi_naive/corpus/i1/transitive_chain_004.transformed.mm2 @@ -0,0 +1,10 @@ +(f (edge n000 n001)) +(f (edge n001 n002)) +(f (edge n002 n003)) +(f (edge n003 n004)) +(d0 (edge n000 n001)) +(d0 (edge n001 n002)) +(d0 (edge n002 n003)) +(d0 (edge n003 n004)) +(t d0 d1) +(exec (s 4 0 0) (, (t $sn_phase_0 $sn_phase_1) (exec (s 4 0 0) $sn_controller_pattern $sn_controller_template)) (, (exec (s 0 0 0) (, ($sn_phase_0 (edge $sn_phase_2 $sn_phase_3)) (f (edge $sn_phase_3 $sn_phase_4))) (, (c (edge $sn_phase_2 $sn_phase_4)))) (exec (s 0 0 1) (, (f (edge $sn_phase_2 $sn_phase_3)) ($sn_phase_0 (edge $sn_phase_3 $sn_phase_4))) (, (c (edge $sn_phase_2 $sn_phase_4)))) (exec (s 1 0 0) (, (c $sn_phase_2) (f $sn_phase_2)) (O (- (c $sn_phase_2)))) (exec (s 2 0 0) (, ($sn_phase_0 $sn_phase_2)) (O (- ($sn_phase_0 $sn_phase_2)))) (exec (s 2 0 1) (, (t $sn_phase_0 $sn_phase_1)) (O (- (t $sn_phase_0 $sn_phase_1)))) (exec (s 3 0 0) (, (c $sn_phase_2)) (O (+ (f $sn_phase_2)) (+ ($sn_phase_1 $sn_phase_2)) (+ (t $sn_phase_1 $sn_phase_0)) (- (c $sn_phase_2)))) (exec (s 4 0 0) $sn_controller_pattern $sn_controller_template))) diff --git a/tools/semi_naive/corpus/i1/transitive_chain_032.source.mm2 b/tools/semi_naive/corpus/i1/transitive_chain_032.source.mm2 new file mode 100644 index 00000000..c7a5a346 --- /dev/null +++ b/tools/semi_naive/corpus/i1/transitive_chain_032.source.mm2 @@ -0,0 +1,38 @@ +; 32-edge chain and one two-factor transitive-closure rule. + +(edge n000 n001) +(edge n001 n002) +(edge n002 n003) +(edge n003 n004) +(edge n004 n005) +(edge n005 n006) +(edge n006 n007) +(edge n007 n008) +(edge n008 n009) +(edge n009 n010) +(edge n010 n011) +(edge n011 n012) +(edge n012 n013) +(edge n013 n014) +(edge n014 n015) +(edge n015 n016) +(edge n016 n017) +(edge n017 n018) +(edge n018 n019) +(edge n019 n020) +(edge n020 n021) +(edge n021 n022) +(edge n022 n023) +(edge n023 n024) +(edge n024 n025) +(edge n025 n026) +(edge n026 n027) +(edge n027 n028) +(edge n028 n029) +(edge n029 n030) +(edge n030 n031) +(edge n031 n032) + +(exec 0 + (, (edge $x $y) (edge $y $z)) + (, (edge $x $z))) diff --git a/tools/semi_naive/corpus/i1/transitive_chain_032.transformed.mm2 b/tools/semi_naive/corpus/i1/transitive_chain_032.transformed.mm2 new file mode 100644 index 00000000..1c309584 --- /dev/null +++ b/tools/semi_naive/corpus/i1/transitive_chain_032.transformed.mm2 @@ -0,0 +1,66 @@ +(f (edge n000 n001)) +(f (edge n001 n002)) +(f (edge n002 n003)) +(f (edge n003 n004)) +(f (edge n004 n005)) +(f (edge n005 n006)) +(f (edge n006 n007)) +(f (edge n007 n008)) +(f (edge n008 n009)) +(f (edge n009 n010)) +(f (edge n010 n011)) +(f (edge n011 n012)) +(f (edge n012 n013)) +(f (edge n013 n014)) +(f (edge n014 n015)) +(f (edge n015 n016)) +(f (edge n016 n017)) +(f (edge n017 n018)) +(f (edge n018 n019)) +(f (edge n019 n020)) +(f (edge n020 n021)) +(f (edge n021 n022)) +(f (edge n022 n023)) +(f (edge n023 n024)) +(f (edge n024 n025)) +(f (edge n025 n026)) +(f (edge n026 n027)) +(f (edge n027 n028)) +(f (edge n028 n029)) +(f (edge n029 n030)) +(f (edge n030 n031)) +(f (edge n031 n032)) +(d0 (edge n000 n001)) +(d0 (edge n001 n002)) +(d0 (edge n002 n003)) +(d0 (edge n003 n004)) +(d0 (edge n004 n005)) +(d0 (edge n005 n006)) +(d0 (edge n006 n007)) +(d0 (edge n007 n008)) +(d0 (edge n008 n009)) +(d0 (edge n009 n010)) +(d0 (edge n010 n011)) +(d0 (edge n011 n012)) +(d0 (edge n012 n013)) +(d0 (edge n013 n014)) +(d0 (edge n014 n015)) +(d0 (edge n015 n016)) +(d0 (edge n016 n017)) +(d0 (edge n017 n018)) +(d0 (edge n018 n019)) +(d0 (edge n019 n020)) +(d0 (edge n020 n021)) +(d0 (edge n021 n022)) +(d0 (edge n022 n023)) +(d0 (edge n023 n024)) +(d0 (edge n024 n025)) +(d0 (edge n025 n026)) +(d0 (edge n026 n027)) +(d0 (edge n027 n028)) +(d0 (edge n028 n029)) +(d0 (edge n029 n030)) +(d0 (edge n030 n031)) +(d0 (edge n031 n032)) +(t d0 d1) +(exec (s 4 0 0) (, (t $sn_phase_0 $sn_phase_1) (exec (s 4 0 0) $sn_controller_pattern $sn_controller_template)) (, (exec (s 0 0 0) (, ($sn_phase_0 (edge $sn_phase_2 $sn_phase_3)) (f (edge $sn_phase_3 $sn_phase_4))) (, (c (edge $sn_phase_2 $sn_phase_4)))) (exec (s 0 0 1) (, (f (edge $sn_phase_2 $sn_phase_3)) ($sn_phase_0 (edge $sn_phase_3 $sn_phase_4))) (, (c (edge $sn_phase_2 $sn_phase_4)))) (exec (s 1 0 0) (, (c $sn_phase_2) (f $sn_phase_2)) (O (- (c $sn_phase_2)))) (exec (s 2 0 0) (, ($sn_phase_0 $sn_phase_2)) (O (- ($sn_phase_0 $sn_phase_2)))) (exec (s 2 0 1) (, (t $sn_phase_0 $sn_phase_1)) (O (- (t $sn_phase_0 $sn_phase_1)))) (exec (s 3 0 0) (, (c $sn_phase_2)) (O (+ (f $sn_phase_2)) (+ ($sn_phase_1 $sn_phase_2)) (+ (t $sn_phase_1 $sn_phase_0)) (- (c $sn_phase_2)))) (exec (s 4 0 0) $sn_controller_pattern $sn_controller_template))) diff --git a/tools/semi_naive/corpus/i1/transitive_chain_064.source.mm2 b/tools/semi_naive/corpus/i1/transitive_chain_064.source.mm2 new file mode 100644 index 00000000..1513ccda --- /dev/null +++ b/tools/semi_naive/corpus/i1/transitive_chain_064.source.mm2 @@ -0,0 +1,70 @@ +; 64-edge chain and one two-factor transitive-closure rule. + +(edge n000 n001) +(edge n001 n002) +(edge n002 n003) +(edge n003 n004) +(edge n004 n005) +(edge n005 n006) +(edge n006 n007) +(edge n007 n008) +(edge n008 n009) +(edge n009 n010) +(edge n010 n011) +(edge n011 n012) +(edge n012 n013) +(edge n013 n014) +(edge n014 n015) +(edge n015 n016) +(edge n016 n017) +(edge n017 n018) +(edge n018 n019) +(edge n019 n020) +(edge n020 n021) +(edge n021 n022) +(edge n022 n023) +(edge n023 n024) +(edge n024 n025) +(edge n025 n026) +(edge n026 n027) +(edge n027 n028) +(edge n028 n029) +(edge n029 n030) +(edge n030 n031) +(edge n031 n032) +(edge n032 n033) +(edge n033 n034) +(edge n034 n035) +(edge n035 n036) +(edge n036 n037) +(edge n037 n038) +(edge n038 n039) +(edge n039 n040) +(edge n040 n041) +(edge n041 n042) +(edge n042 n043) +(edge n043 n044) +(edge n044 n045) +(edge n045 n046) +(edge n046 n047) +(edge n047 n048) +(edge n048 n049) +(edge n049 n050) +(edge n050 n051) +(edge n051 n052) +(edge n052 n053) +(edge n053 n054) +(edge n054 n055) +(edge n055 n056) +(edge n056 n057) +(edge n057 n058) +(edge n058 n059) +(edge n059 n060) +(edge n060 n061) +(edge n061 n062) +(edge n062 n063) +(edge n063 n064) + +(exec 0 + (, (edge $x $y) (edge $y $z)) + (, (edge $x $z))) diff --git a/tools/semi_naive/corpus/i1/transitive_chain_064.transformed.mm2 b/tools/semi_naive/corpus/i1/transitive_chain_064.transformed.mm2 new file mode 100644 index 00000000..eb2b64f8 --- /dev/null +++ b/tools/semi_naive/corpus/i1/transitive_chain_064.transformed.mm2 @@ -0,0 +1,130 @@ +(f (edge n000 n001)) +(f (edge n001 n002)) +(f (edge n002 n003)) +(f (edge n003 n004)) +(f (edge n004 n005)) +(f (edge n005 n006)) +(f (edge n006 n007)) +(f (edge n007 n008)) +(f (edge n008 n009)) +(f (edge n009 n010)) +(f (edge n010 n011)) +(f (edge n011 n012)) +(f (edge n012 n013)) +(f (edge n013 n014)) +(f (edge n014 n015)) +(f (edge n015 n016)) +(f (edge n016 n017)) +(f (edge n017 n018)) +(f (edge n018 n019)) +(f (edge n019 n020)) +(f (edge n020 n021)) +(f (edge n021 n022)) +(f (edge n022 n023)) +(f (edge n023 n024)) +(f (edge n024 n025)) +(f (edge n025 n026)) +(f (edge n026 n027)) +(f (edge n027 n028)) +(f (edge n028 n029)) +(f (edge n029 n030)) +(f (edge n030 n031)) +(f (edge n031 n032)) +(f (edge n032 n033)) +(f (edge n033 n034)) +(f (edge n034 n035)) +(f (edge n035 n036)) +(f (edge n036 n037)) +(f (edge n037 n038)) +(f (edge n038 n039)) +(f (edge n039 n040)) +(f (edge n040 n041)) +(f (edge n041 n042)) +(f (edge n042 n043)) +(f (edge n043 n044)) +(f (edge n044 n045)) +(f (edge n045 n046)) +(f (edge n046 n047)) +(f (edge n047 n048)) +(f (edge n048 n049)) +(f (edge n049 n050)) +(f (edge n050 n051)) +(f (edge n051 n052)) +(f (edge n052 n053)) +(f (edge n053 n054)) +(f (edge n054 n055)) +(f (edge n055 n056)) +(f (edge n056 n057)) +(f (edge n057 n058)) +(f (edge n058 n059)) +(f (edge n059 n060)) +(f (edge n060 n061)) +(f (edge n061 n062)) +(f (edge n062 n063)) +(f (edge n063 n064)) +(d0 (edge n000 n001)) +(d0 (edge n001 n002)) +(d0 (edge n002 n003)) +(d0 (edge n003 n004)) +(d0 (edge n004 n005)) +(d0 (edge n005 n006)) +(d0 (edge n006 n007)) +(d0 (edge n007 n008)) +(d0 (edge n008 n009)) +(d0 (edge n009 n010)) +(d0 (edge n010 n011)) +(d0 (edge n011 n012)) +(d0 (edge n012 n013)) +(d0 (edge n013 n014)) +(d0 (edge n014 n015)) +(d0 (edge n015 n016)) +(d0 (edge n016 n017)) +(d0 (edge n017 n018)) +(d0 (edge n018 n019)) +(d0 (edge n019 n020)) +(d0 (edge n020 n021)) +(d0 (edge n021 n022)) +(d0 (edge n022 n023)) +(d0 (edge n023 n024)) +(d0 (edge n024 n025)) +(d0 (edge n025 n026)) +(d0 (edge n026 n027)) +(d0 (edge n027 n028)) +(d0 (edge n028 n029)) +(d0 (edge n029 n030)) +(d0 (edge n030 n031)) +(d0 (edge n031 n032)) +(d0 (edge n032 n033)) +(d0 (edge n033 n034)) +(d0 (edge n034 n035)) +(d0 (edge n035 n036)) +(d0 (edge n036 n037)) +(d0 (edge n037 n038)) +(d0 (edge n038 n039)) +(d0 (edge n039 n040)) +(d0 (edge n040 n041)) +(d0 (edge n041 n042)) +(d0 (edge n042 n043)) +(d0 (edge n043 n044)) +(d0 (edge n044 n045)) +(d0 (edge n045 n046)) +(d0 (edge n046 n047)) +(d0 (edge n047 n048)) +(d0 (edge n048 n049)) +(d0 (edge n049 n050)) +(d0 (edge n050 n051)) +(d0 (edge n051 n052)) +(d0 (edge n052 n053)) +(d0 (edge n053 n054)) +(d0 (edge n054 n055)) +(d0 (edge n055 n056)) +(d0 (edge n056 n057)) +(d0 (edge n057 n058)) +(d0 (edge n058 n059)) +(d0 (edge n059 n060)) +(d0 (edge n060 n061)) +(d0 (edge n061 n062)) +(d0 (edge n062 n063)) +(d0 (edge n063 n064)) +(t d0 d1) +(exec (s 4 0 0) (, (t $sn_phase_0 $sn_phase_1) (exec (s 4 0 0) $sn_controller_pattern $sn_controller_template)) (, (exec (s 0 0 0) (, ($sn_phase_0 (edge $sn_phase_2 $sn_phase_3)) (f (edge $sn_phase_3 $sn_phase_4))) (, (c (edge $sn_phase_2 $sn_phase_4)))) (exec (s 0 0 1) (, (f (edge $sn_phase_2 $sn_phase_3)) ($sn_phase_0 (edge $sn_phase_3 $sn_phase_4))) (, (c (edge $sn_phase_2 $sn_phase_4)))) (exec (s 1 0 0) (, (c $sn_phase_2) (f $sn_phase_2)) (O (- (c $sn_phase_2)))) (exec (s 2 0 0) (, ($sn_phase_0 $sn_phase_2)) (O (- ($sn_phase_0 $sn_phase_2)))) (exec (s 2 0 1) (, (t $sn_phase_0 $sn_phase_1)) (O (- (t $sn_phase_0 $sn_phase_1)))) (exec (s 3 0 0) (, (c $sn_phase_2)) (O (+ (f $sn_phase_2)) (+ ($sn_phase_1 $sn_phase_2)) (+ (t $sn_phase_1 $sn_phase_0)) (- (c $sn_phase_2)))) (exec (s 4 0 0) $sn_controller_pattern $sn_controller_template))) diff --git a/tools/semi_naive/corpus/i1/transitive_chain_128.source.mm2 b/tools/semi_naive/corpus/i1/transitive_chain_128.source.mm2 new file mode 100644 index 00000000..df49f612 --- /dev/null +++ b/tools/semi_naive/corpus/i1/transitive_chain_128.source.mm2 @@ -0,0 +1,134 @@ +; 128-edge chain and one two-factor transitive-closure rule. + +(edge n000 n001) +(edge n001 n002) +(edge n002 n003) +(edge n003 n004) +(edge n004 n005) +(edge n005 n006) +(edge n006 n007) +(edge n007 n008) +(edge n008 n009) +(edge n009 n010) +(edge n010 n011) +(edge n011 n012) +(edge n012 n013) +(edge n013 n014) +(edge n014 n015) +(edge n015 n016) +(edge n016 n017) +(edge n017 n018) +(edge n018 n019) +(edge n019 n020) +(edge n020 n021) +(edge n021 n022) +(edge n022 n023) +(edge n023 n024) +(edge n024 n025) +(edge n025 n026) +(edge n026 n027) +(edge n027 n028) +(edge n028 n029) +(edge n029 n030) +(edge n030 n031) +(edge n031 n032) +(edge n032 n033) +(edge n033 n034) +(edge n034 n035) +(edge n035 n036) +(edge n036 n037) +(edge n037 n038) +(edge n038 n039) +(edge n039 n040) +(edge n040 n041) +(edge n041 n042) +(edge n042 n043) +(edge n043 n044) +(edge n044 n045) +(edge n045 n046) +(edge n046 n047) +(edge n047 n048) +(edge n048 n049) +(edge n049 n050) +(edge n050 n051) +(edge n051 n052) +(edge n052 n053) +(edge n053 n054) +(edge n054 n055) +(edge n055 n056) +(edge n056 n057) +(edge n057 n058) +(edge n058 n059) +(edge n059 n060) +(edge n060 n061) +(edge n061 n062) +(edge n062 n063) +(edge n063 n064) +(edge n064 n065) +(edge n065 n066) +(edge n066 n067) +(edge n067 n068) +(edge n068 n069) +(edge n069 n070) +(edge n070 n071) +(edge n071 n072) +(edge n072 n073) +(edge n073 n074) +(edge n074 n075) +(edge n075 n076) +(edge n076 n077) +(edge n077 n078) +(edge n078 n079) +(edge n079 n080) +(edge n080 n081) +(edge n081 n082) +(edge n082 n083) +(edge n083 n084) +(edge n084 n085) +(edge n085 n086) +(edge n086 n087) +(edge n087 n088) +(edge n088 n089) +(edge n089 n090) +(edge n090 n091) +(edge n091 n092) +(edge n092 n093) +(edge n093 n094) +(edge n094 n095) +(edge n095 n096) +(edge n096 n097) +(edge n097 n098) +(edge n098 n099) +(edge n099 n100) +(edge n100 n101) +(edge n101 n102) +(edge n102 n103) +(edge n103 n104) +(edge n104 n105) +(edge n105 n106) +(edge n106 n107) +(edge n107 n108) +(edge n108 n109) +(edge n109 n110) +(edge n110 n111) +(edge n111 n112) +(edge n112 n113) +(edge n113 n114) +(edge n114 n115) +(edge n115 n116) +(edge n116 n117) +(edge n117 n118) +(edge n118 n119) +(edge n119 n120) +(edge n120 n121) +(edge n121 n122) +(edge n122 n123) +(edge n123 n124) +(edge n124 n125) +(edge n125 n126) +(edge n126 n127) +(edge n127 n128) + +(exec 0 + (, (edge $x $y) (edge $y $z)) + (, (edge $x $z))) diff --git a/tools/semi_naive/corpus/i1/transitive_chain_128.transformed.mm2 b/tools/semi_naive/corpus/i1/transitive_chain_128.transformed.mm2 new file mode 100644 index 00000000..bb58480e --- /dev/null +++ b/tools/semi_naive/corpus/i1/transitive_chain_128.transformed.mm2 @@ -0,0 +1,258 @@ +(f (edge n000 n001)) +(f (edge n001 n002)) +(f (edge n002 n003)) +(f (edge n003 n004)) +(f (edge n004 n005)) +(f (edge n005 n006)) +(f (edge n006 n007)) +(f (edge n007 n008)) +(f (edge n008 n009)) +(f (edge n009 n010)) +(f (edge n010 n011)) +(f (edge n011 n012)) +(f (edge n012 n013)) +(f (edge n013 n014)) +(f (edge n014 n015)) +(f (edge n015 n016)) +(f (edge n016 n017)) +(f (edge n017 n018)) +(f (edge n018 n019)) +(f (edge n019 n020)) +(f (edge n020 n021)) +(f (edge n021 n022)) +(f (edge n022 n023)) +(f (edge n023 n024)) +(f (edge n024 n025)) +(f (edge n025 n026)) +(f (edge n026 n027)) +(f (edge n027 n028)) +(f (edge n028 n029)) +(f (edge n029 n030)) +(f (edge n030 n031)) +(f (edge n031 n032)) +(f (edge n032 n033)) +(f (edge n033 n034)) +(f (edge n034 n035)) +(f (edge n035 n036)) +(f (edge n036 n037)) +(f (edge n037 n038)) +(f (edge n038 n039)) +(f (edge n039 n040)) +(f (edge n040 n041)) +(f (edge n041 n042)) +(f (edge n042 n043)) +(f (edge n043 n044)) +(f (edge n044 n045)) +(f (edge n045 n046)) +(f (edge n046 n047)) +(f (edge n047 n048)) +(f (edge n048 n049)) +(f (edge n049 n050)) +(f (edge n050 n051)) +(f (edge n051 n052)) +(f (edge n052 n053)) +(f (edge n053 n054)) +(f (edge n054 n055)) +(f (edge n055 n056)) +(f (edge n056 n057)) +(f (edge n057 n058)) +(f (edge n058 n059)) +(f (edge n059 n060)) +(f (edge n060 n061)) +(f (edge n061 n062)) +(f (edge n062 n063)) +(f (edge n063 n064)) +(f (edge n064 n065)) +(f (edge n065 n066)) +(f (edge n066 n067)) +(f (edge n067 n068)) +(f (edge n068 n069)) +(f (edge n069 n070)) +(f (edge n070 n071)) +(f (edge n071 n072)) +(f (edge n072 n073)) +(f (edge n073 n074)) +(f (edge n074 n075)) +(f (edge n075 n076)) +(f (edge n076 n077)) +(f (edge n077 n078)) +(f (edge n078 n079)) +(f (edge n079 n080)) +(f (edge n080 n081)) +(f (edge n081 n082)) +(f (edge n082 n083)) +(f (edge n083 n084)) +(f (edge n084 n085)) +(f (edge n085 n086)) +(f (edge n086 n087)) +(f (edge n087 n088)) +(f (edge n088 n089)) +(f (edge n089 n090)) +(f (edge n090 n091)) +(f (edge n091 n092)) +(f (edge n092 n093)) +(f (edge n093 n094)) +(f (edge n094 n095)) +(f (edge n095 n096)) +(f (edge n096 n097)) +(f (edge n097 n098)) +(f (edge n098 n099)) +(f (edge n099 n100)) +(f (edge n100 n101)) +(f (edge n101 n102)) +(f (edge n102 n103)) +(f (edge n103 n104)) +(f (edge n104 n105)) +(f (edge n105 n106)) +(f (edge n106 n107)) +(f (edge n107 n108)) +(f (edge n108 n109)) +(f (edge n109 n110)) +(f (edge n110 n111)) +(f (edge n111 n112)) +(f (edge n112 n113)) +(f (edge n113 n114)) +(f (edge n114 n115)) +(f (edge n115 n116)) +(f (edge n116 n117)) +(f (edge n117 n118)) +(f (edge n118 n119)) +(f (edge n119 n120)) +(f (edge n120 n121)) +(f (edge n121 n122)) +(f (edge n122 n123)) +(f (edge n123 n124)) +(f (edge n124 n125)) +(f (edge n125 n126)) +(f (edge n126 n127)) +(f (edge n127 n128)) +(d0 (edge n000 n001)) +(d0 (edge n001 n002)) +(d0 (edge n002 n003)) +(d0 (edge n003 n004)) +(d0 (edge n004 n005)) +(d0 (edge n005 n006)) +(d0 (edge n006 n007)) +(d0 (edge n007 n008)) +(d0 (edge n008 n009)) +(d0 (edge n009 n010)) +(d0 (edge n010 n011)) +(d0 (edge n011 n012)) +(d0 (edge n012 n013)) +(d0 (edge n013 n014)) +(d0 (edge n014 n015)) +(d0 (edge n015 n016)) +(d0 (edge n016 n017)) +(d0 (edge n017 n018)) +(d0 (edge n018 n019)) +(d0 (edge n019 n020)) +(d0 (edge n020 n021)) +(d0 (edge n021 n022)) +(d0 (edge n022 n023)) +(d0 (edge n023 n024)) +(d0 (edge n024 n025)) +(d0 (edge n025 n026)) +(d0 (edge n026 n027)) +(d0 (edge n027 n028)) +(d0 (edge n028 n029)) +(d0 (edge n029 n030)) +(d0 (edge n030 n031)) +(d0 (edge n031 n032)) +(d0 (edge n032 n033)) +(d0 (edge n033 n034)) +(d0 (edge n034 n035)) +(d0 (edge n035 n036)) +(d0 (edge n036 n037)) +(d0 (edge n037 n038)) +(d0 (edge n038 n039)) +(d0 (edge n039 n040)) +(d0 (edge n040 n041)) +(d0 (edge n041 n042)) +(d0 (edge n042 n043)) +(d0 (edge n043 n044)) +(d0 (edge n044 n045)) +(d0 (edge n045 n046)) +(d0 (edge n046 n047)) +(d0 (edge n047 n048)) +(d0 (edge n048 n049)) +(d0 (edge n049 n050)) +(d0 (edge n050 n051)) +(d0 (edge n051 n052)) +(d0 (edge n052 n053)) +(d0 (edge n053 n054)) +(d0 (edge n054 n055)) +(d0 (edge n055 n056)) +(d0 (edge n056 n057)) +(d0 (edge n057 n058)) +(d0 (edge n058 n059)) +(d0 (edge n059 n060)) +(d0 (edge n060 n061)) +(d0 (edge n061 n062)) +(d0 (edge n062 n063)) +(d0 (edge n063 n064)) +(d0 (edge n064 n065)) +(d0 (edge n065 n066)) +(d0 (edge n066 n067)) +(d0 (edge n067 n068)) +(d0 (edge n068 n069)) +(d0 (edge n069 n070)) +(d0 (edge n070 n071)) +(d0 (edge n071 n072)) +(d0 (edge n072 n073)) +(d0 (edge n073 n074)) +(d0 (edge n074 n075)) +(d0 (edge n075 n076)) +(d0 (edge n076 n077)) +(d0 (edge n077 n078)) +(d0 (edge n078 n079)) +(d0 (edge n079 n080)) +(d0 (edge n080 n081)) +(d0 (edge n081 n082)) +(d0 (edge n082 n083)) +(d0 (edge n083 n084)) +(d0 (edge n084 n085)) +(d0 (edge n085 n086)) +(d0 (edge n086 n087)) +(d0 (edge n087 n088)) +(d0 (edge n088 n089)) +(d0 (edge n089 n090)) +(d0 (edge n090 n091)) +(d0 (edge n091 n092)) +(d0 (edge n092 n093)) +(d0 (edge n093 n094)) +(d0 (edge n094 n095)) +(d0 (edge n095 n096)) +(d0 (edge n096 n097)) +(d0 (edge n097 n098)) +(d0 (edge n098 n099)) +(d0 (edge n099 n100)) +(d0 (edge n100 n101)) +(d0 (edge n101 n102)) +(d0 (edge n102 n103)) +(d0 (edge n103 n104)) +(d0 (edge n104 n105)) +(d0 (edge n105 n106)) +(d0 (edge n106 n107)) +(d0 (edge n107 n108)) +(d0 (edge n108 n109)) +(d0 (edge n109 n110)) +(d0 (edge n110 n111)) +(d0 (edge n111 n112)) +(d0 (edge n112 n113)) +(d0 (edge n113 n114)) +(d0 (edge n114 n115)) +(d0 (edge n115 n116)) +(d0 (edge n116 n117)) +(d0 (edge n117 n118)) +(d0 (edge n118 n119)) +(d0 (edge n119 n120)) +(d0 (edge n120 n121)) +(d0 (edge n121 n122)) +(d0 (edge n122 n123)) +(d0 (edge n123 n124)) +(d0 (edge n124 n125)) +(d0 (edge n125 n126)) +(d0 (edge n126 n127)) +(d0 (edge n127 n128)) +(t d0 d1) +(exec (s 4 0 0) (, (t $sn_phase_0 $sn_phase_1) (exec (s 4 0 0) $sn_controller_pattern $sn_controller_template)) (, (exec (s 0 0 0) (, ($sn_phase_0 (edge $sn_phase_2 $sn_phase_3)) (f (edge $sn_phase_3 $sn_phase_4))) (, (c (edge $sn_phase_2 $sn_phase_4)))) (exec (s 0 0 1) (, (f (edge $sn_phase_2 $sn_phase_3)) ($sn_phase_0 (edge $sn_phase_3 $sn_phase_4))) (, (c (edge $sn_phase_2 $sn_phase_4)))) (exec (s 1 0 0) (, (c $sn_phase_2) (f $sn_phase_2)) (O (- (c $sn_phase_2)))) (exec (s 2 0 0) (, ($sn_phase_0 $sn_phase_2)) (O (- ($sn_phase_0 $sn_phase_2)))) (exec (s 2 0 1) (, (t $sn_phase_0 $sn_phase_1)) (O (- (t $sn_phase_0 $sn_phase_1)))) (exec (s 3 0 0) (, (c $sn_phase_2)) (O (+ (f $sn_phase_2)) (+ ($sn_phase_1 $sn_phase_2)) (+ (t $sn_phase_1 $sn_phase_0)) (- (c $sn_phase_2)))) (exec (s 4 0 0) $sn_controller_pattern $sn_controller_template))) diff --git a/tools/semi_naive/corpus/i1/transitive_chain_256.source.mm2 b/tools/semi_naive/corpus/i1/transitive_chain_256.source.mm2 new file mode 100644 index 00000000..d119420e --- /dev/null +++ b/tools/semi_naive/corpus/i1/transitive_chain_256.source.mm2 @@ -0,0 +1,262 @@ +; 256-edge chain and one two-factor transitive-closure rule. + +(edge n000 n001) +(edge n001 n002) +(edge n002 n003) +(edge n003 n004) +(edge n004 n005) +(edge n005 n006) +(edge n006 n007) +(edge n007 n008) +(edge n008 n009) +(edge n009 n010) +(edge n010 n011) +(edge n011 n012) +(edge n012 n013) +(edge n013 n014) +(edge n014 n015) +(edge n015 n016) +(edge n016 n017) +(edge n017 n018) +(edge n018 n019) +(edge n019 n020) +(edge n020 n021) +(edge n021 n022) +(edge n022 n023) +(edge n023 n024) +(edge n024 n025) +(edge n025 n026) +(edge n026 n027) +(edge n027 n028) +(edge n028 n029) +(edge n029 n030) +(edge n030 n031) +(edge n031 n032) +(edge n032 n033) +(edge n033 n034) +(edge n034 n035) +(edge n035 n036) +(edge n036 n037) +(edge n037 n038) +(edge n038 n039) +(edge n039 n040) +(edge n040 n041) +(edge n041 n042) +(edge n042 n043) +(edge n043 n044) +(edge n044 n045) +(edge n045 n046) +(edge n046 n047) +(edge n047 n048) +(edge n048 n049) +(edge n049 n050) +(edge n050 n051) +(edge n051 n052) +(edge n052 n053) +(edge n053 n054) +(edge n054 n055) +(edge n055 n056) +(edge n056 n057) +(edge n057 n058) +(edge n058 n059) +(edge n059 n060) +(edge n060 n061) +(edge n061 n062) +(edge n062 n063) +(edge n063 n064) +(edge n064 n065) +(edge n065 n066) +(edge n066 n067) +(edge n067 n068) +(edge n068 n069) +(edge n069 n070) +(edge n070 n071) +(edge n071 n072) +(edge n072 n073) +(edge n073 n074) +(edge n074 n075) +(edge n075 n076) +(edge n076 n077) +(edge n077 n078) +(edge n078 n079) +(edge n079 n080) +(edge n080 n081) +(edge n081 n082) +(edge n082 n083) +(edge n083 n084) +(edge n084 n085) +(edge n085 n086) +(edge n086 n087) +(edge n087 n088) +(edge n088 n089) +(edge n089 n090) +(edge n090 n091) +(edge n091 n092) +(edge n092 n093) +(edge n093 n094) +(edge n094 n095) +(edge n095 n096) +(edge n096 n097) +(edge n097 n098) +(edge n098 n099) +(edge n099 n100) +(edge n100 n101) +(edge n101 n102) +(edge n102 n103) +(edge n103 n104) +(edge n104 n105) +(edge n105 n106) +(edge n106 n107) +(edge n107 n108) +(edge n108 n109) +(edge n109 n110) +(edge n110 n111) +(edge n111 n112) +(edge n112 n113) +(edge n113 n114) +(edge n114 n115) +(edge n115 n116) +(edge n116 n117) +(edge n117 n118) +(edge n118 n119) +(edge n119 n120) +(edge n120 n121) +(edge n121 n122) +(edge n122 n123) +(edge n123 n124) +(edge n124 n125) +(edge n125 n126) +(edge n126 n127) +(edge n127 n128) +(edge n128 n129) +(edge n129 n130) +(edge n130 n131) +(edge n131 n132) +(edge n132 n133) +(edge n133 n134) +(edge n134 n135) +(edge n135 n136) +(edge n136 n137) +(edge n137 n138) +(edge n138 n139) +(edge n139 n140) +(edge n140 n141) +(edge n141 n142) +(edge n142 n143) +(edge n143 n144) +(edge n144 n145) +(edge n145 n146) +(edge n146 n147) +(edge n147 n148) +(edge n148 n149) +(edge n149 n150) +(edge n150 n151) +(edge n151 n152) +(edge n152 n153) +(edge n153 n154) +(edge n154 n155) +(edge n155 n156) +(edge n156 n157) +(edge n157 n158) +(edge n158 n159) +(edge n159 n160) +(edge n160 n161) +(edge n161 n162) +(edge n162 n163) +(edge n163 n164) +(edge n164 n165) +(edge n165 n166) +(edge n166 n167) +(edge n167 n168) +(edge n168 n169) +(edge n169 n170) +(edge n170 n171) +(edge n171 n172) +(edge n172 n173) +(edge n173 n174) +(edge n174 n175) +(edge n175 n176) +(edge n176 n177) +(edge n177 n178) +(edge n178 n179) +(edge n179 n180) +(edge n180 n181) +(edge n181 n182) +(edge n182 n183) +(edge n183 n184) +(edge n184 n185) +(edge n185 n186) +(edge n186 n187) +(edge n187 n188) +(edge n188 n189) +(edge n189 n190) +(edge n190 n191) +(edge n191 n192) +(edge n192 n193) +(edge n193 n194) +(edge n194 n195) +(edge n195 n196) +(edge n196 n197) +(edge n197 n198) +(edge n198 n199) +(edge n199 n200) +(edge n200 n201) +(edge n201 n202) +(edge n202 n203) +(edge n203 n204) +(edge n204 n205) +(edge n205 n206) +(edge n206 n207) +(edge n207 n208) +(edge n208 n209) +(edge n209 n210) +(edge n210 n211) +(edge n211 n212) +(edge n212 n213) +(edge n213 n214) +(edge n214 n215) +(edge n215 n216) +(edge n216 n217) +(edge n217 n218) +(edge n218 n219) +(edge n219 n220) +(edge n220 n221) +(edge n221 n222) +(edge n222 n223) +(edge n223 n224) +(edge n224 n225) +(edge n225 n226) +(edge n226 n227) +(edge n227 n228) +(edge n228 n229) +(edge n229 n230) +(edge n230 n231) +(edge n231 n232) +(edge n232 n233) +(edge n233 n234) +(edge n234 n235) +(edge n235 n236) +(edge n236 n237) +(edge n237 n238) +(edge n238 n239) +(edge n239 n240) +(edge n240 n241) +(edge n241 n242) +(edge n242 n243) +(edge n243 n244) +(edge n244 n245) +(edge n245 n246) +(edge n246 n247) +(edge n247 n248) +(edge n248 n249) +(edge n249 n250) +(edge n250 n251) +(edge n251 n252) +(edge n252 n253) +(edge n253 n254) +(edge n254 n255) +(edge n255 n256) + +(exec 0 + (, (edge $x $y) (edge $y $z)) + (, (edge $x $z))) diff --git a/tools/semi_naive/corpus/i1/transitive_chain_256.transformed.mm2 b/tools/semi_naive/corpus/i1/transitive_chain_256.transformed.mm2 new file mode 100644 index 00000000..5279990f --- /dev/null +++ b/tools/semi_naive/corpus/i1/transitive_chain_256.transformed.mm2 @@ -0,0 +1,514 @@ +(f (edge n000 n001)) +(f (edge n001 n002)) +(f (edge n002 n003)) +(f (edge n003 n004)) +(f (edge n004 n005)) +(f (edge n005 n006)) +(f (edge n006 n007)) +(f (edge n007 n008)) +(f (edge n008 n009)) +(f (edge n009 n010)) +(f (edge n010 n011)) +(f (edge n011 n012)) +(f (edge n012 n013)) +(f (edge n013 n014)) +(f (edge n014 n015)) +(f (edge n015 n016)) +(f (edge n016 n017)) +(f (edge n017 n018)) +(f (edge n018 n019)) +(f (edge n019 n020)) +(f (edge n020 n021)) +(f (edge n021 n022)) +(f (edge n022 n023)) +(f (edge n023 n024)) +(f (edge n024 n025)) +(f (edge n025 n026)) +(f (edge n026 n027)) +(f (edge n027 n028)) +(f (edge n028 n029)) +(f (edge n029 n030)) +(f (edge n030 n031)) +(f (edge n031 n032)) +(f (edge n032 n033)) +(f (edge n033 n034)) +(f (edge n034 n035)) +(f (edge n035 n036)) +(f (edge n036 n037)) +(f (edge n037 n038)) +(f (edge n038 n039)) +(f (edge n039 n040)) +(f (edge n040 n041)) +(f (edge n041 n042)) +(f (edge n042 n043)) +(f (edge n043 n044)) +(f (edge n044 n045)) +(f (edge n045 n046)) +(f (edge n046 n047)) +(f (edge n047 n048)) +(f (edge n048 n049)) +(f (edge n049 n050)) +(f (edge n050 n051)) +(f (edge n051 n052)) +(f (edge n052 n053)) +(f (edge n053 n054)) +(f (edge n054 n055)) +(f (edge n055 n056)) +(f (edge n056 n057)) +(f (edge n057 n058)) +(f (edge n058 n059)) +(f (edge n059 n060)) +(f (edge n060 n061)) +(f (edge n061 n062)) +(f (edge n062 n063)) +(f (edge n063 n064)) +(f (edge n064 n065)) +(f (edge n065 n066)) +(f (edge n066 n067)) +(f (edge n067 n068)) +(f (edge n068 n069)) +(f (edge n069 n070)) +(f (edge n070 n071)) +(f (edge n071 n072)) +(f (edge n072 n073)) +(f (edge n073 n074)) +(f (edge n074 n075)) +(f (edge n075 n076)) +(f (edge n076 n077)) +(f (edge n077 n078)) +(f (edge n078 n079)) +(f (edge n079 n080)) +(f (edge n080 n081)) +(f (edge n081 n082)) +(f (edge n082 n083)) +(f (edge n083 n084)) +(f (edge n084 n085)) +(f (edge n085 n086)) +(f (edge n086 n087)) +(f (edge n087 n088)) +(f (edge n088 n089)) +(f (edge n089 n090)) +(f (edge n090 n091)) +(f (edge n091 n092)) +(f (edge n092 n093)) +(f (edge n093 n094)) +(f (edge n094 n095)) +(f (edge n095 n096)) +(f (edge n096 n097)) +(f (edge n097 n098)) +(f (edge n098 n099)) +(f (edge n099 n100)) +(f (edge n100 n101)) +(f (edge n101 n102)) +(f (edge n102 n103)) +(f (edge n103 n104)) +(f (edge n104 n105)) +(f (edge n105 n106)) +(f (edge n106 n107)) +(f (edge n107 n108)) +(f (edge n108 n109)) +(f (edge n109 n110)) +(f (edge n110 n111)) +(f (edge n111 n112)) +(f (edge n112 n113)) +(f (edge n113 n114)) +(f (edge n114 n115)) +(f (edge n115 n116)) +(f (edge n116 n117)) +(f (edge n117 n118)) +(f (edge n118 n119)) +(f (edge n119 n120)) +(f (edge n120 n121)) +(f (edge n121 n122)) +(f (edge n122 n123)) +(f (edge n123 n124)) +(f (edge n124 n125)) +(f (edge n125 n126)) +(f (edge n126 n127)) +(f (edge n127 n128)) +(f (edge n128 n129)) +(f (edge n129 n130)) +(f (edge n130 n131)) +(f (edge n131 n132)) +(f (edge n132 n133)) +(f (edge n133 n134)) +(f (edge n134 n135)) +(f (edge n135 n136)) +(f (edge n136 n137)) +(f (edge n137 n138)) +(f (edge n138 n139)) +(f (edge n139 n140)) +(f (edge n140 n141)) +(f (edge n141 n142)) +(f (edge n142 n143)) +(f (edge n143 n144)) +(f (edge n144 n145)) +(f (edge n145 n146)) +(f (edge n146 n147)) +(f (edge n147 n148)) +(f (edge n148 n149)) +(f (edge n149 n150)) +(f (edge n150 n151)) +(f (edge n151 n152)) +(f (edge n152 n153)) +(f (edge n153 n154)) +(f (edge n154 n155)) +(f (edge n155 n156)) +(f (edge n156 n157)) +(f (edge n157 n158)) +(f (edge n158 n159)) +(f (edge n159 n160)) +(f (edge n160 n161)) +(f (edge n161 n162)) +(f (edge n162 n163)) +(f (edge n163 n164)) +(f (edge n164 n165)) +(f (edge n165 n166)) +(f (edge n166 n167)) +(f (edge n167 n168)) +(f (edge n168 n169)) +(f (edge n169 n170)) +(f (edge n170 n171)) +(f (edge n171 n172)) +(f (edge n172 n173)) +(f (edge n173 n174)) +(f (edge n174 n175)) +(f (edge n175 n176)) +(f (edge n176 n177)) +(f (edge n177 n178)) +(f (edge n178 n179)) +(f (edge n179 n180)) +(f (edge n180 n181)) +(f (edge n181 n182)) +(f (edge n182 n183)) +(f (edge n183 n184)) +(f (edge n184 n185)) +(f (edge n185 n186)) +(f (edge n186 n187)) +(f (edge n187 n188)) +(f (edge n188 n189)) +(f (edge n189 n190)) +(f (edge n190 n191)) +(f (edge n191 n192)) +(f (edge n192 n193)) +(f (edge n193 n194)) +(f (edge n194 n195)) +(f (edge n195 n196)) +(f (edge n196 n197)) +(f (edge n197 n198)) +(f (edge n198 n199)) +(f (edge n199 n200)) +(f (edge n200 n201)) +(f (edge n201 n202)) +(f (edge n202 n203)) +(f (edge n203 n204)) +(f (edge n204 n205)) +(f (edge n205 n206)) +(f (edge n206 n207)) +(f (edge n207 n208)) +(f (edge n208 n209)) +(f (edge n209 n210)) +(f (edge n210 n211)) +(f (edge n211 n212)) +(f (edge n212 n213)) +(f (edge n213 n214)) +(f (edge n214 n215)) +(f (edge n215 n216)) +(f (edge n216 n217)) +(f (edge n217 n218)) +(f (edge n218 n219)) +(f (edge n219 n220)) +(f (edge n220 n221)) +(f (edge n221 n222)) +(f (edge n222 n223)) +(f (edge n223 n224)) +(f (edge n224 n225)) +(f (edge n225 n226)) +(f (edge n226 n227)) +(f (edge n227 n228)) +(f (edge n228 n229)) +(f (edge n229 n230)) +(f (edge n230 n231)) +(f (edge n231 n232)) +(f (edge n232 n233)) +(f (edge n233 n234)) +(f (edge n234 n235)) +(f (edge n235 n236)) +(f (edge n236 n237)) +(f (edge n237 n238)) +(f (edge n238 n239)) +(f (edge n239 n240)) +(f (edge n240 n241)) +(f (edge n241 n242)) +(f (edge n242 n243)) +(f (edge n243 n244)) +(f (edge n244 n245)) +(f (edge n245 n246)) +(f (edge n246 n247)) +(f (edge n247 n248)) +(f (edge n248 n249)) +(f (edge n249 n250)) +(f (edge n250 n251)) +(f (edge n251 n252)) +(f (edge n252 n253)) +(f (edge n253 n254)) +(f (edge n254 n255)) +(f (edge n255 n256)) +(d0 (edge n000 n001)) +(d0 (edge n001 n002)) +(d0 (edge n002 n003)) +(d0 (edge n003 n004)) +(d0 (edge n004 n005)) +(d0 (edge n005 n006)) +(d0 (edge n006 n007)) +(d0 (edge n007 n008)) +(d0 (edge n008 n009)) +(d0 (edge n009 n010)) +(d0 (edge n010 n011)) +(d0 (edge n011 n012)) +(d0 (edge n012 n013)) +(d0 (edge n013 n014)) +(d0 (edge n014 n015)) +(d0 (edge n015 n016)) +(d0 (edge n016 n017)) +(d0 (edge n017 n018)) +(d0 (edge n018 n019)) +(d0 (edge n019 n020)) +(d0 (edge n020 n021)) +(d0 (edge n021 n022)) +(d0 (edge n022 n023)) +(d0 (edge n023 n024)) +(d0 (edge n024 n025)) +(d0 (edge n025 n026)) +(d0 (edge n026 n027)) +(d0 (edge n027 n028)) +(d0 (edge n028 n029)) +(d0 (edge n029 n030)) +(d0 (edge n030 n031)) +(d0 (edge n031 n032)) +(d0 (edge n032 n033)) +(d0 (edge n033 n034)) +(d0 (edge n034 n035)) +(d0 (edge n035 n036)) +(d0 (edge n036 n037)) +(d0 (edge n037 n038)) +(d0 (edge n038 n039)) +(d0 (edge n039 n040)) +(d0 (edge n040 n041)) +(d0 (edge n041 n042)) +(d0 (edge n042 n043)) +(d0 (edge n043 n044)) +(d0 (edge n044 n045)) +(d0 (edge n045 n046)) +(d0 (edge n046 n047)) +(d0 (edge n047 n048)) +(d0 (edge n048 n049)) +(d0 (edge n049 n050)) +(d0 (edge n050 n051)) +(d0 (edge n051 n052)) +(d0 (edge n052 n053)) +(d0 (edge n053 n054)) +(d0 (edge n054 n055)) +(d0 (edge n055 n056)) +(d0 (edge n056 n057)) +(d0 (edge n057 n058)) +(d0 (edge n058 n059)) +(d0 (edge n059 n060)) +(d0 (edge n060 n061)) +(d0 (edge n061 n062)) +(d0 (edge n062 n063)) +(d0 (edge n063 n064)) +(d0 (edge n064 n065)) +(d0 (edge n065 n066)) +(d0 (edge n066 n067)) +(d0 (edge n067 n068)) +(d0 (edge n068 n069)) +(d0 (edge n069 n070)) +(d0 (edge n070 n071)) +(d0 (edge n071 n072)) +(d0 (edge n072 n073)) +(d0 (edge n073 n074)) +(d0 (edge n074 n075)) +(d0 (edge n075 n076)) +(d0 (edge n076 n077)) +(d0 (edge n077 n078)) +(d0 (edge n078 n079)) +(d0 (edge n079 n080)) +(d0 (edge n080 n081)) +(d0 (edge n081 n082)) +(d0 (edge n082 n083)) +(d0 (edge n083 n084)) +(d0 (edge n084 n085)) +(d0 (edge n085 n086)) +(d0 (edge n086 n087)) +(d0 (edge n087 n088)) +(d0 (edge n088 n089)) +(d0 (edge n089 n090)) +(d0 (edge n090 n091)) +(d0 (edge n091 n092)) +(d0 (edge n092 n093)) +(d0 (edge n093 n094)) +(d0 (edge n094 n095)) +(d0 (edge n095 n096)) +(d0 (edge n096 n097)) +(d0 (edge n097 n098)) +(d0 (edge n098 n099)) +(d0 (edge n099 n100)) +(d0 (edge n100 n101)) +(d0 (edge n101 n102)) +(d0 (edge n102 n103)) +(d0 (edge n103 n104)) +(d0 (edge n104 n105)) +(d0 (edge n105 n106)) +(d0 (edge n106 n107)) +(d0 (edge n107 n108)) +(d0 (edge n108 n109)) +(d0 (edge n109 n110)) +(d0 (edge n110 n111)) +(d0 (edge n111 n112)) +(d0 (edge n112 n113)) +(d0 (edge n113 n114)) +(d0 (edge n114 n115)) +(d0 (edge n115 n116)) +(d0 (edge n116 n117)) +(d0 (edge n117 n118)) +(d0 (edge n118 n119)) +(d0 (edge n119 n120)) +(d0 (edge n120 n121)) +(d0 (edge n121 n122)) +(d0 (edge n122 n123)) +(d0 (edge n123 n124)) +(d0 (edge n124 n125)) +(d0 (edge n125 n126)) +(d0 (edge n126 n127)) +(d0 (edge n127 n128)) +(d0 (edge n128 n129)) +(d0 (edge n129 n130)) +(d0 (edge n130 n131)) +(d0 (edge n131 n132)) +(d0 (edge n132 n133)) +(d0 (edge n133 n134)) +(d0 (edge n134 n135)) +(d0 (edge n135 n136)) +(d0 (edge n136 n137)) +(d0 (edge n137 n138)) +(d0 (edge n138 n139)) +(d0 (edge n139 n140)) +(d0 (edge n140 n141)) +(d0 (edge n141 n142)) +(d0 (edge n142 n143)) +(d0 (edge n143 n144)) +(d0 (edge n144 n145)) +(d0 (edge n145 n146)) +(d0 (edge n146 n147)) +(d0 (edge n147 n148)) +(d0 (edge n148 n149)) +(d0 (edge n149 n150)) +(d0 (edge n150 n151)) +(d0 (edge n151 n152)) +(d0 (edge n152 n153)) +(d0 (edge n153 n154)) +(d0 (edge n154 n155)) +(d0 (edge n155 n156)) +(d0 (edge n156 n157)) +(d0 (edge n157 n158)) +(d0 (edge n158 n159)) +(d0 (edge n159 n160)) +(d0 (edge n160 n161)) +(d0 (edge n161 n162)) +(d0 (edge n162 n163)) +(d0 (edge n163 n164)) +(d0 (edge n164 n165)) +(d0 (edge n165 n166)) +(d0 (edge n166 n167)) +(d0 (edge n167 n168)) +(d0 (edge n168 n169)) +(d0 (edge n169 n170)) +(d0 (edge n170 n171)) +(d0 (edge n171 n172)) +(d0 (edge n172 n173)) +(d0 (edge n173 n174)) +(d0 (edge n174 n175)) +(d0 (edge n175 n176)) +(d0 (edge n176 n177)) +(d0 (edge n177 n178)) +(d0 (edge n178 n179)) +(d0 (edge n179 n180)) +(d0 (edge n180 n181)) +(d0 (edge n181 n182)) +(d0 (edge n182 n183)) +(d0 (edge n183 n184)) +(d0 (edge n184 n185)) +(d0 (edge n185 n186)) +(d0 (edge n186 n187)) +(d0 (edge n187 n188)) +(d0 (edge n188 n189)) +(d0 (edge n189 n190)) +(d0 (edge n190 n191)) +(d0 (edge n191 n192)) +(d0 (edge n192 n193)) +(d0 (edge n193 n194)) +(d0 (edge n194 n195)) +(d0 (edge n195 n196)) +(d0 (edge n196 n197)) +(d0 (edge n197 n198)) +(d0 (edge n198 n199)) +(d0 (edge n199 n200)) +(d0 (edge n200 n201)) +(d0 (edge n201 n202)) +(d0 (edge n202 n203)) +(d0 (edge n203 n204)) +(d0 (edge n204 n205)) +(d0 (edge n205 n206)) +(d0 (edge n206 n207)) +(d0 (edge n207 n208)) +(d0 (edge n208 n209)) +(d0 (edge n209 n210)) +(d0 (edge n210 n211)) +(d0 (edge n211 n212)) +(d0 (edge n212 n213)) +(d0 (edge n213 n214)) +(d0 (edge n214 n215)) +(d0 (edge n215 n216)) +(d0 (edge n216 n217)) +(d0 (edge n217 n218)) +(d0 (edge n218 n219)) +(d0 (edge n219 n220)) +(d0 (edge n220 n221)) +(d0 (edge n221 n222)) +(d0 (edge n222 n223)) +(d0 (edge n223 n224)) +(d0 (edge n224 n225)) +(d0 (edge n225 n226)) +(d0 (edge n226 n227)) +(d0 (edge n227 n228)) +(d0 (edge n228 n229)) +(d0 (edge n229 n230)) +(d0 (edge n230 n231)) +(d0 (edge n231 n232)) +(d0 (edge n232 n233)) +(d0 (edge n233 n234)) +(d0 (edge n234 n235)) +(d0 (edge n235 n236)) +(d0 (edge n236 n237)) +(d0 (edge n237 n238)) +(d0 (edge n238 n239)) +(d0 (edge n239 n240)) +(d0 (edge n240 n241)) +(d0 (edge n241 n242)) +(d0 (edge n242 n243)) +(d0 (edge n243 n244)) +(d0 (edge n244 n245)) +(d0 (edge n245 n246)) +(d0 (edge n246 n247)) +(d0 (edge n247 n248)) +(d0 (edge n248 n249)) +(d0 (edge n249 n250)) +(d0 (edge n250 n251)) +(d0 (edge n251 n252)) +(d0 (edge n252 n253)) +(d0 (edge n253 n254)) +(d0 (edge n254 n255)) +(d0 (edge n255 n256)) +(t d0 d1) +(exec (s 4 0 0) (, (t $sn_phase_0 $sn_phase_1) (exec (s 4 0 0) $sn_controller_pattern $sn_controller_template)) (, (exec (s 0 0 0) (, ($sn_phase_0 (edge $sn_phase_2 $sn_phase_3)) (f (edge $sn_phase_3 $sn_phase_4))) (, (c (edge $sn_phase_2 $sn_phase_4)))) (exec (s 0 0 1) (, (f (edge $sn_phase_2 $sn_phase_3)) ($sn_phase_0 (edge $sn_phase_3 $sn_phase_4))) (, (c (edge $sn_phase_2 $sn_phase_4)))) (exec (s 1 0 0) (, (c $sn_phase_2) (f $sn_phase_2)) (O (- (c $sn_phase_2)))) (exec (s 2 0 0) (, ($sn_phase_0 $sn_phase_2)) (O (- ($sn_phase_0 $sn_phase_2)))) (exec (s 2 0 1) (, (t $sn_phase_0 $sn_phase_1)) (O (- (t $sn_phase_0 $sn_phase_1)))) (exec (s 3 0 0) (, (c $sn_phase_2)) (O (+ (f $sn_phase_2)) (+ ($sn_phase_1 $sn_phase_2)) (+ (t $sn_phase_1 $sn_phase_0)) (- (c $sn_phase_2)))) (exec (s 4 0 0) $sn_controller_pattern $sn_controller_template))) diff --git a/tools/semi_naive/corpus/i3/multiple_heads.source.mm2 b/tools/semi_naive/corpus/i3/multiple_heads.source.mm2 new file mode 100644 index 00000000..cb2a15e3 --- /dev/null +++ b/tools/semi_naive/corpus/i3/multiple_heads.source.mm2 @@ -0,0 +1,8 @@ +; One match emits two heads. + +(seed a) +(seed b) + +(exec (source 7) + (, (seed $x)) + (, (left $x) (right $x))) diff --git a/tools/semi_naive/corpus/i3/multiple_rules.source.mm2 b/tools/semi_naive/corpus/i3/multiple_rules.source.mm2 new file mode 100644 index 00000000..4346423a --- /dev/null +++ b/tools/semi_naive/corpus/i3/multiple_rules.source.mm2 @@ -0,0 +1,12 @@ +; Both rules share one round controller and retain their source priorities. + +(seed a) +(seed b) + +(exec 20 + (, (seed $x)) + (, (mid $x))) + +(exec 3 + (, (mid $x)) + (, (out $x))) diff --git a/tools/semi_naive/corpus/i3/three_factor.source.mm2 b/tools/semi_naive/corpus/i3/three_factor.source.mm2 new file mode 100644 index 00000000..e6b933a3 --- /dev/null +++ b/tools/semi_naive/corpus/i3/three_factor.source.mm2 @@ -0,0 +1,12 @@ +; Three body factors require three delta variants. + +(a x) +(a y) +(b x one) +(b y two) +(c one) +(c two) + +(exec 7 + (, (a $x) (b $x $y) (c $y)) + (, (joined $x $y))) diff --git a/tools/semi_naive/corpus/i4/direct_controller.mm2 b/tools/semi_naive/corpus/i4/direct_controller.mm2 new file mode 100644 index 00000000..3d7629a2 --- /dev/null +++ b/tools/semi_naive/corpus/i4/direct_controller.mm2 @@ -0,0 +1,8 @@ +(seed a) +(active) +(exec 5 + (, (active) (exec 5 $controller-pattern $controller-template)) + (, (exec 0 (, (seed $x)) (, (left $x))) + (exec 1 (, (seed $x)) (, (right $x))) + (exec 2 (, (active)) (O (- (active)))) + (exec 5 $controller-pattern $controller-template))) diff --git a/tools/semi_naive/corpus/refusals/bare_pattern.mm2 b/tools/semi_naive/corpus/refusals/bare_pattern.mm2 new file mode 100644 index 00000000..60ea96fc --- /dev/null +++ b/tools/semi_naive/corpus/refusals/bare_pattern.mm2 @@ -0,0 +1,2 @@ +(seed a) +(exec 0 (, $x) (, (seen $x))) diff --git a/tools/semi_naive/corpus/refusals/bare_template.mm2 b/tools/semi_naive/corpus/refusals/bare_template.mm2 new file mode 100644 index 00000000..60fd0573 --- /dev/null +++ b/tools/semi_naive/corpus/refusals/bare_template.mm2 @@ -0,0 +1,2 @@ +(seed a) +(exec 0 (, (seed $x)) (, $x)) diff --git a/tools/semi_naive/corpus/refusals/controller_variable_limit.mm2 b/tools/semi_naive/corpus/refusals/controller_variable_limit.mm2 new file mode 100644 index 00000000..19e44a64 --- /dev/null +++ b/tools/semi_naive/corpus/refusals/controller_variable_limit.mm2 @@ -0,0 +1,2 @@ +(seed $v0 $v1 $v2 $v3 $v4 $v5 $v6 $v7 $v8 $v9 $v10 $v11 $v12 $v13 $v14 $v15 $v16 $v17 $v18 $v19 $v20 $v21 $v22 $v23 $v24 $v25 $v26 $v27 $v28 $v29 $v30 $v31 $v32 $v33 $v34 $v35 $v36 $v37 $v38 $v39 $v40 $v41 $v42 $v43 $v44 $v45 $v46 $v47 $v48 $v49 $v50 $v51 $v52 $v53 $v54 $v55 $v56 $v57 $v58 $v59 $v60) +(exec 0 (, (seed $v0 $v1 $v2 $v3 $v4 $v5 $v6 $v7 $v8 $v9 $v10 $v11 $v12 $v13 $v14 $v15 $v16 $v17 $v18 $v19 $v20 $v21 $v22 $v23 $v24 $v25 $v26 $v27 $v28 $v29 $v30 $v31 $v32 $v33 $v34 $v35 $v36 $v37 $v38 $v39 $v40 $v41 $v42 $v43 $v44 $v45 $v46 $v47 $v48 $v49 $v50 $v51 $v52 $v53 $v54 $v55 $v56 $v57 $v58 $v59 $v60)) (, (out))) diff --git a/tools/semi_naive/corpus/refusals/counted_exec_head.mm2 b/tools/semi_naive/corpus/refusals/counted_exec_head.mm2 new file mode 100644 index 00000000..cd95152f --- /dev/null +++ b/tools/semi_naive/corpus/refusals/counted_exec_head.mm2 @@ -0,0 +1,2 @@ +(seed a) +(exec 0 (, (seed $x)) (, (seen $x)) (, (count $x))) diff --git a/tools/semi_naive/corpus/refusals/empty_body.mm2 b/tools/semi_naive/corpus/refusals/empty_body.mm2 new file mode 100644 index 00000000..008760b0 --- /dev/null +++ b/tools/semi_naive/corpus/refusals/empty_body.mm2 @@ -0,0 +1,2 @@ +(seed a) +(exec 0 (,) (, (seen))) diff --git a/tools/semi_naive/corpus/refusals/empty_head.mm2 b/tools/semi_naive/corpus/refusals/empty_head.mm2 new file mode 100644 index 00000000..8d8e19c4 --- /dev/null +++ b/tools/semi_naive/corpus/refusals/empty_head.mm2 @@ -0,0 +1,2 @@ +(seed a) +(exec 0 (, (seed $x)) (,)) diff --git a/tools/semi_naive/corpus/refusals/foreign_exec_template.mm2 b/tools/semi_naive/corpus/refusals/foreign_exec_template.mm2 new file mode 100644 index 00000000..64a548db --- /dev/null +++ b/tools/semi_naive/corpus/refusals/foreign_exec_template.mm2 @@ -0,0 +1,4 @@ +(seed a) +(exec loop + (, (seed $x) (exec loop $pattern $template)) + (, (out $x) (exec other $pattern $template) (exec loop $pattern $template))) diff --git a/tools/semi_naive/corpus/refusals/io_sink.mm2 b/tools/semi_naive/corpus/refusals/io_sink.mm2 new file mode 100644 index 00000000..ee0b21aa --- /dev/null +++ b/tools/semi_naive/corpus/refusals/io_sink.mm2 @@ -0,0 +1,2 @@ +(seed a) +(exec 0 (, (seed $x)) (O (+ (seen $x)))) diff --git a/tools/semi_naive/corpus/refusals/io_source.mm2 b/tools/semi_naive/corpus/refusals/io_source.mm2 new file mode 100644 index 00000000..ccc34d18 --- /dev/null +++ b/tools/semi_naive/corpus/refusals/io_source.mm2 @@ -0,0 +1 @@ +(exec 0 (I (ACT data (row $x))) (, (seen $x))) diff --git a/tools/semi_naive/corpus/refusals/malformed_exec.mm2 b/tools/semi_naive/corpus/refusals/malformed_exec.mm2 new file mode 100644 index 00000000..20124ee8 --- /dev/null +++ b/tools/semi_naive/corpus/refusals/malformed_exec.mm2 @@ -0,0 +1 @@ +(exec 0 (, (seed $x))) diff --git a/tools/semi_naive/corpus/refusals/no_rules.mm2 b/tools/semi_naive/corpus/refusals/no_rules.mm2 new file mode 100644 index 00000000..abaf7ca5 --- /dev/null +++ b/tools/semi_naive/corpus/refusals/no_rules.mm2 @@ -0,0 +1 @@ +(seed a) diff --git a/tools/semi_naive/corpus/refusals/removal_template.mm2 b/tools/semi_naive/corpus/refusals/removal_template.mm2 new file mode 100644 index 00000000..e4e23d33 --- /dev/null +++ b/tools/semi_naive/corpus/refusals/removal_template.mm2 @@ -0,0 +1,2 @@ +(seed a) +(exec 0 (, (seed $x)) (O (- (seed $x)))) diff --git a/tools/semi_naive/corpus/refusals/reserved_source_form.mm2 b/tools/semi_naive/corpus/refusals/reserved_source_form.mm2 new file mode 100644 index 00000000..6b0a4e3b --- /dev/null +++ b/tools/semi_naive/corpus/refusals/reserved_source_form.mm2 @@ -0,0 +1,2 @@ +(I data) +(exec 0 (, (other)) (, (seen))) diff --git a/tools/semi_naive/corpus/refusals/self_modifying_rule.mm2 b/tools/semi_naive/corpus/refusals/self_modifying_rule.mm2 new file mode 100644 index 00000000..7dd25116 --- /dev/null +++ b/tools/semi_naive/corpus/refusals/self_modifying_rule.mm2 @@ -0,0 +1,4 @@ +(seed a) +(exec (loop 0) + (, (seed $x) (exec (loop $round) $pattern $template)) + (, (out $x) (exec (loop 1) $pattern $template))) diff --git a/tools/semi_naive/corpus/refusals/too_many_variables.mm2 b/tools/semi_naive/corpus/refusals/too_many_variables.mm2 new file mode 100644 index 00000000..e8674e25 --- /dev/null +++ b/tools/semi_naive/corpus/refusals/too_many_variables.mm2 @@ -0,0 +1,2 @@ +(seed $v0 $v1 $v2 $v3 $v4 $v5 $v6 $v7 $v8 $v9 $v10 $v11 $v12 $v13 $v14 $v15 $v16 $v17 $v18 $v19 $v20 $v21 $v22 $v23 $v24 $v25 $v26 $v27 $v28 $v29 $v30 $v31 $v32 $v33 $v34 $v35 $v36 $v37 $v38 $v39 $v40 $v41 $v42 $v43 $v44 $v45 $v46 $v47 $v48 $v49 $v50 $v51 $v52 $v53 $v54 $v55 $v56 $v57 $v58 $v59 $v60 $v61 $v62 $v63 $v64) +(exec 0 (, (seed $v0 $v1 $v2 $v3 $v4 $v5 $v6 $v7 $v8 $v9 $v10 $v11 $v12 $v13 $v14 $v15 $v16 $v17 $v18 $v19 $v20 $v21 $v22 $v23 $v24 $v25 $v26 $v27 $v28 $v29 $v30 $v31 $v32 $v33 $v34 $v35 $v36 $v37 $v38 $v39 $v40 $v41 $v42 $v43 $v44 $v45 $v46 $v47 $v48 $v49 $v50 $v51 $v52 $v53 $v54 $v55 $v56 $v57 $v58 $v59 $v60 $v61 $v62 $v63 $v64)) (, (out))) diff --git a/tools/semi_naive/corpus/refusals/unbound_head_variable.mm2 b/tools/semi_naive/corpus/refusals/unbound_head_variable.mm2 new file mode 100644 index 00000000..e336bfdb --- /dev/null +++ b/tools/semi_naive/corpus/refusals/unbound_head_variable.mm2 @@ -0,0 +1,2 @@ +(seed a) +(exec 0 (, (seed $x)) (, (seen $y))) diff --git a/tools/semi_naive/corpus/refusals/unclassifiable_fact.mm2 b/tools/semi_naive/corpus/refusals/unclassifiable_fact.mm2 new file mode 100644 index 00000000..ffe3c8c7 --- /dev/null +++ b/tools/semi_naive/corpus/refusals/unclassifiable_fact.mm2 @@ -0,0 +1,2 @@ +seed +(exec 0 (, (other)) (, (seen))) diff --git a/tools/semi_naive/corpus/refusals/variable_priority.mm2 b/tools/semi_naive/corpus/refusals/variable_priority.mm2 new file mode 100644 index 00000000..a65683ca --- /dev/null +++ b/tools/semi_naive/corpus/refusals/variable_priority.mm2 @@ -0,0 +1,2 @@ +(seed a) +(exec $priority (, (seed $x)) (, (seen $x))) diff --git a/tools/semi_naive/corpus/refusals/variable_relation_pattern.mm2 b/tools/semi_naive/corpus/refusals/variable_relation_pattern.mm2 new file mode 100644 index 00000000..255d2ab8 --- /dev/null +++ b/tools/semi_naive/corpus/refusals/variable_relation_pattern.mm2 @@ -0,0 +1,2 @@ +(seed a) +(exec 0 (, ($relation $x)) (, (seen $x))) diff --git a/tools/semi_naive/corpus/repository/manifest.tsv b/tools/semi_naive/corpus/repository/manifest.tsv new file mode 100644 index 00000000..093b0255 --- /dev/null +++ b/tools/semi_naive/corpus/repository/manifest.tsv @@ -0,0 +1,24 @@ +# label|source|expected|source-mode|source-steps|engine-specific-counters +kernel/string_convert|kernel/resources/string_convert.mm2|differential/expected/string_convert.expected|persistent|-|- +kernel/transitive|kernel/resources/transitive.mm2|tools/semi_naive/expected/repository/kernel/transitive.expected|persistent|-|- +programs/cross_join_dict|differential/corpus/programs/cross_join_dict.mm2|differential/expected/programs/cross_join_dict.expected|persistent|-|- +programs/cross_join_tuple|differential/corpus/programs/cross_join_tuple.mm2|differential/expected/programs/cross_join_tuple.expected|persistent|-|- +programs/lens_aunt|differential/corpus/programs/lens_aunt.mm2|tools/semi_naive/expected/repository/programs/lens_aunt.expected|natural|1|unifications +programs/lens_composition|differential/corpus/programs/lens_composition.mm2|differential/expected/programs/lens_composition.expected|persistent|-|- +programs/pattern_mining|differential/corpus/programs/pattern_mining.mm2|differential/expected/programs/pattern_mining.expected|persistent|-|- +programs/stv_roman|differential/corpus/programs/stv_roman.mm2|differential/expected/programs/stv_roman.expected|persistent|-|- +unify/coref_absorbed_by_data_varref|differential/corpus/unify/coref_absorbed_by_data_varref.mm2|differential/expected/unify/coref_absorbed_by_data_varref.expected|persistent|-|- +unify/func_type_unification|differential/corpus/unify/func_type_unification.mm2|differential/expected/unify/func_type_unification.expected|persistent|-|- +unify/two_bipolar_equal_crossed|differential/corpus/unify/two_bipolar_equal_crossed.mm2|differential/expected/unify/two_bipolar_equal_crossed.expected|persistent|-|- +wiki/mm2_basics_02|differential/corpus/wiki/mm2_basics_02.mm2|tools/semi_naive/expected/repository/wiki/mm2_basics_02.expected|persistent|-|- +wiki/mm2_basics_05|differential/corpus/wiki/mm2_basics_05.mm2|differential/expected/wiki/mm2_basics_05.expected|persistent|-|- +wiki/reachability_p1_13|differential/corpus/wiki/reachability_p1_13.mm2|tools/semi_naive/expected/repository/wiki/reachability_p1_13.expected|persistent|-|- +wiki/reachability_p2_06|differential/corpus/wiki/reachability_p2_06.mm2|tools/semi_naive/expected/repository/wiki/reachability_p2_06.expected|persistent|-|- +wiki/reachability_p2_07|differential/corpus/wiki/reachability_p2_07.mm2|tools/semi_naive/expected/repository/wiki/reachability_p2_07.expected|persistent|-|- +wiki/reachability_p2_08|differential/corpus/wiki/reachability_p2_08.mm2|tools/semi_naive/expected/repository/wiki/reachability_p2_08.expected|persistent|-|- +wiki/reachability_p3_03|differential/corpus/wiki/reachability_p3_03.mm2|tools/semi_naive/expected/repository/wiki/reachability_p3_03.expected|persistent|-|- +wiki/reachability_p3_04|differential/corpus/wiki/reachability_p3_04.mm2|tools/semi_naive/expected/repository/wiki/reachability_p3_04.expected|persistent|-|- +wiki/reachability_p3_09|differential/corpus/wiki/reachability_p3_09.mm2|tools/semi_naive/expected/repository/wiki/reachability_p3_09.expected|persistent|-|- +wiki/reachability_p3_12|differential/corpus/wiki/reachability_p3_12.mm2|tools/semi_naive/expected/repository/wiki/reachability_p3_12.expected|persistent|-|- +wiki/reachability_p3_18|differential/corpus/wiki/reachability_p3_18.mm2|differential/expected/wiki/reachability_p3_18.expected|persistent|-|- +wiki/reachability_p4_03|differential/corpus/wiki/reachability_p4_03.mm2|tools/semi_naive/expected/repository/wiki/reachability_p4_03.expected|persistent|-|- diff --git a/tools/semi_naive/driver.py b/tools/semi_naive/driver.py new file mode 100755 index 00000000..c5661ff4 --- /dev/null +++ b/tools/semi_naive/driver.py @@ -0,0 +1,954 @@ +#!/usr/bin/env python3 +"""Compare an MM2 program with a semi-naive transformed program.""" + +import argparse +from dataclasses import dataclass +import os +import re +import subprocess +import sys +import tempfile +import time + + +HERE = os.path.dirname(os.path.abspath(__file__)) +REPO = os.path.dirname(os.path.dirname(HERE)) +sys.path.insert(0, HERE) +import sexpr + +GENERATORS = os.path.join(HERE, "generators") +sys.path.insert(0, GENERATORS) +import gen_process_calculus +import gen_transitive + + +DEFAULT_BINARY = os.path.join(REPO, "target", "release", "mork") +DEFAULT_STEPS = 1_000_000_000_000_000 +REPOSITORY_MANIFEST = os.path.join(HERE, "corpus", "repository", "manifest.tsv") +METRIC_FIELDS = ("steps", "milliseconds", "unifications", "writes", "transitions") +ENGINE_SPECIFIC_COUNTER_FIELDS = ("unifications",) + +METRICS_RE = re.compile( + rb"executing (\d+) steps took (\d+) ms " + rb"\(unifications (\d+), writes (\d+), transitions (\d+)" + rb"(?:, max unify \d+)?\)" +) +EXPECTED_SOURCE_STEPS_RE = re.compile(r"^;+\s*@source-steps\s+([0-9]+)\s*$") +BOOKKEEPING_PREFIXES = ( + b"(d0 ", + b"(d1 ", + b"(c ", + b"(t ", + b"(dc ", + b"(dn ", + b"(cand ", + b"(phase ", + b"(controller ", + b"(active)", +) + + +@dataclass(frozen=True) +class OracleCase: + label: str + source: str + transformed: str + expected: str | None = None + required: str | None = None + source_mode: str = "persistent" + source_steps: int | None = None + engine_specific_fields: tuple[str, ...] = () + + +@dataclass(frozen=True) +class RepositorySpec: + label: str + source: str + expected: str + source_mode: str + source_steps: int | None + engine_specific_fields: tuple[str, ...] + + +def capture(command, timeout=None): + return subprocess.run( + command, + cwd=REPO, + stdout=subprocess.PIPE, + stderr=subprocess.STDOUT, + check=False, + timeout=timeout, + ) + + +def parse_metrics(output): + match = METRICS_RE.search(output) + if match is None: + raise ValueError("EXECUTION_METRICS_MISSING") + steps_run, milliseconds, unifications, writes, transitions = ( + int(value) for value in match.groups() + ) + return { + "steps": steps_run, + "milliseconds": milliseconds, + "unifications": unifications, + "writes": writes, + "transitions": transitions, + } + + +def run_program(binary, program, dump_path, steps, timeout=None): + command = [ + binary, + "run", + program, + "--steps", + str(steps), + "--instrumentation", + "0", + dump_path, + ] + completed = capture(command, timeout=timeout) + if completed.returncode != 0: + sys.stderr.buffer.write(completed.stdout) + raise RuntimeError( + "%s exited %d" % (os.path.relpath(program, REPO), completed.returncode) + ) + + try: + result = parse_metrics(completed.stdout) + except ValueError: + sys.stderr.buffer.write(completed.stdout) + raise RuntimeError( + "%s produced no execution metrics" % os.path.relpath(program, REPO) + ) from None + with open(dump_path, "rb") as stream: + result["dump"] = stream.read() + return result + + +def materialize_naive_program(text, rounds): + forms = sexpr.parse(text) + facts = [ + form + for form in forms + if not (isinstance(form, sexpr.ListExpr) and form and form[0] == "exec") + ] + rules = [ + form + for form in forms + if isinstance(form, sexpr.ListExpr) and form and form[0] == "exec" + ] + materialized = [sexpr.dump(fact) for fact in facts] + for round_number in range(rounds): + for rule_number, rule in enumerate(rules): + if len(rule) != 4: + raise ValueError("exec must have priority, pattern, and template") + priority = "(naive r%06d %s q%06d)" % ( + round_number, + sexpr.dump(rule[1]), + rule_number, + ) + materialized.append( + "(exec %s\n %s\n %s)" + % (priority, sexpr.dump(rule[2]), sexpr.dump(rule[3])) + ) + return "\n\n".join(materialized) + "\n" + + +def source_rules(text): + return [ + sexpr.dump(form) + for form in sexpr.parse(text) + if isinstance(form, sexpr.ListExpr) and form and form[0] == "exec" + ] + + +def timeout_until(deadline_ns): + if deadline_ns is None: + return None + remaining_ns = deadline_ns - time.perf_counter_ns() + if remaining_ns <= 0: + raise subprocess.TimeoutExpired("repeated-evaluation protocol", 0) + return remaining_ns / 1_000_000_000 + + +def run_source_protocol( + binary, + program, + workdir, + steps, + max_rounds, + deadline_ns=None, +): + with open(program, "r", encoding="utf-8") as stream: + rules = source_rules(stream.read()) + + totals = {field: 0 for field in METRIC_FIELDS} + if not rules: + result = run_program( + binary, + program, + os.path.join(workdir, "source.space"), + steps, + timeout=timeout_until(deadline_ns), + ) + for field in METRIC_FIELDS: + totals[field] += result[field] + totals.update( + { + "rounds": 1, + "dump": result["dump"], + "projection": sorted_projection(result["dump"], transformed=False), + } + ) + return totals + + round_program = program + previous = None + for round_number in range(1, max_rounds + 1): + result = run_program( + binary, + round_program, + os.path.join(workdir, "source-%04d.space" % round_number), + steps, + timeout=timeout_until(deadline_ns), + ) + for field in METRIC_FIELDS: + totals[field] += result[field] + projection = sorted_projection(result["dump"], transformed=False) + if projection == previous: + totals.update( + { + "rounds": round_number, + "dump": result["dump"], + "projection": projection, + } + ) + return totals + previous = projection + + round_program = os.path.join(workdir, "source-%04d.mm2" % (round_number + 1)) + with open(round_program, "wb") as stream: + stream.write(result["dump"]) + stream.write(b"\n") + stream.write("\n\n".join(rules).encode("utf-8")) + stream.write(b"\n") + raise RuntimeError( + "%s did not reach a fixed point in %d source rounds" + % (os.path.relpath(program, REPO), max_rounds) + ) + + +def run_source_to_fixpoint(binary, program, workdir, steps, max_rounds): + with open(program, "r", encoding="utf-8") as stream: + text = stream.read() + if not source_rules(text): + return run_source_protocol(binary, program, workdir, steps, max_rounds) + + pilot = run_source_protocol(binary, program, workdir, steps, max_rounds) + + measured_program = os.path.join(workdir, "source-materialized.mm2") + with open(measured_program, "w", encoding="utf-8") as stream: + stream.write(materialize_naive_program(text, pilot["rounds"])) + measured = run_program( + binary, measured_program, os.path.join(workdir, "source-measured.space"), steps + ) + measured_projection = sorted_projection(measured["dump"], transformed=False) + if measured_projection != pilot["projection"]: + line, expected, actual = first_difference( + pilot["projection"], measured_projection + ) + raise RuntimeError( + "materialized source diverged from fixed-point pilot at line %d: %r != %r" + % (line, expected, actual) + ) + measured["rounds"] = pilot["rounds"] + return measured + + +def run_source_natural(binary, program, workdir, steps, source_steps): + effective_steps = source_steps if source_steps is not None else steps + result = run_program( + binary, + program, + os.path.join(workdir, "source-natural.space"), + effective_steps, + ) + result["projection"] = sorted_projection( + result["dump"], transformed=False, strip_exec=True + ) + result["source_mode"] = "natural" + if source_steps is not None: + result["step_bound"] = source_steps + return result + + +def read_repository_path(relative, field, line_number): + if os.path.isabs(relative): + raise ValueError( + "REPOSITORY_MANIFEST_ABSOLUTE_%s: line %d" % (field, line_number) + ) + normalized = os.path.normpath(relative) + if normalized == ".." or normalized.startswith(".." + os.sep): + raise ValueError( + "REPOSITORY_MANIFEST_ESCAPES_REPO_%s: line %d" + % (field, line_number) + ) + path = os.path.join(REPO, normalized) + if not os.path.isfile(path): + raise ValueError( + "REPOSITORY_MANIFEST_MISSING_%s: line %d: %s" + % (field, line_number, relative) + ) + return path + + +def read_expected_source_steps(path): + found = None + with open(path, "r", encoding="utf-8") as stream: + for line_number, line in enumerate(stream, 1): + if not line.startswith(";"): + break + match = EXPECTED_SOURCE_STEPS_RE.match(line.rstrip("\n")) + if match is None: + continue + if found is not None: + raise ValueError( + "EXPECTED_DUPLICATE_SOURCE_STEPS: %s line %d" + % (os.path.relpath(path, REPO), line_number) + ) + found = int(match.group(1)) + return found + + +def load_repository_manifest(path=REPOSITORY_MANIFEST): + specs = [] + labels = set() + sources = set() + with open(path, "r", encoding="utf-8") as stream: + for line_number, raw_line in enumerate(stream, 1): + line = raw_line.rstrip("\n") + if not line or line.startswith("#"): + continue + fields = line.split("|") + if len(fields) != 6: + raise ValueError( + "REPOSITORY_MANIFEST_FIELDS: line %d" % line_number + ) + ( + label, + source_relative, + expected_relative, + source_mode, + steps_text, + engine_specific_text, + ) = fields + if not label or os.path.normpath(label) != label or label.startswith("."): + raise ValueError( + "REPOSITORY_MANIFEST_LABEL: line %d" % line_number + ) + if label in labels: + raise ValueError( + "REPOSITORY_MANIFEST_DUPLICATE_LABEL: line %d: %s" + % (line_number, label) + ) + if source_mode not in ("persistent", "natural"): + raise ValueError( + "REPOSITORY_MANIFEST_SOURCE_MODE: line %d: %s" + % (line_number, source_mode) + ) + if steps_text == "-": + source_steps = None + else: + try: + source_steps = int(steps_text) + except ValueError: + raise ValueError( + "REPOSITORY_MANIFEST_SOURCE_STEPS: line %d: %s" + % (line_number, steps_text) + ) from None + if source_steps <= 0: + raise ValueError( + "REPOSITORY_MANIFEST_SOURCE_STEPS: line %d: %s" + % (line_number, steps_text) + ) + if source_mode == "persistent" and source_steps is not None: + raise ValueError( + "REPOSITORY_MANIFEST_PERSISTENT_STEPS: line %d" % line_number + ) + if engine_specific_text == "-": + engine_specific_fields = () + else: + engine_specific_fields = tuple(engine_specific_text.split(",")) + if ( + len(engine_specific_fields) != len(set(engine_specific_fields)) + or not set(engine_specific_fields) + <= set(ENGINE_SPECIFIC_COUNTER_FIELDS) + ): + raise ValueError( + "REPOSITORY_MANIFEST_ENGINE_SPECIFIC_FIELDS: line %d: %s" + % (line_number, engine_specific_text) + ) + source = read_repository_path(source_relative, "SOURCE", line_number) + expected = read_repository_path( + expected_relative, "EXPECTED", line_number + ) + recorded_steps = read_expected_source_steps(expected) + if source_mode == "natural" and source_steps != recorded_steps: + raise ValueError( + "REPOSITORY_MANIFEST_EXPECTED_SOURCE_STEPS: line %d: %r != %r" + % (line_number, source_steps, recorded_steps) + ) + if source_mode == "persistent" and recorded_steps is not None: + raise ValueError( + "REPOSITORY_MANIFEST_PERSISTENT_EXPECTED_STEPS: line %d" + % line_number + ) + if source in sources: + raise ValueError( + "REPOSITORY_MANIFEST_DUPLICATE_SOURCE: line %d: %s" + % (line_number, source_relative) + ) + labels.add(label) + sources.add(source) + specs.append( + RepositorySpec( + label, + source, + expected, + source_mode, + source_steps, + engine_specific_fields, + ) + ) + if not specs: + raise ValueError("REPOSITORY_MANIFEST_EMPTY") + return specs + + +def sorted_projection(dump, transformed, strip_exec=False): + projected = [] + for line in dump.splitlines(): + if not line or line.startswith(b";"): + continue + if strip_exec and line.startswith(b"(exec "): + continue + if transformed and line.startswith(BOOKKEEPING_PREFIXES): + continue + if transformed and line.startswith(b"(f ") and line.endswith(b")"): + line = line[3:-1] + projected.append(line) + projected.sort() + if not projected: + return b"" + return b"\n".join(projected) + b"\n" + + +def first_difference(expected, actual): + expected_lines = expected.splitlines() + actual_lines = actual.splitlines() + limit = max(len(expected_lines), len(actual_lines)) + for index in range(limit): + left = expected_lines[index] if index < len(expected_lines) else b"" + right = actual_lines[index] if index < len(actual_lines) else b"" + if left != right: + return index + 1, left, right + raise AssertionError("different byte strings have no differing line") + + +def assert_no_bare_top_level_variable_facts(program): + with open(program, "r", encoding="utf-8") as stream: + expressions = sexpr.parse(stream.read()) + for form_number, expression in enumerate(expressions, 1): + if isinstance(expression, sexpr.Atom) and expression.startswith("$"): + raise ValueError( + "BARE_TOP_LEVEL_VARIABLE_FACT: %s form %d" + % (os.path.relpath(program, REPO), form_number) + ) + + +def display_metrics(label, result): + details = [] + if "rounds" in result: + details.append("rounds=%d" % result["rounds"]) + if "step_bound" in result: + details.append("step-bound=%d" % result["step_bound"]) + suffix = " " + " ".join(details) if details else "" + print( + "%s:%s steps=%d unifications=%d writes=%d transitions=%d" + % ( + label, + suffix, + result["steps"], + result["unifications"], + result["writes"], + result["transitions"], + ) + ) + + +def report_difference(label, expected, actual): + line, expected_line, actual_line = first_difference(expected, actual) + print("FAIL %s differs at sorted line %d" % (label, line)) + print("expected: %s" % expected_line.decode("utf-8", errors="replace")) + print("actual: %s" % actual_line.decode("utf-8", errors="replace")) + + +def evaluate_case( + binary, + source, + transformed, + expected, + steps, + max_source_rounds, + required=None, + engine_label=None, + source_mode="persistent", + source_steps=None, +): + assert_no_bare_top_level_variable_facts(transformed) + if source_mode == "persistent" and source_steps is not None: + raise ValueError("PERSISTENT_SOURCE_STEPS") + if source_mode not in ("persistent", "natural"): + raise ValueError("UNSUPPORTED_SOURCE_MODE: %s" % source_mode) + temp_root = os.path.join(REPO, "target", "semi_naive") + os.makedirs(temp_root, exist_ok=True) + with tempfile.TemporaryDirectory(prefix="semi-naive-", dir=temp_root) as workdir: + if source_mode == "persistent": + source_result = run_source_to_fixpoint( + binary, source, workdir, steps, max_source_rounds + ) + else: + source_result = run_source_natural( + binary, source, workdir, steps, source_steps + ) + transformed_result = run_program( + binary, + transformed, + os.path.join(workdir, "transformed.space"), + steps, + ) + + source_projection = source_result.get("projection") + if source_projection is None: + source_projection = sorted_projection( + source_result["dump"], transformed=False + ) + transformed_projection = sorted_projection( + transformed_result["dump"], transformed=True + ) + + label_prefix = "%s/" % engine_label if engine_label else "" + display_metrics(label_prefix + "source", source_result) + display_metrics(label_prefix + "transformed", transformed_result) + if transformed_result["unifications"]: + print( + "%sunification-ratio=%.6fx" + % ( + label_prefix, + source_result["unifications"] + / transformed_result["unifications"], + ) + ) + + failed = False + if source_projection != transformed_projection: + report_difference( + label_prefix + "projection", source_projection, transformed_projection + ) + failed = True + else: + print( + "OK %sprojection identical: %d bytes, %d lines" + % ( + label_prefix, + len(source_projection), + source_projection.count(b"\n"), + ) + ) + if expected is not None: + with open(expected, "rb") as stream: + expected_projection = sorted_projection(stream.read(), transformed=False) + if source_projection != expected_projection: + report_difference( + label_prefix + "expected projection", + expected_projection, + source_projection, + ) + failed = True + else: + print( + "OK %sexpected projection: %s" + % (label_prefix, os.path.relpath(expected, REPO)) + ) + if required is not None: + with open(required, "rb") as stream: + required_lines = set(stream.read().splitlines()) + if not required_lines or b"" in required_lines: + raise ValueError("required projection must contain nonempty lines") + projected_lines = set(source_projection.splitlines()) + missing = sorted(required_lines - projected_lines) + if missing: + print("FAIL %srequired projection line is absent" % label_prefix) + print("missing: %s" % missing[0].decode("utf-8", errors="replace")) + failed = True + else: + print( + "OK %srequired projection: %s" + % (label_prefix, os.path.basename(required)) + ) + return int(failed), { + "source": source_result, + "transformed": transformed_result, + "source_projection": source_projection, + "transformed_projection": transformed_projection, + } + + +def compare_cross_engine( + left_label, + left, + right_label, + right, + engine_specific_fields=(), +): + failed = False + for arm in ("source", "transformed"): + projection_key = arm + "_projection" + if left[projection_key] != right[projection_key]: + report_difference( + "cross-engine %s %s != %s" % (arm, left_label, right_label), + left[projection_key], + right[projection_key], + ) + failed = True + else: + print( + "OK cross-engine %s projection %s=%s: %d bytes, %d lines" + % ( + arm, + left_label, + right_label, + len(left[projection_key]), + left[projection_key].count(b"\n"), + ) + ) + + invariant_fields = [ + field + for field in ("steps", "unifications", "writes") + if field not in engine_specific_fields + ] + if "rounds" in left[arm] or "rounds" in right[arm]: + invariant_fields.append("rounds") + if "step_bound" in left[arm] or "step_bound" in right[arm]: + invariant_fields.append("step_bound") + mismatches = [ + field + for field in invariant_fields + if left[arm].get(field) != right[arm].get(field) + ] + if mismatches: + field = mismatches[0] + print( + "FAIL cross-engine %s counter %s differs: %s=%r, %s=%r" + % ( + arm, + field, + left_label, + left[arm].get(field), + right_label, + right[arm].get(field), + ) + ) + failed = True + else: + counters = " ".join( + "%s=%d" % (field, left[arm][field]) for field in invariant_fields + ) + specific_fields = ("transitions",) + tuple(engine_specific_fields) + specific = " ".join( + "%s %s=%d %s=%d" + % ( + field, + left_label, + left[arm][field], + right_label, + right[arm][field], + ) + for field in specific_fields + ) + print( + "OK cross-engine %s counters %s=%s: %s; %s (engine-specific)" + % ( + arm, + left_label, + right_label, + counters, + specific, + ) + ) + return int(failed) + + +def compare( + binary, + source, + transformed, + expected, + steps, + max_source_rounds, + required=None, +): + failed, _ = evaluate_case( + binary, + source, + transformed, + expected, + steps, + max_source_rounds, + required, + ) + return failed + + +def transform_program(source, output): + command = [sys.executable, os.path.join(HERE, "transform.py"), source, output] + completed = capture(command) + if completed.returncode != 0: + sys.stderr.buffer.write(completed.stdout) + raise RuntimeError( + "transform failed for %s" % os.path.relpath(source, REPO) + ) + + +def generate_benchmark_corpus(output_root): + gen_process_calculus.generate( + os.path.join(output_root, "process_calculus"), + gen_process_calculus.DEFAULT_INSTANCES, + ) + gen_transitive.generate( + os.path.join(output_root, "transitive"), + gen_transitive.DEFAULT_LENGTHS, + ) + + +def discover_cases(transformed_root, generate_all=False, benchmark_root=None): + corpus = os.path.join(HERE, "corpus") + cases = [] + roots = [(corpus, "", True)] + if benchmark_root is not None: + roots.extend( + [ + ( + os.path.join(benchmark_root, "process_calculus"), + "generated/process_calculus", + False, + ), + ( + os.path.join(benchmark_root, "transitive"), + "generated/transitive", + False, + ), + ] + ) + for source_root, label_prefix, checked in roots: + for directory, dirnames, filenames in os.walk(source_root): + dirnames.sort() + for filename in sorted(filenames): + if not filename.endswith(".source.mm2"): + continue + source = os.path.join(directory, filename) + stem = filename[: -len(".source.mm2")] + relative_directory = os.path.relpath(directory, source_root) + label = os.path.normpath( + os.path.join(label_prefix, relative_directory, filename) + ) + checked_transform = os.path.join( + directory, stem + ".transformed.mm2" + ) + if checked and not generate_all and os.path.isfile(checked_transform): + transformed = checked_transform + else: + output_group = label_prefix or "corpus" + transformed = os.path.join( + transformed_root, + output_group, + relative_directory, + stem + ".transformed.mm2", + ) + os.makedirs(os.path.dirname(transformed), exist_ok=True) + transform_program(source, transformed) + expected = None + if checked: + expected = os.path.join( + HERE, "expected", relative_directory, stem + ".expected" + ) + if not os.path.isfile(expected): + expected = None + required = os.path.join(directory, stem + ".required") + if not os.path.isfile(required): + required = None + cases.append( + OracleCase(label, source, transformed, expected, required) + ) + if not cases: + raise RuntimeError("no .source.mm2 corpus cases found") + return cases + + +def discover_repository_cases(transformed_root, manifest=REPOSITORY_MANIFEST): + cases = [] + for spec in load_repository_manifest(manifest): + transformed = os.path.join( + transformed_root, "repository", spec.label + ".transformed.mm2" + ) + os.makedirs(os.path.dirname(transformed), exist_ok=True) + transform_program(spec.source, transformed) + cases.append( + OracleCase( + "repository/" + spec.label, + spec.source, + transformed, + spec.expected, + source_mode=spec.source_mode, + source_steps=spec.source_steps, + engine_specific_fields=spec.engine_specific_fields, + ) + ) + return cases + + +def main(): + parser = argparse.ArgumentParser(description=__doc__) + parser.add_argument("source", nargs="?") + parser.add_argument("transformed", nargs="?") + parser.add_argument("--all", action="store_true") + parser.add_argument("--generate", action="store_true") + parser.add_argument( + "--suite", + action="append", + choices=("existing", "repository"), + dest="suites", + help="oracle suite; repeat to select both (default: both)", + ) + parser.add_argument("--expected") + parser.add_argument( + "--binary", + action="append", + dest="binaries", + help="mork binary; repeat exactly twice under --all for cross-engine checks", + ) + parser.add_argument("--steps", type=int, default=DEFAULT_STEPS) + parser.add_argument("--max-source-rounds", type=int, default=1024) + args = parser.parse_args() + + binaries = [os.path.abspath(path) for path in (args.binaries or [DEFAULT_BINARY])] + for binary in binaries: + if not os.access(binary, os.X_OK): + parser.error("binary is not executable: %s" % binary) + if len(binaries) > 2: + parser.error("at most two --binary values are supported") + if len(binaries) == 2: + if os.path.samefile(binaries[0], binaries[1]): + parser.error("cross-engine binaries resolve to the same file") + labels = [os.path.basename(binary) for binary in binaries] + if labels[0] == labels[1]: + parser.error("cross-engine binary basenames must be distinct") + else: + labels = [os.path.basename(binaries[0])] + if args.generate and not args.all: + parser.error("--generate requires --all") + if args.suites and not args.all: + parser.error("--suite requires --all") + suites = args.suites or ["existing", "repository"] + if len(suites) != len(set(suites)): + parser.error("duplicate --suite value") + if args.generate and "existing" not in suites: + parser.error("--generate requires the existing suite") + + try: + if args.all: + if args.source is not None or args.transformed is not None or args.expected: + parser.error("--all does not accept source, transformed, or --expected") + failed = 0 + temp_root = os.path.join(REPO, "target", "semi_naive") + os.makedirs(temp_root, exist_ok=True) + with tempfile.TemporaryDirectory( + prefix="semi-naive-generated-", dir=temp_root + ) as generated_root: + transformed_root = os.path.join(generated_root, "transforms") + cases = [] + if "existing" in suites: + benchmark_root = os.path.join(generated_root, "sources") + generate_benchmark_corpus(benchmark_root) + cases.extend( + discover_cases( + transformed_root, + generate_all=args.generate, + benchmark_root=benchmark_root, + ) + ) + if "repository" in suites: + cases.extend(discover_repository_cases(transformed_root)) + for case in cases: + print("== %s ==" % case.label) + case_failed = False + engine_results = [] + for engine_label, binary in zip(labels, binaries): + if len(binaries) == 2: + print("-- %s --" % engine_label) + engine_failed, engine_result = evaluate_case( + binary, + case.source, + case.transformed, + case.expected, + args.steps, + args.max_source_rounds, + case.required, + engine_label if len(binaries) == 2 else None, + case.source_mode, + case.source_steps, + ) + case_failed |= bool(engine_failed) + engine_results.append(engine_result) + if len(binaries) == 2: + case_failed |= bool( + compare_cross_engine( + labels[0], + engine_results[0], + labels[1], + engine_results[1], + case.engine_specific_fields, + ) + ) + failed += int(case_failed) + print("%d cases, %d failed" % (len(cases), failed)) + return 1 if failed else 0 + + if args.source is None or args.transformed is None: + parser.error("source and transformed are required unless --all is used") + if len(binaries) != 1: + parser.error("two --binary values require --all") + source = os.path.abspath(args.source) + transformed = os.path.abspath(args.transformed) + expected = os.path.abspath(args.expected) if args.expected else None + for program in (source, transformed, expected): + if program is not None and not os.path.isfile(program): + parser.error("file does not exist: %s" % program) + return compare( + binaries[0], + source, + transformed, + expected, + args.steps, + args.max_source_rounds, + ) + except (OSError, RuntimeError, ValueError) as error: + print("ERROR: %s" % error, file=sys.stderr) + return 2 + + +if __name__ == "__main__": + sys.exit(main()) diff --git a/tools/semi_naive/expected/i0/bare_whole_fact.expected b/tools/semi_naive/expected/i0/bare_whole_fact.expected new file mode 100644 index 00000000..8f43e61e --- /dev/null +++ b/tools/semi_naive/expected/i0/bare_whole_fact.expected @@ -0,0 +1,3 @@ +(cand (fact absent)) +(fact present) +(bare-hit (fact present)) diff --git a/tools/semi_naive/expected/i0/conditional_respawn.expected b/tools/semi_naive/expected/i0/conditional_respawn.expected new file mode 100644 index 00000000..9c6670fd --- /dev/null +++ b/tools/semi_naive/expected/i0/conditional_respawn.expected @@ -0,0 +1,3 @@ +(cleared item) +(worker (, (dc $a)) (O (- (dc $a)) (+ (cleared $a)))) +(controller (, (dc $a) (worker $b $c) (controller $d $e)) (, (exec 0 $b $c) (exec 1 $d $e))) diff --git a/tools/semi_naive/expected/i0/priority_order.expected b/tools/semi_naive/expected/i0/priority_order.expected new file mode 100644 index 00000000..c4949d26 --- /dev/null +++ b/tools/semi_naive/expected/i0/priority_order.expected @@ -0,0 +1 @@ +(fired priority-0) diff --git a/tools/semi_naive/expected/i0/remove_sink.expected b/tools/semi_naive/expected/i0/remove_sink.expected new file mode 100644 index 00000000..a8425f86 --- /dev/null +++ b/tools/semi_naive/expected/i0/remove_sink.expected @@ -0,0 +1,2 @@ +(removed a) +(survivor b) diff --git a/tools/semi_naive/expected/i0/wrapped_whole_fact.expected b/tools/semi_naive/expected/i0/wrapped_whole_fact.expected new file mode 100644 index 00000000..962df630 --- /dev/null +++ b/tools/semi_naive/expected/i0/wrapped_whole_fact.expected @@ -0,0 +1,3 @@ +(f (fact present)) +(cand (fact absent)) +(wrapped-hit (fact present)) diff --git a/tools/semi_naive/expected/i1/transitive_chain_004.expected b/tools/semi_naive/expected/i1/transitive_chain_004.expected new file mode 100644 index 00000000..381094d4 --- /dev/null +++ b/tools/semi_naive/expected/i1/transitive_chain_004.expected @@ -0,0 +1,10 @@ +(edge n000 n001) +(edge n000 n002) +(edge n000 n003) +(edge n000 n004) +(edge n001 n002) +(edge n001 n003) +(edge n001 n004) +(edge n002 n003) +(edge n002 n004) +(edge n003 n004) diff --git a/tools/semi_naive/expected/i3/multiple_heads.expected b/tools/semi_naive/expected/i3/multiple_heads.expected new file mode 100644 index 00000000..78c767fc --- /dev/null +++ b/tools/semi_naive/expected/i3/multiple_heads.expected @@ -0,0 +1,6 @@ +(seed a) +(seed b) +(left a) +(left b) +(right a) +(right b) diff --git a/tools/semi_naive/expected/i3/multiple_rules.expected b/tools/semi_naive/expected/i3/multiple_rules.expected new file mode 100644 index 00000000..7ff0ee98 --- /dev/null +++ b/tools/semi_naive/expected/i3/multiple_rules.expected @@ -0,0 +1,6 @@ +(seed a) +(seed b) +(mid a) +(mid b) +(out a) +(out b) diff --git a/tools/semi_naive/expected/i3/refusals.expected b/tools/semi_naive/expected/i3/refusals.expected new file mode 100644 index 00000000..678b6dd8 --- /dev/null +++ b/tools/semi_naive/expected/i3/refusals.expected @@ -0,0 +1,19 @@ +bare_pattern.mm2|UNCLASSIFIABLE_PATTERN +bare_template.mm2|UNCLASSIFIABLE_TEMPLATE +controller_variable_limit.mm2|CONTROLLER_VARIABLE_LIMIT +counted_exec_head.mm2|COUNTED_EXEC_HEAD +empty_body.mm2|EMPTY_RULE_BODY +empty_head.mm2|EMPTY_RULE_HEAD +foreign_exec_template.mm2|FOREIGN_EXEC_TEMPLATE +io_sink.mm2|IO_SINK +io_source.mm2|IO_SOURCE +malformed_exec.mm2|MALFORMED_EXEC +no_rules.mm2|NO_RULES +removal_template.mm2|REMOVAL_TEMPLATE +reserved_source_form.mm2|RESERVED_SOURCE_FORM +self_modifying_rule.mm2|SELF_MODIFYING_RULE +too_many_variables.mm2|TOO_MANY_VARIABLES +unbound_head_variable.mm2|UNBOUND_HEAD_VARIABLE +unclassifiable_fact.mm2|UNCLASSIFIABLE_FACT +variable_priority.mm2|VARIABLE_SOURCE_PRIORITY +variable_relation_pattern.mm2|UNCLASSIFIABLE_PATTERN diff --git a/tools/semi_naive/expected/i3/three_factor.expected b/tools/semi_naive/expected/i3/three_factor.expected new file mode 100644 index 00000000..ad423d1a --- /dev/null +++ b/tools/semi_naive/expected/i3/three_factor.expected @@ -0,0 +1,8 @@ +(a x) +(a y) +(b x one) +(b y two) +(c one) +(c two) +(joined x one) +(joined y two) diff --git a/tools/semi_naive/expected/i4/direct_controller.expected b/tools/semi_naive/expected/i4/direct_controller.expected new file mode 100644 index 00000000..5be1fd57 --- /dev/null +++ b/tools/semi_naive/expected/i4/direct_controller.expected @@ -0,0 +1,3 @@ +(left a) +(seed a) +(right a) diff --git a/tools/semi_naive/expected/repository/kernel/transitive.expected b/tools/semi_naive/expected/repository/kernel/transitive.expected new file mode 100644 index 00000000..a9eb65a4 --- /dev/null +++ b/tools/semi_naive/expected/repository/kernel/transitive.expected @@ -0,0 +1,150 @@ +(edge brussels brussels) +(edge brussels istanbul) +(edge brussels london) +(edge brussels paris) +(edge brussels st-petersburg) +(edge istanbul brussels) +(edge istanbul istanbul) +(edge istanbul london) +(edge istanbul paris) +(edge istanbul st-petersburg) +(edge london brussels) +(edge london istanbul) +(edge london london) +(edge london paris) +(edge london st-petersburg) +(edge paris brussels) +(edge paris istanbul) +(edge paris london) +(edge paris paris) +(edge paris st-petersburg) +(edge st-petersburg brussels) +(edge st-petersburg istanbul) +(edge st-petersburg london) +(edge st-petersburg paris) +(edge st-petersburg st-petersburg) +(triangle brussels brussels brussels) +(triangle brussels brussels istanbul) +(triangle brussels brussels london) +(triangle brussels brussels paris) +(triangle brussels brussels st-petersburg) +(triangle brussels istanbul brussels) +(triangle brussels istanbul istanbul) +(triangle brussels istanbul london) +(triangle brussels istanbul paris) +(triangle brussels istanbul st-petersburg) +(triangle brussels london brussels) +(triangle brussels london istanbul) +(triangle brussels london london) +(triangle brussels london paris) +(triangle brussels london st-petersburg) +(triangle brussels paris brussels) +(triangle brussels paris istanbul) +(triangle brussels paris london) +(triangle brussels paris paris) +(triangle brussels paris st-petersburg) +(triangle brussels st-petersburg brussels) +(triangle brussels st-petersburg istanbul) +(triangle brussels st-petersburg london) +(triangle brussels st-petersburg paris) +(triangle brussels st-petersburg st-petersburg) +(triangle istanbul brussels brussels) +(triangle istanbul brussels istanbul) +(triangle istanbul brussels london) +(triangle istanbul brussels paris) +(triangle istanbul brussels st-petersburg) +(triangle istanbul istanbul brussels) +(triangle istanbul istanbul istanbul) +(triangle istanbul istanbul london) +(triangle istanbul istanbul paris) +(triangle istanbul istanbul st-petersburg) +(triangle istanbul london brussels) +(triangle istanbul london istanbul) +(triangle istanbul london london) +(triangle istanbul london paris) +(triangle istanbul london st-petersburg) +(triangle istanbul paris brussels) +(triangle istanbul paris istanbul) +(triangle istanbul paris london) +(triangle istanbul paris paris) +(triangle istanbul paris st-petersburg) +(triangle istanbul st-petersburg brussels) +(triangle istanbul st-petersburg istanbul) +(triangle istanbul st-petersburg london) +(triangle istanbul st-petersburg paris) +(triangle istanbul st-petersburg st-petersburg) +(triangle london brussels brussels) +(triangle london brussels istanbul) +(triangle london brussels london) +(triangle london brussels paris) +(triangle london brussels st-petersburg) +(triangle london istanbul brussels) +(triangle london istanbul istanbul) +(triangle london istanbul london) +(triangle london istanbul paris) +(triangle london istanbul st-petersburg) +(triangle london london brussels) +(triangle london london istanbul) +(triangle london london london) +(triangle london london paris) +(triangle london london st-petersburg) +(triangle london paris brussels) +(triangle london paris istanbul) +(triangle london paris london) +(triangle london paris paris) +(triangle london paris st-petersburg) +(triangle london st-petersburg brussels) +(triangle london st-petersburg istanbul) +(triangle london st-petersburg london) +(triangle london st-petersburg paris) +(triangle london st-petersburg st-petersburg) +(triangle paris brussels brussels) +(triangle paris brussels istanbul) +(triangle paris brussels london) +(triangle paris brussels paris) +(triangle paris brussels st-petersburg) +(triangle paris istanbul brussels) +(triangle paris istanbul istanbul) +(triangle paris istanbul london) +(triangle paris istanbul paris) +(triangle paris istanbul st-petersburg) +(triangle paris london brussels) +(triangle paris london istanbul) +(triangle paris london london) +(triangle paris london paris) +(triangle paris london st-petersburg) +(triangle paris paris brussels) +(triangle paris paris istanbul) +(triangle paris paris london) +(triangle paris paris paris) +(triangle paris paris st-petersburg) +(triangle paris st-petersburg brussels) +(triangle paris st-petersburg istanbul) +(triangle paris st-petersburg london) +(triangle paris st-petersburg paris) +(triangle paris st-petersburg st-petersburg) +(triangle st-petersburg brussels brussels) +(triangle st-petersburg brussels istanbul) +(triangle st-petersburg brussels london) +(triangle st-petersburg brussels paris) +(triangle st-petersburg brussels st-petersburg) +(triangle st-petersburg istanbul brussels) +(triangle st-petersburg istanbul istanbul) +(triangle st-petersburg istanbul london) +(triangle st-petersburg istanbul paris) +(triangle st-petersburg istanbul st-petersburg) +(triangle st-petersburg london brussels) +(triangle st-petersburg london istanbul) +(triangle st-petersburg london london) +(triangle st-petersburg london paris) +(triangle st-petersburg london st-petersburg) +(triangle st-petersburg paris brussels) +(triangle st-petersburg paris istanbul) +(triangle st-petersburg paris london) +(triangle st-petersburg paris paris) +(triangle st-petersburg paris st-petersburg) +(triangle st-petersburg st-petersburg brussels) +(triangle st-petersburg st-petersburg istanbul) +(triangle st-petersburg st-petersburg london) +(triangle st-petersburg st-petersburg paris) +(triangle st-petersburg st-petersburg st-petersburg) diff --git a/tools/semi_naive/expected/repository/programs/lens_aunt.expected b/tools/semi_naive/expected/repository/programs/lens_aunt.expected new file mode 100644 index 00000000..0a8fe391 --- /dev/null +++ b/tools/semi_naive/expected/repository/programs/lens_aunt.expected @@ -0,0 +1,68 @@ +;; @source-steps 1 +(data (poi Ann)) +(data (poi Jim)) +(data (result (Ann aunt of Jim))) +(data (result (Liz aunt of Ann))) +(male Bob) +(male Jim) +(male Tom) +(female Ann) +(female Liz) +(female Pam) +(female Pat) +(Ann != Bob) +(Ann != Jim) +(Ann != Liz) +(Ann != Pam) +(Ann != Pat) +(Ann != Tom) +(Ann == Ann) +(Bob != Ann) +(Bob != Jim) +(Bob != Liz) +(Bob != Pam) +(Bob != Pat) +(Bob != Tom) +(Bob == Bob) +(Jim != Ann) +(Jim != Bob) +(Jim != Liz) +(Jim != Pam) +(Jim != Pat) +(Jim != Tom) +(Jim == Jim) +(Liz != Ann) +(Liz != Bob) +(Liz != Jim) +(Liz != Pam) +(Liz != Pat) +(Liz != Tom) +(Liz == Liz) +(Pam != Ann) +(Pam != Bob) +(Pam != Jim) +(Pam != Liz) +(Pam != Pat) +(Pam != Tom) +(Pam == Pam) +(Pat != Ann) +(Pat != Bob) +(Pat != Jim) +(Pat != Liz) +(Pat != Pam) +(Pat != Tom) +(Pat == Pat) +(Tom != Ann) +(Tom != Bob) +(Tom != Jim) +(Tom != Liz) +(Tom != Pam) +(Tom != Pat) +(Tom == Tom) +(parent Bob Ann) +(parent Bob Pat) +(parent Pam Bob) +(parent Pat Jim) +(parent Tom Bob) +(parent Tom Liz) +(aunt (poi $a) $a $b (result ($b aunt of $a))) diff --git a/tools/semi_naive/expected/repository/wiki/mm2_basics_02.expected b/tools/semi_naive/expected/repository/wiki/mm2_basics_02.expected new file mode 100644 index 00000000..e69de29b diff --git a/tools/semi_naive/expected/repository/wiki/reachability_p1_13.expected b/tools/semi_naive/expected/repository/wiki/reachability_p1_13.expected new file mode 100644 index 00000000..a4757701 --- /dev/null +++ b/tools/semi_naive/expected/repository/wiki/reachability_p1_13.expected @@ -0,0 +1,40 @@ +(ancestor Ann Bob) +(ancestor Ann Fred) +(ancestor Ann Pam) +(ancestor Ann Tom) +(ancestor Vic Whu) +(ancestor Vic Zac) +(child Ann Bob) +(child Bob Pam) +(child Bob Tom) +(child Jim Pat) +(child Liz Tom) +(child Ohm Uru) +(child Ohm Vic) +(child Pat Bob) +(child Tom Fred) +(child Uru Xey) +(child Uru Yip) +(child Vic Whu) +(child Vic Zac) +(generation (S (S Z)) Ann Fred) +(generation (S Z) Ann Pam) +(generation (S Z) Ann Tom) +(generation Z Ann Bob) +(generation Z Vic Whu) +(generation Z Vic Zac) +(parent Bob Ann) +(parent Bob Pat) +(parent Fred Tom) +(parent Pam Bob) +(parent Pat Jim) +(parent Tom Bob) +(parent Tom Liz) +(parent Uru Ohm) +(parent Vic Ohm) +(parent Whu Vic) +(parent Xey Uru) +(parent Yip Uru) +(parent Zac Vic) +(poi Ann) +(poi Vic) diff --git a/tools/semi_naive/expected/repository/wiki/reachability_p2_06.expected b/tools/semi_naive/expected/repository/wiki/reachability_p2_06.expected new file mode 100644 index 00000000..e69de29b diff --git a/tools/semi_naive/expected/repository/wiki/reachability_p2_07.expected b/tools/semi_naive/expected/repository/wiki/reachability_p2_07.expected new file mode 100644 index 00000000..e69de29b diff --git a/tools/semi_naive/expected/repository/wiki/reachability_p2_08.expected b/tools/semi_naive/expected/repository/wiki/reachability_p2_08.expected new file mode 100644 index 00000000..e69de29b diff --git a/tools/semi_naive/expected/repository/wiki/reachability_p3_03.expected b/tools/semi_naive/expected/repository/wiki/reachability_p3_03.expected new file mode 100644 index 00000000..e69de29b diff --git a/tools/semi_naive/expected/repository/wiki/reachability_p3_04.expected b/tools/semi_naive/expected/repository/wiki/reachability_p3_04.expected new file mode 100644 index 00000000..e69de29b diff --git a/tools/semi_naive/expected/repository/wiki/reachability_p3_09.expected b/tools/semi_naive/expected/repository/wiki/reachability_p3_09.expected new file mode 100644 index 00000000..e69de29b diff --git a/tools/semi_naive/expected/repository/wiki/reachability_p3_12.expected b/tools/semi_naive/expected/repository/wiki/reachability_p3_12.expected new file mode 100644 index 00000000..e69de29b diff --git a/tools/semi_naive/expected/repository/wiki/reachability_p4_03.expected b/tools/semi_naive/expected/repository/wiki/reachability_p4_03.expected new file mode 100644 index 00000000..e69de29b diff --git a/tools/semi_naive/generators/gen_process_calculus.py b/tools/semi_naive/generators/gen_process_calculus.py new file mode 100755 index 00000000..e7282f46 --- /dev/null +++ b/tools/semi_naive/generators/gen_process_calculus.py @@ -0,0 +1,80 @@ +#!/usr/bin/env python3 +"""Emit persistent-rule instances of MORK's process-calculus benchmark.""" + +import argparse +import os + + +DEFAULT_INSTANCES = ((32, 32), (64, 64), (128, 128), (200, 200), (320, 320)) + +TEMPLATE = """\ +; Process-calculus addition from `process_calculus_bench`. +; The benchmark's idle rules and IC controller are represented as persistent rules. + +(exec 0 + (, (petri (? $channel $payload $body)) + (petri (! $channel $payload))) + (, (petri $body))) + +(exec 1 + (, (petri (| $left $right))) + (, (petri $left) + (petri $right))) + +(petri (? (add $ret) ((S $x) $y) + (| (! (add (PN $x $y)) ($x $y)) + (? (PN $x $y) $z (! $ret (S $z)))))) +(petri (? (add $ret) (Z $y) (! $ret $y))) +(petri (! (add result) (%(x)s %(y)s))) +""" + + +def peano(value): + return "(S " * value + "Z" + ")" * value + + +def parse_instance(value): + try: + left, right = (int(part) for part in value.split(":", 1)) + except ValueError as error: + raise argparse.ArgumentTypeError("expected LEFT:RIGHT") from error + if left < 0 or right < 0: + raise argparse.ArgumentTypeError("operands must be nonnegative") + return left, right + + +def generate(output_directory, instances): + os.makedirs(output_directory, exist_ok=True) + paths = [] + for left, right in instances: + path = os.path.join( + output_directory, + "process_calculus_%03d_%03d.source.mm2" % (left, right), + ) + with open(path, "w", encoding="utf-8", newline="\n") as stream: + stream.write(TEMPLATE % {"x": peano(left), "y": peano(right)}) + required_path = path[: -len(".source.mm2")] + ".required" + with open(required_path, "w", encoding="utf-8", newline="\n") as stream: + stream.write("(petri (! result %s))\n" % peano(left + right)) + paths.append(path) + return paths + + +def main(): + parser = argparse.ArgumentParser(description=__doc__) + parser.add_argument("output_directory") + parser.add_argument( + "--instance", + action="append", + type=parse_instance, + dest="instances", + help="operand pair LEFT:RIGHT; repeat for multiple programs", + ) + args = parser.parse_args() + for path in generate(args.output_directory, args.instances or DEFAULT_INSTANCES): + print(path) + return 0 + + +if __name__ == "__main__": + raise SystemExit(main()) diff --git a/tools/semi_naive/generators/gen_transitive.py b/tools/semi_naive/generators/gen_transitive.py new file mode 100755 index 00000000..0d12d13c --- /dev/null +++ b/tools/semi_naive/generators/gen_transitive.py @@ -0,0 +1,58 @@ +#!/usr/bin/env python3 +"""Emit chain transitive-closure programs at deterministic sizes.""" + +import argparse +import os + + +DEFAULT_LENGTHS = (64, 128, 256, 384) + +RULE = """\ + +(exec 0 + (, (edge $x $y) (edge $y $z)) + (, (edge $x $z))) +""" + + +def positive_integer(value): + parsed = int(value) + if parsed <= 0: + raise argparse.ArgumentTypeError("length must be positive") + return parsed + + +def generate(output_directory, lengths): + os.makedirs(output_directory, exist_ok=True) + paths = [] + for length in lengths: + path = os.path.join( + output_directory, "transitive_chain_%03d.source.mm2" % length + ) + with open(path, "w", encoding="utf-8", newline="\n") as stream: + stream.write("; %d-edge transitive-closure chain.\n\n" % length) + for index in range(length): + stream.write("(edge n%03d n%03d)\n" % (index, index + 1)) + stream.write(RULE) + paths.append(path) + return paths + + +def main(): + parser = argparse.ArgumentParser(description=__doc__) + parser.add_argument("output_directory") + parser.add_argument( + "--length", + action="append", + type=positive_integer, + dest="lengths", + help="chain edge count; repeat for multiple programs", + ) + args = parser.parse_args() + for path in generate(args.output_directory, args.lengths or DEFAULT_LENGTHS): + print(path) + return 0 + + +if __name__ == "__main__": + raise SystemExit(main()) diff --git a/tools/semi_naive/repository_bench.py b/tools/semi_naive/repository_bench.py new file mode 100644 index 00000000..b6fcc3e8 --- /dev/null +++ b/tools/semi_naive/repository_bench.py @@ -0,0 +1,216 @@ +#!/usr/bin/env python3 +"""Measure repository-corpus source and transformed counters under both engines.""" + +import argparse +import contextlib +import io +import os +import sys +import tempfile + + +HERE = os.path.dirname(os.path.abspath(__file__)) +REPO = os.path.dirname(os.path.dirname(HERE)) +sys.path.insert(0, HERE) +import bench +import driver + + +DEFAULT_REPEATS = 3 +COUNTER_FIELDS = ("steps", "unifications", "writes", "transitions") + + +def counter_record(result): + record = {field: result[field] for field in COUNTER_FIELDS} + if "rounds" in result: + record["rounds"] = result["rounds"] + return record + + +def verify_repeat(reference, actual, context): + for arm in ("source", "transformed"): + expected = counter_record(reference[arm]) + observed = counter_record(actual[arm]) + if observed != expected: + raise RuntimeError( + "NONDETERMINISTIC_COUNTERS: %s %s: %r != %r" + % (context, arm, expected, observed) + ) + projection_key = arm + "_projection" + if actual[projection_key] != reference[projection_key]: + raise RuntimeError( + "NONDETERMINISTIC_PROJECTION: %s %s" % (context, arm) + ) + + +def verdict(source, transformed, source_mode="persistent"): + if source_mode == "natural": + return "BOUNDED_SOURCE" + if source.get("rounds", 0) <= 2: + return "NEUTRAL_SHORT" + if transformed["unifications"] < source["unifications"]: + return "FEWER_UNIFICATIONS" + if transformed["unifications"] == source["unifications"]: + return "NEUTRAL_COUNTER" + return "OVERHEAD" + + +def run_case(case, binaries, repeats, max_source_rounds): + samples = {engine: [] for engine in bench.ENGINE_ORDER} + for repeat in range(1, repeats + 1): + for engine in bench.ENGINE_ORDER: + captured = io.StringIO() + with contextlib.redirect_stdout(captured): + failed, result = driver.evaluate_case( + binaries[engine], + case.source, + case.transformed, + case.expected, + driver.DEFAULT_STEPS, + max_source_rounds, + case.required, + engine, + case.source_mode, + case.source_steps, + ) + if failed: + raise RuntimeError( + "ORACLE_FAILURE: %s %s repeat %d\n%s" + % (case.label, engine, repeat, captured.getvalue()) + ) + if samples[engine]: + verify_repeat( + samples[engine][0], + result, + "%s %s repeat %d" % (case.label, engine, repeat), + ) + samples[engine].append(result) + + first = {engine: samples[engine][0] for engine in bench.ENGINE_ORDER} + captured = io.StringIO() + with contextlib.redirect_stdout(captured): + failed = driver.compare_cross_engine( + "pz", + first["pz"], + "lf", + first["lf"], + case.engine_specific_fields, + ) + if failed: + raise RuntimeError( + "CROSS_ENGINE_FAILURE: %s\n%s" % (case.label, captured.getvalue()) + ) + + return { + "case": case.label, + "source_mode": case.source_mode, + "source_steps": case.source_steps, + "engine_specific_fields": list(case.engine_specific_fields), + "verdict": verdict( + first["pz"]["source"], + first["pz"]["transformed"], + case.source_mode, + ), + "engines": { + engine: { + "source": counter_record(first[engine]["source"]), + "transformed": counter_record(first[engine]["transformed"]), + } + for engine in bench.ENGINE_ORDER + }, + } + + +def render_table(rows): + lines = [ + "| Case | Engine | Source rounds | Source steps | Source unifications | " + "Source writes | Source transitions | Transformed steps | " + "Transformed unifications | Transformed writes | Transformed transitions | " + "Verdict |", + "| :--- | :--- | ---: | ---: | ---: | ---: | ---: | ---: | ---: | ---: | ---: | :--- |", + ] + for row in rows: + for engine in bench.ENGINE_ORDER: + source = row["engines"][engine]["source"] + transformed = row["engines"][engine]["transformed"] + lines.append( + "| %s | %s | %s | %d | %d | %d | %d | %d | %d | %d | %d | %s |" + % ( + row["case"], + engine.upper(), + source.get("rounds", "-"), + source["steps"], + source["unifications"], + source["writes"], + source["transitions"], + transformed["steps"], + transformed["unifications"], + transformed["writes"], + transformed["transitions"], + row["verdict"], + ) + ) + return "\n".join(lines) + "\n" + + +def artifact(rows, binaries, repeats): + return { + "schema": 1, + "git_head": bench.git_head(), + "repeats": repeats, + "binary_sha256": { + engine: bench.sha256_file(binary) + for engine, binary in binaries.items() + }, + "results": rows, + } + + +def main(): + parser = argparse.ArgumentParser(description=__doc__) + parser.add_argument("--pz-binary", default=bench.DEFAULT_PZ_BINARY) + parser.add_argument("--lf-binary", default=bench.DEFAULT_LF_BINARY) + parser.add_argument("--repeats", type=bench.positive_integer, default=DEFAULT_REPEATS) + parser.add_argument( + "--max-source-rounds", + type=bench.positive_integer, + default=bench.DEFAULT_MAX_SOURCE_ROUNDS, + ) + parser.add_argument("--json") + args = parser.parse_args() + + try: + binaries = bench.validate_binaries( + {"pz": args.pz_binary, "lf": args.lf_binary}, + bench.ENGINE_ORDER, + ) + temp_root = os.path.join(REPO, "target", "semi_naive") + os.makedirs(temp_root, exist_ok=True) + with tempfile.TemporaryDirectory( + prefix="semi-naive-repository-bench-", dir=temp_root + ) as workdir: + cases = driver.discover_repository_cases( + os.path.join(workdir, "transforms") + ) + rows = [ + run_case(case, binaries, args.repeats, args.max_source_rounds) + for case in cases + ] + if args.json: + bench.atomic_write_json( + os.path.abspath(args.json), artifact(rows, binaries, args.repeats) + ) + sys.stdout.write(render_table(rows)) + print( + "BENCHMARKED %d cases x 2 engines x %d repeats; " + "projections and counters deterministic" + % (len(rows), args.repeats) + ) + return 0 + except (bench.BenchmarkRefusal, OSError, RuntimeError, ValueError) as error: + print("ERROR: %s" % error, file=sys.stderr) + return 2 + + +if __name__ == "__main__": + sys.exit(main()) diff --git a/tools/semi_naive/sexpr.py b/tools/semi_naive/sexpr.py new file mode 100644 index 00000000..3845d6af --- /dev/null +++ b/tools/semi_naive/sexpr.py @@ -0,0 +1,132 @@ +"""MM2-compatible S-expression reader and deterministic writer.""" + + +class ParseError(ValueError): + pass + + +class Atom(str): + pass + + +class ListExpr(tuple): + pass + + +def tokenize(text): + index = 0 + line = 1 + column = 1 + length = len(text) + + while index < length: + character = text[index] + if character in " \t\n": + if character == "\n": + line += 1 + column = 1 + else: + column += 1 + index += 1 + continue + if character == ";": + while index < length and text[index] != "\n": + index += 1 + column += 1 + continue + if character in "()": + yield character, line, column + index += 1 + column += 1 + continue + + start = index + start_line = line + start_column = column + if character == '"': + index += 1 + column += 1 + escaped = False + while index < length: + character = text[index] + index += 1 + column += 1 + if escaped: + escaped = False + elif character == "\\": + escaped = True + elif character == '"': + break + elif character == "\n": + line += 1 + column = 1 + else: + raise ParseError( + "unterminated string at line %d, column %d" + % (start_line, start_column) + ) + else: + while index < length and text[index] not in "() \t\n": + index += 1 + column += 1 + yield text[start:index], start_line, start_column + + +def parse(text): + roots = [] + stack = [] + for token, line, column in tokenize(text): + if token == "(": + stack.append([]) + elif token == ")": + if not stack: + raise ParseError( + "unexpected ')' at line %d, column %d" % (line, column) + ) + expression = ListExpr(stack.pop()) + if stack: + stack[-1].append(expression) + else: + roots.append(expression) + else: + atom = Atom(token) + if stack: + stack[-1].append(atom) + else: + roots.append(atom) + if stack: + raise ParseError("unterminated expression at end of input") + return roots + + +def dump(expression, render_atom=str): + rendered = [] + stack = [expression] + while stack: + node = stack.pop() + if isinstance(node, ListExpr): + rendered.append("(") + stack.append(")") + for index in range(len(node) - 1, -1, -1): + stack.append(node[index]) + if index > 0: + stack.append(" ") + elif isinstance(node, Atom): + rendered.append(render_atom(node)) + elif isinstance(node, str): + rendered.append(node) + else: + raise TypeError("not an S-expression node: %r" % (node,)) + return "".join(rendered) + + +def dumps(expressions): + return "\n".join(dump(expression) for expression in expressions) + "\n" + + +def atom(value): + return Atom(str(value)) + + +def list_expr(*items): + return ListExpr(items) diff --git a/tools/semi_naive/test_acceptance_sweep.py b/tools/semi_naive/test_acceptance_sweep.py new file mode 100644 index 00000000..9a3666c9 --- /dev/null +++ b/tools/semi_naive/test_acceptance_sweep.py @@ -0,0 +1,242 @@ +#!/usr/bin/env python3 + +import glob +import os +import sys +import unittest + + +HERE = os.path.dirname(os.path.abspath(__file__)) +REPO = os.path.dirname(os.path.dirname(HERE)) +sys.path.insert(0, HERE) +import sexpr +import transform + + +EXPECTED_BEFORE = { + "kernel/resources/ancestor.mm2": "UNCLASSIFIABLE_PATTERN", + "kernel/resources/counter_machine_5.mm2": "UNCLASSIFIABLE_FACT", + "kernel/resources/decision_tree_learning.mm2": "UNCLASSIFIABLE_TEMPLATE", + "kernel/resources/decision_tree_learning_without_min_sink.mm2": "UNCLASSIFIABLE_TEMPLATE", + "kernel/resources/grounding.mm2": "IO_SINK", + "kernel/resources/ip_sudoku.mm2": "IO_SINK", + "kernel/resources/odd_even_sort.mm2": "UNCLASSIFIABLE_FACT", + "kernel/resources/std.mm2": "NO_RULES", + "kernel/resources/string_convert.mm2": "ACCEPT", + "kernel/resources/transitive.mm2": "ACCEPT", + "kernel/resources/zip_add.mm2": "NO_RULES", + "differential/corpus/programs/bc0.mm2": "UNCLASSIFIABLE_FACT", + "differential/corpus/programs/bfc7.mm2": "UNCLASSIFIABLE_TEMPLATE", + "differential/corpus/programs/cross_join_dict.mm2": "ACCEPT", + "differential/corpus/programs/cross_join_tuple.mm2": "ACCEPT", + "differential/corpus/programs/ctl.mm2": "UNCLASSIFIABLE_PATTERN", + "differential/corpus/programs/exponential.mm2": "UNCLASSIFIABLE_FACT", + "differential/corpus/programs/exponential_fringe.mm2": "UNCLASSIFIABLE_FACT", + "differential/corpus/programs/lens_aunt.mm2": "UNCLASSIFIABLE_PATTERN", + "differential/corpus/programs/lens_composition.mm2": "ACCEPT", + "differential/corpus/programs/meta_ana.mm2": "REMOVAL_TEMPLATE", + "differential/corpus/programs/meta_ana_exec.mm2": "UNCLASSIFIABLE_FACT", + "differential/corpus/programs/pattern_mining.mm2": "ACCEPT", + "differential/corpus/programs/process_calculus_reverse.mm2": "UNCLASSIFIABLE_PATTERN", + "differential/corpus/programs/roman_disjoin_final.mm2": "REMOVAL_TEMPLATE", + "differential/corpus/programs/stv_roman.mm2": "ACCEPT", + "differential/corpus/unify/bipolar.mm2": "UNCLASSIFIABLE_TEMPLATE", + "differential/corpus/unify/bipolar_equal.mm2": "UNCLASSIFIABLE_TEMPLATE", + "differential/corpus/unify/coref_absorbed_by_data_varref.mm2": "ACCEPT", + "differential/corpus/unify/data_varref_absorbs_query_compound_newvars.mm2": "UNCLASSIFIABLE_TEMPLATE", + "differential/corpus/unify/func_type_unification.mm2": "ACCEPT", + "differential/corpus/unify/issue_43.mm2": "UNCLASSIFIABLE_FACT", + "differential/corpus/unify/large_statement.mm2": "UNCLASSIFIABLE_PATTERN", + "differential/corpus/unify/lookup.mm2": "UNCLASSIFIABLE_TEMPLATE", + "differential/corpus/unify/negative.mm2": "UNCLASSIFIABLE_TEMPLATE", + "differential/corpus/unify/negative_equal.mm2": "UNCLASSIFIABLE_TEMPLATE", + "differential/corpus/unify/positive.mm2": "UNCLASSIFIABLE_TEMPLATE", + "differential/corpus/unify/positive_equal.mm2": "UNCLASSIFIABLE_TEMPLATE", + "differential/corpus/unify/roman_disjoin_initial.mm2": "REMOVAL_TEMPLATE", + "differential/corpus/unify/top_level_match.mm2": "UNCLASSIFIABLE_FACT", + "differential/corpus/unify/top_level_symbol.mm2": "UNCLASSIFIABLE_FACT", + "differential/corpus/unify/two_bipolar_equal_crossed.mm2": "ACCEPT", + "differential/corpus/unify/two_positive_equal.mm2": "UNCLASSIFIABLE_TEMPLATE", + "differential/corpus/unify/two_positive_equal_crossed.mm2": "UNCLASSIFIABLE_TEMPLATE", + "differential/corpus/unify/variable_priority.mm2": "VARIABLE_SOURCE_PRIORITY", + "differential/corpus/unify/variables_in_priority.mm2": "VARIABLE_SOURCE_PRIORITY", +} + +EXPECTED_AFTER = dict(EXPECTED_BEFORE) +EXPECTED_AFTER.update( + { + "differential/corpus/programs/bc0.mm2": "FOREIGN_EXEC_TEMPLATE", + "differential/corpus/programs/bfc7.mm2": "FOREIGN_EXEC_TEMPLATE", + "differential/corpus/programs/ctl.mm2": "SELF_MODIFYING_RULE", + "differential/corpus/programs/exponential.mm2": "FOREIGN_EXEC_TEMPLATE", + "differential/corpus/programs/exponential_fringe.mm2": "SELF_MODIFYING_RULE", + "differential/corpus/programs/lens_aunt.mm2": "ACCEPT", + "differential/corpus/programs/meta_ana.mm2": "FOREIGN_EXEC_TEMPLATE", + "differential/corpus/programs/meta_ana_exec.mm2": "FOREIGN_EXEC_TEMPLATE", + "differential/corpus/programs/process_calculus_reverse.mm2": "SELF_MODIFYING_RULE", + "differential/corpus/unify/large_statement.mm2": "FOREIGN_EXEC_TEMPLATE", + "kernel/resources/ancestor.mm2": "SELF_MODIFYING_RULE", + "kernel/resources/counter_machine_5.mm2": "SELF_MODIFYING_RULE", + "kernel/resources/decision_tree_learning.mm2": "FOREIGN_EXEC_TEMPLATE", + "kernel/resources/decision_tree_learning_without_min_sink.mm2": "FOREIGN_EXEC_TEMPLATE", + "kernel/resources/ip_sudoku.mm2": "SELF_MODIFYING_RULE", + "kernel/resources/odd_even_sort.mm2": "FOREIGN_EXEC_TEMPLATE", + } +) + +EXPECTED_WIKI = { + "differential/corpus/wiki/comment_before_closing_bracket.mm2": "NO_RULES", + "differential/corpus/wiki/ctl_model_checking_01.mm2": "SELF_MODIFYING_RULE", + "differential/corpus/wiki/hexlife_04.mm2": "IO_SINK", + "differential/corpus/wiki/hexlife_07.mm2": "IO_SINK", + "differential/corpus/wiki/hexlife_08.mm2": "REMOVAL_TEMPLATE", + "differential/corpus/wiki/hexlife_09.mm2": "REMOVAL_TEMPLATE", + "differential/corpus/wiki/mm2_basics_02.mm2": "ACCEPT", + "differential/corpus/wiki/mm2_basics_04.mm2": "UNCLASSIFIABLE_FACT", + "differential/corpus/wiki/mm2_basics_05.mm2": "ACCEPT", + "differential/corpus/wiki/reachability_p1_07.mm2": "SELF_MODIFYING_RULE", + "differential/corpus/wiki/reachability_p1_09.mm2": "SELF_MODIFYING_RULE", + "differential/corpus/wiki/reachability_p1_10.mm2": "SELF_MODIFYING_RULE", + "differential/corpus/wiki/reachability_p1_11.mm2": "SELF_MODIFYING_RULE", + "differential/corpus/wiki/reachability_p1_12.mm2": "SELF_MODIFYING_RULE", + "differential/corpus/wiki/reachability_p1_13.mm2": "ACCEPT", + "differential/corpus/wiki/reachability_p1_16.mm2": "SELF_MODIFYING_RULE", + "differential/corpus/wiki/reachability_p1_18.mm2": "SELF_MODIFYING_RULE", + "differential/corpus/wiki/reachability_p2_04.mm2": "REMOVAL_TEMPLATE", + "differential/corpus/wiki/reachability_p2_05.mm2": "IO_SINK", + "differential/corpus/wiki/reachability_p2_06.mm2": "ACCEPT", + "differential/corpus/wiki/reachability_p2_07.mm2": "ACCEPT", + "differential/corpus/wiki/reachability_p2_08.mm2": "ACCEPT", + "differential/corpus/wiki/reachability_p2_10.mm2": "FOREIGN_EXEC_TEMPLATE", + "differential/corpus/wiki/reachability_p2_13.mm2": "FOREIGN_EXEC_TEMPLATE", + "differential/corpus/wiki/reachability_p2_14.mm2": "FOREIGN_EXEC_TEMPLATE", + "differential/corpus/wiki/reachability_p2_15.mm2": "FOREIGN_EXEC_TEMPLATE", + "differential/corpus/wiki/reachability_p2_16.mm2": "FOREIGN_EXEC_TEMPLATE", + "differential/corpus/wiki/reachability_p2_17.mm2": "FOREIGN_EXEC_TEMPLATE", + "differential/corpus/wiki/reachability_p2_18.mm2": "FOREIGN_EXEC_TEMPLATE", + "differential/corpus/wiki/reachability_p2_19.mm2": "FOREIGN_EXEC_TEMPLATE", + "differential/corpus/wiki/reachability_p2_20.mm2": "FOREIGN_EXEC_TEMPLATE", + "differential/corpus/wiki/reachability_p2_21.mm2": "FOREIGN_EXEC_TEMPLATE", + "differential/corpus/wiki/reachability_p2_23.mm2": "FOREIGN_EXEC_TEMPLATE", + "differential/corpus/wiki/reachability_p3_03.mm2": "ACCEPT", + "differential/corpus/wiki/reachability_p3_04.mm2": "ACCEPT", + "differential/corpus/wiki/reachability_p3_06.mm2": "UNCLASSIFIABLE_PATTERN", + "differential/corpus/wiki/reachability_p3_09.mm2": "ACCEPT", + "differential/corpus/wiki/reachability_p3_10.mm2": "COUNTED_EXEC_HEAD", + "differential/corpus/wiki/reachability_p3_11.mm2": "COUNTED_EXEC_HEAD", + "differential/corpus/wiki/reachability_p3_12.mm2": "ACCEPT", + "differential/corpus/wiki/reachability_p3_13.mm2": "SELF_MODIFYING_RULE", + "differential/corpus/wiki/reachability_p3_14.mm2": "SELF_MODIFYING_RULE", + "differential/corpus/wiki/reachability_p3_15.mm2": "SELF_MODIFYING_RULE", + "differential/corpus/wiki/reachability_p3_16.mm2": "SELF_MODIFYING_RULE", + "differential/corpus/wiki/reachability_p3_17.mm2": "SELF_MODIFYING_RULE", + "differential/corpus/wiki/reachability_p3_18.mm2": "ACCEPT", + "differential/corpus/wiki/reachability_p4_03.mm2": "ACCEPT", + "differential/corpus/wiki/reachability_p4_04.mm2": "REMOVAL_TEMPLATE", + "differential/corpus/wiki/reachability_p4_05.mm2": "SELF_MODIFYING_RULE", + "differential/corpus/wiki/reachability_p4_06.mm2": "SELF_MODIFYING_RULE", + "differential/corpus/wiki/reachability_p4_07.mm2": "SELF_MODIFYING_RULE", + "differential/corpus/wiki/reachability_p4_08.mm2": "SELF_MODIFYING_RULE", + "differential/corpus/wiki/reachability_p4_09.mm2": "SELF_MODIFYING_RULE", + "differential/corpus/wiki/reachability_p4_10.mm2": "SELF_MODIFYING_RULE", + "differential/corpus/wiki/reachability_p4_11.mm2": "SELF_MODIFYING_RULE", + "differential/corpus/wiki/testing_your_code_00.mm2": "SELF_MODIFYING_RULE", + "differential/corpus/wiki/transition_system_00.mm2": "FOREIGN_EXEC_TEMPLATE", +} + +EXPECTED_CURRENT = {**EXPECTED_AFTER, **EXPECTED_WIKI} + + +def sweep_paths(): + patterns = ( + os.path.join(REPO, "kernel", "resources", "*.mm2"), + os.path.join(REPO, "differential", "corpus", "**", "*.mm2"), + ) + return sorted( + os.path.relpath(path, REPO) + for pattern in patterns + for path in glob.glob(pattern, recursive=True) + ) + + +def classify(relative): + with open(os.path.join(REPO, relative), "r", encoding="utf-8") as stream: + expressions = sexpr.parse(stream.read()) + try: + transform.transform(expressions) + except transform.Refusal as error: + return str(error) + return "ACCEPT" + + +class AcceptanceSweepTest(unittest.TestCase): + def test_literal_repository_sweep_is_pinned(self): + paths = sweep_paths() + self.assertEqual(paths, sorted(EXPECTED_CURRENT)) + + def test_current_sweep_is_pinned(self): + paths = sweep_paths() + self.assertEqual( + {path: classify(path) for path in paths}, + EXPECTED_CURRENT, + ) + + def test_pre_respawn_accepted_set_is_exact(self): + accepted = { + path for path, outcome in EXPECTED_BEFORE.items() if outcome == "ACCEPT" + } + self.assertEqual( + accepted, + { + "kernel/resources/string_convert.mm2", + "kernel/resources/transitive.mm2", + "differential/corpus/programs/cross_join_dict.mm2", + "differential/corpus/programs/cross_join_tuple.mm2", + "differential/corpus/programs/lens_composition.mm2", + "differential/corpus/programs/pattern_mining.mm2", + "differential/corpus/programs/stv_roman.mm2", + "differential/corpus/unify/coref_absorbed_by_data_varref.mm2", + "differential/corpus/unify/func_type_unification.mm2", + "differential/corpus/unify/two_bipolar_equal_crossed.mm2", + }, + ) + + def test_post_respawn_accepted_set_adds_lens_aunt(self): + accepted = { + path for path, outcome in EXPECTED_AFTER.items() if outcome == "ACCEPT" + } + self.assertEqual( + accepted, + { + path + for path, outcome in EXPECTED_BEFORE.items() + if outcome == "ACCEPT" + } + | {"differential/corpus/programs/lens_aunt.mm2"}, + ) + + def test_wiki_accepted_set_is_exact(self): + accepted = { + path for path, outcome in EXPECTED_WIKI.items() if outcome == "ACCEPT" + } + self.assertEqual( + accepted, + { + "differential/corpus/wiki/mm2_basics_02.mm2", + "differential/corpus/wiki/mm2_basics_05.mm2", + "differential/corpus/wiki/reachability_p1_13.mm2", + "differential/corpus/wiki/reachability_p2_06.mm2", + "differential/corpus/wiki/reachability_p2_07.mm2", + "differential/corpus/wiki/reachability_p2_08.mm2", + "differential/corpus/wiki/reachability_p3_03.mm2", + "differential/corpus/wiki/reachability_p3_04.mm2", + "differential/corpus/wiki/reachability_p3_09.mm2", + "differential/corpus/wiki/reachability_p3_12.mm2", + "differential/corpus/wiki/reachability_p3_18.mm2", + "differential/corpus/wiki/reachability_p4_03.mm2", + }, + ) + + +if __name__ == "__main__": + unittest.main() diff --git a/tools/semi_naive/test_analyze.py b/tools/semi_naive/test_analyze.py new file mode 100644 index 00000000..44e8a11e --- /dev/null +++ b/tools/semi_naive/test_analyze.py @@ -0,0 +1,193 @@ +#!/usr/bin/env python3 + +import copy +import hashlib +import json +import os +import sys +import tempfile +import unittest + + +sys.path.insert(0, os.path.dirname(os.path.abspath(__file__))) +import analyze +import bench + + +def projection_hash(workload, size): + return hashlib.sha256(("%s:%d" % (workload, size)).encode()).hexdigest() + + +def result_row(workload, size, protocol, engine): + scale = 2 if protocol == "transformed" else 1 + transitions = size ** (3 if engine == "pz" else 2) + if protocol == "naive" and engine == "lf": + transitions = 0 + engine_ms = { + ("naive", "pz"): size * 100, + ("naive", "lf"): size * 50, + ("transformed", "pz"): size * 10, + ("transformed", "lf"): size, + }[(protocol, engine)] + counters = { + "steps": size * scale, + "unifications": size * 3 * scale, + "writes": size * 4 * scale, + "transitions": transitions, + "rounds": size if protocol == "naive" else 1, + } + samples = [ + { + "repeat": repeat, + **counters, + "engine_ms": engine_ms + repeat - 1, + "wall_ns": (engine_ms + repeat) * 1_000_000, + "wall_ms": engine_ms + repeat, + } + for repeat in (1, 2, 3) + ] + return { + "workload": workload, + "size": size, + "instance": "%d+%d" % (size, size) + if workload == "process_calculus" + else str(size), + "protocol": protocol, + "protocol_label": bench.protocol_label(protocol), + "engine": engine, + "status": "measured", + **counters, + "engine_ms": engine_ms, + "wall_ns": (engine_ms + 1) * 1_000_000, + "wall_ms": engine_ms + 1, + "selected_engine_repeat": 1, + "selected_wall_repeat": 1, + "projection_bytes": size * size, + "projection_lines": size, + "projection_sha256": projection_hash(workload, size), + "samples": samples, + } + + +def complete_artifact(): + rows = [ + result_row(workload, size, protocol, engine) + for workload, sizes in bench.WORKLOAD_SIZES.items() + for size in sizes + for protocol in bench.PROTOCOL_ORDER + for engine in bench.ENGINE_ORDER + ] + return { + "schema": 1, + "resolved": True, + "all_measured": True, + "git_head": "a" * 40, + "binaries": { + "pz": {"sha256": "1" * 64}, + "lf": {"sha256": "2" * 64}, + }, + "methodology": {"repeats": 3}, + "results": rows, + } + + +def write_artifact(root, name, artifact): + path = os.path.join(root, name) + with open(path, "w", encoding="utf-8") as stream: + json.dump(artifact, stream) + return path + + +class AnalyzeTest(unittest.TestCase): + def load(self, artifact): + with tempfile.TemporaryDirectory() as root: + path = write_artifact(root, "bench.json", artifact) + return analyze.load_and_validate([path]) + + def test_complete_matrix_has_expected_power_fits_and_ratios(self): + rows, hashes, sources = self.load(complete_artifact()) + result = analyze.analyze(rows, hashes, sources) + self.assertEqual(result["validation"]["cells"], 32) + self.assertAlmostEqual( + result["scaling"]["process_calculus"]["pz"]["fit"]["exponent"], + 3, + ) + self.assertAlmostEqual( + result["scaling"]["process_calculus"]["lf"]["fit"]["exponent"], + 2, + ) + self.assertAlmostEqual( + result["projection_scaling"]["process_calculus"]["fit"]["exponent"], + 2, + ) + growth = result["scaling"]["process_calculus"]["pz"]["adjacent_growth"] + self.assertTrue(all(abs(item["per_doubling"] - 8) < 1e-12 for item in growth)) + ratios = result["composition_at_process_calculus_320"]["ratios"] + self.assertEqual(ratios["stock_to_combined"], 100) + self.assertEqual(ratios["same_lf_naive_to_transformed"], 50) + + def test_fragments_must_use_the_same_binary_hashes(self): + artifact = complete_artifact() + left = copy.deepcopy(artifact) + right = copy.deepcopy(artifact) + left["results"] = artifact["results"][:16] + right["results"] = artifact["results"][16:] + right["binaries"]["lf"]["sha256"] = "3" * 64 + with tempfile.TemporaryDirectory() as root: + paths = [ + write_artifact(root, "left.json", left), + write_artifact(root, "right.json", right), + ] + with self.assertRaisesRegex( + analyze.AnalysisRefusal, "^MIXED_BINARY_HASHES" + ): + analyze.load_and_validate(paths) + + def test_duplicate_cell_is_refused(self): + artifact = complete_artifact() + artifact["results"].append(copy.deepcopy(artifact["results"][0])) + with self.assertRaisesRegex(analyze.AnalysisRefusal, "^DUPLICATE_CELL"): + self.load(artifact) + + def test_missing_cell_is_refused(self): + artifact = complete_artifact() + artifact["results"].pop() + with self.assertRaisesRegex(analyze.AnalysisRefusal, "^INCOMPLETE_MATRIX"): + self.load(artifact) + + def test_skipped_cell_is_refused(self): + artifact = complete_artifact() + artifact["all_measured"] = False + artifact["results"][0] = { + **artifact["results"][0], + "status": "skipped", + "reason": "timeout", + } + with self.assertRaisesRegex(analyze.AnalysisRefusal, "^BENCHMARK_HAS_SKIPS"): + self.load(artifact) + + def test_counter_change_between_repeats_is_refused(self): + artifact = complete_artifact() + artifact["results"][0]["samples"][1]["writes"] += 1 + with self.assertRaisesRegex( + analyze.AnalysisRefusal, "^NONDETERMINISTIC_COUNTERS" + ): + self.load(artifact) + + def test_nonminimum_timer_is_refused(self): + artifact = complete_artifact() + artifact["results"][0]["engine_ms"] += 1 + with self.assertRaisesRegex(analyze.AnalysisRefusal, "^ENGINE_MS_NOT_MINIMUM"): + self.load(artifact) + + def test_projection_disagreement_is_refused(self): + artifact = complete_artifact() + artifact["results"][1]["projection_sha256"] = "f" * 64 + with self.assertRaisesRegex( + analyze.AnalysisRefusal, "^CROSS_CELL_PROJECTION_MISMATCH" + ): + self.load(artifact) + + +if __name__ == "__main__": + unittest.main() diff --git a/tools/semi_naive/test_bench.py b/tools/semi_naive/test_bench.py new file mode 100644 index 00000000..b8e84e76 --- /dev/null +++ b/tools/semi_naive/test_bench.py @@ -0,0 +1,224 @@ +#!/usr/bin/env python3 + +import argparse +import contextlib +import io +import os +import subprocess +import sys +import tempfile +import unittest +from unittest import mock + + +sys.path.insert(0, os.path.dirname(os.path.abspath(__file__))) +import bench + + +def sample(wall_ns=10, transitions=5, unifications=3): + return { + "steps": 2, + "unifications": unifications, + "writes": 4, + "transitions": transitions, + "engine_ms": 1, + "wall_ns": wall_ns, + "rounds": 1, + "projection": b"(fact a)\n", + } + + +class BenchTest(unittest.TestCase): + def test_timeout_parser_rejects_nonfinite_values(self): + for value in ("nan", "inf", "-inf", "0"): + with self.subTest(value=value), self.assertRaises( + argparse.ArgumentTypeError + ): + bench.positive_float(value) + + def test_case_specs_require_one_workload_for_custom_sizes(self): + with self.assertRaisesRegex( + bench.BenchmarkRefusal, "^SIZES_REQUIRE_ONE_WORKLOAD$" + ): + bench.case_specs(["process_calculus", "transitive"], [8]) + + def test_interleaved_schedule_rotates_each_repeat(self): + cells = [("naive", "pz"), ("naive", "lf"), ("transformed", "pz")] + self.assertEqual( + list(bench.interleaved_schedule(cells, 2)), + [ + (0, cells[0]), + (0, cells[1]), + (0, cells[2]), + (1, cells[1]), + (1, cells[2]), + (1, cells[0]), + ], + ) + + def test_interleaved_schedule_is_a_permutation_for_many_shapes(self): + for cell_count in range(1, 9): + cells = [("cell", index) for index in range(cell_count)] + schedule = list(bench.interleaved_schedule(cells, 11)) + for repeat in range(11): + observed = [cell for row, cell in schedule if row == repeat] + self.assertEqual(len(observed), cell_count) + self.assertEqual(set(observed), set(cells)) + + def test_counter_signature_excludes_time_but_includes_transitions(self): + left = sample(wall_ns=10, transitions=5) + right = dict(left, wall_ns=20, engine_ms=9) + self.assertEqual(bench.counter_bytes(left), bench.counter_bytes(right)) + different = dict(right, transitions=6) + self.assertNotEqual(bench.counter_bytes(left), bench.counter_bytes(different)) + + def test_changed_counter_repeat_hard_errors(self): + with self.assertRaisesRegex(RuntimeError, "^NONDETERMINISTIC_COUNTERS"): + bench.verify_counter_repeat( + [sample(unifications=3)], sample(unifications=4), "case" + ) + + def test_engine_and_wall_minima_are_selected_independently(self): + case = { + "workload": "transitive", + "size": 4, + "instance": "4", + } + slow = sample(wall_ns=20) + slow["engine_ms"] = 2 + fast = sample(wall_ns=10) + fast["engine_ms"] = 7 + row = bench.completed_row(case, "transformed", "pz", [slow, fast], 2) + self.assertEqual(row["selected_wall_repeat"], 2) + self.assertEqual(row["selected_engine_repeat"], 1) + self.assertEqual(row["wall_ns"], 10) + self.assertEqual(row["engine_ms"], 2) + + def test_cross_engine_invariants_ignore_transitions(self): + case = { + "workload": "transitive", + "size": 4, + "instance": "4", + } + pz = bench.completed_row( + case, "transformed", "pz", [sample(transitions=99)], 1 + ) + lf = bench.completed_row( + case, "transformed", "lf", [sample(transitions=1)], 1 + ) + bench.verify_cross_engine_counters([pz, lf]) + lf["unifications"] = 100 + with self.assertRaisesRegex( + RuntimeError, "^CROSS_ENGINE_COUNTER_MISMATCH" + ): + bench.verify_cross_engine_counters([pz, lf]) + + def test_cross_cell_projection_mismatch_hard_errors(self): + case = {"required": None} + with self.assertRaisesRegex( + RuntimeError, "^CROSS_CELL_PROJECTION_MISMATCH" + ): + bench.verify_projection( + case, + b"(fact a)\n", + dict(sample(), projection=b"(fact b)\n"), + "case", + ) + + def test_binary_validation_rejects_identical_copies(self): + with tempfile.TemporaryDirectory() as workdir: + pz = os.path.join(workdir, "pz") + lf = os.path.join(workdir, "lf") + for path in (pz, lf): + with open(path, "wb") as stream: + stream.write(b"binary") + os.chmod(path, 0o755) + with self.assertRaisesRegex( + bench.BenchmarkRefusal, "^ENGINE_BINARIES_IDENTICAL$" + ): + bench.validate_binaries({"pz": pz, "lf": lf}, ["pz", "lf"]) + + @mock.patch.object(bench, "run_cell_once") + def test_naive_timeout_prints_skip_and_keeps_transformed_cell(self, run_cell): + def side_effect(protocol, *args, **kwargs): + if protocol == "naive": + raise subprocess.TimeoutExpired("mork", 1) + return sample() + + run_cell.side_effect = side_effect + with tempfile.TemporaryDirectory() as workdir: + transformed = os.path.join(workdir, "transformed.mm2") + with open(transformed, "w", encoding="utf-8") as stream: + stream.write("(f (fact a))\n") + case = { + "workload": "transitive", + "size": 4, + "instance": "4", + "source": os.path.join(workdir, "source.mm2"), + "transformed": transformed, + "required": None, + } + output = io.StringIO() + with contextlib.redirect_stdout(output): + rows = bench.benchmark_case( + case, + [("naive", "pz"), ("transformed", "pz")], + {"pz": "/mork"}, + 1, + 100, + 8, + 1, + workdir, + ) + self.assertEqual(rows[0]["status"], "skipped") + self.assertEqual(rows[1]["status"], "measured") + self.assertIn( + "SKIP transitive 4 naive repeated-evaluation protocol PZ repeat 1: " + "repeated-evaluation protocol exceeded 1 seconds in repeat 1", + output.getvalue(), + ) + + @mock.patch.object(bench.driver, "run_source_protocol") + @mock.patch.object(bench.time, "perf_counter_ns", side_effect=[0, 2_000_000_000]) + def test_naive_protocol_checks_total_wall_after_final_round(self, _, protocol): + protocol.return_value = { + "steps": 1, + "milliseconds": 1, + "unifications": 1, + "writes": 1, + "transitions": 1, + "rounds": 1, + "projection": b"(fact a)\n", + } + case = {"source": "/source.mm2"} + with self.assertRaises(subprocess.TimeoutExpired): + bench.run_naive_once("/mork", case, "/work", 10, 2, 1) + + def test_table_never_labels_naive_as_one_shot(self): + case = { + "workload": "transitive", + "size": 4, + "instance": "4", + } + row = bench.completed_row(case, "naive", "pz", [sample()], 1) + table = bench.render_table([row], 1) + self.assertIn("naive repeated-evaluation protocol", table) + self.assertNotIn("one-shot", table) + + def test_artifact_distinguishes_resolved_skips_from_all_measured(self): + case = { + "workload": "transitive", + "size": 4, + "instance": "4", + } + rows = [bench.skipped_row(case, "naive", "pz", "timeout")] + with mock.patch.object(bench, "git_head", return_value="abc"), mock.patch.object( + bench, "sha256_file", return_value="def" + ): + artifact = bench.artifact(rows, {"pz": "/pz"}, 3, 900, 8, 10) + self.assertTrue(artifact["resolved"]) + self.assertFalse(artifact["all_measured"]) + + +if __name__ == "__main__": + unittest.main() diff --git a/tools/semi_naive/test_driver.py b/tools/semi_naive/test_driver.py new file mode 100644 index 00000000..a21ff837 --- /dev/null +++ b/tools/semi_naive/test_driver.py @@ -0,0 +1,357 @@ +#!/usr/bin/env python3 + +import contextlib +import io +import os +import subprocess +import sys +import tempfile +import unittest +from unittest import mock + + +sys.path.insert(0, os.path.dirname(os.path.abspath(__file__))) +import driver + + +def cross_engine_fixture(): + projection = b"(fact a)\n" + return { + "source_projection": projection, + "transformed_projection": projection, + "source": { + "steps": 1, + "milliseconds": 1, + "unifications": 2, + "writes": 3, + "transitions": 4, + "rounds": 1, + }, + "transformed": { + "steps": 1, + "milliseconds": 1, + "unifications": 2, + "writes": 3, + "transitions": 4, + }, + } + + +class DriverTest(unittest.TestCase): + def test_metrics_accept_product_zipper_and_leapfrog_formats(self): + expected = { + "steps": 8659, + "milliseconds": 1123, + "unifications": 6732, + "writes": 19872, + "transitions": 12798481, + } + product_zipper = ( + b"executing 8659 steps took 1123 ms " + b"(unifications 6732, writes 19872, transitions 12798481)\n" + ) + leapfrog = ( + b"executing 8659 steps took 1123 ms " + b"(unifications 6732, writes 19872, transitions 12798481, max unify 9)\n" + ) + self.assertEqual(driver.parse_metrics(product_zipper), expected) + self.assertEqual(driver.parse_metrics(leapfrog), expected) + + def test_missing_metrics_has_a_named_error(self): + with self.assertRaisesRegex(ValueError, "^EXECUTION_METRICS_MISSING$"): + driver.parse_metrics(b"no counters here") + + def test_materializer_handles_comments_strings_and_semicolons_in_atoms(self): + program = ''' + ; (ignored) + (fact foo;bar "text; ) still text") ; trailing comment + (exec (priority 0) (, (fact $x $y)) (, (seen $x $y))) + ''' + materialized = driver.materialize_naive_program(program, rounds=1) + self.assertIn('(fact foo;bar "text; ) still text")', materialized) + self.assertIn("(naive r000000 (priority 0) q000000)", materialized) + + def test_materializer_rejects_unbalanced_input(self): + with self.assertRaisesRegex(ValueError, "unterminated expression"): + driver.materialize_naive_program("(fact", rounds=1) + with self.assertRaisesRegex(ValueError, "unexpected"): + driver.materialize_naive_program("fact)", rounds=1) + + def test_materialized_rounds_have_ordered_unique_priorities(self): + program = """ + (seed) + (exec (source 2) (, (seed)) (, (two))) + (exec (source 1) (, (seed)) (, (one))) + """ + materialized = driver.materialize_naive_program(program, rounds=2) + self.assertEqual(materialized.count("(exec "), 4) + self.assertIn("(naive r000000 (source 2) q000000)", materialized) + self.assertIn("(naive r000001 (source 1) q000001)", materialized) + + @mock.patch.object(driver, "run_program") + def test_source_protocol_sums_external_rounds(self, run_program): + run_program.side_effect = [ + { + "steps": 2, + "milliseconds": 3, + "unifications": 5, + "writes": 7, + "transitions": 11, + "dump": b"(out a)\n(seed a)\n", + }, + { + "steps": 2, + "milliseconds": 4, + "unifications": 5, + "writes": 7, + "transitions": 13, + "dump": b"(seed a)\n(out a)\n", + }, + ] + with tempfile.TemporaryDirectory() as workdir: + program = os.path.join(workdir, "source.mm2") + with open(program, "w", encoding="utf-8") as stream: + stream.write( + "(seed a)\n(exec 0 (, (seed $x)) (, (out $x)))\n" + ) + result = driver.run_source_protocol( + "/mork", program, workdir, driver.DEFAULT_STEPS, 8 + ) + self.assertEqual(result["rounds"], 2) + self.assertEqual(result["steps"], 4) + self.assertEqual(result["milliseconds"], 7) + self.assertEqual(result["unifications"], 10) + self.assertEqual(result["writes"], 14) + self.assertEqual(result["transitions"], 24) + self.assertEqual(result["projection"], b"(out a)\n(seed a)\n") + + @mock.patch.object(driver, "run_program") + def test_natural_source_uses_bound_and_strips_live_exec(self, run_program): + run_program.return_value = { + "steps": 1, + "milliseconds": 2, + "unifications": 3, + "writes": 4, + "transitions": 5, + "dump": b"(fact a)\n(exec loop (, (fact $x)) (, (fact $x)))\n", + } + with tempfile.TemporaryDirectory() as workdir: + result = driver.run_source_natural( + "/mork", "/source.mm2", workdir, driver.DEFAULT_STEPS, 7 + ) + self.assertEqual(run_program.call_args.args[3], 7) + self.assertEqual(result["projection"], b"(fact a)\n") + self.assertEqual(result["step_bound"], 7) + self.assertEqual(result["source_mode"], "natural") + + @mock.patch.object(driver.time, "perf_counter_ns", return_value=101) + def test_expired_protocol_deadline_is_named(self, _): + with self.assertRaises(subprocess.TimeoutExpired) as raised: + driver.timeout_until(100) + self.assertEqual(raised.exception.cmd, "repeated-evaluation protocol") + + def test_projection_unwraps_and_drops_bookkeeping(self): + dump = b"""\ +(phase p q r) +(f (edge b c)) +(cand (edge a c)) +(d0 (edge b c)) +(d1 (edge a c)) +(c d0 d1 (edge a c)) +(t d0 d1) +(f (edge a b)) +(controller p q) +(active) +""" + self.assertEqual( + driver.sorted_projection(dump, transformed=True), + b"(edge a b)\n(edge b c)\n", + ) + + def test_expected_projection_comments_and_source_exec_are_optional_metadata(self): + dump = b"; @source-steps 1\n(fact a)\n(exec loop (, (fact $x)) (, (fact $x)))\n" + self.assertEqual( + driver.sorted_projection(dump, transformed=False, strip_exec=True), + b"(fact a)\n", + ) + with tempfile.NamedTemporaryFile("w", encoding="utf-8") as stream: + stream.write(";; @source-steps 7\n(fact a)\n") + stream.flush() + self.assertEqual(driver.read_expected_source_steps(stream.name), 7) + + def test_first_difference_reports_missing_lines(self): + self.assertEqual( + driver.first_difference(b"a\nb\n", b"a\n"), + (2, b"b", b""), + ) + + def test_bare_top_level_variable_fact_is_a_named_error(self): + with tempfile.TemporaryDirectory() as workdir: + program = os.path.join(workdir, "bare.mm2") + with open(program, "w", encoding="utf-8") as stream: + stream.write("(fixed $x)\n$bare\n") + with self.assertRaisesRegex( + ValueError, "^BARE_TOP_LEVEL_VARIABLE_FACT: .* form 2$" + ): + driver.assert_no_bare_top_level_variable_facts(program) + + def test_all_generated_transforms_have_no_bare_top_level_variable_facts(self): + temp_root = os.path.join(driver.REPO, "target", "semi_naive") + os.makedirs(temp_root, exist_ok=True) + with tempfile.TemporaryDirectory( + prefix="semi-naive-bare-variable-test-", dir=temp_root + ) as root: + benchmark_root = os.path.join(root, "sources") + driver.generate_benchmark_corpus(benchmark_root) + cases = driver.discover_cases( + os.path.join(root, "transforms"), + generate_all=True, + benchmark_root=benchmark_root, + ) + self.assertEqual(len(cases), 17) + for case in cases: + with self.subTest(label=case.label): + driver.assert_no_bare_top_level_variable_facts( + case.transformed + ) + + def test_repository_manifest_pins_persistent_and_self_respawn_cases(self): + specs = driver.load_repository_manifest() + self.assertEqual(len(specs), 23) + self.assertEqual( + [spec.label for spec in specs], + [ + "kernel/string_convert", + "kernel/transitive", + "programs/cross_join_dict", + "programs/cross_join_tuple", + "programs/lens_aunt", + "programs/lens_composition", + "programs/pattern_mining", + "programs/stv_roman", + "unify/coref_absorbed_by_data_varref", + "unify/func_type_unification", + "unify/two_bipolar_equal_crossed", + "wiki/mm2_basics_02", + "wiki/mm2_basics_05", + "wiki/reachability_p1_13", + "wiki/reachability_p2_06", + "wiki/reachability_p2_07", + "wiki/reachability_p2_08", + "wiki/reachability_p3_03", + "wiki/reachability_p3_04", + "wiki/reachability_p3_09", + "wiki/reachability_p3_12", + "wiki/reachability_p3_18", + "wiki/reachability_p4_03", + ], + ) + persistent = [spec for spec in specs if spec.source_mode == "persistent"] + natural = [spec for spec in specs if spec.source_mode == "natural"] + self.assertEqual(len(persistent), 22) + self.assertTrue(all(spec.source_steps is None for spec in persistent)) + self.assertEqual( + [(spec.label, spec.source_steps) for spec in natural], + [("programs/lens_aunt", 1)], + ) + self.assertEqual(natural[0].engine_specific_fields, ("unifications",)) + + def test_repository_manifest_rejects_escape_and_duplicate_rows(self): + with tempfile.TemporaryDirectory() as workdir: + manifest = os.path.join(workdir, "manifest.tsv") + with open(manifest, "w", encoding="utf-8") as stream: + stream.write("bad|../source.mm2|../expected|persistent|-|-\n") + with self.assertRaisesRegex( + ValueError, "^REPOSITORY_MANIFEST_ESCAPES_REPO_SOURCE" + ): + driver.load_repository_manifest(manifest) + + source = os.path.relpath(__file__, driver.REPO) + with open(manifest, "w", encoding="utf-8") as stream: + stream.write("one|%s|%s|persistent|-|-\n" % (source, source)) + stream.write("one|%s|%s|persistent|-|-\n" % (source, source)) + with self.assertRaisesRegex( + ValueError, "^REPOSITORY_MANIFEST_DUPLICATE_LABEL" + ): + driver.load_repository_manifest(manifest) + + def test_cross_engine_agreement_ignores_transitions_and_time(self): + projection = b"(fact a)\n" + left = { + "source_projection": projection, + "transformed_projection": projection, + "source": { + "steps": 3, + "milliseconds": 20, + "unifications": 4, + "writes": 5, + "transitions": 100, + "rounds": 2, + }, + "transformed": { + "steps": 7, + "milliseconds": 10, + "unifications": 8, + "writes": 9, + "transitions": 200, + }, + } + right = { + "source_projection": projection, + "transformed_projection": projection, + "source": dict(left["source"], milliseconds=12, transitions=0), + "transformed": dict( + left["transformed"], milliseconds=1, transitions=30 + ), + } + with contextlib.redirect_stdout(io.StringIO()): + self.assertEqual( + driver.compare_cross_engine("bin-pz", left, "bin-lf", right), + 0, + ) + + def test_cross_engine_counter_mismatch_fails(self): + result = cross_engine_fixture() + different = dict(result) + different["transformed"] = dict(result["transformed"], unifications=99) + with contextlib.redirect_stdout(io.StringIO()): + self.assertEqual( + driver.compare_cross_engine( + "bin-pz", result, "bin-lf", different + ), + 1, + ) + + def test_declared_engine_specific_unifications_are_reported_not_failed(self): + result = cross_engine_fixture() + different = dict(result) + different["source"] = dict(result["source"], unifications=99) + different["transformed"] = dict( + result["transformed"], unifications=101 + ) + with contextlib.redirect_stdout(io.StringIO()): + self.assertEqual( + driver.compare_cross_engine( + "bin-pz", + result, + "bin-lf", + different, + ("unifications",), + ), + 0, + ) + + def test_cross_engine_projection_mismatch_fails(self): + result = cross_engine_fixture() + different = dict(result, transformed_projection=b"(fact b)\n") + with contextlib.redirect_stdout(io.StringIO()): + self.assertEqual( + driver.compare_cross_engine( + "bin-pz", result, "bin-lf", different + ), + 1, + ) + + +if __name__ == "__main__": + unittest.main() diff --git a/tools/semi_naive/test_generators.py b/tools/semi_naive/test_generators.py new file mode 100644 index 00000000..1fd59734 --- /dev/null +++ b/tools/semi_naive/test_generators.py @@ -0,0 +1,78 @@ +#!/usr/bin/env python3 + +import argparse +import os +import sys +import tempfile +import unittest + + +HERE = os.path.dirname(os.path.abspath(__file__)) +REPO = os.path.dirname(os.path.dirname(HERE)) +GENERATORS = os.path.join(HERE, "generators") +sys.path.insert(0, GENERATORS) +import gen_process_calculus +import gen_transitive + + +def tree_bytes(root): + contents = {} + for directory, dirnames, filenames in os.walk(root): + dirnames.sort() + for filename in sorted(filenames): + path = os.path.join(directory, filename) + with open(path, "rb") as stream: + contents[os.path.relpath(path, root)] = stream.read() + return contents + + +class GeneratorTest(unittest.TestCase): + def deterministic_generation(self, generate): + temp_root = os.path.join(REPO, "target", "semi_naive") + os.makedirs(temp_root, exist_ok=True) + with tempfile.TemporaryDirectory( + prefix="semi-naive-generator-a-", dir=temp_root + ) as first, tempfile.TemporaryDirectory( + prefix="semi-naive-generator-b-", dir=temp_root + ) as second: + generate(first) + generate(second) + self.assertEqual(tree_bytes(first), tree_bytes(second)) + return tree_bytes(first) + + def test_process_calculus_is_deterministic_and_checks_the_sum(self): + contents = self.deterministic_generation( + lambda root: gen_process_calculus.generate(root, ((3, 4), (0, 0))) + ) + self.assertEqual( + contents["process_calculus_003_004.required"], + b"(petri (! result (S (S (S (S (S (S (S Z)))))))))\n", + ) + source = contents["process_calculus_003_004.source.mm2"] + self.assertEqual(source.count(b"(exec "), 2) + self.assertIn(b"(petri (! (add result)", source) + + def test_transitive_is_deterministic_and_has_the_requested_edges(self): + contents = self.deterministic_generation( + lambda root: gen_transitive.generate(root, (1, 4)) + ) + self.assertEqual( + contents["transitive_chain_001.source.mm2"].count(b"(edge "), + 4, + ) + self.assertEqual( + contents["transitive_chain_004.source.mm2"].count(b"(edge "), + 7, + ) + + def test_process_instance_parser_rejects_negative_operands(self): + with self.assertRaises(argparse.ArgumentTypeError): + gen_process_calculus.parse_instance("-1:2") + + def test_transitive_length_rejects_zero(self): + with self.assertRaises(argparse.ArgumentTypeError): + gen_transitive.positive_integer("0") + + +if __name__ == "__main__": + unittest.main() diff --git a/tools/semi_naive/test_randomized.py b/tools/semi_naive/test_randomized.py new file mode 100755 index 00000000..31644581 --- /dev/null +++ b/tools/semi_naive/test_randomized.py @@ -0,0 +1,108 @@ +#!/usr/bin/env python3 +"""Run deterministic generated add-only programs through the projection oracle.""" + +import argparse +import contextlib +import io +import os +import random +import sys +import tempfile + + +HERE = os.path.dirname(os.path.abspath(__file__)) +REPO = os.path.dirname(os.path.dirname(HERE)) +sys.path.insert(0, HERE) +import driver +import sexpr +import transform + + +VALUES = ("a", "b", "c", "d") + + +def generate(seed): + rng = random.Random(seed) + lines = ["; deterministic generated case %d" % seed, ""] + relation_count = rng.randint(2, 5) + for relation_index in range(relation_count): + selected = [value for value in VALUES if rng.randrange(2)] + if not selected: + selected = [VALUES[rng.randrange(len(VALUES))]] + for value in selected: + lines.append("(r%d %s)" % (relation_index, value)) + + lines.append("") + rule_count = rng.randint(1, 4) + for rule_index in range(rule_count): + factor_count = rng.randint(1, 4) + factors = [ + "(r%d $x)" % rng.randrange(relation_count) + for _ in range(factor_count) + ] + heads = ["(out%d $x)" % rule_index] + if rng.randrange(2): + heads.append("(mirror%d $x)" % rule_index) + source_priority = ( + str(rng.randrange(10)) + if rng.randrange(2) + else "(source %d)" % rng.randrange(10) + ) + lines.extend( + [ + "(exec %s" % source_priority, + " (, %s)" % " ".join(factors), + " (, %s))" % " ".join(heads), + "", + ] + ) + return "\n".join(lines) + + +def run(seed_count, binary): + temp_root = os.path.join(REPO, "target", "semi_naive") + os.makedirs(temp_root, exist_ok=True) + with tempfile.TemporaryDirectory(prefix="semi-naive-random-", dir=temp_root) as root: + for seed in range(seed_count): + source_path = os.path.join(root, "%04d.source.mm2" % seed) + transformed_path = os.path.join(root, "%04d.transformed.mm2" % seed) + source = generate(seed) + with open(source_path, "w", encoding="utf-8", newline="\n") as stream: + stream.write(source) + with open( + transformed_path, "w", encoding="utf-8", newline="\n" + ) as stream: + stream.write(sexpr.dumps(transform.transform(sexpr.parse(source)))) + output = io.StringIO() + with contextlib.redirect_stdout(output): + result = driver.compare( + binary, + source_path, + transformed_path, + None, + driver.DEFAULT_STEPS, + 64, + ) + if result: + sys.stdout.write(output.getvalue()) + print("FAIL generated seed %d" % seed) + return 1 + print("OK %d deterministic generated programs" % seed_count) + return 0 + + +def main(): + parser = argparse.ArgumentParser(description=__doc__) + parser.add_argument("--seeds", type=int, default=64) + parser.add_argument("--binary", default=driver.DEFAULT_BINARY) + args = parser.parse_args() + if args.seeds <= 0: + parser.error("--seeds must be positive") + binary = os.path.abspath(args.binary) + if not os.access(binary, os.X_OK): + parser.error("binary is not executable: %s" % binary) + return run(args.seeds, binary) + + +if __name__ == "__main__": + sys.exit(main()) diff --git a/tools/semi_naive/test_refusals.py b/tools/semi_naive/test_refusals.py new file mode 100644 index 00000000..572cca4b --- /dev/null +++ b/tools/semi_naive/test_refusals.py @@ -0,0 +1,75 @@ +#!/usr/bin/env python3 + +import os +import subprocess +import sys +import tempfile +import unittest + + +HERE = os.path.dirname(os.path.abspath(__file__)) +REFUSALS = os.path.join(HERE, "corpus", "refusals") +EXPECTED = os.path.join(HERE, "expected", "i3", "refusals.expected") +TRANSFORM = os.path.join(HERE, "transform.py") + + +def expected_refusals(): + refusals = [] + with open(EXPECTED, "r", encoding="utf-8") as stream: + for line in stream: + filename, reason = line.rstrip("\n").split("|", 1) + refusals.append((filename, reason)) + return refusals + + +class RefusalTest(unittest.TestCase): + def test_refusal_matrix(self): + expected = expected_refusals() + self.assertEqual( + [filename for filename, _ in expected], sorted(os.listdir(REFUSALS)) + ) + with tempfile.TemporaryDirectory() as workdir: + for filename, reason in expected: + with self.subTest(filename=filename): + output = os.path.join(workdir, filename) + completed = subprocess.run( + [ + sys.executable, + TRANSFORM, + os.path.join(REFUSALS, filename), + output, + ], + stdout=subprocess.PIPE, + stderr=subprocess.PIPE, + check=False, + ) + self.assertEqual(completed.returncode, 2) + self.assertEqual(completed.stdout, b"") + self.assertEqual( + completed.stderr, + ("REFUSE %s\n" % reason).encode("utf-8"), + ) + self.assertFalse(os.path.exists(output)) + + def test_parse_error_is_named_and_writes_nothing(self): + with tempfile.TemporaryDirectory() as workdir: + source = os.path.join(workdir, "broken.mm2") + output = os.path.join(workdir, "output.mm2") + with open(source, "w", encoding="utf-8") as stream: + stream.write("(broken") + completed = subprocess.run( + [sys.executable, TRANSFORM, source, output], + stdout=subprocess.PIPE, + stderr=subprocess.PIPE, + check=False, + ) + self.assertEqual(completed.returncode, 2) + self.assertEqual( + completed.stderr, + b"REFUSE PARSE_ERROR: unterminated expression at end of input\n", + ) + self.assertFalse(os.path.exists(output)) + + +if __name__ == "__main__": + unittest.main() diff --git a/tools/semi_naive/test_repository_bench.py b/tools/semi_naive/test_repository_bench.py new file mode 100644 index 00000000..843e1d9a --- /dev/null +++ b/tools/semi_naive/test_repository_bench.py @@ -0,0 +1,76 @@ +#!/usr/bin/env python3 + +import os +import sys +import unittest + + +HERE = os.path.dirname(os.path.abspath(__file__)) +sys.path.insert(0, HERE) +import repository_bench + + +def result(rounds=3, unifications=10, transitions=20): + return { + "source": { + "rounds": rounds, + "steps": 3, + "unifications": unifications, + "writes": 11, + "transitions": transitions, + }, + "transformed": { + "steps": 7, + "unifications": 8, + "writes": 12, + "transitions": transitions + 1, + }, + "source_projection": b"(fact)\n", + "transformed_projection": b"(fact)\n", + } + + +class RepositoryBenchTest(unittest.TestCase): + def test_short_programs_are_labeled_neutral(self): + sample = result(rounds=2, unifications=1) + self.assertEqual( + repository_bench.verdict(sample["source"], sample["transformed"]), + "NEUTRAL_SHORT", + ) + + def test_longer_programs_report_reduction_or_overhead(self): + reduced = result(rounds=3, unifications=10) + overhead = result(rounds=3, unifications=4) + self.assertEqual( + repository_bench.verdict( + reduced["source"], reduced["transformed"] + ), + "FEWER_UNIFICATIONS", + ) + self.assertEqual( + repository_bench.verdict( + overhead["source"], overhead["transformed"] + ), + "OVERHEAD", + ) + self.assertEqual( + repository_bench.verdict( + overhead["source"], overhead["transformed"], "natural" + ), + "BOUNDED_SOURCE", + ) + + def test_repeat_counter_or_projection_change_hard_errors(self): + reference = result() + changed_counter = result(transitions=21) + with self.assertRaisesRegex(RuntimeError, "^NONDETERMINISTIC_COUNTERS"): + repository_bench.verify_repeat(reference, changed_counter, "case") + + changed_projection = result() + changed_projection["source_projection"] = b"(different)\n" + with self.assertRaisesRegex(RuntimeError, "^NONDETERMINISTIC_PROJECTION"): + repository_bench.verify_repeat(reference, changed_projection, "case") + + +if __name__ == "__main__": + unittest.main() diff --git a/tools/semi_naive/test_transform.py b/tools/semi_naive/test_transform.py new file mode 100644 index 00000000..70d464e2 --- /dev/null +++ b/tools/semi_naive/test_transform.py @@ -0,0 +1,320 @@ +#!/usr/bin/env python3 + +import os +import sys +import unittest + + +HERE = os.path.dirname(os.path.abspath(__file__)) +sys.path.insert(0, HERE) +import sexpr +import transform + + +def alpha_normalize(expression): + names = {} + + def rename(node): + if node.startswith("$"): + return names.setdefault(node, "$v%d" % len(names)) + return str(node) + + return sexpr.dump(expression, rename) + + +class SExpressionTest(unittest.TestCase): + def test_comments_strings_and_atoms_round_trip(self): + source = ''' + ; ignored + (fact "semi; (quoted) \\"text\\"") + (symbol foo;bar) + atom + () + ''' + expressions = sexpr.parse(source) + self.assertEqual( + sexpr.dumps(expressions), + '(fact "semi; (quoted) \\"text\\"")\n(symbol foo;bar)\natom\n()\n', + ) + + def test_parser_reports_unbalanced_input(self): + with self.assertRaisesRegex(sexpr.ParseError, "unterminated expression"): + sexpr.parse("(fact") + with self.assertRaisesRegex(sexpr.ParseError, "unexpected"): + sexpr.parse("fact)") + with self.assertRaisesRegex(sexpr.ParseError, "unterminated string"): + sexpr.parse('"fact') + + def test_deep_expression_does_not_recurse(self): + source = "(f " * 5000 + "x" + ")" * 5000 + self.assertEqual(sexpr.dumps(sexpr.parse(source)), source + "\n") + + +class TransformTest(unittest.TestCase): + def transform_fixture(self, name): + path = os.path.join(HERE, "corpus", "i3", name + ".source.mm2") + with open(path, "r", encoding="utf-8") as stream: + return transform.transform(sexpr.parse(stream.read())) + + def embedded_phases(self, generated): + controller = generated[-1] + self.assertEqual(controller[0], "exec") + self.assertEqual(controller[1][1], "4") + return controller[3][1:-1] + + def test_i1_hand_transform_matches_modulo_variable_names(self): + source_path = os.path.join( + HERE, "corpus", "i1", "transitive_chain_004.source.mm2" + ) + hand_path = os.path.join( + HERE, "corpus", "i1", "transitive_chain_004.transformed.mm2" + ) + with open(source_path, "r", encoding="utf-8") as stream: + generated = transform.transform(sexpr.parse(stream.read())) + with open(hand_path, "r", encoding="utf-8") as stream: + hand = sexpr.parse(stream.read()) + self.assertEqual( + [alpha_normalize(item) for item in generated], + [alpha_normalize(item) for item in hand], + ) + + def test_checked_transforms_match_current_encoder(self): + corpus = os.path.join(HERE, "corpus") + checked = 0 + for directory, dirnames, filenames in os.walk(corpus): + dirnames.sort() + for filename in sorted(filenames): + if not filename.endswith(".source.mm2"): + continue + source_path = os.path.join(directory, filename) + transformed_path = ( + source_path[: -len(".source.mm2")] + ".transformed.mm2" + ) + if not os.path.isfile(transformed_path): + continue + with self.subTest(path=os.path.relpath(transformed_path, HERE)): + with open(source_path, "r", encoding="utf-8") as stream: + generated = sexpr.dumps( + transform.transform(sexpr.parse(stream.read())) + ) + with open(transformed_path, "r", encoding="utf-8") as stream: + self.assertEqual(stream.read(), generated) + checked += 1 + self.assertGreater(checked, 0) + + def test_transform_bytes_are_deterministic(self): + source = "(edge a b) (edge b c) (exec 0 (, (edge $x $y) (edge $y $z)) (, (edge $x $z)))" + first = sexpr.dumps(transform.transform(sexpr.parse(source))) + second = sexpr.dumps(transform.transform(sexpr.parse(source))) + self.assertEqual(first, second) + + def test_embedded_phases_reuse_a_bounded_variable_namespace(self): + left = " ".join("$left%d" % index for index in range(40)) + right = " ".join("$right%d" % index for index in range(40)) + source = """ + (left %s) + (right %s) + (exec 0 (, (left %s)) (, (left-out))) + (exec 1 (, (right %s)) (, (right-out))) + """ % (left, right, left, right) + generated = transform.transform(sexpr.parse(source)) + self.assertLessEqual(len(transform.variables(generated[-1])), 64) + + def test_three_factor_rule_has_three_delta_variants(self): + generated = self.transform_fixture("three_factor") + derives = [ + item + for item in self.embedded_phases(generated) + if item[1][1] == "0" + ] + self.assertEqual(len(derives), 3) + for variant, derive in enumerate(derives): + factors = derive[2][1:] + self.assertEqual(len(factors), 3) + self.assertEqual( + [factor[0] for factor in factors], + [ + "$sn_phase_0" if index == variant else "f" + for index in range(3) + ], + ) + + def test_multiple_rules_share_controller_and_keep_priorities(self): + generated = self.transform_fixture("multiple_rules") + derives = [ + item + for item in self.embedded_phases(generated) + if item[1][1] == "0" + ] + self.assertEqual( + [sexpr.dump(item[1]) for item in derives], + ["(s 0 20 0)", "(s 0 3 1000000)"], + ) + self.assertEqual( + sum(item[0] == "exec" and item[1][1] == "4" for item in generated), + 1, + ) + + def test_multiple_heads_become_candidates_in_one_variant(self): + generated = self.transform_fixture("multiple_heads") + derives = [ + item + for item in self.embedded_phases(generated) + if item[1][1] == "0" + ] + self.assertEqual(len(derives), 1) + self.assertEqual( + [sexpr.dump(head) for head in derives[0][3][1:]], + [ + "(c (left $sn_phase_2))", + "(c (right $sn_phase_2))", + ], + ) + + def test_double_buffer_has_no_advance_phase(self): + generated = self.transform_fixture("three_factor") + self.assertTrue(any(item[0] == "d0" for item in generated)) + self.assertFalse(any(item[0] in ("dc", "dn", "active") for item in generated)) + self.assertEqual(sexpr.dump(generated[-2]), "(t d0 d1)") + + phases = self.embedded_phases(generated) + self.assertEqual( + [str(item[1][1]) for item in phases], + ["0", "0", "0", "1", "2", "2", "3"], + ) + promote = phases[-1] + self.assertEqual( + [sexpr.dump(item) for item in promote[3][1:]], + [ + "(+ (f $sn_phase_2))", + "(+ ($sn_phase_1 $sn_phase_2))", + "(+ (t $sn_phase_1 $sn_phase_0))", + "(- (c $sn_phase_2))", + ], + ) + + def test_internal_parity_names_do_not_capture_source_variables(self): + source = """ + (seed a b) + (exec 0 + (, (seed $sn_internal_current $sn_phase_0)) + (, (out $sn_internal_current $sn_phase_0))) + """ + generated = transform.transform(sexpr.parse(source)) + derive = self.embedded_phases(generated)[0] + self.assertEqual( + sexpr.dump(derive[2]), + "(, ($sn_phase_0 (seed $sn_phase_2 $sn_phase_3)))", + ) + self.assertEqual( + sexpr.dump(derive[3]), + "(, (c (out $sn_phase_2 $sn_phase_3)))", + ) + + def test_sixty_source_variables_fit_the_controller(self): + names = " ".join("$v%d" % index for index in range(60)) + source = "(seed %s) (exec 0 (, (seed %s)) (, (out)))" % ( + names, + names, + ) + generated = transform.transform(sexpr.parse(source)) + self.assertEqual(len(transform.variables(generated[-1])), 64) + + def test_exact_self_respawn_is_stripped_from_body_and_head(self): + source = """ + (seed a) + (exec loop + (, (seed $x) (exec loop $pattern $template)) + (, (out $x) (exec loop $pattern $template))) + """ + generated = transform.transform(sexpr.parse(source)) + derives = [ + item + for item in self.embedded_phases(generated) + if item[1][1] == "0" + ] + self.assertEqual(len(derives), 1) + self.assertEqual( + [sexpr.dump(item) for item in derives[0][2][1:]], + ["($sn_phase_0 (seed $sn_phase_2))"], + ) + self.assertEqual( + [sexpr.dump(item) for item in derives[0][3][1:]], + ["(c (out $sn_phase_2))"], + ) + + def test_fixed_infix_operator_is_not_a_variable_relation_head(self): + source = """ + (left a) + (a != b) + (exec 0 (, (left $x) ($x != $y)) (, (pair $x $y))) + """ + generated = transform.transform(sexpr.parse(source)) + derives = [ + item + for item in self.embedded_phases(generated) + if item[1][1] == "0" + ] + self.assertEqual(len(derives), 2) + self.assertEqual( + [sexpr.dump(item) for item in derives[0][3][1:]], + ["(c (pair $sn_phase_2 $sn_phase_3))"], + ) + + def test_self_modifying_and_foreign_exec_templates_are_named(self): + cases = { + "SELF_MODIFYING_RULE": """ + (seed a) + (exec (loop 0) + (, (seed $x) (exec (loop $n) $pattern $template)) + (, (out $x) (exec (loop 1) $pattern $template))) + """, + "FOREIGN_EXEC_TEMPLATE": """ + (seed a) + (exec loop + (, (seed $x) (exec loop $pattern $template)) + (, (out $x) (exec other $pattern $template) + (exec loop $pattern $template))) + """, + } + for reason, source in cases.items(): + with self.subTest(reason=reason): + with self.assertRaisesRegex(transform.Refusal, "^%s$" % reason): + transform.transform(sexpr.parse(source)) + + def test_self_handle_must_not_match_another_source_rule(self): + source = """ + (seed a) + (exec $priority + (, (seed $x) (exec $priority $pattern $template)) + (, (out $x) (exec $priority $pattern $template))) + (exec other (, (seed $x)) (, (other $x))) + """ + with self.assertRaisesRegex( + transform.Refusal, "^FOREIGN_EXEC_TEMPLATE$" + ): + transform.transform(sexpr.parse(source)) + + def test_i2_refusals_are_named(self): + cases = { + "NO_RULES": "(fact a)", + "COUNTED_EXEC_HEAD": "(exec 0 (, (a)) (, (b)) (, (count)))", + "MALFORMED_EXEC": "(exec 0 (, (a)))", + "IO_SOURCE": "(exec 0 (I (a)) (, (b)))", + "IO_SINK": "(a) (exec 0 (, (a)) (O (+ (b))))", + "REMOVAL_TEMPLATE": "(a) (exec 0 (, (a)) (O (- (a))))", + "UNCLASSIFIABLE_PATTERN": "(a) (exec 0 (, $x) (, (b)))", + "UNCLASSIFIABLE_TEMPLATE": "(a) (exec 0 (, (a)) (, b))", + "FOREIGN_EXEC_TEMPLATE": "(a) (exec 0 (, (a)) (, (exec 1 (, (a)) (, (b)))))", + "UNBOUND_HEAD_VARIABLE": "(a) (exec 0 (, (a)) (, (b $x)))", + "CONTROLLER_VARIABLE_LIMIT": "(a) (exec 0 (, (a %s)) (, (b)))" + % " ".join("$v%d" % index for index in range(61)), + } + for reason, source in cases.items(): + with self.subTest(reason=reason): + with self.assertRaisesRegex(transform.Refusal, "^%s$" % reason): + transform.transform(sexpr.parse(source)) + + +if __name__ == "__main__": + unittest.main() diff --git a/tools/semi_naive/transform.py b/tools/semi_naive/transform.py new file mode 100755 index 00000000..10b943f7 --- /dev/null +++ b/tools/semi_naive/transform.py @@ -0,0 +1,496 @@ +#!/usr/bin/env python3 +"""Transform add-only MM2 rules into MM2-native semi-naive rounds.""" + +import argparse +import os +import sys + + +sys.path.insert(0, os.path.dirname(os.path.abspath(__file__))) +import sexpr + + +class Refusal(ValueError): + pass + + +def relation(expression, reason): + expression = require_list(expression, reason) + if ( + not expression + or not isinstance(expression[0], sexpr.Atom) + or expression[0].startswith("$") + ): + raise Refusal(reason) + return expression + + +def require_list(expression, reason): + if not isinstance(expression, sexpr.ListExpr): + raise Refusal(reason) + return expression + + +def validate_fact(fact): + expression = relation(fact, "UNCLASSIFIABLE_FACT") + if expression[0] in ("exec", "I", "O"): + raise Refusal("RESERVED_SOURCE_FORM") + if len(variables(expression)) > 64: + raise Refusal("TOO_MANY_VARIABLES") + return expression + + +def is_exec_form(expression): + return ( + isinstance(expression, sexpr.ListExpr) + and expression + and expression[0] == "exec" + ) + + +def structural_equal(left, right): + stack = [(left, right)] + while stack: + left_node, right_node = stack.pop() + if isinstance(left_node, sexpr.ListExpr): + if not isinstance(right_node, sexpr.ListExpr) or len(left_node) != len( + right_node + ): + return False + stack.extend(zip(left_node, right_node)) + elif not isinstance(right_node, sexpr.Atom) or left_node != right_node: + return False + return True + + +def pattern_matches(pattern, value): + bindings = {} + stack = [(pattern, value)] + while stack: + pattern_node, value_node = stack.pop() + if isinstance(pattern_node, sexpr.Atom) and pattern_node.startswith("$"): + if pattern_node in bindings: + if not structural_equal(bindings[pattern_node], value_node): + return False + else: + bindings[pattern_node] = value_node + elif isinstance(pattern_node, sexpr.ListExpr): + if not isinstance(value_node, sexpr.ListExpr) or len(pattern_node) != len( + value_node + ): + return False + stack.extend(zip(pattern_node, value_node)) + elif not isinstance(value_node, sexpr.Atom) or pattern_node != value_node: + return False + return True + + +def body_exec_forms(body): + if not isinstance(body, sexpr.ListExpr) or not body or body[0] != ",": + return [] + return [ + (index, item) + for index, item in enumerate(body[1:]) + if is_exec_form(item) + ] + + +def emitted_exec_forms(heads): + if not isinstance(heads, sexpr.ListExpr) or not heads: + return [] + if heads[0] == ",": + return [ + (index, item) + for index, item in enumerate(heads[1:]) + if is_exec_form(item) + ] + if heads[0] == "O": + emitted = [] + for index, item in enumerate(heads[1:]): + if not isinstance(item, sexpr.ListExpr) or len(item) < 2: + continue + if item[0] in ("+", "pure") and is_exec_form(item[1]): + emitted.append((index, item[1])) + return emitted + if is_exec_form(heads): + return [(0, heads)] + return [] + + +def is_modified_self(emitted, handle): + if len(emitted) != 4 or len(handle) != 4: + return False + same_priority = structural_equal(emitted[1], handle[1]) + same_body_and_head = structural_equal( + emitted[2], handle[2] + ) and structural_equal(emitted[3], handle[3]) + priority_family = ( + isinstance(emitted[1], sexpr.ListExpr) + and isinstance(handle[1], sexpr.ListExpr) + and emitted[1] + and handle[1] + and structural_equal(emitted[1][0], handle[1][0]) + ) + return same_priority or (same_body_and_head and priority_family) + + +def analyze_respawn(expression): + if len(expression) != 4: + return None + handles = body_exec_forms(expression[2]) + emitted = emitted_exec_forms(expression[3]) + if not emitted: + return None + + self_handles = [ + (index, handle) + for index, handle in handles + if pattern_matches(handle, expression) + ] + for _, emitted_form in emitted: + if any( + not structural_equal(emitted_form, handle) + and is_modified_self(emitted_form, handle) + for _, handle in self_handles + ): + raise Refusal("SELF_MODIFYING_RULE") + + exact_emitted = [ + (index, emitted_form) + for index, emitted_form in emitted + if any( + structural_equal(emitted_form, handle) + for _, handle in self_handles + ) + ] + if len(exact_emitted) != len(emitted): + raise Refusal("FOREIGN_EXEC_TEMPLATE") + if ( + len(handles) != 1 + or len(self_handles) != 1 + or len(exact_emitted) != 1 + or not isinstance(expression[3], sexpr.ListExpr) + or not expression[3] + or expression[3][0] != "," + ): + raise Refusal("FOREIGN_EXEC_TEMPLATE") + return self_handles[0][0], exact_emitted[0][0], self_handles[0][1] + + +def analyze_program_respawns(rules): + analyses = {} + for rule in rules: + analyses[id(rule)] = analyze_respawn(rule) + for rule in rules: + analysis = analyses[id(rule)] + if analysis is None: + continue + handle = analysis[2] + for other in rules: + if other is rule or structural_equal(other, rule): + continue + if pattern_matches(handle, other): + raise Refusal("FOREIGN_EXEC_TEMPLATE") + return analyses + + +def parse_rule(expression, respawn=None): + if len(expression) > 4: + raise Refusal("COUNTED_EXEC_HEAD") + if len(expression) < 4: + raise Refusal("MALFORMED_EXEC") + priority, body, heads = expression[1:] + if variables(priority): + raise Refusal("VARIABLE_SOURCE_PRIORITY") + body = require_list(body, "UNCLASSIFIABLE_PATTERN") + heads = require_list(heads, "UNCLASSIFIABLE_TEMPLATE") + if not body or body[0] != ",": + if body and body[0] == "I": + raise Refusal("IO_SOURCE") + raise Refusal("UNCLASSIFIABLE_PATTERN") + if not heads or heads[0] != ",": + if heads and heads[0] == "O": + if any( + isinstance(item, sexpr.ListExpr) and item and item[0] == "-" + for item in heads[1:] + ): + raise Refusal("REMOVAL_TEMPLATE") + raise Refusal("IO_SINK") + raise Refusal("UNCLASSIFIABLE_TEMPLATE") + body_items = body[1:] + head_items = heads[1:] + if respawn is not None: + body_index, head_index, _ = respawn + body_items = tuple( + item for index, item in enumerate(body_items) if index != body_index + ) + head_items = tuple( + item for index, item in enumerate(head_items) if index != head_index + ) + factors = tuple(validate_pattern(item) for item in body_items) + templates = tuple(validate_template(item) for item in head_items) + if not factors: + raise Refusal("EMPTY_RULE_BODY") + if not templates: + raise Refusal("EMPTY_RULE_HEAD") + bound = set().union(*(variables(factor) for factor in factors)) + if len(bound) > 64: + raise Refusal("TOO_MANY_VARIABLES") + if len(bound) > 60: + raise Refusal("CONTROLLER_VARIABLE_LIMIT") + for template in templates: + if not variables(template) <= bound: + raise Refusal("UNBOUND_HEAD_VARIABLE") + return priority, factors, templates + + +def validate_pattern(pattern): + expression = require_list(pattern, "UNCLASSIFIABLE_PATTERN") + if not expression: + raise Refusal("UNCLASSIFIABLE_PATTERN") + if not isinstance(expression[0], sexpr.Atom): + raise Refusal("UNCLASSIFIABLE_PATTERN") + if expression[0].startswith("$"): + if ( + len(expression) != 3 + or not isinstance(expression[1], sexpr.Atom) + or expression[1].startswith("$") + or expression[1] in ("exec", "I", "O") + ): + raise Refusal("UNCLASSIFIABLE_PATTERN") + if expression[0] in ("exec", "I", "O"): + raise Refusal("UNCLASSIFIABLE_PATTERN") + return expression + + +def validate_template(template): + expression = relation(template, "UNCLASSIFIABLE_TEMPLATE") + if expression[0] == "O": + raise Refusal("IO_SINK") + if expression[0] in ("exec", "I"): + raise Refusal("UNCLASSIFIABLE_TEMPLATE") + return expression + + +def variables(expression): + found = set() + stack = [expression] + while stack: + node = stack.pop() + if isinstance(node, sexpr.ListExpr): + stack.extend(reversed(node)) + elif isinstance(node, sexpr.Atom) and node.startswith("$"): + found.add(node) + return found + + +def canonicalize_variables(expression, fixed_names=None): + names = dict(fixed_names or {}) + + def rename(node): + if node.startswith("$"): + return names.setdefault(node, "$sn_phase_%d" % len(names)) + return str(node) + + return sexpr.parse(sexpr.dump(expression, rename))[0] + + +def wrap(tag, expression): + return sexpr.list_expr(sexpr.atom(tag), expression) + + +def tagged(tag, *items): + if isinstance(tag, str): + tag = sexpr.atom(tag) + return sexpr.list_expr(tag, *items) + + +def turn(current, next_delta): + return tagged("t", current, next_delta) + + +def candidate(fact): + return tagged("c", fact) + + +def comma(*items): + return sexpr.list_expr(sexpr.atom(","), *items) + + +def output(*items): + return sexpr.list_expr(sexpr.atom("O"), *items) + + +def sink(operator, expression): + return sexpr.list_expr(sexpr.atom(operator), expression) + + +def priority(phase, source_priority, rule_index, variant_index): + return sexpr.list_expr( + sexpr.atom("s"), + sexpr.atom(phase), + source_priority, + sexpr.atom(rule_index * 1_000_000 + variant_index), + ) + + +def exec_rule(exec_priority, body, heads): + return sexpr.list_expr(sexpr.atom("exec"), exec_priority, body, heads) + + +def transform(expressions): + rule_expressions = [ + expression for expression in expressions if is_exec_form(expression) + ] + respawns = analyze_program_respawns(rule_expressions) + facts = [] + rules = [] + for expression in expressions: + if is_exec_form(expression): + rules.append(parse_rule(expression, respawns[id(expression)])) + else: + facts.append(validate_fact(expression)) + if not rules: + raise Refusal("NO_RULES") + + transformed = [] + for fact in facts: + transformed.append(wrap("f", fact)) + for fact in facts: + transformed.append(wrap("d0", fact)) + transformed.append(turn(sexpr.atom("d0"), sexpr.atom("d1"))) + + source_variable_names = set().union(*(variables(item) for item in expressions)) + current_name = "$sn_internal_current" + while current_name in source_variable_names: + current_name += "_" + source_variable_names.add(current_name) + next_name = "$sn_internal_next" + while next_name in source_variable_names: + next_name += "_" + current_delta = sexpr.atom(current_name) + next_delta = sexpr.atom(next_name) + parity_names = { + current_name: "$sn_phase_0", + next_name: "$sn_phase_1", + } + + phases = [] + for rule_index, (source_priority, factors, templates) in enumerate(rules): + for variant_index in range(len(factors)): + body = [] + for factor_index, factor in enumerate(factors): + if factor_index == variant_index: + body.append(tagged(current_delta, factor)) + else: + body.append(wrap("f", factor)) + heads = [ + candidate(template) + for template in templates + ] + phases.append( + exec_rule( + priority("0", source_priority, rule_index, variant_index), + comma(*body), + comma(*heads), + ) + ) + + fact = sexpr.atom("$sn_fact") + candidate_fact = candidate(fact) + phases.extend( + [ + exec_rule( + priority("1", sexpr.atom("0"), 0, 0), + comma(candidate_fact, wrap("f", fact)), + output(sink("-", candidate_fact)), + ), + exec_rule( + priority("2", sexpr.atom("0"), 0, 0), + comma(tagged(current_delta, fact)), + output(sink("-", tagged(current_delta, fact))), + ), + exec_rule( + priority("2", sexpr.atom("0"), 0, 1), + comma(turn(current_delta, next_delta)), + output(sink("-", turn(current_delta, next_delta))), + ), + exec_rule( + priority("3", sexpr.atom("0"), 0, 0), + comma(candidate_fact), + output( + sink("+", wrap("f", fact)), + sink("+", tagged(next_delta, fact)), + sink("+", turn(next_delta, current_delta)), + sink("-", candidate_fact), + ), + ), + ] + ) + phases = [ + canonicalize_variables(phase, parity_names) + for phase in phases + ] + + controller_pattern = sexpr.atom("$sn_controller_pattern") + controller_template = sexpr.atom("$sn_controller_template") + controller_current = sexpr.atom("$sn_phase_0") + controller_next = sexpr.atom("$sn_phase_1") + controller_priority = priority("4", sexpr.atom("0"), 0, 0) + controller_body = comma( + turn(controller_current, controller_next), + exec_rule( + controller_priority, + controller_pattern, + controller_template, + ), + ) + controller_heads = comma( + *phases, + exec_rule( + controller_priority, + controller_pattern, + controller_template, + ), + ) + + controller = exec_rule( + controller_priority, + controller_body, + controller_heads, + ) + if len(variables(controller)) > 64: + raise Refusal("CONTROLLER_VARIABLE_LIMIT") + transformed.append(controller) + return transformed + + +def main(): + parser = argparse.ArgumentParser(description=__doc__) + parser.add_argument("input") + parser.add_argument("output", nargs="?") + args = parser.parse_args() + + try: + with open(args.input, "r", encoding="utf-8") as stream: + source = stream.read() + rendered = sexpr.dumps(transform(sexpr.parse(source))) + if args.output: + with open(args.output, "w", encoding="utf-8", newline="\n") as stream: + stream.write(rendered) + else: + sys.stdout.write(rendered) + except Refusal as error: + print("REFUSE %s" % error, file=sys.stderr) + return 2 + except sexpr.ParseError as error: + print("REFUSE PARSE_ERROR: %s" % error, file=sys.stderr) + return 2 + except OSError as error: + print("ERROR IO_ERROR: %s" % error, file=sys.stderr) + return 2 + return 0 + + +if __name__ == "__main__": + sys.exit(main())