diff --git a/research/odd-native-common-grid/EXPECTED-BOUNDS.json b/research/odd-native-common-grid/EXPECTED-BOUNDS.json new file mode 100644 index 0000000000..10a6bfdfd7 --- /dev/null +++ b/research/odd-native-common-grid/EXPECTED-BOUNDS.json @@ -0,0 +1,43 @@ +{ + "caller": { + "coarse_height": 1240, + "coarse_mass_bits": 4362, + "denominator_height": 163, + "events": 3221, + "mass_bits": 126, + "maximum_mass": "16246698892210214036146399419475929893435/256", + "operations": { + "ADD": 2198, + "IDLE_ONE": 100, + "J": 18, + "LAMBDA": 206, + "QUERY": 10, + "SCALE": 180, + "SWAP": 509 + }, + "pre_joint_height": 154, + "pre_joint_mass_bits": 124 + }, + "word": { + "coefficient_numerator_bits": 24, + "coefficient_visits": 14060742, + "dyadic_height": 24, + "events": 71069, + "mass_witness": [ + 63297, + "stored add" + ], + "maximum_scaled_mass": "1636447290138225/16384", + "odd_scale": 1125, + "operations": { + "ADD": 60978, + "CLEAR": 54, + "COPY": 1, + "INIT": 54, + "MOVE": 6330, + "SCALE": 3652 + }, + "public_fields": 1452, + "scaled_mass_bits": 37 + } +} diff --git a/research/odd-native-common-grid/INDEPENDENT-BOUNDS.json b/research/odd-native-common-grid/INDEPENDENT-BOUNDS.json new file mode 100644 index 0000000000..653c1cbbd2 --- /dev/null +++ b/research/odd-native-common-grid/INDEPENDENT-BOUNDS.json @@ -0,0 +1,36 @@ +{ + "caller": { + "denominator_height": 163, + "maximum_mass": "16246698892210214036146399419475929893435/256", + "pre_joint_height": 154, + "pre_joint_mass": "758143798823020519902612486795530419693/64" + }, + "negative_scales": { + "225": "integer grid rejection at event 1101: denominator 250", + "375": "integer grid rejection at event 36915: denominator 48" + }, + "source_sha256": { + "caller.json": "5489eee96950881b0dd8fdecd6c02a3f663c60ba5bed0d5e5cbeed50fb9ae5fb", + "word.json.gz": "1cb1dd9acac7cc13dd5ef58162c9b89ac07215bf0364170db6940191d3605af5" + }, + "threshold": { + "357Kstar_bits": 14075, + "H": 1339210000000000000, + "Kstar_bits": 14066, + "gap_denominator": 10000000000000, + "integer_threshold_index": 133921, + "logarithm_power": 2224, + "source_check_sha256": "f1d6831810200ae6b677a32fc0e7fcf2c8bd9f033ae9fca7f8b1918ea5ed9f28" + }, + "word": { + "coefficient_visits": 14060742, + "dyadic_height": 24, + "mass_witness": [ + 63297, + "stored add" + ], + "maximum_scaled_mass": "1636447290138225/16384", + "numerator_bits": 24, + "odd_scale_lcm": 1125 + } +} diff --git a/research/odd-native-common-grid/INDEPENDENT-REVIEW.md b/research/odd-native-common-grid/INDEPENDENT-REVIEW.md new file mode 100644 index 0000000000..3c23f8560f --- /dev/null +++ b/research/odd-native-common-grid/INDEPENDENT-REVIEW.md @@ -0,0 +1,134 @@ +# Independent review of the odd native common-grid draft + +Reviewer: same-session research subagent, with substantial OpenAI assistance. +This is author-side independent-method review, not a human or formal-kernel +acceptance. No root-owned files were modified. + +## Frozen scope + +The reviewer froze the pre-clarification draft during the run. Its SHA-256 pins were: + +- `PROOF.md`: `0a3b37c82869c37afbcea50ed1e440a8c8e6e9f01f3a84476c004586c1bec82e` +- `audit_bounds.py`: `1e859d997e667514864871fd64e2b01039107708a848ddfec340e3947d0bbbcb` + +The exact source word/caller and threshold source are recorded in +`SOURCE-BYTES.json` and the executed `INDEPENDENT-BOUNDS.json`. Canonical base remains +`7c49fe32c55de02c2c873655c804b16e4c3fef0a`. The source-specific mathematical +claim is the per-call scale-1125 precision implication for candidate #6934, +not a proof of the candidate's native maps, physical supplier or complete bill. + +## Verdict + +No mathematical counterexample or blocking gap was found within the stated +ideal endpoint, same-root-factor, ownership, scheduling and source interfaces. +The conclusion remains conditional on those interfaces. The independent +integer engines reproduce the finite bounds used in the all-size argument. + +Two wording clarifications would improve the proof and make the inherited +scope harder to misread: + +1. Section 2's fresh helper mass 1 and height 0 are **relative to the current + raw-call entrance**. A helper introduced inside a nested compiler call + carries its actual entrance expansion in original root inputs; its root + mass/debt is not reset to 1/0. Section 3 and the credited #6901 proof imply + this interpretation, but the present short sentence should say so. +2. Interface 1 should explicitly say **Gaussian-dyadic Clifford**, including + absolute phase. A generic Clifford with an arbitrary global phase would + not imply the stated binary grid. The source construction is in the + Gaussian-dyadic subgroup; no extension to arbitrary global phases follows. + +It is also useful to state the short compiler size check: 153<2^8 and +8*1920=0 and D>=1. Finite external row counts, dirty public inputs, correlations +and spectators are arbitrary. Root preprocessing must supply p,h and layouts. + +## 2. Exact finite source envelopes + +The independent rational row interpreter treats MOVE as a chart change, +INIT as owned zero, CLEAR as lifetime completion, and ADD/COPY/SCALE as +literal row operations. It checks common-frame use and completed frames. +All stored rows and separate pre-ADD products, multiplied by S=1125, are +dyadic; completed public rows themselves are dyadic. The full scan visits +14,060,742 coefficients and obtains: + +| Local property | Exact bound | +|---|---:| +| Dyadic denominator height after scaling | 24 | +| Maximum scaled row/product l1 mass | 1636447290138225/16384 <2^37 | +| Scalar numerator bit length | 24 | + +Input scaling is included because S<2^37. These are finite source +certificates, not an independent native-map or all-size proof. + +A separate caller recurrence majorizes expansions in **products of Clifford +operators**, without commuting the products or substituting numerical +characters. For ADD, use M_t+|q|M_s and +max(H_t,H_s+v2(den(q))). SCALE, SWAP and QUERY use their literal rules. +IDLE is a Clifford product. LAMBDA is expanded as +((1+s i)I+(1-s i)Q^2)/2 for s=+-1. With Gaussian coefficient mass +|Re|+|Im|, its safe update is M<-2M and H<-H+1. + +At a joint event use the two actual type-A shear endpoints and type-B +(x-Qy,(Q^-1 x+y)/2), followed by the relevant Clifford. Their roles are +disjoint; both old B bounds are read before either is updated. The complete +current caller gives: + +| Cut | Dyadic height | Coefficient mass | +|---|---:|---:| +| Any completed caller event | <=163 | <=16246698892210214036146399419475929893435/256 <2^126 | +| Entrance of any joint call | <=154 | <=2^124 | + +Fresh productive helpers have mass1 and height0 relative to the current +raw-call entrance. A nested helper retains its actual entrance expansion and +all inherited debt relative to the original root inputs. During a local +call, composition with its scaled word adds the local bounds. Therefore, +including both caller-only and local-interior cuts, the raw caller has + +A=max(163,154+24)=178 exterior denominator bits, +B=max(126,124+37)=161 coefficient-mass bits, per unfinished context. + +A separate whole-stream product bound gives caller height1240 and mass +below2^4362. It cross-checks the eventwise numerical result using a different, +coarser aggregation. The written induction on these source operations is the +proof; endpoint norms alone would be insufficient. + +## 3. Per-call odd clearing and recursive reset + +For formal input row R and current chart D_v, the scaled local word holds +D_v(S R x). The source certificate makes its exterior coefficients dyadic. +The same certificate covers a pre-ADD product. Thus the odd part of each +divisor divides the stored integer numerator on every sufficiently fine +binary grid. At completion the unscaled endpoint is dyadic, so final +division by S is exact too. + +Each nested invocation scales its own actual entrances, runs the word and +unscales its completed outputs. Unfinished contexts accumulate mass and +binary denominator debt. A completed positive Gaussian endpoint resets the +**extra exterior debt relative to its entrance**, retaining all debt already +present at that entrance. Its Gaussian action joins the Clifford factor. +No numerical grid is reset. + +One S is charged per unfinished local context. Completed siblings add no +persistent debt. Scaling once by S at the outer boundary is a different +program and cannot replace arbitrary nesting: the boundary-only program +needs S raised to a proved depth bound, as #104 prescribes. The verifier +includes a nested exact-division countercontrol to this mistaken shortcut. + +This is a formal linear expansion in original complete root inputs, so no +independence of their values is needed. The expansion is proof state, not a +runtime data structure. Exterior scalars stay outside tensor powers. + +## 4. Current compiler depth and the integer threshold + +The candidate parameters are v=1920, carrier153, separated paid ceiling11^v, +productive floor12^v and m=153^v. In particular r_max=2. +These apply to the separated rule, not the unpowered raw rank-one targets. + +The retained compiler has complement n-s<(1-1/m)n and deepest-exit ratio +at most (r_max/m)(r_max/k_min)^G <=1-1/m. Its path has at most +m(1+floor(log2 n)) nonbase frames, each carrying at most +v(1+floor(log2 n)) raw contexts. Thus the credited recurrence specializes to + +K(n) <= v m (1+floor(log2 n))^2. + +Independently regenerate the written threshold from the source's exact +candidate/tested rationals and logarithm power2224: +H=1,339,210,000,000,000,000, N=2^H, and +K_star=1920*153^1920*(H+1)^2. +K_star has14066 bits; 357K_star has14075 bits, so 357K_star<2^H. +The threshold search has one crossing: with L=2224 and step=10^13, +(step*j+1)^L>2^j for j<=2L. For j>=2L the ratio of successive +((step*j+1)^L/2^j) values is strictly below +(1+1/j)^L/2 < 1/(2(1-L/j)) <=1. Thus checking the adjacent +integer indices justifies the regenerated threshold. +No floating logarithm or construction of N is used. Also153<2^8 and +8*1920=1, N ell<=N^ell<=D; for ell=0, t=0. Therefore 356t None: + if not ok: + raise ValueError(message) + + +def ceil_log2(q: Fraction | int) -> int: + q = Fraction(q) + require(q > 0, "positive logarithm argument") + k = q.numerator.bit_length() - q.denominator.bit_length() + if k >= 0: + if q.numerator > q.denominator << k: + k += 1 + elif q.numerator << -k > q.denominator: + k += 1 + return k + + +def v2(n: int) -> int: + require(n > 0, "positive denominator") + return (n & -n).bit_length() - 1 + + +def word_bounds(word: dict, scale: int = 1125) -> dict: + n = len(word["initial"]) + rows = [{i: Fraction(1)} for i in range(n)] + [dict() for _ in range(word["owned_fields"])] + frames = list(word["initial"]) + [None] * word["owned_fields"] + active = set() + maximum_mass = Fraction(scale) + height = 0 + max_numerator_bits = 0 + visits = 0 + witness = None + operations = Counter() + + def visit(row: dict, event: int, kind: str) -> None: + nonlocal maximum_mass, height, visits, witness + mass = Fraction(0) + for value in row.values(): + value *= scale + require(value.denominator == 1 << v2(value.denominator), + f"odd clearing fails at event {event} ({kind})") + height = max(height, v2(value.denominator)) + mass += abs(value) + visits += 1 + if mass > maximum_mass: + maximum_mass, witness = mass, (event, kind) + + for index, event in enumerate(word["program"]): + op, target = event[:2] + operations[op] += 1 + if op == "INIT": + require(target >= n and target not in active, "fresh owned INIT") + active.add(target) + frames[target] = event[2] + rows[target] = {} + elif op == "CLEAR": + require(target in active and frames[target] == event[2], "owned CLEAR") + active.remove(target) + frames[target] = None + rows[target] = {} + elif op == "MOVE": + require(frames[target] == event[2], "MOVE source frame") + frames[target] = event[3] + elif op == "SCALE": + factor = Fraction(event[2]) + require(frames[target] == event[3], "SCALE frame") + max_numerator_bits = max(max_numerator_bits, abs(factor.numerator).bit_length()) + rows[target] = {key: factor * value for key, value in rows[target].items() if factor * value} + visit(rows[target], index, "scale") + elif op in ("ADD", "COPY"): + source, factor = event[2], Fraction(event[3]) + require(source != target and frames[source] == frames[target] == event[4], "ADD common frame") + require(op != "COPY" or target in active and not rows[target], "COPY into owned zero") + max_numerator_bits = max(max_numerator_bits, abs(factor.numerator).bit_length()) + product = {key: factor * value for key, value in rows[source].items() if factor * value} + visit(product, index, "pre-add product") + new = rows[target].copy() + for key, value in product.items(): + new[key] = new.get(key, Fraction(0)) + value + if not new[key]: + del new[key] + rows[target] = new + visit(new, index, "stored add") + else: + raise ValueError("unknown word opcode " + op) + require(not active, "all owned lifetimes complete") + require(frames[:n] == word["final"], "public endpoint frames") + require(all(value.denominator == 1 << v2(value.denominator) + for row in rows[:n] for value in row.values()), "public endpoint dyadic") + require(all(not row for row in rows[n:]), "owned endpoint zero") + return {"events": len(word["program"]), "public_fields": n, "odd_scale": scale, + "dyadic_height": height, "maximum_scaled_mass": str(maximum_mass), + "scaled_mass_bits": ceil_log2(maximum_mass), "mass_witness": witness, + "coefficient_numerator_bits": max_numerator_bits, "coefficient_visits": visits, + "operations": dict(sorted(operations.items()))} + + +def caller_bounds(caller: dict) -> dict: + """Majorize the noncommutative expansion in Clifford words, not a character. + + Each complete native/idle/query Clifford has coefficient mass one. LAMBDA + is expanded as ((1+s*i) I + (1-s*i) Q^2)/2. Gaussian coefficient mass is + |Re|+|Im|; both coefficients therefore have mass one. No commutativity + or cancellation is used in this bound. + """ + count = caller["roles"] + masses = [Fraction(1) for _ in range(count)] + heights = [0 for _ in range(count)] + peak = Fraction(1) + peak_height = 0 + pre_joint_peak = Fraction(1) + pre_joint_height = 0 + crude_mass_bits = crude_height = 0 + operations = Counter() + + def note() -> None: + nonlocal peak, peak_height + peak = max(peak, *masses) + peak_height = max(peak_height, *heights) + + def combine(t: int, s: int, factor: Fraction) -> None: + nonlocal crude_mass_bits, crude_height + require(t != s, "caller aliases") + require(factor.denominator == 1 << v2(factor.denominator), "caller scalar must be dyadic") + masses[t] += abs(factor) * masses[s] + heights[t] = max(heights[t], heights[s] + v2(factor.denominator)) + + for event in caller["events"]: + if event[0] == "J": + operations["J"] += 1 + pre_joint_peak = max(pre_joint_peak, *masses) + pre_joint_height = max(pre_joint_height, *heights) + s, t, x, y = event[2] + require(len({s, t, x, y}) == 4, "four distinct A ports") + a2 = Fraction(caller["types"]["A"]["alpha2"]) + combine(t, s, Fraction(1)) + combine(x, y, a2) + bs, bt, al, be = event[3] + al, be = Fraction(al), Fraction(be) + require(bs != bt and {bs, bt}.isdisjoint({s, t, x, y}), "joint ports disjoint") + ms, mt, hs, ht = masses[bs], masses[bt], heights[bs], heights[bt] + require((al, be) == (Fraction(-1), Fraction(1, 2)), "retained B endpoint") + masses[bs] = ms + mt + masses[bt] = (ms + mt) / 2 + heights[bs] = max(hs, ht) + heights[bt] = max(hs, ht) + 1 + crude_mass_bits += max(1, ceil_log2(1 + abs(a2))) + crude_height += 1 + note() + continue + op = event[1] + operations[op] += 1 + t = event[2] + if op == "ADD": + q = Fraction(event[4]); combine(t, event[3], q) + crude_mass_bits += max(0, ceil_log2(1 + abs(q))) + crude_height += v2(q.denominator) + elif op == "SCALE": + q = Fraction(event[3]); require(q != 0, "nonzero SCALE") + require(q.denominator == 1 << v2(q.denominator), "dyadic SCALE") + masses[t] *= abs(q); heights[t] += v2(q.denominator) + crude_mass_bits += max(0, ceil_log2(abs(q))) + crude_height += v2(q.denominator) + elif op == "SWAP": + s = event[3]; require(s != t, "distinct SWAP") + masses[t], masses[s] = masses[s], masses[t] + heights[t], heights[s] = heights[s], heights[t] + elif op == "QUERY": + combine(t, event[3], Fraction(1)); crude_mass_bits += 1 + elif op == "LAMBDA": + require(event[3] in (-1, 1), "LAMBDA sign") + masses[t] *= 2; heights[t] += 1 + crude_mass_bits += 1; crude_height += 1 + elif op == "IDLE_ONE": + pass + else: + raise ValueError("unknown caller opcode " + op) + note() + require(peak <= 2**crude_mass_bits and peak_height <= crude_height, "independent coarse envelope") + return {"events": len(caller["events"]), "maximum_mass": str(peak), + "mass_bits": ceil_log2(peak), "denominator_height": peak_height, + "pre_joint_mass_bits": ceil_log2(pre_joint_peak), "pre_joint_height": pre_joint_height, + "coarse_mass_bits": crude_mass_bits, "coarse_height": crude_height, + "operations": dict(sorted(operations.items()))} + + +def main() -> None: + ap = argparse.ArgumentParser() + ap.add_argument("--source", type=Path, required=True) + args = ap.parse_args() + word = json.loads(gzip.decompress((args.source / "word.json.gz").read_bytes())) + caller = json.loads((args.source / "caller.json").read_text()) + result = {"word": word_bounds(word), "caller": caller_bounds(caller)} + print(json.dumps(result, indent=2, sort_keys=True)) + + +if __name__ == "__main__": + main() diff --git a/research/odd-native-common-grid/audit_controls.py b/research/odd-native-common-grid/audit_controls.py new file mode 100644 index 0000000000..9c1b99873c --- /dev/null +++ b/research/odd-native-common-grid/audit_controls.py @@ -0,0 +1,119 @@ +"""Adversarial controls on the theorem's scope, not a physical simulator. + +Prepared for @CubeJerry with substantial OpenAI assistance. Apache-2.0. +""" +from __future__ import annotations + +from copy import deepcopy +from fractions import Fraction as Q + +from audit_bounds import caller_bounds, ceil_log2, require, word_bounds + + +def rejects(call, phrase): + try: + call() + except ValueError as error: + require(phrase in str(error), "specific control rejection: " + str(error)) + return str(error) + raise ValueError("negative control unexpectedly accepted: " + phrase) + + +def controls(word, caller): + checks = {} + count = 0 + for a in range(1, 130): + for b in range(1, 130): + value = Q(a, b) + k = ceil_log2(value) + upper = Q(2) ** k + require(upper / 2 < value <= upper, "independent exact logarithm bracket") + count += 1 + checks["exact_logarithm_brackets"] = count + checks["too_small_S225"] = rejects(lambda: word_bounds(word, 225), "odd clearing fails at event 1101") + + tiny = {"initial": [0, 0], "final": [0, 0], "owned_fields": 0, + "program": [["ADD", 0, 1, "1/7", 0]]} + checks["unfunded_prime"] = rejects(lambda: word_bounds(tiny, 1125), "odd clearing fails") + tiny["program"] = [["ADD", 0, 1, "1", 1]] + checks["wrong_frame"] = rejects(lambda: word_bounds(tiny), "ADD common frame") + tiny["program"] = [["COPY", 0, 1, "1", 0]] + checks["copy_nonzero_public"] = rejects(lambda: word_bounds(tiny), "COPY into owned zero") + tiny["program"] = [["MOVE", 0, 1, 0, False]] + checks["wrong_move_source"] = rejects(lambda: word_bounds(tiny), "MOVE source frame") + tiny["program"] = [["SCALE", 0, "1/3", 0]] + checks["nondyadic_completed_endpoint"] = rejects(lambda: word_bounds(tiny), "public endpoint dyadic") + + bad = deepcopy(caller) + entry = next(e for e in bad["events"] if e[0] != "J" and e[1] == "ADD") + entry[4] = "1/3" + checks["odd_caller_scalar"] = rejects(lambda: caller_bounds(bad), "caller scalar must be dyadic") + bad = deepcopy(caller) + joint = next(e for e in bad["events"] if e[0] == "J") + joint[2][1] = joint[2][0] + checks["joint_alias"] = rejects(lambda: caller_bounds(bad), "four distinct A ports") + bad = deepcopy(caller) + joint = next(e for e in bad["events"] if e[0] == "J") + joint[3][3] = "1/3" + checks["changed_B_endpoint"] = rejects(lambda: caller_bounds(bad), "retained B endpoint") + + # An identity endpoint can still incur one odd division per unfinished + # context. A single outer scale3 funds depth1 and fails at depth2. + def once_scaled(depth, initial): + value = initial + for _ in range(depth): + require(value.denominator == 1 and value.numerator % 3 == 0, + "nested boundary-only odd remainder") + value /= 3 + for _ in range(depth): + value *= 3 + return value + + require(once_scaled(1, Q(3)) == 3, "one-level positive control") + checks["one_outer_scale_fails_at_depth_two"] = rejects( + lambda: once_scaled(2, Q(3)), "nested boundary-only odd remainder") + + def per_call(depth, x): + scaled = 3*x + require(scaled.denominator == 1 and scaled.numerator % 3 == 0, + "per-call exact odd division") + middle = scaled/3 + if depth: + middle = per_call(depth-1, middle) + scaled_out = 3*middle + require(scaled_out.numerator % 3 == 0, "per-call exact return division") + return scaled_out/3 + + for depth in range(21): + for x in range(-5, 6): + require(per_call(depth, Q(x)) == x, "per-call scaled nested identity") + checks["per_call_nested_signed_cases"] = 21*11 + value = Q(1) + for _ in range(100): + value = per_call(0, value) + require(value == 1, "completed siblings preserve entrance debt") + checks["completed_siblings"] = 100 + + # D=1 and P=diag(1,0): (P C P)^3 has (-1+i)/4, exceeding the + # Clifford denominator cap 2^ceil(D/2). Thus active selection is excluded. + def cmul(a, b): + return (a[0]*b[0]-a[1]*b[1], a[0]*b[1]+a[1]*b[0]) + z = (Q(1), Q(0)) + for _ in range(3): + z = cmul(z, (Q(1,2), Q(1,2))) + require(z == (Q(-1,4), Q(1,4)) and max(x.denominator for x in z) > 2, + "active projection destroys fixed-root Clifford denominator cap") + checks["active_projector_counterexample"] = [str(x) for x in z] + + # The text proves the quantified inequalities; this detects off-by-one + # mistakes at finite boundary cases and is not their universal proof. + samples = 0 + for D in range(1, 2001): + for t in {0, (D-1)//356}: + require(356*t < D, "boundary depth sample") + require((D+1)//2+178*t <= D, "fractional format boundary") + require((D+2)//2+161*t+1 <= D+2, "magnitude format boundary") + samples += 1 + checks["format_integer_boundary_samples"] = samples + checks["universal_proof_from_finite_sweep"] = False + return checks diff --git a/research/odd-native-common-grid/independent_bounds.py b/research/odd-native-common-grid/independent_bounds.py new file mode 100644 index 0000000000..8fe729386f --- /dev/null +++ b/research/odd-native-common-grid/independent_bounds.py @@ -0,0 +1,267 @@ +"""Read-only author-side audit of the odd-grid package. + +Independent fixed-grid integer word engine and positive transfer matrix caller +engine. This does not prove native/endpoint identities or run a physical tape. +Prepared for @CubeJerry with substantial OpenAI assistance. +""" +from __future__ import annotations + +from collections import Counter +from hashlib import sha256 +from math import gcd, lcm +from pathlib import Path +import ast +import gzip +import json + +ROOT = Path(__file__).resolve().parent +SOURCE = ROOT / "source/data" + + +def need(ok, message): + if not ok: + raise ValueError(message) + + +def rational(text): + bits = str(text).split("/") + return (int(bits[0]), int(bits[1]) if len(bits) == 2 else 1) + + +def height(n): + need(n > 0 and n & (n - 1) == 0, "dyadic denominator") + return n.bit_length() - 1 + + +def reduced(n, d): + g = gcd(n, d) + return str(n // g) if d // g == 1 else f"{n//g}/{d//g}" + + +def word_run(word, scale=1125, frac=24): + """Store every formal row on the *one fixed* scale*2^frac integer grid.""" + n = len(word["initial"]) + unit = 1 << frac + rows = [{i: scale * unit} for i in range(n)] + rows += [{} for _ in range(word["owned_fields"])] + frames = list(word["initial"]) + [None] * word["owned_fields"] + live = set() + peak, odd_lcm, high, visits = scale * unit, 1, 0, 0 + numerator_bits = 0 + witness = None + + def observe(row, index, kind): + nonlocal peak, odd_lcm, high, visits, witness + mass = sum(abs(value) for value in row.values()) + if mass > peak: + peak, witness = mass, (index, kind) + for value in row.values(): + if not value: + continue + odd_lcm = lcm(odd_lcm, scale // gcd(value, scale)) + trailing = (abs(value) & -abs(value)).bit_length() - 1 + high = max(high, frac - trailing) + visits += 1 + + def multiply(row, q, index): + a, b = rational(q) + result = {} + for key, value in row.items(): + quotient, residue = divmod(value * a, b) + need(residue == 0, f"integer grid rejection at event {index}: denominator {b}") + if quotient: + result[key] = quotient + return result + + for index, event in enumerate(word["program"]): + op, target = event[:2] + if op == "INIT": + need(target >= n and target not in live, "fresh owner") + live.add(target); rows[target] = {}; frames[target] = event[2] + elif op == "CLEAR": + need(target in live and frames[target] == event[2], "owner clear") + live.remove(target); rows[target] = {}; frames[target] = None + elif op == "MOVE": + need(frames[target] == event[2], "source chart") + frames[target] = event[3] + elif op == "SCALE": + need(frames[target] == event[3], "scale chart") + numerator_bits = max(numerator_bits, abs(rational(event[2])[0]).bit_length()) + rows[target] = multiply(rows[target], event[2], index) + observe(rows[target], index, "scale") + elif op in ("ADD", "COPY"): + source = event[2] + need(target != source and frames[target] == frames[source] == event[4], "common chart") + need(op != "COPY" or target in live and not rows[target], "copy zero") + numerator_bits = max(numerator_bits, abs(rational(event[3])[0]).bit_length()) + product = multiply(rows[source], event[3], index) + observe(product, index, "pre-add product") + result = rows[target].copy() + for key, value in product.items(): + result[key] = result.get(key, 0) + value + if not result[key]: + del result[key] + rows[target] = result + observe(result, index, "stored add") + else: + raise ValueError(op) + need(not live and frames[:n] == word["final"], "completed owned/frame endpoints") + need(all(value % scale == 0 for row in rows[:n] for value in row.values()), "unscaled public rows dyadic") + need(all(not row for row in rows[n:]), "private rows gone") + return dict(odd_scale_lcm=odd_lcm, dyadic_height=high, + maximum_scaled_mass=reduced(peak, unit), mass_witness=witness, + numerator_bits=numerator_bits, coefficient_visits=visits) + + +def caller_run(caller): + """Propagate all 78 positive input contributions on a common integer grid. + + Matrix entries count triangle-inequality contributions; they do not commute + Clifford words or evaluate numerical characters. The common scale only + grows and all divisions below are integer-exact after that scale change. + """ + count = caller["roles"] + rows = [[int(i == j) for j in range(count)] for i in range(count)] + debts = [0] * count + scale = 0 + maximum = pre_joint = (1, 0) + maximum_debt = joint_debt = 0 + + def larger(pair, candidate): + a, k = pair; b, ell = candidate + return candidate if (b << k) > (a << ell) else pair + + def denominator(bits): + nonlocal scale, rows + if bits: + rows = [[value << bits for value in row] for row in rows] + scale += bits + + for event in caller["events"]: + if event[0] == "J": + pre_joint = larger(pre_joint, (max(map(sum, rows)), scale)) + joint_debt = max(joint_debt, *debts) + s, t, x, y = event[2] + bs, bt, alpha, beta = event[3] + need(len({s, t, x, y, bs, bt}) == 6, "joint owner separation") + need(rational(alpha) == (-1, 1) and rational(beta) == (1, 2), "actual B pair") + a, b = rational(caller["types"]["A"]["alpha2"]) + need(b == 1, "actual A integer shear") + denominator(1) + rows[t] = [u + v for u, v in zip(rows[t], rows[s])] + rows[x] = [u + abs(a) * v for u, v in zip(rows[x], rows[y])] + combo = [u + v for u, v in zip(rows[bs], rows[bt])] + need(all(v % 2 == 0 for v in combo), "B integer halving") + rows[bs], rows[bt] = combo, [v // 2 for v in combo] + debts[t], debts[x] = max(debts[t], debts[s]), max(debts[x], debts[y]) + newdebt = max(debts[bs], debts[bt]) + debts[bs], debts[bt] = newdebt, newdebt + 1 + else: + op, t = event[1:3] + if op in ("ADD", "SCALE"): + a, b = rational(event[4] if op == "ADD" else event[3]) + k = height(b); denominator(k) + if op == "ADD": + source = event[3] + need(all(abs(a) * v % b == 0 for v in rows[source]), "ADD integer grid") + rows[t] = [u + abs(a) * v // b for u, v in zip(rows[t], rows[source])] + debts[t] = max(debts[t], debts[source] + k) + else: + need(all(abs(a) * v % b == 0 for v in rows[t]), "SCALE integer grid") + rows[t] = [abs(a) * v // b for v in rows[t]] + debts[t] += k + elif op == "QUERY": + source = event[3] + rows[t] = [u + v for u, v in zip(rows[t], rows[source])] + debts[t] = max(debts[t], debts[source]) + elif op == "SWAP": + source = event[3] + rows[t], rows[source] = rows[source], rows[t] + debts[t], debts[source] = debts[source], debts[t] + elif op == "LAMBDA": + rows[t] = [2 * v for v in rows[t]] + debts[t] += 1 + elif op != "IDLE_ONE": + raise ValueError(op) + maximum = larger(maximum, (max(map(sum, rows)), scale)) + maximum_debt = max(maximum_debt, *debts) + return dict(maximum_mass=reduced(maximum[0], 1 << maximum[1]), + pre_joint_mass=reduced(pre_joint[0], 1 << pre_joint[1]), + denominator_height=maximum_debt, pre_joint_height=joint_debt) + + +def threshold_run(): + """Read source literals by AST and regenerate the threshold by integers.""" + check = SOURCE.parent / "check.py" + nodes = ast.parse(check.read_text()).body + values = {} + for node in nodes: + if not isinstance(node, ast.Assign) or len(node.targets) != 1: + continue + target = node.targets[0] + if isinstance(target, ast.Tuple) and all(isinstance(x, ast.Name) for x in target.elts): + names = [x.id for x in target.elts] + if names == ["KAPPA", "TESTED"]: + for name, value in zip(names, node.value.elts): + need(isinstance(value, ast.Call) and isinstance(value.args[0], ast.Constant), "price source literal") + digits = value.args[0].value + before, after = digits.split(".") + values[name] = (int((before or "0") + after), 10 ** len(after)) + elif names == ["LPMIN", "LP"]: + values["LP"] = node.value.elts[1].value + a, b = values["KAPPA"] + c, d = values["TESTED"] + numerator, denominator = c*b-a*d, 7*b*d + common = gcd(numerator, denominator) + need(numerator // common == 1, "unit exact source gap") + step = denominator // common + power = values["LP"] + def wins(j): + return pow(step*j+1, power) < 1 << j + lo, hi = 1, 2 + while not wins(hi): + lo, hi = hi, hi*2 + while hi-lo > 1: + mid = (hi+lo)//2 + if wins(mid): + hi = mid + else: + lo = mid + h = step*hi + need(wins(hi) and not wins(hi-1), "threshold neighbors") + kstar = 1920*pow(153, 1920)*pow(h+1, 2) + need(h == 1339210000000000000 and kstar.bit_length() == 14066 + and (357*kstar).bit_length() == 14075 < h, "symbolic threshold margin") + return {"H": h, "integer_threshold_index": hi, "gap_denominator": step, + "logarithm_power": power, "Kstar_bits": kstar.bit_length(), + "357Kstar_bits": (357*kstar).bit_length(), + "source_check_sha256": sha256(check.read_bytes()).hexdigest()} + + +def main(): + word = json.loads(gzip.decompress((SOURCE / "word.json.gz").read_bytes())) + caller = json.loads((SOURCE / "caller.json").read_text()) + result = {"source_sha256": {n: sha256((SOURCE/n).read_bytes()).hexdigest() + for n in ("word.json.gz", "caller.json")}, + "word": word_run(word), "caller": caller_run(caller), "negative_scales": {}} + for scale in (375, 225): + try: + word_run(word, scale=scale) + except ValueError as error: + result["negative_scales"][str(scale)] = str(error) + else: + raise ValueError("insufficient odd scale was accepted") + expected = json.loads((ROOT / "EXPECTED-BOUNDS.json").read_text()) + for key in ("dyadic_height", "maximum_scaled_mass", "coefficient_visits"): + need(result["word"][key] == expected["word"][key], "independent word agreement: " + key) + need(result["word"]["odd_scale_lcm"] == 1125, "minimal source-derived scale") + need(result["word"]["numerator_bits"] == 24, "literal numerator width") + for key in ("maximum_mass", "denominator_height", "pre_joint_height"): + need(result["caller"][key] == expected["caller"][key], "independent caller agreement: " + key) + result["threshold"] = threshold_run() + print(json.dumps(result, sort_keys=True, indent=2)) + print("PASS_INDEPENDENT_ODD_GRID_BOUNDS") + + +if __name__ == "__main__": + main() diff --git a/research/odd-native-common-grid/source/LICENSE b/research/odd-native-common-grid/source/LICENSE new file mode 100644 index 0000000000..261eeb9e9f --- /dev/null +++ b/research/odd-native-common-grid/source/LICENSE @@ -0,0 +1,201 @@ + Apache License + Version 2.0, January 2004 + http://www.apache.org/licenses/ + + TERMS AND CONDITIONS FOR USE, REPRODUCTION, AND DISTRIBUTION + + 1. Definitions. + + "License" shall mean the terms and conditions for use, reproduction, + and distribution as defined by Sections 1 through 9 of this document. + + "Licensor" shall mean the copyright owner or entity authorized by + the copyright owner that is granting the License. + + "Legal Entity" shall mean the union of the acting entity and all + other entities that control, are controlled by, or are under common + control with that entity. For the purposes of this definition, + "control" means (i) the power, direct or indirect, to cause the + direction or management of such entity, whether by contract or + otherwise, or (ii) ownership of fifty percent (50%) or more of the + outstanding shares, or (iii) beneficial ownership of such entity. + + "You" (or "Your") shall mean an individual or Legal Entity + exercising permissions granted by this License. + + "Source" form shall mean the preferred form for making modifications, + including but not limited to software source code, documentation + source, and configuration files. + + "Object" form shall mean any form resulting from mechanical + transformation or translation of a Source form, including but + not limited to compiled object code, generated documentation, + and conversions to other media types. + + "Work" shall mean the work of authorship, whether in Source or + Object form, made available under the License, as indicated by a + copyright notice that is included in or attached to the work + (an example is provided in the Appendix below). + + "Derivative Works" shall mean any work, whether in Source or Object + form, that is based on (or derived from) the Work and for which the + editorial revisions, annotations, elaborations, or other modifications + represent, as a whole, an original work of authorship. For the purposes + of this License, Derivative Works shall not include works that remain + separable from, or merely link (or bind by name) to the interfaces of, + the Work and Derivative Works thereof. + + "Contribution" shall mean any work of authorship, including + the original version of the Work and any modifications or additions + to that Work or Derivative Works thereof, that is intentionally + submitted to Licensor for inclusion in the Work by the copyright owner + or by an individual or Legal Entity authorized to submit on behalf of + the copyright owner. For the purposes of this definition, "submitted" + means any form of electronic, verbal, or written communication sent + to the Licensor or its representatives, including but not limited to + communication on electronic mailing lists, source code control systems, + and issue tracking systems that are managed by, or on behalf of, the + Licensor for the purpose of discussing and improving the Work, but + excluding communication that is conspicuously marked or otherwise + designated in writing by the copyright owner as "Not a Contribution." + + "Contributor" shall mean Licensor and any individual or Legal Entity + on behalf of whom a Contribution has been received by Licensor and + subsequently incorporated within the Work. + + 2. Grant of Copyright License. Subject to the terms and conditions of + this License, each Contributor hereby grants to You a perpetual, + worldwide, non-exclusive, no-charge, royalty-free, irrevocable + copyright license to reproduce, prepare Derivative Works of, + publicly display, publicly perform, sublicense, and distribute the + Work and such Derivative Works in Source or Object form. + + 3. Grant of Patent License. Subject to the terms and conditions of + this License, each Contributor hereby grants to You a perpetual, + worldwide, non-exclusive, no-charge, royalty-free, irrevocable + (except as stated in this section) patent license to make, have made, + use, offer to sell, sell, import, and otherwise transfer the Work, + where such license applies only to those patent claims licensable + by such Contributor that are necessarily infringed by their + Contribution(s) alone or by combination of their Contribution(s) + with the Work to which such Contribution(s) was submitted. If You + institute patent litigation against any entity (including a + cross-claim or counterclaim in a lawsuit) alleging that the Work + or a Contribution incorporated within the Work constitutes direct + or contributory patent infringement, then any patent licenses + granted to You under this License for that Work shall terminate + as of the date such litigation is filed. + + 4. Redistribution. You may reproduce and distribute copies of the + Work or Derivative Works thereof in any medium, with or without + modifications, and in Source or Object form, provided that You + meet the following conditions: + + (a) You must give any other recipients of the Work or + Derivative Works a copy of this License; and + + (b) You must cause any modified files to carry prominent notices + stating that You changed the files; and + + (c) You must retain, in the Source form of any Derivative Works + that You distribute, all copyright, patent, trademark, and + attribution notices from the Source form of the Work, + excluding those notices that do not pertain to any part of + the Derivative Works; and + + (d) If the Work includes a "NOTICE" text file as part of its + distribution, then any Derivative Works that You distribute must + include a readable copy of the attribution notices contained + within such NOTICE file, excluding those notices that do not + pertain to any part of the Derivative Works, in at least one + of the following places: within a NOTICE text file distributed + as part of the Derivative Works; within the Source form or + documentation, if provided along with the Derivative Works; or, + within a display generated by the Derivative Works, if and + wherever such third-party notices normally appear. The contents + of the NOTICE file are for informational purposes only and + do not modify the License. You may add Your own attribution + notices within Derivative Works that You distribute, alongside + or as an addendum to the NOTICE text from the Work, provided + that such additional attribution notices cannot be construed + as modifying the License. + + You may add Your own copyright statement to Your modifications and + may provide additional or different license terms and conditions + for use, reproduction, or distribution of Your modifications, or + for any such Derivative Works as a whole, provided Your use, + reproduction, and distribution of the Work otherwise complies with + the conditions stated in this License. + + 5. Submission of Contributions. Unless You explicitly state otherwise, + any Contribution intentionally submitted for inclusion in the Work + by You to the Licensor shall be under the terms and conditions of + this License, without any additional terms or conditions. + Notwithstanding the above, nothing herein shall supersede or modify + the terms of any separate license agreement you may have executed + with Licensor regarding such Contributions. + + 6. Trademarks. This License does not grant permission to use the trade + names, trademarks, service marks, or product names of the Licensor, + except as required for reasonable and customary use in describing the + origin of the Work and reproducing the content of the NOTICE file. + + 7. Disclaimer of Warranty. Unless required by applicable law or + agreed to in writing, Licensor provides the Work (and each + Contributor provides its Contributions) on an "AS IS" BASIS, + WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or + implied, including, without limitation, any warranties or conditions + of TITLE, NON-INFRINGEMENT, MERCHANTABILITY, or FITNESS FOR A + PARTICULAR PURPOSE. You are solely responsible for determining the + appropriateness of using or redistributing the Work and assume any + risks associated with Your exercise of permissions under this License. + + 8. Limitation of Liability. In no event and under no legal theory, + whether in tort (including negligence), contract, or otherwise, + unless required by applicable law (such as deliberate and grossly + negligent acts) or agreed to in writing, shall any Contributor be + liable to You for damages, including any direct, indirect, special, + incidental, or consequential damages of any character arising as a + result of this License or out of the use or inability to use the + Work (including but not limited to damages for loss of goodwill, + work stoppage, computer failure or malfunction, or any and all + other commercial damages or losses), even if such Contributor + has been advised of the possibility of such damages. + + 9. Accepting Warranty or Additional Liability. While redistributing + the Work or Derivative Works thereof, You may choose to offer, + and charge a fee for, acceptance of support, warranty, indemnity, + or other liability obligations and/or rights consistent with this + License. However, in accepting such obligations, You may act only + on Your own behalf and on Your sole responsibility, not on behalf + of any other Contributor, and only if You agree to indemnify, + defend, and hold each Contributor harmless for any liability + incurred by, or claims asserted against, such Contributor by reason + of your accepting any such warranty or additional liability. + + END OF TERMS AND CONDITIONS + + APPENDIX: How to apply the Apache License to your work. + + To apply the Apache License to your work, attach the following + boilerplate notice, with the fields enclosed by brackets "[]" + replaced with your own identifying information. (Don't include + the brackets!) The text should be enclosed in the appropriate + comment syntax for the file format. We also recommend that a + file or class name and description of purpose be included on the + same "printed page" as the copyright notice for easier + identification within third-party archives. + + Copyright [yyyy] [name of copyright owner] + + Licensed under the Apache License, Version 2.0 (the "License"); + you may not use this file except in compliance with the License. + You may obtain a copy of the License at + + http://www.apache.org/licenses/LICENSE-2.0 + + Unless required by applicable law or agreed to in writing, software + distributed under the License is distributed on an "AS IS" BASIS, + WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied. + See the License for the specific language governing permissions and + limitations under the License. diff --git a/research/odd-native-common-grid/source/NOTICE b/research/odd-native-common-grid/source/NOTICE new file mode 100644 index 0000000000..06a4064bf1 --- /dev/null +++ b/research/odd-native-common-grid/source/NOTICE @@ -0,0 +1,5 @@ +Hosted chain-nested root, hosted native word, caller replay and checks: DreamingOfClouds with Claude Opus 5.5 (Anthropic), via Claude Code. Apache-2.0. + +Retained, unchanged (native.py with the changes listed in README.md): retained/runtime (interval engines and outer ledger) and retained/native/clifford_exact.py, retained/native/native_verify.py and native.py (the exact native replay, Adapted from Ali Romman's independent-helper verifier, inventory and retiming extension by Jerry Chen / @CubeJerry) keep their original headers and lineage from the #6833 package. The native word run verbatim is the #6824 word (#6702 native source by DreamingOfClouds, helper-basis mechanism by Ali Romman, retiming and helper retirement by Jerry Chen / @CubeJerry with OpenAI Codex assistance). The caller line follows #6726 (zxv) and #6716 (thu-nmrc). + +Odd gate scalars: the grid with one numerator scale and exact division follows #104 (icekylinx, notes/stopped-product-complex.tex lines 75-106) and its merged notes. The type A constant blocks of the caller (data/caller_6912_after.json) are from #6912 (CubeJerry); check_caller_blocks.py and jclib.py check them, and check_a6.py with a6lib.py ports the owned-rise argument of #6914 (CubeJerry, with OpenAI Codex) and the width-2 phase test of #6930 (unpaidmoon, with Cursor Grok); this code is by DreamingOfClouds with Claude Opus 5.5 (Anthropic), via Claude Code. The verifier verify_host3_dyadic.py and its odd-scalar version verify_host3_odd.py, physical_exact.py, mutants.py, division_pass.py and controls.py: DreamingOfClouds with Claude Opus 5.5 (Anthropic), via Claude Code. Apache-2.0. The word of #6932 is the comparison word (data/prior_word_6932.json.gz). diff --git a/research/odd-native-common-grid/source/check.py b/research/odd-native-common-grid/source/check.py new file mode 100644 index 0000000000..acb43c64bb --- /dev/null +++ b/research/odd-native-common-grid/source/check.py @@ -0,0 +1,563 @@ +#!/usr/bin/env python3 +"""The shared odd-grid native word with gate scalars 1/3 and 1/5 (a declared framework change): exact replay of the word over A = Z[1/2, 1/3, 1/5] with the certificate S = 1125, both roots, the joint caller, +the complete invoice and the outer constants. Standard library only (plus the retained interval engines). +python3 -I -B check.py (writes nothing) +Steps: (1) event-by-event exact replay of data/word.json.gz with the endpoint of each port type, the alphabet A, the odd certificate S (every prefix row and every pre-ADD product), heights, scans; the odd verifier and its rejections; +(2) both roots with failing controls; (3) the joint caller (78 roles, block diagonal, one stage value per stage) at the four central characters, with wrong-root, wrong-port-type and swapped-assignment controls; +(4) the invoice recounted from the emitted events and rebuilt from the two roots, with the #6932, #6931, #6919, #6917 and #6911 words and #6833 as controls; (5) raw bound by three definitions, the LAMBDA recharge, the root-scale and +per-input scale readings, growth; (6) BIT pins, interval engines, strictification, compiler and outer ledger; departures. Prints PASS_P104_SHARED_ODD_NATIVE. +(physical.py, physical_exact.py, caller_physical.py, native_maps.py, second_engine.py, mutants.py, division_pass.py, controls.py, ordinary.py, check_caller_blocks.py and check_a6.py are the other commands.)""" +import gzip, json, os, sys, subprocess, importlib.util, random, hashlib, math, copy +from collections import Counter +from decimal import Decimal as D, getcontext +from fractions import Fraction as Q +getcontext().prec = 60 +HERE = os.path.dirname(os.path.abspath(__file__)) +def need(ok, msg): + if not ok: raise SystemExit('FAIL ' + msg) + print('PASS', msg, flush=True) +data = lambda n: os.path.join(HERE, 'data', n) +PIN = Q(376669, 100000000) # ordinary BIT saving of the open #6726 two-fragment admission (retained/bit/FRAGMENT-BIT-ADMISSION.json) +def ldmod(path, name): + s = importlib.util.spec_from_file_location(name, path); m = importlib.util.module_from_spec(s); sys.modules[name] = m; s.loader.exec_module(m); return m + +# ---- (1) replay of the word ------------------------------------------------------------------- +W = json.load(gzip.open(data('word.json.gz'), 'rt')) +def span(b): + s = {0} + for v in b: + if not (isinstance(v, int) and 0 < v < 512 and v not in s): raise SystemExit('FAIL dependent basis') + s |= {x ^ v for x in s} + return frozenset(s) +fr = W['frames']; sp = [span(b) for b in fr]; dim = [len(b) for b in fr] +n = len(W['initial']); NO = W['owned_fields']; NR = n + NO +cur = list(W['initial']) + [None] * NO; row = [({r: Q(1)} if r < n else {}) for r in range(NR)] +owned = set(); viol = Counter(); owned_up = Counter(); up_idx = []; paid = Counter(); peak = life = dirty = 0; maxq = Q(0); logq = 0.0; pmax = Q(0); dmaxb = 0; nbits = dbits = 0 +dy = lambda q: q.denominator & (q.denominator - 1) == 0 +def sm(m, ps=(2, 3, 5)): + m = abs(m) + for p_ in ps: + while m % p_ == 0: m //= p_ + return m == 1 +def oddpart(m): + m = abs(m) + while m % 2 == 0: m //= 2 + return m +SC = 1125 # the declared certificate: S = 3^2 * 5^3 +odd_dens = set(); v2max = 0; dmax = 1; mass = Q(0); odd_div = Counter(); odd_events = Counter(); bad_S = Counter() +def note(rw, tag): + global mass, v2max, dmax + m = Q(0) + for v in rw.values(): + d = v.denominator; v2max = max(v2max, (d & -d).bit_length() - 1); dmax = max(dmax, d) + if d & (d - 1): odd_dens.add(oddpart(d)) + if not dy(SC * v): bad_S[tag] += 1 + m += abs(SC * v) + if m > mass: mass = m +for i, e in enumerate(W['program']): + op, r = e[0], e[1] + if op == 'MOVE': + _, r, a, b, pv = e + if cur[r] != a or (r in owned) != bool(pv): viol['transport source or ownership'] += 1 + if pv: + if sp[a] < sp[b]: owned_up[dim[b] - dim[a]] += 1; up_idx.append(i) + elif not sp[b] < sp[a]: viol['owned move not nested'] += 1 + elif not sp[a] < sp[b]: viol['public move not strictly ascending'] += 1 + paid[abs(dim[b] - dim[a])] += 1; cur[r] = b + elif op == 'INIT': + if not (r >= n and r not in owned): viol['INIT'] += 1 + owned.add(r); life += 1; peak = max(peak, len(owned)); cur[r] = e[2]; row[r] = {} + elif op == 'CLEAR': + if not (r in owned and cur[r] == e[2]): viol['CLEAR'] += 1 + dirty += bool(row[r]); owned.discard(r); cur[r] = None; row[r] = {} + else: + q = Q(e[2] if op == 'SCALE' else e[3]); f = e[-1] + if q == 0 or not sm(q.denominator) or not abs(q) + 1 < 2 ** 16: viol['coefficient alphabet'] += 1 + if oddpart(q.denominator) > 1: odd_events[op] += 1 + maxq = max(maxq, abs(q)); nbits = max(nbits, abs(q.numerator).bit_length()); dbits = max(dbits, q.denominator.bit_length()) + if op != 'SCALE': logq += math.log2(1 + float(abs(q))) + if op == 'SCALE': + if cur[r] != f or not sm(q.numerator): viol['SCALE'] += 1 + row[r] = {k: v * q for k, v in row[r].items()}; note(row[r], 'scale row') + for v in row[r].values(): + if abs(v) > pmax: pmax = abs(v) + if v.denominator.bit_length() > dmaxb: dmaxb = v.denominator.bit_length() + else: + s = e[2] + if not (cur[r] == f == cur[s] and s != r): viol['common chart'] += 1 + if op == 'COPY': + if not (r in owned and not row[r]): viol['COPY'] += 1 + row[r] = {} + note({k: q * v for k, v in row[s].items()}, 'pre-ADD product') + for k, v in row[s].items(): + t = row[r].get(k, 0) + q * v + if t: + row[r][k] = t + if abs(t) > pmax: pmax = abs(t) + if t.denominator.bit_length() > dmaxb: dmaxb = t.denominator.bit_length() + else: row[r].pop(k, None) + note(row[r], 'ADD row') +need(not owned and cur[:n] == W['final'], 'owned all cleared; final frames as declared') +need(dict(viol) == {}, 'frame law, common chart, alphabet A = Z[1/2, 1/3, 1/5] with |q|+1 < 2^16, SCALE units of A, public ascent: no violation beyond the declared one') +up_mass = sum(k * v for k, v in owned_up.items()) +need(up_mass == 56 and sum(owned_up.values()) == 23, 'declared OWNED UP: %d events, rank mass %d (convention: owned ascent)' % (sum(owned_up.values()), up_mass)) +def verifier(name): + return subprocess.run([sys.executable, '-I', '-B', os.path.join(HERE, name), data('word.json.gz')], capture_output=True, text=True).stdout +os_, or_ = verifier('verify_strict.py'), verifier('verify_relaxed.py') +rej = [int(x) for x in os_.split('indices')[1].split('\n')[0].split()] +need(os_.strip().endswith('REJECTED_STRICT') and rej == up_idx and "['move nesting']" in os_, 'rejection control: the strict (predecessor) verifier rejects this word at exactly the %d owned-ascent events and nothing else' % len(rej)) +need(or_.strip().endswith('ACCEPTED_RELAXED'), 'relaxed verifier (only the owned-move direction rule changed, paid |delta dim| either way) accepts every event') +# ---- (1b) the odd grid (framework change): certificate, heights, odd divisions, scans, the odd verifier ------- +Smin = 1 +for d_ in odd_dens: Smin = Smin * d_ // math.gcd(Smin, d_) +def val_(m, p_): + c = 0 + while m % p_ == 0: m //= p_; c += 1 + return c +h3 = max([val_(d_, 3) for d_ in odd_dens] or [0]); h5 = max([val_(d_, 5) for d_ in odd_dens] or [0]) +need(Smin == SC == 1125 and not bad_S and all(sm(d_, (3, 5)) for d_ in odd_dens) and (h3, h5) == (2, 3), + 'certificate: S = 1125 = 3^2 5^3 times every prefix row and every pre-ADD product has dyadic entries (0 failures over %d odd denominators); the 3-adic and 5-adic heights are %d and %d and no other prime occurs; S is minimal (the least common multiple of the odd parts of all denominators is %d)' % (len(odd_dens), h3, h5, Smin)) +need(v2max == 24, 'width debt per unfinished context: 2-adic denominator height %d bits (odd part at most 1125, 10.1 bits), largest denominator of any row or product 2^%.2f; the coefficients are given by their own bit lengths below (numerators up to %d bits, denominators up to %d bits)' % (v2max, math.log2(dmax), nbits, dbits)) +need(all(any(s_ % d_ for d_ in odd_dens) for s_ in (375, 225, 75, 45, 15, 25, 9, 1)), 'S = 375 (= 1125/3), 225 (= 1125/5), 75, 45, 15, 25, 9 and 1 are each insufficient (some odd denominator does not divide them)') +oddfinal = sum(1 for r in range(NR) if not all(dy(v) for v in row[r].values())) +need(oddfinal == 0, 'every one of the %d final rows (public and owned) has dyadic entries: no odd denominator survives to an output' % NR) +n_odd = sum(odd_events.values()); scans = 2 * n_odd +need((odd_events['SCALE'], odd_events['ADD'], odd_events['COPY'], n_odd, scans) == (60, 4065, 0, 4125, 8250), + 'odd divisions per call: %d SCALE and %d ADD events have an odd denominator = %d divisions = %d scans (one multiply-and-check, one division, each a least-significant-bit-first pass), listed separately from the reviewed scalar count' % (odd_events['SCALE'], odd_events['ADD'], n_odd, scans)) +need(abs(math.log2(float(mass)) - 36.54) < 0.005 and 2 * (math.log2(10) + math.log2(float(mass))) < 80, 'largest l1 mass of S times a row or product at any prefix: 2^%.2f (the magnitude debt per unfinished context, scale included); 2 (log2 10 + %.2f) = %.2f < 80, so 80 t < d replaces the 82 t < d of the dyadic-caller-mass placeholder form' % (math.log2(float(mass)), math.log2(float(mass)), 2 * (math.log2(10) + math.log2(float(mass))))) +def vodd(*a): + return subprocess.run([sys.executable, '-I', '-B', os.path.join(HERE, 'verify_host3_odd.py'), data('word.json.gz')] + [str(x) for x in a], capture_output=True, text=True) +v1125, v375, v225, v1 = vodd(1125), vodd(375), vodd(225), vodd(1) +need('PASS_HOST3' in v1125.stdout, 'odd verifier (verify_host3_odd.py: A-membership, |q|+1 < 2^16, S certificate on every prefix row and pre-ADD product, public rows dyadic) accepts the word at S = 1125') +need(v375.returncode != 0 and v375.stderr.strip().endswith('AssertionError: 36915') and v225.returncode != 0 and v225.stderr.strip().endswith('AssertionError: 1101') and v1.returncode != 0 and v1.stderr.strip().endswith('AssertionError: 152'), 'odd verifier rejects S = 375 at event 36915 and S = 225 at event 1101 (the two divisors of 1125 by 3 and by 5), and S = 1 at event 152; controls.py runs the other rejections') +H = W['hosted']; al, be = Q(H['alpha']), Q(H['beta']); a2, b2 = Q(H['alpha2']), Q(H['beta2']); DP = H['Dports'] +live = W['live']; X = set(live); Y = {r + 112 for r in live}; X2 = H['X2']; Y2 = H['Y2']; X2s = set(X2); Y2s = set(Y2) +BP = [i for i in range(104) if i not in set(DP)]; dX = {live[i] for i in DP} +need(H['mode'] == 'mix-t0' and (al, be, a2, b2) == (-1, Q(1, 2), -1, 0) and len(DP) == len(set(DP)) == len(X2) == len(Y2) == 96 and len(BP) == 8 and not ((X2s | Y2s) & (X | Y)) and len(X2s | Y2s) == 192 and len(live) == len(W['ports']) == 104, + 'two port types: 96 ports in the two-chain form (second mains, plane 2 alpha2=%s beta2=%s) and 8 ports in the hosted form (pair alpha=%s beta=%s, t = %s, no second mains)' % (a2, b2, al, be, al * be)) +x2of = dict(zip(X2, Y2)); bad = 0 +for r in range(NR): + if r >= n: ex = {} + elif r in X: ex = {r: Q(1)} if r in dX else {r: Q(1), r + 112: al} + elif r in Y: ex = {r - 112: Q(1), r: Q(1)} if r - 112 in dX else {r - 112: be, r: 1 + al * be} + elif r in X2s: ex = {r: Q(1), x2of[r]: a2} + elif r in Y2s: ex = {r: Q(1)} + else: ex = {r: Q(1)} + bad += row[r] != ex +need(bad == 0, 'endpoint exact on all %d public and owned rows: two-chain ports X=x, Y=x+y, X2=x2-y2, Y2=y2; hosted ports X=x-y, Y=(x+y)/2; helpers identity, owned empty' % NR) +for i, (r, q) in enumerate(zip(live, W['ports'])): + if fr[W['initial'][r]] != [q] or dim[W['final'][r]] != 9 or dim[W['initial'][r + 112]] != 0 or sp[W['final'][r + 112]] != frozenset(x for x in range(512) if not (x & q).bit_count() % 2): raise SystemExit('FAIL main frames') +for i, x2, y2 in zip(DP, X2, Y2): + r = live[i] + if W['initial'][x2] != W['initial'][r] or W['final'][x2] != W['final'][r] or W['initial'][y2] != W['initial'][r + 112] or W['final'][y2] != W['final'][r + 112]: raise SystemExit('FAIL second main frames') +need(True, '104 literal central ports; the second mains of the 96 two-chain ports carry the same initial and final frame labels as the first mains (declared: same-label second mains)') +main = X | Y | X2s | Y2s +hel = Counter(dim[W['final'][r]] - dim[W['initial'][r]] for r in range(n) if r not in main) +need(min(hel) > 0 and all(sp[W['initial'][r]] < sp[W['final'][r]] for r in range(n) if r not in main), 'every helper strictly ascends (rank > 0); %d helpers, %d mains, %d public' % (sum(hel.values()), len(main), n)) +print(' events', len(W['program']), 'public', n, 'owned roles', NO, 'peak owned', peak, 'owned lifetimes', life, 'dirty owned erasures', dirty, 'max |coefficient|', maxq) +W19 = json.load(gzip.open(data('prior_word_6919.json.gz'), 'rt')); WB = json.load(gzip.open(data('prior_word_6932.json.gz'), 'rt')); W31 = json.load(gzip.open(data('prior_word_6931.json.gz'), 'rt')) +need(peak == 40 and len(W['program']) == 71069 and n == 1452 and sum(hel.values()) == 1052, 'peak owned fields %d; events %d; public %d; helpers %d (the #6932 word, data/prior_word_6932.json.gz: events %d, public %d, helpers %d)' % (peak, len(W['program']), n, sum(hel.values()), len(WB['program']), len(WB['initial']), len(WB['initial']) - 400)) +def lives_of(Wx): + st = {}; lf = Counter(); om = Counter() + for e_ in Wx['program']: + if e_[0] == 'INIT': st[e_[1]] = e_[2] + elif e_[0] == 'CLEAR': lf[(st.pop(e_[1]), e_[2])] += 1 + elif e_[0] == 'MOVE' and e_[4]: om[(e_[2], e_[3])] += 1 + return lf, om +lfn, omn = lives_of(W); lfo, omo = lives_of(WB) +pkWB = 0; lvWB = 0 +for e_ in WB['program']: + if e_[0] == 'INIT': lvWB += 1; pkWB = max(pkWB, lvWB) + elif e_[0] == 'CLEAR': lvWB -= 1 +need(W['frames'] == WB['frames'] and lfn == lfo and omn == omo and sum(lfn.values()) == 54 and W['owned_fields'] == WB['owned_fields'] == 51 and sum(omn.values()) == sum(omo.values()), + 'owned side against the #6932 word: the same frame table (%d frames), the same %d owned lifetimes as a multiset of (initial frame, clear frame), the same multiset of %d owned MOVEs (a, b), the same %d owned fields; only the timing differs, so the peak of concurrent owned fields is %d here and %d there (retiming only)' % (len(W['frames']), sum(lfn.values()), sum(omn.values()), W['owned_fields'], peak, pkWB)) +sc = [e for e in W['program'] if e[0] == 'SCALE'] +hX = {live[i] for i in BP}; gpos = {} +for k_, e in enumerate(W['program']): + if e[0] == 'SCALE' and e[1] in hX and e[1] not in gpos: gpos[e[1]] = (k_, Q(e[2])) +need(sorted(k for k, _ in gpos.values()) == list(range(8)) and {v for _, v in gpos.values()} == {Q(1, 2)} and len(gpos) == 8 and [e_[0] for e_ in W['program'][:8]] == ['SCALE'] * 8, 'gauge: the first 8 events of the word are the 8 SCALEs by 1/2 of the hosted-port mains X (events %d to %d), so the clause of the dyadic words \"the first 8 SCALEs are the hosted-port gauge\" holds literally for this word; the gauge is in any case covered by the exact endpoint X = x - y, Y = (x + y)/2' % (min(k for k, _ in gpos.values()), max(k for k, _ in gpos.values()))) + +# ---- (2) the roots ------------------------------------------------------------------------------ +RC = ldmod(os.path.join(HERE, 'root_check.py'), 'rootcheck') +RA = json.load(open(data('root_A.json'))); RB = json.load(open(data('root_B.json'))); RB0 = json.load(open(data('control_root_B_other_gauge.json'))) +need(RC.run(RA) == [], 'type A root (two #6833 chain roots, t = 0): 21/21 units of each chain regenerated, cross Gram 0, SPEC-level identities, each stage variable once and affine') +Rm = copy.deepcopy(RA); Rm['X'][5][3] = str(Q(Rm['X'][5][3]) + 1) +need(RC.blocks(Rm) != [] and RC.run(Rm) != [], 'wrong-root control A: a wrong X entry in the type A root FAILS (%s)' % RC.blocks(Rm)[:1]) +hsrc = open(os.path.join(HERE, 'root_check_hosted.py')).read() +def hosted_run(RR): + """root_check_hosted.py (the checker of the hosted root of #6889) executed on RR; returns its list of failed lines.""" + code = hsrc.replace("R=json.load(open(sys.argv[1] if len(sys.argv)>1 else os.path.join(os.path.dirname(os.path.abspath(__file__)),'data','root.json')))", 'R=_R').replace('sys.exit(1 if bad else 0)', '') + ns = {'_R': RR, 'sys': sys, '__file__': os.path.join(HERE, 'root_check_hosted.py'), 'print': lambda *a, **k: None} + exec(compile(code, 'root_check_hosted.py', 'exec'), ns) + return ns['bad'] +need(hosted_run(RB) == [], 'type B root (the hosted root of #6889, t = -1/2, n = 38, pairs (-1, 1/2)): every line of its checker passes') +Rm = copy.deepcopy(RB); Rm['X'][5][3] = str(Q(Rm['X'][5][3]) + 1) +need(hosted_run(Rm) != [], 'wrong-root control B: a wrong X entry in the hosted root FAILS its checker') +Rm = copy.deepcopy(RA); Rm['X'][7], Rm['X'][9] = Rm['X'][9], Rm['X'][7] +need(RC.run(Rm) != [], 'wrong-root control: two unit rows swapped in the type A root FAIL') + +# ---- (3) the joint caller ----------------------------------------------------------------------- +J = json.load(open(data('caller.json'))) +pM = 2147483629 +IM = next(pow(g, (pM - 1) // 4, pM) for g in range(2, 99) if pow(g, (pM - 1) // 2, pM) == pM - 1); HALF = (pM + 1) // 2 +fm = lambda x: (lambda f: f.numerator % pM * pow(f.denominator, pM - 2, pM) % pM)(Q(x)) +def root_pairs(root): + dot = lambda a_, b_: sum(Q(u) * Q(v) for u, v in zip(a_, b_) if Q(u) and Q(v)); out = {} + for k, s_ in enumerate(root['stages']): + u, v = s_['units']; out[k + 1] = (dot(root['Y'][u], root['X'][v]), dot(root['Y'][v], root['X'][u])) + return out +mask_inc = lambda root, c: [int(c in set(s['mask'])) for s in root['stages']] +PB = root_pairs(RB); TA, TB = J['types']['A'], J['types']['B'] +need(set(PB.values()) == {(al, be)} and len(PB) == 18, 'every one of the 18 hosted stages of root B has the word\'s pair (alpha,beta)=(%s,%s), read from the root' % (al, be)) +need(all(TA['diagonal'][c][2:] == mask_inc(RA, c) for c in range(40)) and all(TB['diagonal'][c][2:] == mask_inc(RB, c) for c in range(38)), 'caller target exponents equal the mask incidence of the root of their type, field by field and stage by stage (type A 40 roles, type B 38 roles)') +need(Q(TA['alpha2']) == a2 and Q(TA['beta2']) == b2 and all(str(e[3][2]) == str(al) and str(e[3][3]) == str(be) for e in J['events'] if e[0] == 'J'), 'type A plane-2 parameters and every joint contact\'s hosted pair equal the word\'s') +need(J['roles'] == 78 and J['stages'] == 18 and sum(e[0] == 'J' for e in J['events']) == 18, 'joint caller: 78 roles (type A 0-39, type B 40-77), 18 joint contacts (one per stage; HOST2 at the two-chain ports and HOST at the hosted ports in one event)') +need(sorted(TA['ports']) == sorted(DP) and sorted(TB['ports']) == BP and len(TA['ports']) == 96 and len(TB['ports']) == 8, 'port types of the caller equal the word\'s: type A = the 96 two-chain ports, type B = the 8 hosted ports') +Jp = copy.deepcopy(J); Jp['types']['A']['ports'][0], Jp['types']['B']['ports'][0] = Jp['types']['B']['ports'][0], Jp['types']['A']['ports'][0] +need(sorted(Jp['types']['A']['ports']) != sorted(DP) or sorted(Jp['types']['B']['ports']) != BP, 'swapped-assignment control: exchanging the types of one two-chain port and one hosted port in the caller breaks the match with the word') +NRr = J['roles'] +def target(Jc, role, qv, Dv): + t, off = (Jc['types']['A'], 0) if role < 40 else (Jc['types']['B'], 40); dg = t['diagonal'][role - off] + c = pow(qv, dg[0] % 4, pM) + for k, bit in enumerate(dg[2:]): + if bit: c = c * Dv[k + 1] % pM + return c +def replay(Jc, qv, Dv, a2_=a2, pairs=PB, types='AB'): + Rm_ = [[int(i == j) for j in range(NRr)] for i in range(NRr)]; qi = pow(qv, pM - 2, pM); seen = [] + for e in Jc['events']: + tag = e[0] + if tag == 'J': + st = e[1]; seen.append(st); d = Dv[st] + if 'A' in types: + src, dst, x2, y2 = e[2] + Rm_[dst] = [(a_ + qi * b_) % pM for a_, b_ in zip(Rm_[dst], Rm_[src])] + Rm_[x2] = [(a_ + fm(a2_) * qv % pM * b_) % pM for a_, b_ in zip(Rm_[x2], Rm_[y2])] + for r_ in (src, dst, x2, y2): Rm_[r_] = [a_ * d % pM for a_ in Rm_[r_]] + if 'B' in types: + src, dst = e[3][0], e[3][1]; a_, b_ = fm(pairs[st][0]), fm(pairs[st][1]); tt_ = a_ * b_ % pM + ns = [(x + a_ * qv % pM * y) % pM * d % pM for x, y in zip(Rm_[src], Rm_[dst])] + nd = [(b_ * qi % pM * x + (1 + tt_) * y) % pM * d % pM for x, y in zip(Rm_[src], Rm_[dst])] + Rm_[src], Rm_[dst] = ns, nd + continue + if tag not in types: continue + op = e[1] + if op == 'ADD': Rm_[e[2]] = [(a_ + fm(e[4]) * b_) % pM for a_, b_ in zip(Rm_[e[2]], Rm_[e[3]])] + elif op == 'SCALE': c = fm(e[3]); Rm_[e[2]] = [a_ * c % pM for a_ in Rm_[e[2]]] + elif op == 'SWAP': Rm_[e[2]], Rm_[e[3]] = Rm_[e[3]], Rm_[e[2]] + elif op == 'QUERY': c = pow(qv, e[4] % 4, pM); Rm_[e[2]] = [(a_ + c * b_) % pM for a_, b_ in zip(Rm_[e[2]], Rm_[e[3]])] + elif op == 'LAMBDA': + s_ = e[3]; c = ((1 + s_ * IM) * HALF + (1 - s_ * IM) * HALF * qv * qv) % pM; Rm_[e[2]] = [a_ * c % pM for a_ in Rm_[e[2]]] + elif op == 'IDLE_ONE': + c = 1 + for k in e[3]: c = c * Dv[k] % pM + Rm_[e[2]] = [a_ * c % pM for a_ in Rm_[e[2]]] + else: raise SystemExit('FAIL unknown caller event ' + op) + if seen != list(range(1, 19)): return 10 ** 6 + roles = [r for r in range(NRr) if ('A' in types and r < 40) or ('B' in types and r >= 40)] + return sum(Rm_[i][j] != (target(Jc, i, qv, Dv) if i == j else 0) for i in roles for j in range(NRr)) +rnd = random.Random(11); tot = cnt = 0 +for qv in (1, IM, pM - 1, pM - IM): + for _ in range(3): + Dv = {s_: rnd.randrange(2, pM) for s_ in range(1, 19)}; tot += replay(J, qv, Dv); cnt += 1 +need(tot == 0, 'composition: the ONE joint stream (78 roles, one stage value per stage common to both types) replays to the block-diagonal target at all four central characters (%d evaluations, 0 bad of %d entries each; all cross-type blocks are 0)' % (cnt, NRr * NRr)) +for ty in 'AB': + t2 = sum(replay(J, qv, {s_: rnd.randrange(2, pM) for s_ in range(1, 19)}, types=ty) for qv in (1, IM, pM - 1, pM - IM)) + need(t2 == 0, 'type %s alone replays to its own target at the four characters' % ty) +Dv = {s_: rnd.randrange(2, pM) for s_ in range(1, 19)} +def rej(Jc=J, **kw): return replay(Jc, IM, Dv, **kw) +def mut(f): + Jm = copy.deepcopy(J); f(Jm); return Jm +idx = lambda Jc, pred: next(i for i, e in enumerate(Jc['events']) if pred(e)) +first = lambda tag, op: (lambda e: e[0] == tag and e[1] == op) +ctr = [('type A wrong alpha2', rej(a2_=Q(1)))] +for nm, fn in (('type B alpha sign', lambda x: x.__setitem__(0, -x[0])), ('type B beta sign', lambda x: x.__setitem__(1, -x[1])), ('type B pair swapped', lambda x: x.reverse())): + pm = {k: list(v) for k, v in PB.items()}; fn(pm[13]); ctr.append((nm + ' at stage 13', rej(pairs=pm))) +ctr.append(('type B root in the other gauge', rej(pairs=root_pairs(RB0)))) +for ty in 'AB': + ctr.append(('type %s deleted idle' % ty, rej(mut(lambda Jm: Jm['events'].pop(idx(Jm, first(ty, 'IDLE_ONE'))))))) + ctr.append(('type %s deleted query' % ty, rej(mut(lambda Jm: Jm['events'].pop(idx(Jm, first(ty, 'QUERY'))))))) + def flip(Jm): + j0 = idx(Jm, lambda e: e[0] == 'J'); k = max(i for i in range(j0) if Jm['events'][i][0] == ty and Jm['events'][i][1] == 'LAMBDA'); Jm['events'][k][3] *= -1 + ctr.append(('type %s flipped LAMBDA before the first contact' % ty, rej(mut(flip)))) +for nm, b in ctr: print(' control %-52s -> %d bad' % (nm, b)) +need(all(b > 0 for _, b in ctr), 'controls: wrong alpha2, a wrong or other-gauge hosted pair, a deleted idle, a deleted query, a flipped LAMBDA at a contact, in each type: all rejected by the replay') +for ty, role in (('A', 3), ('B', 3)): + Jm = mut(lambda x: x['types'][ty]['diagonal'][role].__setitem__(2 + 4, x['types'][ty]['diagonal'][role][2 + 4] ^ 1)) + need(rej(Jm) > 0 and Jm['types'][ty]['diagonal'][role][2:] != (mask_inc(RA, role) if ty == 'A' else mask_inc(RB, role)), 'mask control, type %s: a wrong mask bit in the caller target fails the replay and the mask comparison' % ty) +need(rej(mut(lambda x: x['events'].insert(idx(x, lambda e: e[0] == 'J'), ['A', 'ADD', 5, 45, '1']))) > 0 and rej(mut(lambda x: x['events'].insert(idx(x, lambda e: e[0] == 'J'), ['B', 'ADD', 45, 5, '1']))) > 0, 'cross-type controls: one ADD from a type A role into a type B role, and the other way, are rejected: the types do not interact') +def swapst(x): + js = [e for e in x['events'] if e[0] == 'J']; js[0][1], js[1][1] = js[1][1], js[0][1] +def rot(x): + e = x['events'][idx(x, lambda e: e[0] == 'J')]; a = e[2]; e[2] = [a[0], a[1], a[3], a[2]] +need(rej(mut(swapst)) > 0 and rej(mut(rot)) > 0, 'controls: two joint contacts with exchanged stages, and exchanged second-plane roles in a contact, are rejected') +print(' note: the composition reads each root only through its masks and pairs; wrong X or Y entries are caught by the root checkers above') + +# ---- (4) invoice --------------------------------------------------------------------------------- +def kappa(T, P): + rs = sorted(set(T) | set(P)); ln = {r: D(r).ln() for r in rs} + e = lambda k: sum((D(T.get(r, 0)) - D(P.get(r, 0))) * (ln[r] * (1 - k)).exp() for r in rs) + lo, hi = D('1e-6'), D('0.05') + for _ in range(220): + m = (lo + hi) / 2 + if e(m) > 0: lo = m + else: hi = m + return lo +def root_fields(RR): + S_ = RR['stages']; Xr = RR['X']; Yr = RR['Y']; F = [] + for c in range(RR['n']): + ms = [k for k, s_ in enumerate(S_) if c in set(s_['mask'])] + F.append((ms, [k for k in ms if any(Q(Yr[u][c]) != 0 for u in S_[k]['units'])])) + dot = lambda a_, b_: sum(Q(u) * Q(v) for u, v in zip(a_, b_) if Q(u) and Q(v)); planes = [] + for s_ in S_: + u, v = s_['units']; planes.append(2 if dot(Yr[u], Xr[v]) == 0 and dot(Yr[v], Xr[u]) == 0 else 1) + return F, planes, RR['N'] - sum(len(s_['units']) for s_ in S_) +def outer(F, planes, thin, ports, nst=18): + T = Counter(); P = Counter(); hc = Counter() + for ms, host in F: + T[8 * len(ms) + 1] += ports + for k in host: hc[k] += 1 + run = 0; prev = None + for k in ms: + if k in host: + if run: P[8 * run] += ports + run = 0; prev = None; continue + if prev is not None and k == prev + 1: run += 1 + else: + if run: P[8 * run] += ports + run = 1 + prev = k + if run: P[8 * run] += ports + for k in range(nst): + if hc[k] > 2 * planes[k]: P[8] += ports * (hc[k] - 2 * planes[k]) + P[1] += ports * thin + return T, P +def census(Wx): + nx = len(Wx['initial']); lx = set(Wx['live']); mx = lx | {r_ + 112 for r_ in lx} + if Wx.get('hosted', {}).get('X2'): mx |= set(Wx['hosted']['X2']) | set(Wx['hosted']['Y2']) + dx = [len(b_) for b_ in Wx['frames']] + return (Counter(dx[Wx['final'][r_]] - dx[Wx['initial'][r_]] for r_ in range(nx) if r_ not in mx), Counter(abs(dx[e_[3]] - dx[e_[2]]) for e_ in Wx['program'] if e_[0] == 'MOVE')) +def invoice_roots(hel_, paid_, roots): + T = Counter(); P = Counter() + for RR, ports in roots: + F, pl, th = root_fields(RR); t_, p_ = outer(F, pl, th, ports); T.update(t_); P.update(p_) + for r, k in hel_.items(): T[r] += 18 * k + for r, k in paid_.items(): P[r] += 18 * k + return T, P +bi = json.load(open(data('base_invoice.json'))) +T0 = Counter({int(k): v for k, v in bi['targets'].items()}); P0 = Counter({int(k): v for k, v in bi['paid'].items()}) +chain = [(list(range(18)), list(range(18)))] + [(list(range(i, 9)), [i]) for i in range(9)] + [(list(range(9, 10 + m)), [9 + m]) for m in range(9)] + [([], [])] +Tc_, Pc_ = outer(chain, [1] * 18, 3, 104) +Tb, Pb = Counter(Tc_), Counter(Pc_) +for r_, k_ in bi['helpers'].items(): Tb[int(r_)] += 18 * k_ +for r_, k_ in bi['local_paid'].items(): Pb[int(r_)] += 18 * k_ +need(+Tb == T0 and +Pb == P0, 'control: the same code rebuilds the #6833 invoice term for term') +kb = kappa(T0, P0) +need(abs(kb - D(bi['kappa_literal'])) < D('1e-17'), 'control: #6833 kappa %s' % str(kb)[:20]) +nA, nB = len(TA['ports']), len(TB['ports']); cnt_ty = {'A': nA, 'B': nB} +T = Counter(); P = Counter(); nj = 0 +for e in J['events']: + if e[0] == 'J': nj += 1; T.update(hel); P.update(paid) + elif e[1] == 'QUERY': P[1] += cnt_ty[e[0]] + elif e[1] == 'IDLE_ONE': P[8 * len(e[3])] += cnt_ty[e[0]] +for ty, t in (('A', TA), ('B', TB)): + for dg in t['diagonal']: T[int(dg[0] % 2) + 8 * sum(dg[2:])] += cnt_ty[ty] +T2, P2 = invoice_roots(hel, paid, ((RA, nA), (RB, nB))) +need(nj == 18 and +T == +T2 and +P == +P2, 'the invoice recounted from the emitted joint events equals the invoice rebuilt from the TWO ROOTS (per type, per port count) plus the word, term for term (18 native calls, helpers and paid jobs once per call)') +kn = kappa(T, P); Tn, Pn = T, P +need(abs(kn - D('0.0036238597350766513')) < D('1e-17'), 'new kappa %s' % str(kn)[:26]) +S = sum(r * (Tn.get(r, 0) - Pn.get(r, 0)) for r in set(Tn) | set(Pn)) +need(S == 1520, 'rank-mass surplus S = %d (104*34 - 36*56, net of the 56 owned-ascent mass per call)' % S) +Wp = json.load(gzip.open(data('prior_word_6911.json.gz'), 'rt')); hp, pp = census(Wp) +Tp, Pp = invoice_roots(hp, pp, ((RA, nA), (RB, nB))); kp = kappa(Tp, Pp) +need(abs(kp - D('0.0035194870841667550646')) < D('1e-17'), 'control: the #6911 word through the two roots (96 + 8 ports) and the same code gives %s (its crossing)' % str(kp)[:26]) +W17 = json.load(gzip.open(data('prior_word_6917.json.gz'), 'rt')); h17, p17 = census(W17) +T17, P17 = invoice_roots(h17, p17, ((RA, nA), (RB, nB))); k17 = kappa(T17, P17) +need(abs(k17 - D('0.0035301044238995680260')) < D('1e-17'), 'control: the #6917 word through the two roots (96 + 8 ports) and the same code gives %s (its crossing)' % str(k17)[:26]) +h19, p19 = census(W19); T19, P19 = invoice_roots(h19, p19, ((RA, nA), (RB, nB))); k19 = kappa(T19, P19) +need(abs(k19 - D('0.0035952826938257874494')) < D('1e-17'), 'control: the #6919 word (data/prior_word_6919.json.gz) through the two roots (96 + 8 ports) and the same code gives %s (the crossing of #6919)' % str(k19)[:26]) +h31, p31 = census(W31); T31, P31 = invoice_roots(h31, p31, ((RA, nA), (RB, nB))); k31 = kappa(T31, P31) +need(abs(k31 - D('0.0036041048151080063894')) < D('1e-17'), 'control: the #6931 word (data/prior_word_6931.json.gz) through the two roots (96 + 8 ports) and the same code gives %s' % str(k31)[:26]) +h32, p32 = census(WB); Tb0, Pb0 = invoice_roots(h32, p32, ((RA, nA), (RB, nB))); kbase = kappa(Tb0, Pb0) +need(abs(kbase - D('0.0036210586137481460837')) < D('1e-17'), 'control: the #6932 word (data/prior_word_6932.json.gz, the word this one is compared with) through the two roots (96 + 8 ports) and the same code gives %s' % str(kbase)[:26]) +need(sum(r * (Tb0.get(r, 0) - Pb0.get(r, 0)) for r in set(Tb0) | set(Pb0)) == 1520, 'the #6932 word has rank-mass surplus S = 1520 as well') +print(' gain over the #6932 word: %.5f%% (exactly kappa_new / kappa_6932 - 1 = %s)' % (100 * float(kn / kbase - 1), str(kn / kbase - 1)[:12])) +need(str(100 * (kn / kbase - 1))[:5] == '0.077', 'the gain over the #6932 word (crossing %s) is +0.077%% (ratio - 1 = %s); no other comparison is made' % (str(kbase)[:22], str(kn / kbase - 1)[:12])) +dT = {r: Tn[r] - Tb0[r] for r in sorted(set(Tn) | set(Tb0)) if Tn[r] != Tb0[r]}; dPp = {r: Pn[r] - Pb0[r] for r in sorted(set(Pn) | set(Pb0)) if Pn[r] != Pb0[r]} +print(' T change against the #6932 word (all 18 calls):', dT); print(' P change against the #6932 word (all 18 calls):', dPp) +need(dT == {1: 18, 6: 36, 9: -36} and dPp == {1: -108, 2: 36, 4: -18, 5: -18, 6: 18} and sum(r * c for r, c in dT.items()) == sum(r * c for r, c in dPp.items()), + 'T and P change against the #6932 word, per call (all 18 calls divided by 18): T %s (productive fields by rank: one more of rank 1, two more of rank 6, two fewer of rank 9), P %s (paid jobs by rank); the rank mass of T and of P changes by the same amount (%d), so S stays %d' % ({r: c // 18 for r, c in dT.items()}, {r: c // 18 for r, c in dPp.items()}, sum(r * c for r, c in dT.items()) // 18, S)) +dDT = sum(c * r * D(r).ln() for r, c in dT.items()) / 18; dDP = -sum(c * r * D(r).ln() for r, c in dPp.items()) / 18 +need(dDT + dDP < 0, 'the whole gain is in the kernel term D = sum (T - P) r ln r, per call: the T change moves it by %s and the P change by %s (net %s; the rank mass S stays %d). The word is a full rebuild, so this is the net difference of the two whole words, not the effect of any single move' % (str(dDT)[:8], str(dDP)[:8], str(dDT + dDP)[:8], S)) +nlA = sum(1 for e in J['events'] if e[0] == 'A' and e[1] == 'LAMBDA'); nlB = sum(1 for e in J['events'] if e[0] == 'B' and e[1] == 'LAMBDA') +lam_cost = nA * nlA + nB * nlB +need((nlA, nlB) == (124, 82) and S - lam_cost < 0, 'review question, stated plainly: type A callers have %d LAMBDA events and type B callers %d; if each LAMBDA had to be paid as a rank-1 job per port, the cost is %d*%d + %d*%d = %d and S = %d - %d = %d < 0, so no crossing exists; kappa rests on pricing LAMBDA as ordinary work, as in every caller of this line' % (nlA, nlB, nA, nlA, nB, nlB, lam_cost, S, lam_cost, S - lam_cost)) + +# ---- (5) raw bound, growth, alphabet -------------------------------------------------------------- +def swaps(sel): + wanted = set(range(len(sel))); return len(list(zip(sorted(set(sel) - wanted), sorted(wanted - set(sel))))) +def shim(ty): + t = J['types'][ty]; off = t['offset']; ev = [] + for e in J['events']: + if e[0] == 'J': ev.append(['HOST', e[1]]) + elif e[0] == ty: + e = list(e[1:]) + if e[0] in ('ADD', 'SWAP', 'QUERY'): e[1] -= off; e[2] -= off + else: e[1] -= off + ev.append(e) + return dict(events=ev, roles=t['roles'], ambient_rank=J['ambient_rank'], diagonal=t['diagonal']) +def rest_of(C, ports): + ev = C['events']; roles = C['roles']; amb = C['ambient_rank']; mx = mn = mp = 0 + for role, (qp, zero, *sel) in enumerate(C['diagonal']): + axes = ([0] if qp else []) + [a for st, y in enumerate(sel, 1) if y for a in range(9 + 8 * (st - 1), 9 + 8 * st)] + k = swaps(axes); mx += 2 * k * ports; mn += 2 * bool(qp) * ports; mp += int(qp == -1) * ports + ie = 0; qn = qph = 0 + for e in ev: + if e[0] == 'IDLE_ONE': ie += 2 * swaps([a for st in e[2] for a in range(9 + 8 * (st - 1), 9 + 8 * st)]) * ports + elif e[0] == 'QUERY': qn += 2 * ports; qph += int(e[3] == -1) * ports + return 32 * roles * ports * len(ev) + sum(e[0] == 'QUERY' for e in ev) * 16 * ports + roles * ports * 26 + (mx + mn + mp) * 1000 + ie * 1000 + (qn + qph) * 1000 +rest = rest_of(shim('A'), nA) + rest_of(shim('B'), nB) +allow = upper = 0 +for e in W['program']: + if e[0] in ('INIT', 'CLEAR'): allow += 2 + elif e[0] == 'SCALE': + q = Q(e[2]); a_, d_ = abs(q.numerator), q.denominator + allow += 2 * (abs(a_.bit_length() - d_.bit_length()) + int(q < 0)); upper += 4 * (a_.bit_length() + d_.bit_length() + 1) + elif e[0] in ('ADD', 'COPY'): + q = Q(e[3]); a_, d_ = abs(q.numerator), q.denominator + allow += 2 * (3 + a_.bit_length() - 1 + bin(a_).count('1') + d_.bit_length() - 1); upper += 4 * (a_.bit_length() + bin(a_).count('1') + d_.bit_length() + 1) +routes = (sum(paid.values()) + 2 * sum(hel.values()) + 208 + 2 * nA + 4 * 104 + 4 * nA + 4 * life) * 1000 # boundary terms of the second planes only at the two-chain ports +per_call = allow + routes; per_up = upper + routes +raw_lit, raw_act, raw_rev = 18 * 10 ** 7 + rest, 18 * per_call + rest, 18 * per_up + rest +print(' raw pieces: per-port terms = %d; per call (word scalar + routes) = %d (allowance) or %d (reviewed upper) against the displayed 10^7' % (rest, per_call, per_up)) +need((raw_lit, raw_act, raw_rev) == (802809952, 815759836, 832029136) and max(raw_lit, raw_act, raw_rev) < 10 ** 9, 'raw bound, all three definitions below 10^9: literal %d, actual per-call work %d, reviewed scalar upper %d (margins %d, %d, %d); the %d odd divisions are inside these bit-length terms (argued) and are also listed as %d scans per call' % (raw_lit, raw_act, raw_rev, 10 ** 9 - raw_lit, 10 ** 9 - raw_act, 10 ** 9 - raw_rev, n_odd, scans)) +debit = 1000 * lam_cost +need(raw_rev + debit == 844589136 and raw_rev + debit < 10 ** 9, 'conservative recharge: the reviewed upper count %d already contains every LAMBDA event of the caller (through the envelope 32 * roles * ports * len(events); rest_of: the events of each type include its LAMBDA events); the second check of #6913 counts the LAMBDA translations a second time, %d LAMBDA jobs at 1,000 each = %d for this mix, on top of the whole reviewed bound; with the scale applied once at the boundary (no per-call charge) the total is %d, below 10^9 (margin %d), so no reading of the raw count exceeds 10^9 with this caller; no term of the outer ledger reads either count' % (raw_rev, lam_cost, debit, raw_rev + debit, 10 ** 9 - raw_rev - debit)) +sc_cost = 4 * (SC.bit_length() + 1 + 1) + 4 * (1 + SC.bit_length() + 1) # one SCALE by S = 1125 at entry and one by 1/1125 at exit, at the reviewed upper rate 4 * (bits(a) + bits(d) + 1) +per_in = 18 * n * sc_cost +need(sc_cost == 104 and raw_rev + per_in == 834747280 and raw_rev + per_in + debit == 847307280 and raw_rev + per_in + debit < 10 ** 9, 'per-input scale reading (every one of the %d public registers scaled by 1125 at entry and unscaled at exit on each of the 18 calls, %d x %d x 18 = %d, an upper reading): upper %d; with the second LAMBDA count %d, below 10^9 (margin %d)' % (n, sc_cost, n, per_in, raw_rev + per_in, raw_rev + per_in + debit, 10 ** 9 - raw_rev - per_in - debit)) +Rm_paid = sum(r_ * v_ for r_, v_ in Pn.items()) +print(' CONSTANT SUBSTITUTION (FINITE-PRECOMPILATION.md:278-283): events %d; scalar allowance %d; reviewed scalar upper %d; routes %d; per call %d or %d; raw upper %d (allowance) or %d (reviewed upper); paid rank mass R = %d; growth bound 2^(raw + R f) = 2^(%d + %d f) on the conservative count' % (len(W['program']), allow, upper, routes, per_call, per_up, raw_act, raw_rev, Rm_paid, raw_rev, Rm_paid)) +src_ep = open(os.path.join(HERE, 'retained', 'runtime', 'endpoint.py')).read() +need(not any(t_ in src_ep for t_ in ('10**9', '10 ** 9', '10**7', '10 ** 7', '1e9')), 'the outer ledger source contains no scalar-work or 10^9 term') +def logsum(Wx): return sum(math.log2(1 + float(abs(Q(e_[3])))) for e_ in Wx['program'] if e_[0] in ('ADD', 'COPY')) +l02 = logsum(WB) +print(' GROWTH: events %d (#6932 word %d); sum of log2(1+|q|) over the ADD coefficients %d (#6932 word %d) against 416000; peak |row entry| on any prefix 2^%.2f; peak row denominator 2^%d; coefficient bits numerator <= %d, denominator <= %d; largest |q| %s' % (len(W['program']), len(WB['program']), round(logq), round(l02), math.log2(float(pmax)), dmaxb - 1, nbits, dbits, maxq)) +big_ = sum(1 for e_ in W['program'] if e_[0] in ('ADD', 'COPY') and abs(Q(e_[3])) >= 2 ** 12) +need(round(logq) == 82770 and maxq == Q(227445, 8) and (nbits, dbits) == (24, 19) and big_ == 10 and maxq + 1 < 2 ** 16, 'sum of log2(1+|q|) %d (below 416000; the #6932 word %d); largest |q| %s = %.1f with |q| + 1 < 2^16; coefficient bits %d / %d (the #6932 word: largest |q| %s, 16 / 16); %d ADD events here have |q| >= 2^12' % (round(logq), round(l02), maxq, float(maxq), nbits, dbits, max(abs(Q(e_[3])) for e_ in WB['program'] if e_[0] in ('ADD', 'COPY')), big_)) +cf_ = [(abs(Q(e_[3])).numerator, Q(e_[3]).denominator, i_) for i_, e_ in enumerate(W['program']) if e_[0] in ('ADD', 'COPY')] +num_max = max(cf_, key=lambda t_: (t_[0], -t_[2])); den_max = max(cf_, key=lambda t_: (t_[1], -t_[2])); n40k = sum(1 for t_ in cf_ if t_[0] > 40864) +need(num_max[0].bit_length() == nbits == 24 and den_max[1].bit_length() == dbits == 19 and (num_max[2], den_max[2], n40k) == (250, 2796, 864), 'temporaries: the coefficient numerators of the ADD events reach %d bits (largest numerator %d, first at event %d) and their denominators %d bits (largest denominator %d, at event %d); %d ADD events have a numerator above 40864 (the #6932 word: none, 16 / 16 bits). A multiply-by-a, check-divisibility, divide-by-b temporary holds a times a stored value, so its coefficient factor is %d bits wide, not 16' % (num_max[0].bit_length(), num_max[0], num_max[2], den_max[1].bit_length(), den_max[1], den_max[2], n40k, nbits)) +cb = max(abs(Q(e_[4] if e_[1] == 'ADD' else e_[3])).numerator.bit_length() for e_ in J['events'] if e_[1] in ('ADD', 'SCALE')); cd = max(Q(e_[4] if e_[1] == 'ADD' else e_[3]).denominator.bit_length() for e_ in J['events'] if e_[1] in ('ADD', 'SCALE')) +need((cb, cd) == (9, 8) and round(math.log2(float(pmax)), 2) == 23.55 and dmaxb - 1 == 27, 'coefficients: caller coefficient bits %d / %d (SCALE 256 and the gauge 1/128, in the type B caller, unchanged; the type A caller now uses only +-1, +-2, SCALE -1 and SWAP); word: largest |q| %s, peak |row entry| 2^%.2f, peak row denominator 2^%d (odd part at most 1125)' % (cb, cd, maxq, math.log2(float(pmax)), dmaxb - 1)) +nid = Counter(e_[0] for e_ in J['events'] if e_[1] == 'IDLE_ONE') +need(nid == Counter({'A': 32, 'B': 68}), 'IDLE_ONE events: %d in the type A caller, %d in the type B caller (one-site idles priced as whole H8 jobs; declared, inherited)' % (nid['A'], nid['B'])) +Y2set = set(Y2) +oy = [i_ for i_, e_ in enumerate(W['program']) if e_[0] == 'ADD' and e_[1] >= n and e_[2] in Y2set] +ox = [i_ for i_, e_ in enumerate(W['program']) if e_[0] == 'ADD' and e_[1] >= n and e_[2] in X] +ox2 = [i_ for i_, e_ in enumerate(W['program']) if e_[0] == 'ADD' and e_[1] >= n and e_[2] in X2s] +oyY = [i_ for i_, e_ in enumerate(W['program']) if e_[0] == 'ADD' and e_[1] >= n and e_[2] in Y] +def owned_reads(Wx): + nx = len(Wx['initial']); Hx = Wx['hosted']; lx = Wx['live']; Xs = set(lx); Ys = {r_ + 112 for r_ in lx}; X2x = set(Hx['X2']); Y2x = set(Hx['Y2']) + return tuple(sum(1 for e_ in Wx['program'] if e_[0] == 'ADD' and e_[1] >= nx and e_[2] in grp) for grp in (Y2x, Xs, X2x, Ys)) +ob = owned_reads(WB) +def peak_owned(Wx): + live_, pk_ = 0, 0 + for e_ in Wx['program']: + if e_[0] == 'INIT': live_ += 1; pk_ = max(pk_, live_) + elif e_[0] == 'CLEAR': live_ -= 1 + return pk_ +peakb = peak_owned(WB) +need(peakb == 36 == pkWB and peak_owned(W) == peak == 40, 'peak owned fields: %d in the #6932 word, %d in this word (same number of owned lifetimes %d against %d)' % (peakb, peak, life, sum(e_[0] == 'INIT' for e_ in WB['program']))) +need((len(oy), len(ox), len(ox2), len(oyY)) == (8, 7, 1, 0) and ob == (8, 9, 2, 0), 'owned registers reading a main register: %d events read Y2 %s, %d read X %s, %d read X2 %s, none reads Y: %d events in all (the #6932 word: %d, %d, %d, %d for Y2, X, X2, Y, %d in all); the same kinds of read, three fewer; declared with A6; peak owned fields %d' % (len(oy), oy, len(ox), ox, len(ox2), ox2, len(oy) + len(ox) + len(ox2), ob[0], ob[1], ob[2], ob[3], sum(ob), peak)) + + +# ---- (6) outer conditions ---------------------------------------------------------------------- +E, SE, OUT = ldmod(os.path.join(HERE, 'retained', 'runtime', 'intervals.py'), 'intervals'), ldmod(os.path.join(HERE, 'retained', 'runtime', 'second_intervals.py'), 'second_intervals'), ldmod(os.path.join(HERE, 'retained', 'runtime', 'endpoint.py'), 'endpoint') +BITF = json.load(open(os.path.join(HERE, 'retained', 'bit', 'FRAGMENT-BIT-ADMISSION.json'))) +need(hashlib.sha256(open(os.path.join(HERE, 'retained', 'bit', 'FRAGMENT-BIT-ADMISSION.json'), 'rb').read()).hexdigest() == '86955dcd74bc3fa1a940419474d45054fa7b0366b71b242568680366923d9311' and BITF['status'] == 'PASS_TWO_FRAGMENTS_BIT_ORDINARY_00376669' and Q(BITF['ordinary_admitted']) == PIN, 'BIT pin %s = ordinary_admitted of the pinned #6726 admission file (status %s); not re-derived here' % (float(PIN), BITF['status'])) +KAPPA, TESTED = Q('.00362385973'), Q('.0036238597307') +LOW, UP = Q('.003623859735076'), Q('.003623859735077') +Tq = Counter({r: v for r, v in Tn.items() if v}); Pq = Counter({r: v for r, v in Pn.items() if v}) +need(KAPPA < TESTED < LOW < UP and TESTED < PIN and Q(BITF['raw_crossing'][0]) > Q(BITF['raw_tested']) > PIN, 'claim %s, tested %s, both strictly below the raw crossing %s; BIT side: raw crossing > raw tested saving > pin > tested price' % (float(KAPPA), float(TESTED), str(kn)[:19])) +print(' BIT margins: pin - tested complex price = %.3e; raw BIT tested saving - pin = %.1e; raw BIT crossing lower bound - raw BIT tested saving = %.3e' % (float(PIN - TESTED), float(Q(BITF['raw_tested']) - PIN), float(Q(BITF['raw_crossing'][0]) - Q(BITF['raw_tested'])))) +for name, k, pos in (('lower', LOW, 1), ('upper', UP, -1), ('tested', TESTED, 1)): + a, b = E.moment(Tq, 1 - k), E.moment(Pq, 1 - k); first = (a[0] - b[1], a[1] - b[0]) + tl, th = SE.moment(Tq, k); pl, ph = SE.moment(Pq, k); second = (tl - ph, th - pl) + need((first[0] > 0 and second[0] > 0) if pos > 0 else (first[1] < 0 and second[1] < 0), 'both interval engines (rational interval arithmetic, no Decimal): sign of the margin at the %s price endpoint' % name) +signed = Counter(Tq); signed.subtract(Pq); d = Q(0) +for r, c in signed.items(): + lg = E.log_bounds(r); d -= c * (E.mul(E.power(r, 1 - PIN), lg)[0] if c >= 0 else r * lg[1]) +need(d < 0, 'unique raw crossing through the BIT pin (derivative upper bound negative at the pin)') +cutoff, floor, power, offset = 11, 12, 1920, Q(1, 7); LPMIN, LP = 2223, 2224 +tt_ = 1 - TESTED; target, paidm = E.moment(Tq, tt_), E.moment(Pq, tt_) +alpha = E.divide(paidm, target); gamma = E.divide(E.moment(Pq, tt_ + offset), E.mul(E.power(cutoff, offset), target)) +delta = E.divide((Q(sum(Tq.values()) * floor),) * 2, E.mul(E.power(cutoff, TESTED), target)) +reserve, decay = Q(1, 10 ** 27), Q(31, 32) +need(alpha[1] < 1 - reserve and gamma[1] < decay and delta[1] < decay, 'tail ratios (interval engine): alpha %.12f gamma %.4f delta %.4f (cutoff 11, floor 12, offset 1/7, power 1920)' % (float(alpha[1]), float(gamma[1]), float(delta[1]))) +normalized = 1 / (1 + power * reserve) + 4 * decay ** power +need(normalized < 1, 'composite bound (predecessor pricing.py:211): 1/(1+power*reserve) + 4*decay^power < 1 at power 1920 (excess over the first term %.2e)' % float(4 * decay ** power)) +maxT = max(Tq); carrier = max(maxT, int(J['ambient_rank'])) # the compiler fit m*c <= N (FP:111-114) is on the literal carrier, 9 base rows + 8 per stage = 153 +quarter = E.power(carrier, Q(power, 4) * TESTED); factor = E.mul(E.mul(quarter, quarter), E.mul(quarter, quarter)) +eta = E.scale(E.divide((Q(1), Q(1)), factor), tt_) +need(eta[0] > Q(63, 64) ** LP and factor[1] < 2 ** LP and cutoff ** 64 < floor ** 63 and 2 * (cutoff ** power) ** 64 <= (carrier ** power) ** 63, 'compiler complement capacity and shifted exits at logarithm power %d on the literal carrier %d (the largest target rank is %d)' % (LP, carrier, maxT)) +lp_ = LPMIN + 40 +while eta[0] > Q(63, 64) ** (lp_ - 1): lp_ -= 1 +need(lp_ == LPMIN and Q(63, 64) ** (LPMIN - 1) > eta[0], 'logarithm power: on the literal carrier 153 the smallest admissible value at this price is %d (%d fails), written as %d (it is a free parameter, LOG-MAJORANT.md:110-122); the written value 2224 is the one the compiler and outer ledger lines above use' % (lp_, LPMIN - 1, LP)) +gap = (TESTED - KAPPA) / 7; need(gap.numerator == 1, 'compiler grid: (tested-kappa)/7 = %s' % gap) +step = gap.denominator +wins = lambda j: (step * j + 1) ** LP < 2 ** j +lo_, hi_ = 1, 2 +while not wins(hi_): lo_, hi_ = hi_, 2 * hi_ +while hi_ - lo_ > 1: + m = (lo_ + hi_) // 2 + if wins(m): hi_ = m + else: lo_ = m +need(step * hi_ > 8 * power and wins(hi_) and not wins(hi_ - 1), 'explicit uniform threshold H=%d (logarithm power %d)' % (step * hi_, LP)) +Hw = step * hi_; Kbits = math.log2(power) + power * math.log2(carrier) + 2 * math.log2(Hw + 1) # K_star = v m (H+1)^2, v = the chronological power 1920, m = carrier^v (#6901 eq. (4a)) +CALLER_MASS_BITS, PATH_HEIGHT_BITS = 120.35, 157 # QUOTED, not recomputed here: majorants of the #6932 caller, computed by a script that is not part of this package +c_exact = 2 * max(v2max + PATH_HEIGHT_BITS, math.log2(float(mass)) + CALLER_MASS_BITS) +need(c_exact == 362 and abs(Kbits - 14065.5) < 0.1 and math.log2(c_exact + 1) + Kbits < Hw, 'K_star = v m (H+1)^2 with v = %d, m = %d^%d: log2 K_star = %.1f bits at the written H (computed here); with the QUOTED caller majorants (mass <= 2^%.2f, path-maximum height 157 bits; computed on the #6932 caller, not recomputed on this package\'s caller) the per-context bound is height <= %d + 157 = %d bits and magnitude <= %.2f + %.2f = %.2f bits, so c = %d and %d K_star < 2^H holds with %.3e bits to spare; status: argued from #6901 eq. (4a) and lines 299-304, computed, not reviewed' % (power, carrier, power, Kbits, CALLER_MASS_BITS, v2max, v2max + PATH_HEIGHT_BITS, math.log2(float(mass)), CALLER_MASS_BITS, math.log2(float(mass)) + CALLER_MASS_BITS, c_exact, c_exact + 1, Hw - math.log2(c_exact + 1) - Kbits)) +params = {'kappa': KAPPA, 'tested_saving': TESTED, 'complex_uniform_saving': KAPPA + 6 * gap, 'b': KAPPA + 5 * gap, 'a': KAPPA + 4 * gap, 'q': KAPPA + 3 * gap, 'bit_saving': PIN, + 'epsilon': 1 - gap, 'beta': 1 - 3 * gap, 'r0': gap / 10, 'stop': gap, 'layout': gap, 'd': gap} +led = OUT.ledger(params); led['functional_checks']['actual_new_BIT_stock_sublinear'] = params['beta'] * (1 - Q(1, 250)) +need(len(led['strict_checks']) == 54 and len(led['functional_checks']) == 4 and all(v > 0 for k in ('strict_checks', 'functional_checks') for v in led[k].values()), 'outer inventory: 54 strict and 4 functional inequalities all positive at the pin') +PINS = [('main admitted', Q('.0034'), False), ('.00343', Q('.00343'), False), ('main ordinary stock', Q('.0034363538396'), False), ('#5421', Q('.00344412'), False), + ('#4760', Q('.0034597'), False), ('#4814', Q('.003475458'), False), ('#5512', Q('.003483969976'), False), ('#6726 (the pin used)', PIN, True)] +for lab_, pin_, want_ in PINS: # the ledger needs bit_saving > kappa + 4 gap = .00351406004 + L_ = OUT.ledger(dict(params, bit_saving=pin_)); L_['functional_checks']['actual_new_BIT_stock_sublinear'] = params['beta'] * (1 - Q(1, 250)) + ok_ = TESTED < pin_ and all(v > 0 for kk in ('strict_checks', 'functional_checks') for v in L_[kk].values()) + need(ok_ == want_, 'ledger at the BIT saving %s (%s): %s%s' % (float(pin_), lab_, 'all 54 + 4 positive' if ok_ else 'fails', ', margin over the tested price %.3e' % float(pin_ - TESTED) if ok_ else '')) +need(any(v <= 0 for kk in ('strict_checks', 'functional_checks') for v in OUT.ledger(dict(params, bit_saving=params['a'] - Q(1, 10 ** 12)))[kk].values()), 'control: a BIT saving just below kappa + 4 gap (%s) is rejected' % float(params['a'])) +plus = [(7, 1), (3, 1), (5, 1)]; minus = [(9, 1), (4, 1), (1, 2)] +def dlog(terms): + lo = hi = Q(0) + for x, c in terms: + a_ = E.mul((Q(x), Q(x)), E.log_bounds(x)); lo += c * a_[0]; hi += c * a_[1] + return lo, hi +def d2log(terms): + hi = Q(0) + for x, c in terms: + a_ = E.mul(E.mul((Q(x), Q(x)), E.log_bounds(x)), E.log_bounds(x)); hi += c * a_[1] + return hi +dpl, dmi = dlog(plus), dlog(minus); d1 = (dpl[0] - dmi[1], dpl[1] - dmi[0]); Mq = d2log(plus) + d2log(minus) +need(d1[1] + PIN * Mq < 0, 'input-lift saving lemma of #6833 (pricing.py:128-156), cap moved to the pin: g prime negative on 1-pin..1 (its crude bound holds to about .0037765)') +for nm, k_ in (('claim', KAPPA), ('tested', TESTED)): + tl_ = 1 - k_; gl = sum(c * E.power(x, tl_)[0] for x, c in plus) - sum(c * E.power(x, tl_)[1] for x, c in minus) + need(gl > 0 and k_ * (-d1[1]) - k_ * k_ * Mq / 2 > 0, 'input-lift saving positive at the %s price' % nm) + +# ---- declared departures ----------------------------------------------------------------------- +print('DEPARTURES (class; exact count here):') +for cls, what in ( + ('FRAMEWORK CHANGE (this package): odd gate scalars', 'the scalar alphabet of the native word. Dyadic coefficients and SCALE units (local.py:146,149, the verifier copies, native.py:65) become elements and units of A = Z[1/2, 1/3, 1/5], with |q|+1 < 2^16 kept, a declared certificate S = 3^e 5^g (here 1125 = 3^2 5^3) for which S times every prefix row and every pre-ADD product is dyadic, and dyadic public output rows; execution multiplies every root input by S, divides by the odd part of each denominator after a checked divisibility, and divides by S at the exit. The word has %d odd divisions (%d SCALE, %d ADD), %d scans per call. Maintainers must accept this clause; it is not a result of this package. PROOF.md names the changed clauses, the replacement and the penalty; exactness is conditional on exact child returns.' % (n_odd, odd_events['SCALE'], odd_events['ADD'], scans)), + ('new form: per-port root', 'unchanged from the #6932 word: type A (96 ports) is the two-chain root of #6902 (two #6833 roots, t = 0, n = 40), type B (8 ports) is the hosted root of #6889 (t = -1/2, n = 38); the caller is block diagonal over 78 roles, with one stage variable per stage common to both types and 18 joint contacts, each one native event serving both types (HOST2 at the type A ports, HOST at the type B ports). Type A fails the same three family lines as #6902 (t != 0, alpha and beta dyadic units, strongly connected); type B passes every line of its checker. No new failing line.'), + ('new form', 'unchanged: the 8 hosted ports keep the hosted form with no second mains (their X and Y are single planes); the 96 other ports have second mains with the same frame labels as the first mains; 400 mains in total (96 x 4 + 8 x 2). The gauge SCALE 1/2 of the hosted mains is informational here (the endpoint X = x - y, Y = (x + y)/2 covers it).'), + ('new form: type A caller blocks', 'the constant blocks of the type A caller (maximal runs of ADD, SCALE -1 and SWAP between two nonconstant events or joint contacts) are the blocks of #6912 (CubeJerry); check_caller_blocks.py proves each changed block has the same 40 x 40 integer matrix and the joint caller the same 78 x 78 matrix at eight points; the type B caller is unchanged and not covered by that rewrite.'), + ('convention (A6, load-bearing)', 'owned ascent: 23 owned rises (rank mass 56) against native.py:55 / local.py:126; peak owned %d; owned registers read mains: Y2 %d events, X %d events, X2 %d events (%d events in all; %d in the #6932 word). check_a6.py runs the rises as in #6914 and the width-2 phase test of #6930. No ascent, no word.' % (peak, len(oy), len(ox), len(ox2), len(oy) + len(ox) + len(ox2), sum(ob))), + ('new form: full rebuild of the word', 'against the #6932 word (data/prior_word_6932.json.gz, replayed exactly here): public %d against %d registers (one more helper); the frame table, the 54 owned lifetimes and 51 owned fields are the same (as multisets), the peak of concurrent owned fields is %d against %d; T and P differ as printed above (the rank mass of both changes by the same amount per call, S = 1520); the gain is measured on the whole word, not per move.' % (n, len(WB['initial']), peak, pkWB)), + ('verifier', 'endpoint literal native.py:75-77 / local.py:168: the target is X=x, Y=x+y, X2=x2-y2, Y2=y2 at 96 ports and X=x-y, Y=(x+y)/2 at 8 ports; verify_host3_odd.py replaces the dyadic clauses as above (diff against verify_host3_dyadic.py: the helper lines, the SCALE clause, the ADD and COPY clause with the S certificate, the public-row clause).'), + ('verifier', 'events %d, public %d, owned roles %d, lifetimes %d, peak owned %d against local.py:52,54,103 and pricing.py:84-87 literals; per-call scalar work %d against the displayed 10^7 (pricing.py:93); coefficient bits %d/%d against 8/7 (pricing.py:96-97); the event count is declared as this package\'s own bound (the retained 26,000 cap of other packages is not used).' % (len(W['program']), n, NO, life, peak, per_call, nbits, dbits)), + ('convention', 'LAMBDA (%d + %d = 206 events by type), IDLE_ONE (32 + 68 events) as in the #6932 word; not on main; the price of LAMBDA is a review question (above).' % (nlA, nlB)), + ('assumption', 'dirty owned erasure (%d erasures): the owned_erasure assumption, unchanged.' % dirty)): + print(' [%s] %s' % (cls, what)) +need(True, 'departures listed') +print('PASS_P104_SHARED_ODD_NATIVE') diff --git a/research/odd-native-common-grid/source/data/caller.json b/research/odd-native-common-grid/source/data/caller.json new file mode 100644 index 0000000000..08830cee27 --- /dev/null +++ b/research/odd-native-common-grid/source/data/caller.json @@ -0,0 +1 @@ +{"schema":"mixed-root-caller/1","stages":18,"ambient_rank":153,"roles":78,"types":{"A":{"form":"two-chain-HOST2","roles":40,"offset":0,"ports":[0,1,2,3,4,5,6,7,8,9,10,11,12,13,14,16,18,19,20,21,22,23,24,25,26,28,29,30,31,32,33,36,37,38,39,40,41,43,44,45,46,48,49,50,51,52,53,54,56,57,58,59,60,61,62,63,64,65,66,67,68,69,70,71,72,73,74,75,76,77,78,79,80,81,82,83,84,85,86,87,88,89,90,91,92,93,94,95,96,97,98,99,100,101,102,103],"alpha2":"-1","beta2":"0","diagonal":[[-1,0,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1],[-1,0,1,1,1,1,1,1,1,1,1,0,0,0,0,0,0,0,0,0],[-1,0,0,1,1,1,1,1,1,1,1,0,0,0,0,0,0,0,0,0],[-1,0,0,0,1,1,1,1,1,1,1,0,0,0,0,0,0,0,0,0],[-1,0,0,0,0,1,1,1,1,1,1,0,0,0,0,0,0,0,0,0],[-1,0,0,0,0,0,1,1,1,1,1,0,0,0,0,0,0,0,0,0],[-1,0,0,0,0,0,0,1,1,1,1,0,0,0,0,0,0,0,0,0],[-1,0,0,0,0,0,0,0,1,1,1,0,0,0,0,0,0,0,0,0],[-1,0,0,0,0,0,0,0,0,1,1,0,0,0,0,0,0,0,0,0],[-1,0,0,0,0,0,0,0,0,0,1,0,0,0,0,0,0,0,0,0],[-1,0,0,0,0,0,0,0,0,0,0,1,0,0,0,0,0,0,0,0],[-1,0,0,0,0,0,0,0,0,0,0,1,1,0,0,0,0,0,0,0],[-1,0,0,0,0,0,0,0,0,0,0,1,1,1,0,0,0,0,0,0],[-1,0,0,0,0,0,0,0,0,0,0,1,1,1,1,0,0,0,0,0],[-1,0,0,0,0,0,0,0,0,0,0,1,1,1,1,1,0,0,0,0],[-1,0,0,0,0,0,0,0,0,0,0,1,1,1,1,1,1,0,0,0],[-1,0,0,0,0,0,0,0,0,0,0,1,1,1,1,1,1,1,0,0],[-1,0,0,0,0,0,0,0,0,0,0,1,1,1,1,1,1,1,1,0],[-1,0,0,0,0,0,0,0,0,0,0,1,1,1,1,1,1,1,1,1],[-1,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0],[-1,0,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1],[-1,0,1,1,1,1,1,1,1,1,1,0,0,0,0,0,0,0,0,0],[-1,0,0,1,1,1,1,1,1,1,1,0,0,0,0,0,0,0,0,0],[-1,0,0,0,1,1,1,1,1,1,1,0,0,0,0,0,0,0,0,0],[-1,0,0,0,0,1,1,1,1,1,1,0,0,0,0,0,0,0,0,0],[-1,0,0,0,0,0,1,1,1,1,1,0,0,0,0,0,0,0,0,0],[-1,0,0,0,0,0,0,1,1,1,1,0,0,0,0,0,0,0,0,0],[-1,0,0,0,0,0,0,0,1,1,1,0,0,0,0,0,0,0,0,0],[-1,0,0,0,0,0,0,0,0,1,1,0,0,0,0,0,0,0,0,0],[-1,0,0,0,0,0,0,0,0,0,1,0,0,0,0,0,0,0,0,0],[-1,0,0,0,0,0,0,0,0,0,0,1,0,0,0,0,0,0,0,0],[-1,0,0,0,0,0,0,0,0,0,0,1,1,0,0,0,0,0,0,0],[-1,0,0,0,0,0,0,0,0,0,0,1,1,1,0,0,0,0,0,0],[-1,0,0,0,0,0,0,0,0,0,0,1,1,1,1,0,0,0,0,0],[-1,0,0,0,0,0,0,0,0,0,0,1,1,1,1,1,0,0,0,0],[-1,0,0,0,0,0,0,0,0,0,0,1,1,1,1,1,1,0,0,0],[-1,0,0,0,0,0,0,0,0,0,0,1,1,1,1,1,1,1,0,0],[-1,0,0,0,0,0,0,0,0,0,0,1,1,1,1,1,1,1,1,0],[-1,0,0,0,0,0,0,0,0,0,0,1,1,1,1,1,1,1,1,1],[-1,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0]]},"B":{"form":"hosted-HOST","roles":38,"offset":40,"ports":[15,17,27,34,35,42,47,55],"diagonal":[[-1,0,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1],[-1,0,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1],[-1,0,1,1,1,1,1,1,1,1,1,0,0,0,0,0,0,0,0,0],[-1,0,1,1,1,1,1,1,1,1,1,0,0,0,0,0,0,0,0,0],[-1,0,0,1,1,1,1,1,1,1,1,0,0,0,0,0,0,0,0,0],[-1,0,0,1,1,1,1,1,1,1,1,0,0,0,0,0,0,0,0,0],[-1,0,0,0,1,1,1,1,1,1,1,0,0,0,0,0,0,0,0,0],[-1,0,0,0,1,1,1,1,1,1,1,0,0,0,0,0,0,0,0,0],[-1,0,0,0,0,1,1,1,1,1,1,0,0,0,0,0,0,0,0,0],[-1,0,0,0,0,1,1,1,1,1,1,0,0,0,0,0,0,0,0,0],[-1,0,0,0,0,0,1,1,1,1,1,0,0,0,0,0,0,0,0,0],[-1,0,0,0,0,0,1,1,1,1,1,0,0,0,0,0,0,0,0,0],[-1,0,0,0,0,0,0,1,1,1,1,0,0,0,0,0,0,0,0,0],[-1,0,0,0,0,0,0,1,1,1,1,0,0,0,0,0,0,0,0,0],[-1,0,0,0,0,0,0,0,1,1,1,0,0,0,0,0,0,0,0,0],[-1,0,0,0,0,0,0,0,1,1,1,0,0,0,0,0,0,0,0,0],[-1,0,0,0,0,0,0,0,0,1,1,0,0,0,0,0,0,0,0,0],[-1,0,0,0,0,0,0,0,0,1,1,0,0,0,0,0,0,0,0,0],[-1,0,0,0,0,0,0,0,0,0,1,0,0,0,0,0,0,0,0,0],[-1,0,0,0,0,0,0,0,0,0,1,0,0,0,0,0,0,0,0,0],[-1,0,0,0,0,0,0,0,0,0,0,1,0,0,0,0,0,0,0,0],[-1,0,0,0,0,0,0,0,0,0,0,1,0,0,0,0,0,0,0,0],[-1,0,0,0,0,0,0,0,0,0,0,1,1,0,0,0,0,0,0,0],[-1,0,0,0,0,0,0,0,0,0,0,1,1,0,0,0,0,0,0,0],[-1,0,0,0,0,0,0,0,0,0,0,1,1,1,0,0,0,0,0,0],[-1,0,0,0,0,0,0,0,0,0,0,1,1,1,0,0,0,0,0,0],[-1,0,0,0,0,0,0,0,0,0,0,1,1,1,1,0,0,0,0,0],[-1,0,0,0,0,0,0,0,0,0,0,1,1,1,1,0,0,0,0,0],[-1,0,0,0,0,0,0,0,0,0,0,1,1,1,1,1,0,0,0,0],[-1,0,0,0,0,0,0,0,0,0,0,1,1,1,1,1,0,0,0,0],[-1,0,0,0,0,0,0,0,0,0,0,1,1,1,1,1,1,0,0,0],[-1,0,0,0,0,0,0,0,0,0,0,1,1,1,1,1,1,0,0,0],[-1,0,0,0,0,0,0,0,0,0,0,1,1,1,1,1,1,1,0,0],[-1,0,0,0,0,0,0,0,0,0,0,1,1,1,1,1,1,1,0,0],[-1,0,0,0,0,0,0,0,0,0,0,1,1,1,1,1,1,1,1,0],[-1,0,0,0,0,0,0,0,0,0,0,1,1,1,1,1,1,1,1,0],[-1,0,0,0,0,0,0,0,0,0,0,1,1,1,1,1,1,1,1,1],[-1,0,0,0,0,0,0,0,0,0,0,1,1,1,1,1,1,1,1,1]],"pairs":[[0,1,"-1","1/2","-1/2"],[2,3,"-1","1/2","-1/2"],[4,5,"-1","1/2","-1/2"],[6,7,"-1","1/2","-1/2"],[8,9,"-1","1/2","-1/2"],[10,11,"-1","1/2","-1/2"],[12,13,"-1","1/2","-1/2"],[14,15,"-1","1/2","-1/2"],[16,17,"-1","1/2","-1/2"],[22,23,"-1","1/2","-1/2"],[24,25,"-1","1/2","-1/2"],[26,27,"-1","1/2","-1/2"],[28,29,"-1","1/2","-1/2"],[30,31,"-1","1/2","-1/2"],[32,33,"-1","1/2","-1/2"],[34,35,"-1","1/2","-1/2"],[36,37,"-1","1/2","-1/2"],[38,39,"-1","1/2","-1/2"]]}},"events":[["A","ADD",0,1,"-1"],["A","SWAP",0,1],["A","LAMBDA",0,-1],["A","ADD",20,21,"-1"],["A","SWAP",20,21],["A","SCALE",21,"-1"],["A","LAMBDA",20,1],["B","ADD",42,43,"-2"],["B","ADD",41,43,"1"],["B","ADD",40,43,"2"],["B","ADD",41,42,"1"],["B","ADD",40,42,"1"],["B","ADD",40,41,"-2"],["B","SCALE",41,"256"],["B","ADD",43,41,"-1/128"],["B","ADD",42,41,"1/128"],["B","SCALE",40,"128"],["B","ADD",43,40,"-1/128"],["B","ADD",42,40,"1/64"],["B","ADD",41,40,"1"],["B","LAMBDA",40,-1],["J",1,[1,0,20,21],[41,40,"-1","1/2"]],["A","LAMBDA",20,-1],["A","SCALE",21,"-1"],["A","LAMBDA",0,1],["A","ADD",1,2,"1"],["A","ADD",0,2,"-1"],["A","SCALE",1,"-1"],["A","SWAP",1,2],["A","ADD",2,0,"-1"],["A","SWAP",0,1],["A","LAMBDA",0,-1],["A","ADD",21,22,"1"],["A","ADD",20,22,"-1"],["A","SCALE",21,"-1"],["A","SWAP",21,22],["A","SCALE",20,"-1"],["A","ADD",22,20,"1"],["A","SWAP",20,21],["A","LAMBDA",20,1],["B","LAMBDA",40,1],["B","IDLE_ONE",42,[1]],["B","IDLE_ONE",43,[1]],["B","ADD",44,45,"-2"],["B","ADD",42,45,"-2"],["B","ADD",41,45,"-256"],["B","ADD",40,45,"-128"],["B","ADD",43,44,"1"],["B","ADD",42,44,"-2"],["B","ADD",41,44,"-256"],["B","ADD",41,43,"256"],["B","ADD",40,43,"-128"],["B","ADD",40,42,"-128"],["B","ADD",43,42,"1"],["B","ADD",40,41,"1/2"],["B","SCALE",41,"-1"],["B","ADD",45,41,"-1/128"],["B","ADD",44,41,"1/128"],["B","ADD",43,41,"1/128"],["B","ADD",42,41,"1/128"],["B","SCALE",40,"-1"],["B","ADD",45,40,"1/128"],["B","ADD",43,40,"-1/128"],["B","ADD",42,40,"-1/64"],["B","ADD",41,40,"-1"],["B","LAMBDA",40,-1],["J",2,[1,0,20,21],[41,40,"-1","1/2"]],["A","LAMBDA",20,-1],["A","SCALE",21,"-1"],["A","LAMBDA",0,1],["A","ADD",0,1,"-1"],["A","IDLE_ONE",2,[2,3,4,5,6,7,8,9]],["A","ADD",1,3,"1"],["A","ADD",0,3,"-2"],["A","ADD",0,1,"2"],["A","SCALE",1,"-1"],["A","SCALE",0,"-1"],["A","ADD",1,0,"-1"],["A","SWAP",0,3],["A","LAMBDA",0,-1],["A","ADD",20,21,"-1"],["A","IDLE_ONE",22,[2,3,4,5,6,7,8,9]],["A","ADD",21,23,"1"],["A","ADD",20,23,"-2"],["A","ADD",20,21,"2"],["A","SCALE",20,"-1"],["A","ADD",21,20,"1"],["A","SWAP",20,23],["A","LAMBDA",20,1],["B","LAMBDA",40,1],["B","IDLE_ONE",42,[2,3,4,5,6,7,8,9]],["B","IDLE_ONE",43,[2,3,4,5,6,7,8,9]],["B","IDLE_ONE",44,[2]],["B","IDLE_ONE",45,[2]],["B","ADD",46,47,"-2"],["B","ADD",44,47,"-2"],["B","ADD",41,47,"-256"],["B","ADD",40,47,"-128"],["B","ADD",45,46,"1"],["B","ADD",44,46,"-2"],["B","ADD",41,46,"-256"],["B","ADD",41,45,"256"],["B","ADD",40,45,"-128"],["B","ADD",40,44,"-128"],["B","ADD",45,44,"1"],["B","ADD",40,41,"1/2"],["B","SCALE",41,"-1"],["B","ADD",47,41,"-1/128"],["B","ADD",46,41,"1/128"],["B","ADD",45,41,"1/128"],["B","ADD",44,41,"1/128"],["B","SCALE",40,"-1"],["B","ADD",47,40,"1/128"],["B","ADD",45,40,"-1/128"],["B","ADD",44,40,"-1/64"],["B","ADD",41,40,"-1"],["B","LAMBDA",40,-1],["J",3,[1,0,20,21],[41,40,"-1","1/2"]],["A","LAMBDA",20,-1],["A","SCALE",21,"-1"],["A","LAMBDA",0,1],["A","ADD",0,1,"-1"],["A","IDLE_ONE",3,[3,4,5,6,7,8,9]],["A","ADD",1,4,"1"],["A","ADD",0,4,"-2"],["A","ADD",0,1,"2"],["A","SCALE",1,"-1"],["A","SCALE",0,"-1"],["A","ADD",1,0,"-1"],["A","SWAP",0,4],["A","LAMBDA",0,-1],["A","ADD",20,21,"-1"],["A","IDLE_ONE",23,[3,4,5,6,7,8,9]],["A","ADD",21,24,"1"],["A","ADD",20,24,"-2"],["A","ADD",20,21,"2"],["A","SCALE",20,"-1"],["A","ADD",21,20,"1"],["A","SWAP",20,24],["A","LAMBDA",20,1],["B","LAMBDA",40,1],["B","IDLE_ONE",44,[3,4,5,6,7,8,9]],["B","IDLE_ONE",45,[3,4,5,6,7,8,9]],["B","IDLE_ONE",46,[3]],["B","IDLE_ONE",47,[3]],["B","ADD",48,49,"-2"],["B","ADD",46,49,"-2"],["B","ADD",41,49,"-256"],["B","ADD",40,49,"-128"],["B","ADD",47,48,"1"],["B","ADD",46,48,"-2"],["B","ADD",41,48,"-256"],["B","ADD",41,47,"256"],["B","ADD",40,47,"-128"],["B","ADD",40,46,"-128"],["B","ADD",47,46,"1"],["B","ADD",40,41,"1/2"],["B","SCALE",41,"-1"],["B","ADD",49,41,"-1/128"],["B","ADD",48,41,"1/128"],["B","ADD",47,41,"1/128"],["B","ADD",46,41,"1/128"],["B","SCALE",40,"-1"],["B","ADD",49,40,"1/128"],["B","ADD",47,40,"-1/128"],["B","ADD",46,40,"-1/64"],["B","ADD",41,40,"-1"],["B","LAMBDA",40,-1],["J",4,[1,0,20,21],[41,40,"-1","1/2"]],["A","LAMBDA",20,-1],["A","SCALE",21,"-1"],["A","LAMBDA",0,1],["A","ADD",0,1,"-1"],["A","IDLE_ONE",4,[4,5,6,7,8,9]],["A","ADD",1,5,"1"],["A","ADD",0,5,"-2"],["A","ADD",0,1,"2"],["A","SCALE",1,"-1"],["A","SCALE",0,"-1"],["A","ADD",1,0,"-1"],["A","SWAP",0,5],["A","LAMBDA",0,-1],["A","ADD",20,21,"-1"],["A","IDLE_ONE",24,[4,5,6,7,8,9]],["A","ADD",21,25,"1"],["A","ADD",20,25,"-2"],["A","ADD",20,21,"2"],["A","SCALE",20,"-1"],["A","ADD",21,20,"1"],["A","SWAP",20,25],["A","LAMBDA",20,1],["B","LAMBDA",40,1],["B","IDLE_ONE",46,[4,5,6,7,8,9]],["B","IDLE_ONE",47,[4,5,6,7,8,9]],["B","IDLE_ONE",48,[4]],["B","IDLE_ONE",49,[4]],["B","ADD",50,51,"-2"],["B","ADD",48,51,"-2"],["B","ADD",41,51,"-256"],["B","ADD",40,51,"-128"],["B","ADD",49,50,"1"],["B","ADD",48,50,"-2"],["B","ADD",41,50,"-256"],["B","ADD",41,49,"256"],["B","ADD",40,49,"-128"],["B","ADD",40,48,"-128"],["B","ADD",49,48,"1"],["B","ADD",40,41,"1/2"],["B","SCALE",41,"-1"],["B","ADD",51,41,"-1/128"],["B","ADD",50,41,"1/128"],["B","ADD",49,41,"1/128"],["B","ADD",48,41,"1/128"],["B","SCALE",40,"-1"],["B","ADD",51,40,"1/128"],["B","ADD",49,40,"-1/128"],["B","ADD",48,40,"-1/64"],["B","ADD",41,40,"-1"],["B","LAMBDA",40,-1],["J",5,[1,0,20,21],[41,40,"-1","1/2"]],["A","LAMBDA",20,-1],["A","SCALE",21,"-1"],["A","LAMBDA",0,1],["A","ADD",0,1,"-1"],["A","IDLE_ONE",5,[5,6,7,8,9]],["A","ADD",1,6,"1"],["A","ADD",0,6,"-2"],["A","ADD",0,1,"2"],["A","SCALE",1,"-1"],["A","SCALE",0,"-1"],["A","ADD",1,0,"-1"],["A","SWAP",0,6],["A","LAMBDA",0,-1],["A","ADD",20,21,"-1"],["A","IDLE_ONE",25,[5,6,7,8,9]],["A","ADD",21,26,"1"],["A","ADD",20,26,"-2"],["A","ADD",20,21,"2"],["A","SCALE",20,"-1"],["A","ADD",21,20,"1"],["A","SWAP",20,26],["A","LAMBDA",20,1],["B","LAMBDA",40,1],["B","IDLE_ONE",48,[5,6,7,8,9]],["B","IDLE_ONE",49,[5,6,7,8,9]],["B","IDLE_ONE",50,[5]],["B","IDLE_ONE",51,[5]],["B","ADD",52,53,"-2"],["B","ADD",50,53,"-2"],["B","ADD",41,53,"-256"],["B","ADD",40,53,"-128"],["B","ADD",51,52,"1"],["B","ADD",50,52,"-2"],["B","ADD",41,52,"-256"],["B","ADD",41,51,"256"],["B","ADD",40,51,"-128"],["B","ADD",40,50,"-128"],["B","ADD",51,50,"1"],["B","ADD",40,41,"1/2"],["B","SCALE",41,"-1"],["B","ADD",53,41,"-1/128"],["B","ADD",52,41,"1/128"],["B","ADD",51,41,"1/128"],["B","ADD",50,41,"1/128"],["B","SCALE",40,"-1"],["B","ADD",53,40,"1/128"],["B","ADD",51,40,"-1/128"],["B","ADD",50,40,"-1/64"],["B","ADD",41,40,"-1"],["B","LAMBDA",40,-1],["J",6,[1,0,20,21],[41,40,"-1","1/2"]],["A","LAMBDA",20,-1],["A","SCALE",21,"-1"],["A","LAMBDA",0,1],["A","ADD",0,1,"-1"],["A","IDLE_ONE",6,[6,7,8,9]],["A","ADD",1,7,"1"],["A","ADD",0,7,"-2"],["A","ADD",0,1,"2"],["A","SCALE",1,"-1"],["A","SCALE",0,"-1"],["A","ADD",1,0,"-1"],["A","SWAP",0,7],["A","LAMBDA",0,-1],["A","ADD",20,21,"-1"],["A","IDLE_ONE",26,[6,7,8,9]],["A","ADD",21,27,"1"],["A","ADD",20,27,"-2"],["A","ADD",20,21,"2"],["A","SCALE",20,"-1"],["A","ADD",21,20,"1"],["A","SWAP",20,27],["A","LAMBDA",20,1],["B","LAMBDA",40,1],["B","IDLE_ONE",50,[6,7,8,9]],["B","IDLE_ONE",51,[6,7,8,9]],["B","IDLE_ONE",52,[6]],["B","IDLE_ONE",53,[6]],["B","ADD",54,55,"-2"],["B","ADD",52,55,"-2"],["B","ADD",41,55,"-256"],["B","ADD",40,55,"-128"],["B","ADD",53,54,"1"],["B","ADD",52,54,"-2"],["B","ADD",41,54,"-256"],["B","ADD",41,53,"256"],["B","ADD",40,53,"-128"],["B","ADD",40,52,"-128"],["B","ADD",53,52,"1"],["B","ADD",40,41,"1/2"],["B","SCALE",41,"-1"],["B","ADD",55,41,"-1/128"],["B","ADD",54,41,"1/128"],["B","ADD",53,41,"1/128"],["B","ADD",52,41,"1/128"],["B","SCALE",40,"-1"],["B","ADD",55,40,"1/128"],["B","ADD",53,40,"-1/128"],["B","ADD",52,40,"-1/64"],["B","ADD",41,40,"-1"],["B","LAMBDA",40,-1],["J",7,[1,0,20,21],[41,40,"-1","1/2"]],["A","LAMBDA",20,-1],["A","SCALE",21,"-1"],["A","LAMBDA",0,1],["A","ADD",0,1,"-1"],["A","IDLE_ONE",7,[7,8,9]],["A","ADD",1,8,"1"],["A","ADD",0,8,"-2"],["A","ADD",0,1,"2"],["A","SCALE",1,"-1"],["A","SCALE",0,"-1"],["A","ADD",1,0,"-1"],["A","SWAP",0,8],["A","LAMBDA",0,-1],["A","ADD",20,21,"-1"],["A","IDLE_ONE",27,[7,8,9]],["A","ADD",21,28,"1"],["A","ADD",20,28,"-2"],["A","ADD",20,21,"2"],["A","SCALE",20,"-1"],["A","ADD",21,20,"1"],["A","SWAP",20,28],["A","LAMBDA",20,1],["B","LAMBDA",40,1],["B","IDLE_ONE",52,[7,8,9]],["B","IDLE_ONE",53,[7,8,9]],["B","IDLE_ONE",54,[7]],["B","IDLE_ONE",55,[7]],["B","ADD",56,57,"-2"],["B","ADD",54,57,"-2"],["B","ADD",41,57,"-256"],["B","ADD",40,57,"-128"],["B","ADD",55,56,"1"],["B","ADD",54,56,"-2"],["B","ADD",41,56,"-256"],["B","ADD",41,55,"256"],["B","ADD",40,55,"-128"],["B","ADD",40,54,"-128"],["B","ADD",55,54,"1"],["B","ADD",40,41,"1/2"],["B","SCALE",41,"-1"],["B","ADD",57,41,"-1/128"],["B","ADD",56,41,"1/128"],["B","ADD",55,41,"1/128"],["B","ADD",54,41,"1/128"],["B","SCALE",40,"-1"],["B","ADD",57,40,"1/128"],["B","ADD",55,40,"-1/128"],["B","ADD",54,40,"-1/64"],["B","ADD",41,40,"-1"],["B","LAMBDA",40,-1],["J",8,[1,0,20,21],[41,40,"-1","1/2"]],["A","LAMBDA",20,-1],["A","SCALE",21,"-1"],["A","LAMBDA",0,1],["A","ADD",0,1,"-1"],["A","IDLE_ONE",8,[8,9]],["A","ADD",1,9,"1"],["A","ADD",0,9,"-2"],["A","ADD",0,1,"2"],["A","SCALE",1,"-1"],["A","SCALE",0,"-1"],["A","ADD",1,0,"-1"],["A","SWAP",0,9],["A","LAMBDA",0,-1],["A","ADD",20,21,"-1"],["A","IDLE_ONE",28,[8,9]],["A","ADD",21,29,"1"],["A","ADD",20,29,"-2"],["A","ADD",20,21,"2"],["A","SCALE",20,"-1"],["A","ADD",21,20,"1"],["A","SWAP",20,29],["A","LAMBDA",20,1],["B","LAMBDA",40,1],["B","IDLE_ONE",54,[8,9]],["B","IDLE_ONE",55,[8,9]],["B","IDLE_ONE",56,[8]],["B","IDLE_ONE",57,[8]],["B","ADD",58,59,"-2"],["B","ADD",56,59,"-2"],["B","ADD",41,59,"-256"],["B","ADD",40,59,"-128"],["B","ADD",57,58,"1"],["B","ADD",56,58,"-2"],["B","ADD",41,58,"-256"],["B","ADD",41,57,"256"],["B","ADD",40,57,"-128"],["B","ADD",40,56,"-128"],["B","ADD",57,56,"1"],["B","ADD",40,41,"1/2"],["B","SCALE",41,"-1"],["B","ADD",59,41,"-1/128"],["B","ADD",58,41,"1/128"],["B","ADD",57,41,"1/128"],["B","ADD",56,41,"1/128"],["B","SCALE",40,"-1"],["B","ADD",59,40,"1/128"],["B","ADD",57,40,"-1/128"],["B","ADD",56,40,"-1/64"],["B","ADD",41,40,"-1"],["B","LAMBDA",40,-1],["J",9,[1,0,20,21],[41,40,"-1","1/2"]],["A","LAMBDA",20,-1],["A","SCALE",21,"-1"],["A","LAMBDA",0,1],["A","ADD",0,1,"-1"],["A","IDLE_ONE",9,[9]],["A","SWAP",8,9],["A","SWAP",7,9],["A","SWAP",6,9],["A","SWAP",5,9],["A","SWAP",4,9],["A","SWAP",3,9],["A","SWAP",2,9],["A","ADD",0,1,"1"],["A","SCALE",1,"-1"],["A","SWAP",1,9],["A","ADD",9,0,"1"],["A","ADD",8,0,"2"],["A","ADD",7,0,"2"],["A","ADD",6,0,"2"],["A","ADD",5,0,"2"],["A","ADD",4,0,"2"],["A","ADD",3,0,"2"],["A","ADD",2,0,"2"],["A","ADD",1,0,"2"],["A","ADD",19,1,"-1"],["A","ADD",18,1,"-1"],["A","ADD",17,1,"-1"],["A","ADD",16,1,"-1"],["A","ADD",15,1,"-1"],["A","ADD",14,1,"-1"],["A","ADD",13,1,"-1"],["A","ADD",12,1,"-1"],["A","ADD",11,1,"-1"],["A","ADD",10,1,"-1"],["A","ADD",9,1,"-1"],["A","ADD",8,1,"-1"],["A","ADD",7,1,"-1"],["A","ADD",6,1,"-1"],["A","ADD",5,1,"-1"],["A","ADD",4,1,"-1"],["A","ADD",3,1,"-1"],["A","ADD",2,1,"-1"],["A","SWAP",0,1],["A","LAMBDA",0,-1],["A","QUERY",0,1,-1],["A","LAMBDA",0,1],["A","ADD",0,1,"-1"],["A","ADD",19,0,"1"],["A","ADD",18,0,"1"],["A","ADD",17,0,"1"],["A","ADD",16,0,"1"],["A","ADD",15,0,"1"],["A","ADD",14,0,"1"],["A","ADD",13,0,"1"],["A","ADD",12,0,"1"],["A","ADD",11,0,"1"],["A","ADD",10,0,"1"],["A","ADD",9,0,"1"],["A","ADD",8,0,"1"],["A","ADD",7,0,"1"],["A","ADD",6,0,"1"],["A","ADD",5,0,"1"],["A","ADD",4,0,"1"],["A","ADD",3,0,"1"],["A","ADD",2,0,"1"],["A","SWAP",0,1],["A","ADD",1,19,"-1"],["A","ADD",1,18,"-1"],["A","ADD",1,17,"1"],["A","ADD",1,16,"-1"],["A","ADD",1,15,"1"],["A","ADD",1,14,"-1"],["A","ADD",1,13,"1"],["A","ADD",1,12,"-1"],["A","ADD",1,11,"1"],["A","ADD",1,10,"-1"],["A","ADD",1,9,"1"],["A","ADD",1,8,"-1"],["A","ADD",1,7,"1"],["A","ADD",1,6,"-1"],["A","ADD",1,5,"1"],["A","ADD",1,4,"-1"],["A","ADD",1,3,"1"],["A","ADD",1,2,"-1"],["A","SCALE",1,"-1"],["A","SCALE",0,"-1"],["A","ADD",18,0,"-2"],["A","ADD",17,0,"-2"],["A","ADD",16,0,"-2"],["A","ADD",15,0,"-2"],["A","ADD",14,0,"-2"],["A","ADD",13,0,"-2"],["A","ADD",12,0,"-2"],["A","ADD",11,0,"-2"],["A","ADD",10,0,"-2"],["A","ADD",1,0,"-2"],["A","LAMBDA",0,-1],["A","QUERY",0,1,-1],["A","LAMBDA",0,1],["A","ADD",1,19,"-1"],["A","ADD",0,19,"-1"],["A","ADD",1,18,"-1"],["A","ADD",0,18,"-1"],["A","ADD",19,18,"2"],["A","SWAP",18,19],["A","ADD",1,17,"1"],["A","ADD",0,17,"1"],["A","ADD",18,17,"-2"],["A","SWAP",17,18],["A","ADD",1,16,"-1"],["A","ADD",0,16,"-1"],["A","ADD",17,16,"2"],["A","SWAP",16,17],["A","ADD",1,15,"1"],["A","ADD",0,15,"1"],["A","ADD",16,15,"-2"],["A","SWAP",15,16],["A","ADD",1,14,"-1"],["A","ADD",0,14,"-1"],["A","ADD",15,14,"2"],["A","SWAP",14,15],["A","ADD",1,13,"1"],["A","ADD",0,13,"1"],["A","ADD",14,13,"-2"],["A","SWAP",13,14],["A","ADD",1,12,"-1"],["A","ADD",0,12,"-1"],["A","ADD",13,12,"2"],["A","SWAP",12,13],["A","ADD",1,11,"1"],["A","ADD",0,11,"1"],["A","ADD",12,11,"-2"],["A","SWAP",11,12],["A","ADD",1,10,"-1"],["A","ADD",0,10,"-1"],["A","ADD",11,10,"2"],["A","SWAP",10,11],["A","ADD",1,9,"1"],["A","ADD",0,9,"1"],["A","ADD",10,9,"-2"],["A","SWAP",9,10],["A","ADD",1,8,"-1"],["A","ADD",0,8,"-1"],["A","ADD",9,8,"2"],["A","SWAP",8,9],["A","ADD",1,7,"1"],["A","ADD",0,7,"1"],["A","ADD",8,7,"-2"],["A","SWAP",7,8],["A","ADD",1,6,"-1"],["A","ADD",0,6,"-1"],["A","ADD",7,6,"2"],["A","SWAP",6,7],["A","ADD",1,5,"1"],["A","ADD",0,5,"1"],["A","ADD",6,5,"-2"],["A","SWAP",5,6],["A","ADD",1,4,"-1"],["A","ADD",0,4,"-1"],["A","ADD",5,4,"2"],["A","SWAP",4,5],["A","ADD",1,3,"1"],["A","ADD",0,3,"1"],["A","ADD",4,3,"-2"],["A","SWAP",3,4],["A","ADD",1,2,"-1"],["A","ADD",0,2,"-1"],["A","ADD",3,2,"2"],["A","SWAP",2,3],["A","ADD",0,1,"-1"],["A","SCALE",1,"-1"],["A","ADD",2,1,"-2"],["A","SWAP",1,2],["A","ADD",1,0,"1"],["A","LAMBDA",0,-1],["A","QUERY",0,1,-1],["A","LAMBDA",0,1],["A","ADD",1,19,"-2"],["A","ADD",0,19,"-2"],["A","ADD",1,18,"2"],["A","ADD",0,18,"2"],["A","ADD",1,17,"-2"],["A","ADD",0,17,"-2"],["A","SWAP",17,19],["A","ADD",1,16,"2"],["A","ADD",0,16,"2"],["A","SWAP",16,18],["A","ADD",1,15,"-2"],["A","ADD",0,15,"-2"],["A","SWAP",15,19],["A","ADD",1,14,"2"],["A","ADD",0,14,"2"],["A","SWAP",14,18],["A","ADD",1,13,"-2"],["A","ADD",0,13,"-2"],["A","SWAP",13,19],["A","ADD",1,12,"2"],["A","ADD",0,12,"2"],["A","SWAP",12,18],["A","ADD",1,11,"-1"],["A","SCALE",11,"-1"],["A","SWAP",11,19],["A","ADD",1,10,"2"],["A","ADD",0,10,"2"],["A","SWAP",10,18],["A","ADD",1,9,"-2"],["A","ADD",0,9,"-2"],["A","SWAP",9,17],["A","ADD",1,8,"2"],["A","ADD",0,8,"2"],["A","SWAP",8,16],["A","ADD",1,7,"-2"],["A","ADD",0,7,"-2"],["A","SWAP",7,15],["A","ADD",1,6,"2"],["A","ADD",0,6,"2"],["A","SWAP",6,14],["A","ADD",1,5,"-2"],["A","ADD",0,5,"-2"],["A","SWAP",5,13],["A","ADD",1,4,"2"],["A","ADD",0,4,"2"],["A","SWAP",4,12],["A","ADD",1,3,"-2"],["A","ADD",0,3,"-2"],["A","SWAP",3,11],["A","ADD",1,2,"2"],["A","ADD",0,2,"2"],["A","SWAP",2,10],["A","ADD",0,1,"-1"],["A","SWAP",1,19],["A","ADD",19,0,"-1"],["A","ADD",1,0,"2"],["A","SWAP",0,1],["A","LAMBDA",0,-1],["A","ADD",20,21,"-1"],["A","IDLE_ONE",29,[9]],["A","SWAP",28,29],["A","SWAP",27,29],["A","SWAP",26,29],["A","SWAP",25,29],["A","SWAP",24,29],["A","SWAP",23,29],["A","SWAP",22,29],["A","ADD",20,21,"1"],["A","SCALE",21,"-1"],["A","SWAP",21,29],["A","ADD",29,20,"1"],["A","ADD",28,20,"2"],["A","ADD",27,20,"2"],["A","ADD",26,20,"2"],["A","ADD",25,20,"2"],["A","ADD",24,20,"2"],["A","ADD",23,20,"2"],["A","ADD",22,20,"2"],["A","ADD",21,20,"2"],["A","ADD",39,21,"-1"],["A","ADD",38,21,"-1"],["A","ADD",37,21,"-1"],["A","ADD",36,21,"-1"],["A","ADD",35,21,"-1"],["A","ADD",34,21,"-1"],["A","ADD",33,21,"-1"],["A","ADD",32,21,"-1"],["A","ADD",31,21,"-1"],["A","ADD",30,21,"-1"],["A","ADD",29,21,"-1"],["A","ADD",28,21,"-1"],["A","ADD",27,21,"-1"],["A","ADD",26,21,"-1"],["A","ADD",25,21,"-1"],["A","ADD",24,21,"-1"],["A","ADD",23,21,"-1"],["A","ADD",22,21,"-1"],["A","SWAP",20,21],["A","LAMBDA",20,-1],["A","QUERY",20,21,-1],["A","LAMBDA",20,1],["A","ADD",20,21,"-1"],["A","ADD",39,20,"1"],["A","ADD",38,20,"1"],["A","ADD",37,20,"1"],["A","ADD",36,20,"1"],["A","ADD",35,20,"1"],["A","ADD",34,20,"1"],["A","ADD",33,20,"1"],["A","ADD",32,20,"1"],["A","ADD",31,20,"1"],["A","ADD",30,20,"1"],["A","ADD",29,20,"1"],["A","ADD",28,20,"1"],["A","ADD",27,20,"1"],["A","ADD",26,20,"1"],["A","ADD",25,20,"1"],["A","ADD",24,20,"1"],["A","ADD",23,20,"1"],["A","ADD",22,20,"1"],["A","SWAP",20,21],["A","ADD",21,39,"-1"],["A","ADD",21,38,"-1"],["A","ADD",21,37,"1"],["A","ADD",21,36,"-1"],["A","ADD",21,35,"1"],["A","ADD",21,34,"-1"],["A","ADD",21,33,"1"],["A","ADD",21,32,"-1"],["A","ADD",21,31,"1"],["A","ADD",21,30,"-1"],["A","ADD",21,29,"1"],["A","ADD",21,28,"-1"],["A","ADD",21,27,"1"],["A","ADD",21,26,"-1"],["A","ADD",21,25,"1"],["A","ADD",21,24,"-1"],["A","ADD",21,23,"1"],["A","ADD",21,22,"-1"],["A","SCALE",21,"-1"],["A","SCALE",20,"-1"],["A","ADD",38,20,"-2"],["A","ADD",37,20,"-2"],["A","ADD",36,20,"-2"],["A","ADD",35,20,"-2"],["A","ADD",34,20,"-2"],["A","ADD",33,20,"-2"],["A","ADD",32,20,"-2"],["A","ADD",31,20,"-2"],["A","ADD",30,20,"-2"],["A","ADD",21,20,"-2"],["A","LAMBDA",20,-1],["A","QUERY",20,21,-1],["A","LAMBDA",20,1],["A","ADD",21,39,"-1"],["A","ADD",20,39,"-1"],["A","ADD",21,38,"-1"],["A","ADD",20,38,"-1"],["A","ADD",39,38,"2"],["A","SWAP",38,39],["A","ADD",21,37,"1"],["A","ADD",20,37,"1"],["A","ADD",38,37,"-2"],["A","SWAP",37,38],["A","ADD",21,36,"-1"],["A","ADD",20,36,"-1"],["A","ADD",37,36,"2"],["A","SWAP",36,37],["A","ADD",21,35,"1"],["A","ADD",20,35,"1"],["A","ADD",36,35,"-2"],["A","SWAP",35,36],["A","ADD",21,34,"-1"],["A","ADD",20,34,"-1"],["A","ADD",35,34,"2"],["A","SWAP",34,35],["A","ADD",21,33,"1"],["A","ADD",20,33,"1"],["A","ADD",34,33,"-2"],["A","SWAP",33,34],["A","ADD",21,32,"-1"],["A","ADD",20,32,"-1"],["A","ADD",33,32,"2"],["A","SWAP",32,33],["A","ADD",21,31,"1"],["A","ADD",20,31,"1"],["A","ADD",32,31,"-2"],["A","SWAP",31,32],["A","ADD",21,30,"-1"],["A","ADD",20,30,"-1"],["A","ADD",31,30,"2"],["A","SWAP",30,31],["A","ADD",21,29,"1"],["A","ADD",20,29,"1"],["A","ADD",30,29,"-2"],["A","SWAP",29,30],["A","ADD",21,28,"-1"],["A","ADD",20,28,"-1"],["A","ADD",29,28,"2"],["A","SWAP",28,29],["A","ADD",21,27,"1"],["A","ADD",20,27,"1"],["A","ADD",28,27,"-2"],["A","SWAP",27,28],["A","ADD",21,26,"-1"],["A","ADD",20,26,"-1"],["A","ADD",27,26,"2"],["A","SWAP",26,27],["A","ADD",21,25,"1"],["A","ADD",20,25,"1"],["A","ADD",26,25,"-2"],["A","SWAP",25,26],["A","ADD",21,24,"-1"],["A","ADD",20,24,"-1"],["A","ADD",25,24,"2"],["A","SWAP",24,25],["A","ADD",21,23,"1"],["A","ADD",20,23,"1"],["A","ADD",24,23,"-2"],["A","SWAP",23,24],["A","ADD",21,22,"-1"],["A","ADD",20,22,"-1"],["A","ADD",23,22,"2"],["A","SWAP",22,23],["A","ADD",20,21,"-1"],["A","SCALE",21,"-1"],["A","ADD",22,21,"-2"],["A","SWAP",21,22],["A","ADD",21,20,"1"],["A","LAMBDA",20,-1],["A","QUERY",20,21,-1],["A","LAMBDA",20,1],["A","ADD",21,39,"-2"],["A","ADD",20,39,"-2"],["A","ADD",21,38,"2"],["A","ADD",20,38,"2"],["A","ADD",21,37,"-2"],["A","ADD",20,37,"-2"],["A","SWAP",37,39],["A","ADD",21,36,"2"],["A","ADD",20,36,"2"],["A","SWAP",36,38],["A","ADD",21,35,"-2"],["A","ADD",20,35,"-2"],["A","SWAP",35,39],["A","ADD",21,34,"2"],["A","ADD",20,34,"2"],["A","SWAP",34,38],["A","ADD",21,33,"-2"],["A","ADD",20,33,"-2"],["A","SWAP",33,39],["A","ADD",21,32,"2"],["A","ADD",20,32,"2"],["A","SWAP",32,38],["A","ADD",21,31,"-1"],["A","SCALE",31,"-1"],["A","SWAP",31,39],["A","ADD",21,30,"2"],["A","ADD",20,30,"2"],["A","SWAP",30,38],["A","ADD",21,29,"-2"],["A","ADD",20,29,"-2"],["A","SWAP",29,37],["A","ADD",21,28,"2"],["A","ADD",20,28,"2"],["A","SWAP",28,36],["A","ADD",21,27,"-2"],["A","ADD",20,27,"-2"],["A","SWAP",27,35],["A","ADD",21,26,"2"],["A","ADD",20,26,"2"],["A","SWAP",26,34],["A","ADD",21,25,"-2"],["A","ADD",20,25,"-2"],["A","SWAP",25,33],["A","ADD",21,24,"2"],["A","ADD",20,24,"2"],["A","SWAP",24,32],["A","ADD",21,23,"-2"],["A","ADD",20,23,"-2"],["A","SWAP",23,31],["A","ADD",21,22,"2"],["A","ADD",20,22,"2"],["A","SWAP",22,30],["A","ADD",20,21,"-1"],["A","SWAP",21,39],["A","SCALE",20,"-1"],["A","ADD",39,20,"1"],["A","ADD",21,20,"-2"],["A","SWAP",20,21],["A","LAMBDA",20,1],["B","LAMBDA",40,1],["B","IDLE_ONE",56,[9]],["B","IDLE_ONE",57,[9]],["B","IDLE_ONE",58,[9]],["B","IDLE_ONE",59,[9]],["B","ADD",58,77,"1"],["B","ADD",57,77,"1"],["B","ADD",55,77,"1"],["B","ADD",53,77,"1"],["B","ADD",51,77,"1"],["B","ADD",49,77,"1"],["B","ADD",47,77,"1"],["B","ADD",45,77,"1"],["B","ADD",43,77,"1"],["B","ADD",41,77,"-128"],["B","ADD",40,77,"64"],["B","ADD",58,75,"-1"],["B","ADD",57,75,"-1"],["B","ADD",55,75,"-1"],["B","ADD",53,75,"-1"],["B","ADD",51,75,"-1"],["B","ADD",49,75,"-1"],["B","ADD",47,75,"-1"],["B","ADD",45,75,"-1"],["B","ADD",43,75,"-1"],["B","ADD",41,75,"128"],["B","ADD",40,75,"-64"],["B","ADD",58,74,"2"],["B","ADD",57,74,"2"],["B","ADD",55,74,"2"],["B","ADD",53,74,"2"],["B","ADD",51,74,"2"],["B","ADD",49,74,"2"],["B","ADD",47,74,"2"],["B","ADD",45,74,"2"],["B","ADD",43,74,"2"],["B","ADD",41,74,"-256"],["B","ADD",40,74,"128"],["B","ADD",58,73,"-1"],["B","ADD",57,73,"-1"],["B","ADD",55,73,"-1"],["B","ADD",53,73,"-1"],["B","ADD",51,73,"-1"],["B","ADD",49,73,"-1"],["B","ADD",47,73,"-1"],["B","ADD",45,73,"-1"],["B","ADD",43,73,"-1"],["B","ADD",41,73,"128"],["B","ADD",40,73,"-64"],["B","ADD",58,71,"1"],["B","ADD",57,71,"1"],["B","ADD",55,71,"1"],["B","ADD",53,71,"1"],["B","ADD",51,71,"1"],["B","ADD",49,71,"1"],["B","ADD",47,71,"1"],["B","ADD",45,71,"1"],["B","ADD",43,71,"1"],["B","ADD",41,71,"-128"],["B","ADD",40,71,"64"],["B","ADD",58,70,"-2"],["B","ADD",57,70,"-2"],["B","ADD",55,70,"-2"],["B","ADD",53,70,"-2"],["B","ADD",51,70,"-2"],["B","ADD",49,70,"-2"],["B","ADD",47,70,"-2"],["B","ADD",45,70,"-2"],["B","ADD",43,70,"-2"],["B","ADD",41,70,"256"],["B","ADD",40,70,"-128"],["B","ADD",58,69,"1"],["B","ADD",57,69,"1"],["B","ADD",55,69,"1"],["B","ADD",53,69,"1"],["B","ADD",51,69,"1"],["B","ADD",49,69,"1"],["B","ADD",47,69,"1"],["B","ADD",45,69,"1"],["B","ADD",43,69,"1"],["B","ADD",41,69,"-128"],["B","ADD",40,69,"64"],["B","ADD",58,67,"-1"],["B","ADD",57,67,"-1"],["B","ADD",55,67,"-1"],["B","ADD",53,67,"-1"],["B","ADD",51,67,"-1"],["B","ADD",49,67,"-1"],["B","ADD",47,67,"-1"],["B","ADD",45,67,"-1"],["B","ADD",43,67,"-1"],["B","ADD",41,67,"128"],["B","ADD",40,67,"-64"],["B","ADD",58,66,"2"],["B","ADD",57,66,"2"],["B","ADD",55,66,"2"],["B","ADD",53,66,"2"],["B","ADD",51,66,"2"],["B","ADD",49,66,"2"],["B","ADD",47,66,"2"],["B","ADD",45,66,"2"],["B","ADD",43,66,"2"],["B","ADD",41,66,"-256"],["B","ADD",40,66,"128"],["B","ADD",58,65,"-1"],["B","ADD",57,65,"-1"],["B","ADD",55,65,"-1"],["B","ADD",53,65,"-1"],["B","ADD",51,65,"-1"],["B","ADD",49,65,"-1"],["B","ADD",47,65,"-1"],["B","ADD",45,65,"-1"],["B","ADD",43,65,"-1"],["B","ADD",41,65,"128"],["B","ADD",40,65,"-64"],["B","ADD",58,63,"1"],["B","ADD",57,63,"1"],["B","ADD",55,63,"1"],["B","ADD",53,63,"1"],["B","ADD",51,63,"1"],["B","ADD",49,63,"1"],["B","ADD",47,63,"1"],["B","ADD",45,63,"1"],["B","ADD",43,63,"1"],["B","ADD",41,63,"-128"],["B","ADD",40,63,"64"],["B","ADD",58,62,"-2"],["B","ADD",57,62,"-2"],["B","ADD",55,62,"-2"],["B","ADD",53,62,"-2"],["B","ADD",51,62,"-2"],["B","ADD",49,62,"-2"],["B","ADD",47,62,"-2"],["B","ADD",45,62,"-2"],["B","ADD",43,62,"-2"],["B","ADD",41,62,"256"],["B","ADD",40,62,"-128"],["B","ADD",58,61,"1"],["B","ADD",57,61,"1"],["B","ADD",55,61,"1"],["B","ADD",53,61,"1"],["B","ADD",51,61,"1"],["B","ADD",49,61,"1"],["B","ADD",47,61,"1"],["B","ADD",45,61,"1"],["B","ADD",43,61,"1"],["B","ADD",41,61,"-128"],["B","ADD",40,61,"64"],["B","ADD",41,59,"256"],["B","ADD",40,59,"-128"],["B","ADD",57,58,"-3/2"],["B","ADD",55,58,"-1"],["B","ADD",53,58,"-1"],["B","ADD",51,58,"-1"],["B","ADD",49,58,"-1"],["B","ADD",47,58,"-1"],["B","ADD",45,58,"-1"],["B","ADD",43,58,"-1"],["B","ADD",41,58,"128"],["B","ADD",40,58,"-64"],["B","SCALE",58,"1/2"],["B","ADD",55,57,"-1"],["B","ADD",53,57,"-1"],["B","ADD",51,57,"-1"],["B","ADD",49,57,"-1"],["B","ADD",47,57,"-1"],["B","ADD",45,57,"-1"],["B","ADD",43,57,"-1"],["B","ADD",41,57,"128"],["B","ADD",40,57,"64"],["B","SCALE",57,"-1"],["B","ADD",59,57,"1"],["B","SWAP",57,58],["B","ADD",55,56,"1/2"],["B","ADD",53,56,"1/2"],["B","ADD",51,56,"1/2"],["B","ADD",49,56,"1/2"],["B","ADD",47,56,"1/2"],["B","ADD",45,56,"1/2"],["B","ADD",43,56,"1/2"],["B","ADD",41,56,"-64"],["B","ADD",40,56,"-32"],["B","ADD",59,56,"1/2"],["B","ADD",58,56,"1/2"],["B","ADD",57,56,"1/2"],["B","ADD",53,54,"-1/2"],["B","ADD",51,54,"-1/2"],["B","ADD",49,54,"-1/2"],["B","ADD",47,54,"-1/2"],["B","ADD",45,54,"-1/2"],["B","ADD",43,54,"-1/2"],["B","ADD",41,54,"64"],["B","ADD",40,54,"32"],["B","ADD",59,54,"-1/2"],["B","ADD",58,54,"-1/2"],["B","ADD",57,54,"-1/2"],["B","ADD",55,54,"-1/2"],["B","ADD",51,53,"-1"],["B","ADD",49,53,"-2"],["B","ADD",47,53,"-1"],["B","ADD",45,53,"-1"],["B","ADD",43,53,"-1"],["B","ADD",41,53,"128"],["B","ADD",40,53,"64"],["B","ADD",59,53,"-1"],["B","ADD",58,53,"-1"],["B","ADD",57,53,"-1"],["B","ADD",55,53,"-1"],["B","ADD",49,52,"1/2"],["B","ADD",53,52,"-1/2"],["B","ADD",49,51,"-1"],["B","ADD",47,51,"-1"],["B","ADD",45,51,"-1"],["B","ADD",43,51,"-1"],["B","ADD",41,51,"128"],["B","ADD",40,51,"64"],["B","SCALE",51,"-1"],["B","ADD",59,51,"1"],["B","ADD",58,51,"1"],["B","ADD",57,51,"1"],["B","ADD",55,51,"1"],["B","SWAP",51,53],["B","ADD",49,50,"-1/2"],["B","ADD",51,50,"1/2"],["B","ADD",47,49,"-1"],["B","ADD",45,49,"-1"],["B","ADD",43,49,"-1"],["B","ADD",41,49,"128"],["B","ADD",40,49,"64"],["B","SCALE",49,"-1"],["B","ADD",59,49,"1"],["B","ADD",58,49,"1"],["B","ADD",57,49,"1"],["B","ADD",55,49,"1"],["B","ADD",53,49,"1"],["B","SWAP",49,51],["B","ADD",47,48,"1/2"],["B","ADD",45,48,"1/2"],["B","ADD",43,48,"1/2"],["B","ADD",41,48,"-64"],["B","ADD",40,48,"-32"],["B","ADD",59,48,"1/2"],["B","ADD",58,48,"1/2"],["B","ADD",57,48,"1/2"],["B","ADD",55,48,"1/2"],["B","ADD",53,48,"1/2"],["B","ADD",51,48,"1/2"],["B","ADD",49,48,"1/2"],["B","ADD",45,46,"-1/2"],["B","ADD",43,46,"-1/2"],["B","ADD",41,46,"64"],["B","ADD",40,46,"32"],["B","ADD",59,46,"-1/2"],["B","ADD",58,46,"-1/2"],["B","ADD",57,46,"-1/2"],["B","ADD",55,46,"-1/2"],["B","ADD",53,46,"-1/2"],["B","ADD",51,46,"-1/2"],["B","ADD",49,46,"-1/2"],["B","ADD",47,46,"-1/2"],["B","ADD",43,45,"-1"],["B","ADD",41,45,"128"],["B","ADD",40,45,"64"],["B","SCALE",45,"2"],["B","ADD",59,45,"-1/2"],["B","ADD",58,45,"-1/2"],["B","ADD",57,45,"-1/2"],["B","ADD",55,45,"-1/2"],["B","ADD",53,45,"-1/2"],["B","ADD",51,45,"-1/2"],["B","ADD",49,45,"-1/2"],["B","ADD",47,45,"-1/2"],["B","ADD",45,44,"-1"],["B","ADD",41,43,"128"],["B","ADD",40,43,"64"],["B","SCALE",43,"-1"],["B","ADD",59,43,"1"],["B","ADD",58,43,"1"],["B","ADD",57,43,"1"],["B","ADD",55,43,"1"],["B","ADD",53,43,"1"],["B","ADD",51,43,"1"],["B","ADD",49,43,"1"],["B","ADD",47,43,"1"],["B","SWAP",43,45],["B","ADD",43,42,"1"],["B","ADD",40,41,"-1/2"],["B","SCALE",41,"1/128"],["B","ADD",59,41,"1"],["B","ADD",58,41,"1"],["B","ADD",57,41,"1"],["B","ADD",55,41,"1"],["B","ADD",53,41,"1"],["B","ADD",51,41,"1"],["B","ADD",49,41,"1"],["B","ADD",47,41,"1"],["B","ADD",45,41,"1"],["B","SWAP",41,43],["B","SCALE",40,"1/128"],["B","ADD",59,40,"2"],["B","ADD",58,40,"2"],["B","ADD",57,40,"1"],["B","ADD",55,40,"1"],["B","ADD",53,40,"1"],["B","ADD",51,40,"1"],["B","ADD",49,40,"1"],["B","ADD",47,40,"1"],["B","ADD",45,40,"1"],["B","ADD",43,40,"1"],["B","ADD",41,40,"1"],["B","LAMBDA",40,-1],["B","QUERY",40,41,-1],["B","LAMBDA",40,1],["B","ADD",40,41,"-1"],["B","ADD",41,77,"-1"],["B","ADD",41,75,"1"],["B","ADD",41,74,"-2"],["B","ADD",41,73,"1"],["B","ADD",41,71,"-1"],["B","ADD",41,70,"2"],["B","ADD",41,69,"-1"],["B","ADD",41,67,"1"],["B","ADD",41,66,"-2"],["B","ADD",41,65,"1"],["B","ADD",41,63,"-1"],["B","ADD",41,62,"2"],["B","ADD",41,61,"-1"],["B","ADD",41,58,"-1"],["B","ADD",41,57,"2"],["B","ADD",41,56,"-1"],["B","ADD",41,54,"1"],["B","ADD",41,53,"-2"],["B","ADD",41,52,"1"],["B","ADD",41,50,"-1"],["B","ADD",41,49,"2"],["B","ADD",41,48,"-1"],["B","ADD",41,46,"1"],["B","ADD",41,45,"-2"],["B","ADD",41,44,"1"],["B","ADD",41,42,"-1"],["B","ADD",40,41,"-1"],["B","ADD",59,41,"-1"],["B","ADD",58,41,"-2"],["B","ADD",57,41,"-1"],["B","ADD",56,41,"-2"],["B","ADD",55,41,"-1"],["B","ADD",54,41,"-2"],["B","ADD",53,41,"-1"],["B","ADD",52,41,"-2"],["B","ADD",51,41,"-1"],["B","ADD",50,41,"-2"],["B","ADD",49,41,"-1"],["B","ADD",48,41,"-2"],["B","ADD",47,41,"-1"],["B","ADD",46,41,"-2"],["B","ADD",45,41,"-1"],["B","ADD",44,41,"-2"],["B","ADD",43,41,"-1"],["B","ADD",42,41,"-2"],["B","SCALE",40,"1/2"],["B","ADD",76,40,"-1"],["B","ADD",74,40,"-1"],["B","ADD",72,40,"-1"],["B","ADD",70,40,"-1"],["B","ADD",68,40,"-1"],["B","ADD",66,40,"-1"],["B","ADD",64,40,"-1"],["B","ADD",62,40,"-1"],["B","ADD",60,40,"-1"],["B","ADD",59,40,"-1"],["B","ADD",58,40,"-2"],["B","ADD",57,40,"-1"],["B","ADD",56,40,"-2"],["B","ADD",55,40,"-1"],["B","ADD",54,40,"-2"],["B","ADD",53,40,"-1"],["B","ADD",52,40,"-2"],["B","ADD",51,40,"-1"],["B","ADD",50,40,"-2"],["B","ADD",49,40,"-1"],["B","ADD",48,40,"-2"],["B","ADD",47,40,"-1"],["B","ADD",46,40,"-2"],["B","ADD",45,40,"-1"],["B","ADD",44,40,"-2"],["B","ADD",43,40,"-1"],["B","ADD",42,40,"-2"],["B","ADD",41,40,"1"],["B","LAMBDA",40,-1],["B","QUERY",40,41,-1],["B","LAMBDA",40,1],["B","ADD",40,41,"-1"],["B","SCALE",40,"2"],["B","ADD",77,40,"-1"],["B","ADD",76,40,"-1/2"],["B","ADD",75,40,"-1"],["B","ADD",74,40,"-1/2"],["B","ADD",73,40,"-1"],["B","ADD",72,40,"-1/2"],["B","ADD",71,40,"-1"],["B","ADD",70,40,"-1/2"],["B","ADD",69,40,"-1"],["B","ADD",68,40,"-1/2"],["B","ADD",67,40,"-1"],["B","ADD",66,40,"-1/2"],["B","ADD",65,40,"-1"],["B","ADD",64,40,"-1/2"],["B","ADD",63,40,"-1"],["B","ADD",62,40,"-1/2"],["B","ADD",61,40,"-1"],["B","ADD",60,40,"-1/2"],["B","ADD",59,40,"-1/2"],["B","ADD",57,40,"-1/2"],["B","ADD",55,40,"-1/2"],["B","ADD",53,40,"-1/2"],["B","ADD",51,40,"-1/2"],["B","ADD",49,40,"-1/2"],["B","ADD",47,40,"-1/2"],["B","ADD",45,40,"-1/2"],["B","ADD",43,40,"-1/2"],["B","ADD",41,40,"1/2"],["B","LAMBDA",40,-1],["B","QUERY",40,41,-1],["B","LAMBDA",40,1],["B","ADD",40,41,"-1"],["B","ADD",76,77,"-1/2"],["B","ADD",75,77,"-1"],["B","ADD",74,77,"-1"],["B","ADD",73,77,"-1"],["B","ADD",72,77,"-1"],["B","ADD",71,77,"-1"],["B","ADD",70,77,"-1"],["B","ADD",69,77,"-1"],["B","ADD",68,77,"-1"],["B","ADD",67,77,"-1"],["B","ADD",66,77,"-1"],["B","ADD",65,77,"-1"],["B","ADD",64,77,"-1"],["B","ADD",63,77,"-1"],["B","ADD",62,77,"-1"],["B","ADD",61,77,"-1"],["B","ADD",60,77,"-1"],["B","ADD",58,77,"1"],["B","ADD",56,77,"1"],["B","ADD",54,77,"1"],["B","ADD",52,77,"1"],["B","ADD",50,77,"1"],["B","ADD",48,77,"1"],["B","ADD",46,77,"1"],["B","ADD",44,77,"1"],["B","ADD",42,77,"1"],["B","ADD",40,77,"1"],["B","SCALE",77,"-1/2"],["B","ADD",75,76,"2"],["B","ADD",74,76,"2"],["B","ADD",73,76,"2"],["B","ADD",72,76,"2"],["B","ADD",71,76,"2"],["B","ADD",70,76,"2"],["B","ADD",69,76,"2"],["B","ADD",68,76,"2"],["B","ADD",67,76,"2"],["B","ADD",66,76,"2"],["B","ADD",65,76,"2"],["B","ADD",64,76,"2"],["B","ADD",63,76,"2"],["B","ADD",62,76,"2"],["B","ADD",61,76,"2"],["B","ADD",60,76,"2"],["B","ADD",58,76,"-2"],["B","ADD",56,76,"-2"],["B","ADD",54,76,"-2"],["B","ADD",52,76,"-2"],["B","ADD",50,76,"-2"],["B","ADD",48,76,"-2"],["B","ADD",46,76,"-2"],["B","ADD",44,76,"-2"],["B","ADD",42,76,"-2"],["B","ADD",40,76,"-2"],["B","SCALE",76,"2"],["B","ADD",77,76,"3/2"],["B","SWAP",76,77],["B","ADD",73,74,"-1/2"],["B","ADD",72,74,"-1"],["B","ADD",71,74,"-1"],["B","ADD",70,74,"-1"],["B","ADD",69,74,"-1"],["B","ADD",68,74,"-1"],["B","ADD",67,74,"-1"],["B","ADD",66,74,"-1"],["B","ADD",65,74,"-1"],["B","ADD",64,74,"-1"],["B","ADD",63,74,"-1"],["B","ADD",62,74,"-1"],["B","ADD",61,74,"-1"],["B","ADD",60,74,"-1"],["B","ADD",58,74,"1"],["B","ADD",56,74,"1"],["B","ADD",54,74,"1"],["B","ADD",52,74,"1"],["B","ADD",50,74,"1"],["B","ADD",48,74,"1"],["B","ADD",46,74,"1"],["B","ADD",44,74,"1"],["B","ADD",42,74,"1"],["B","ADD",40,74,"1"],["B","SCALE",74,"-1/2"],["B","ADD",77,74,"2"],["B","ADD",76,74,"2"],["B","ADD",75,74,"2"],["B","ADD",72,73,"2"],["B","ADD",71,73,"2"],["B","ADD",70,73,"2"],["B","ADD",69,73,"2"],["B","ADD",68,73,"2"],["B","ADD",67,73,"2"],["B","ADD",66,73,"2"],["B","ADD",65,73,"2"],["B","ADD",64,73,"2"],["B","ADD",63,73,"2"],["B","ADD",62,73,"2"],["B","ADD",61,73,"2"],["B","ADD",60,73,"2"],["B","ADD",58,73,"-2"],["B","ADD",56,73,"-2"],["B","ADD",54,73,"-2"],["B","ADD",52,73,"-2"],["B","ADD",50,73,"-2"],["B","ADD",48,73,"-2"],["B","ADD",46,73,"-2"],["B","ADD",44,73,"-2"],["B","ADD",42,73,"-2"],["B","ADD",40,73,"-2"],["B","SCALE",73,"2"],["B","ADD",77,73,"1"],["B","ADD",76,73,"1"],["B","ADD",75,73,"1"],["B","ADD",74,73,"3/2"],["B","SWAP",73,74],["B","ADD",71,72,"-1"],["B","ADD",70,72,"-1/2"],["B","ADD",69,72,"-1"],["B","ADD",68,72,"-1"],["B","ADD",67,72,"-1"],["B","ADD",66,72,"-1"],["B","ADD",65,72,"-1"],["B","ADD",64,72,"-1"],["B","ADD",63,72,"-1"],["B","ADD",62,72,"-1"],["B","ADD",61,72,"-1"],["B","ADD",60,72,"-1"],["B","ADD",58,72,"1"],["B","ADD",56,72,"1"],["B","ADD",54,72,"1"],["B","ADD",52,72,"1"],["B","ADD",50,72,"1"],["B","ADD",48,72,"1"],["B","ADD",46,72,"1"],["B","ADD",44,72,"1"],["B","ADD",42,72,"1"],["B","ADD",40,72,"1"],["B","SCALE",72,"-1/2"],["B","ADD",77,72,"2"],["B","ADD",76,72,"2"],["B","ADD",75,72,"2"],["B","ADD",74,72,"2"],["B","ADD",73,72,"2"],["B","ADD",70,71,"1/2"],["B","ADD",69,71,"-1"],["B","ADD",68,71,"-1"],["B","ADD",67,71,"-1"],["B","ADD",66,71,"-1"],["B","ADD",65,71,"-1"],["B","ADD",64,71,"-1"],["B","ADD",63,71,"-1"],["B","ADD",62,71,"-1"],["B","ADD",61,71,"-1"],["B","ADD",60,71,"-1"],["B","ADD",58,71,"1"],["B","ADD",56,71,"1"],["B","ADD",54,71,"1"],["B","ADD",52,71,"1"],["B","ADD",50,71,"1"],["B","ADD",48,71,"1"],["B","ADD",46,71,"1"],["B","ADD",44,71,"1"],["B","ADD",42,71,"1"],["B","ADD",40,71,"1"],["B","SCALE",71,"-1"],["B","ADD",77,71,"1"],["B","ADD",76,71,"1"],["B","ADD",75,71,"1"],["B","ADD",74,71,"1"],["B","ADD",73,71,"1"],["B","ADD",72,71,"3/2"],["B","SWAP",71,72],["B","ADD",69,70,"2"],["B","ADD",68,70,"2"],["B","ADD",67,70,"2"],["B","ADD",66,70,"2"],["B","ADD",65,70,"2"],["B","ADD",64,70,"2"],["B","ADD",63,70,"2"],["B","ADD",62,70,"2"],["B","ADD",61,70,"2"],["B","ADD",60,70,"2"],["B","ADD",58,70,"-2"],["B","ADD",56,70,"-2"],["B","ADD",54,70,"-2"],["B","ADD",52,70,"-2"],["B","ADD",50,70,"-2"],["B","ADD",48,70,"-2"],["B","ADD",46,70,"-2"],["B","ADD",44,70,"-2"],["B","ADD",42,70,"-2"],["B","ADD",40,70,"-2"],["B","SCALE",70,"2"],["B","ADD",77,70,"1"],["B","ADD",76,70,"1"],["B","ADD",75,70,"1"],["B","ADD",74,70,"1"],["B","ADD",73,70,"1"],["B","ADD",72,70,"1"],["B","ADD",71,70,"3/2"],["B","SWAP",70,71],["B","ADD",68,69,"-1/2"],["B","ADD",67,69,"-1"],["B","ADD",66,69,"-1"],["B","ADD",65,69,"-1"],["B","ADD",64,69,"-1"],["B","ADD",63,69,"-1"],["B","ADD",62,69,"-1"],["B","ADD",61,69,"-1"],["B","ADD",60,69,"-1"],["B","ADD",58,69,"1"],["B","ADD",56,69,"1"],["B","ADD",54,69,"1"],["B","ADD",52,69,"1"],["B","ADD",50,69,"1"],["B","ADD",48,69,"1"],["B","ADD",46,69,"1"],["B","ADD",44,69,"1"],["B","ADD",42,69,"1"],["B","ADD",40,69,"1"],["B","SCALE",69,"-1/2"],["B","ADD",77,69,"2"],["B","ADD",76,69,"2"],["B","ADD",75,69,"2"],["B","ADD",74,69,"2"],["B","ADD",73,69,"2"],["B","ADD",72,69,"2"],["B","ADD",71,69,"2"],["B","ADD",70,69,"2"],["B","ADD",67,68,"2"],["B","ADD",66,68,"2"],["B","ADD",65,68,"2"],["B","ADD",64,68,"2"],["B","ADD",63,68,"2"],["B","ADD",62,68,"2"],["B","ADD",61,68,"2"],["B","ADD",60,68,"2"],["B","ADD",58,68,"-2"],["B","ADD",56,68,"-2"],["B","ADD",54,68,"-2"],["B","ADD",52,68,"-2"],["B","ADD",50,68,"-2"],["B","ADD",48,68,"-2"],["B","ADD",46,68,"-2"],["B","ADD",44,68,"-2"],["B","ADD",42,68,"-2"],["B","ADD",40,68,"-2"],["B","SCALE",68,"2"],["B","ADD",77,68,"1"],["B","ADD",76,68,"1"],["B","ADD",75,68,"1"],["B","ADD",74,68,"1"],["B","ADD",73,68,"1"],["B","ADD",72,68,"1"],["B","ADD",71,68,"1"],["B","ADD",70,68,"1"],["B","ADD",69,68,"3/2"],["B","SWAP",68,69],["B","ADD",65,66,"-1/2"],["B","ADD",64,66,"-1"],["B","ADD",63,66,"-1"],["B","ADD",62,66,"-1"],["B","ADD",61,66,"-1"],["B","ADD",60,66,"-1"],["B","ADD",58,66,"1"],["B","ADD",56,66,"1"],["B","ADD",54,66,"1"],["B","ADD",52,66,"1"],["B","ADD",50,66,"1"],["B","ADD",48,66,"1"],["B","ADD",46,66,"1"],["B","ADD",44,66,"1"],["B","ADD",42,66,"1"],["B","ADD",40,66,"1"],["B","SCALE",66,"-1/2"],["B","ADD",77,66,"2"],["B","ADD",76,66,"2"],["B","ADD",75,66,"2"],["B","ADD",74,66,"2"],["B","ADD",73,66,"2"],["B","ADD",72,66,"2"],["B","ADD",71,66,"2"],["B","ADD",70,66,"2"],["B","ADD",69,66,"2"],["B","ADD",68,66,"2"],["B","ADD",67,66,"2"],["B","ADD",64,65,"2"],["B","ADD",63,65,"2"],["B","ADD",62,65,"2"],["B","ADD",61,65,"2"],["B","ADD",60,65,"2"],["B","ADD",58,65,"-2"],["B","ADD",56,65,"-2"],["B","ADD",54,65,"-2"],["B","ADD",52,65,"-2"],["B","ADD",50,65,"-2"],["B","ADD",48,65,"-2"],["B","ADD",46,65,"-2"],["B","ADD",44,65,"-2"],["B","ADD",42,65,"-2"],["B","ADD",40,65,"-2"],["B","SCALE",65,"2"],["B","ADD",77,65,"1"],["B","ADD",76,65,"1"],["B","ADD",75,65,"1"],["B","ADD",74,65,"1"],["B","ADD",73,65,"1"],["B","ADD",72,65,"1"],["B","ADD",71,65,"1"],["B","ADD",70,65,"1"],["B","ADD",69,65,"1"],["B","ADD",68,65,"1"],["B","ADD",67,65,"1"],["B","ADD",66,65,"3/2"],["B","SWAP",65,66],["B","ADD",63,64,"-1"],["B","ADD",62,64,"-1/2"],["B","ADD",61,64,"-1"],["B","ADD",60,64,"-1"],["B","ADD",58,64,"1"],["B","ADD",56,64,"1"],["B","ADD",54,64,"1"],["B","ADD",52,64,"1"],["B","ADD",50,64,"1"],["B","ADD",48,64,"1"],["B","ADD",46,64,"1"],["B","ADD",44,64,"1"],["B","ADD",42,64,"1"],["B","ADD",40,64,"1"],["B","SCALE",64,"-1/2"],["B","ADD",77,64,"2"],["B","ADD",76,64,"2"],["B","ADD",75,64,"2"],["B","ADD",74,64,"2"],["B","ADD",73,64,"2"],["B","ADD",72,64,"2"],["B","ADD",71,64,"2"],["B","ADD",70,64,"2"],["B","ADD",69,64,"2"],["B","ADD",68,64,"2"],["B","ADD",67,64,"2"],["B","ADD",66,64,"2"],["B","ADD",65,64,"2"],["B","ADD",62,63,"1/2"],["B","ADD",61,63,"-1"],["B","ADD",60,63,"-1"],["B","ADD",58,63,"1"],["B","ADD",56,63,"1"],["B","ADD",54,63,"1"],["B","ADD",52,63,"1"],["B","ADD",50,63,"1"],["B","ADD",48,63,"1"],["B","ADD",46,63,"1"],["B","ADD",44,63,"1"],["B","ADD",42,63,"1"],["B","ADD",40,63,"1"],["B","SCALE",63,"-1"],["B","ADD",77,63,"1"],["B","ADD",76,63,"1"],["B","ADD",75,63,"1"],["B","ADD",74,63,"1"],["B","ADD",73,63,"1"],["B","ADD",72,63,"1"],["B","ADD",71,63,"1"],["B","ADD",70,63,"1"],["B","ADD",69,63,"1"],["B","ADD",68,63,"1"],["B","ADD",67,63,"1"],["B","ADD",66,63,"1"],["B","ADD",65,63,"1"],["B","ADD",64,63,"3/2"],["B","SWAP",63,64],["B","ADD",61,62,"2"],["B","ADD",60,62,"2"],["B","ADD",58,62,"-2"],["B","ADD",56,62,"-2"],["B","ADD",54,62,"-2"],["B","ADD",52,62,"-2"],["B","ADD",50,62,"-2"],["B","ADD",48,62,"-2"],["B","ADD",46,62,"-2"],["B","ADD",44,62,"-2"],["B","ADD",42,62,"-2"],["B","ADD",40,62,"-2"],["B","SCALE",62,"2"],["B","ADD",77,62,"1"],["B","ADD",76,62,"1"],["B","ADD",75,62,"1"],["B","ADD",74,62,"1"],["B","ADD",73,62,"1"],["B","ADD",72,62,"1"],["B","ADD",71,62,"1"],["B","ADD",70,62,"1"],["B","ADD",69,62,"1"],["B","ADD",68,62,"1"],["B","ADD",67,62,"1"],["B","ADD",66,62,"1"],["B","ADD",65,62,"1"],["B","ADD",64,62,"1"],["B","ADD",63,62,"3/2"],["B","SWAP",62,63],["B","ADD",60,61,"-1/2"],["B","ADD",58,61,"1"],["B","ADD",56,61,"1"],["B","ADD",54,61,"1"],["B","ADD",52,61,"1"],["B","ADD",50,61,"1"],["B","ADD",48,61,"1"],["B","ADD",46,61,"1"],["B","ADD",44,61,"1"],["B","ADD",42,61,"1"],["B","ADD",40,61,"1"],["B","SCALE",61,"-1/2"],["B","ADD",77,61,"2"],["B","ADD",76,61,"2"],["B","ADD",75,61,"2"],["B","ADD",74,61,"2"],["B","ADD",73,61,"2"],["B","ADD",72,61,"2"],["B","ADD",71,61,"2"],["B","ADD",70,61,"2"],["B","ADD",69,61,"2"],["B","ADD",68,61,"2"],["B","ADD",67,61,"2"],["B","ADD",66,61,"2"],["B","ADD",65,61,"2"],["B","ADD",64,61,"2"],["B","ADD",63,61,"2"],["B","ADD",62,61,"2"],["B","ADD",58,60,"-2"],["B","ADD",56,60,"-2"],["B","ADD",54,60,"-2"],["B","ADD",52,60,"-2"],["B","ADD",50,60,"-2"],["B","ADD",48,60,"-2"],["B","ADD",46,60,"-2"],["B","ADD",44,60,"-2"],["B","ADD",42,60,"-2"],["B","ADD",40,60,"-2"],["B","SCALE",60,"2"],["B","ADD",77,60,"1"],["B","ADD",76,60,"1"],["B","ADD",75,60,"1"],["B","ADD",74,60,"1"],["B","ADD",73,60,"1"],["B","ADD",72,60,"1"],["B","ADD",71,60,"1"],["B","ADD",70,60,"1"],["B","ADD",69,60,"1"],["B","ADD",68,60,"1"],["B","ADD",67,60,"1"],["B","ADD",66,60,"1"],["B","ADD",65,60,"1"],["B","ADD",64,60,"1"],["B","ADD",63,60,"1"],["B","ADD",62,60,"1"],["B","ADD",61,60,"3/2"],["B","SWAP",60,61],["B","ADD",58,59,"-2"],["B","ADD",56,59,"-2"],["B","ADD",54,59,"-2"],["B","ADD",52,59,"-2"],["B","ADD",50,59,"-2"],["B","ADD",48,59,"-2"],["B","ADD",46,59,"-2"],["B","ADD",44,59,"-2"],["B","ADD",42,59,"-2"],["B","ADD",40,59,"-2"],["B","ADD",77,59,"2"],["B","ADD",76,59,"2"],["B","ADD",75,59,"2"],["B","ADD",74,59,"2"],["B","ADD",73,59,"2"],["B","ADD",72,59,"2"],["B","ADD",71,59,"2"],["B","ADD",70,59,"2"],["B","ADD",69,59,"2"],["B","ADD",68,59,"2"],["B","ADD",67,59,"2"],["B","ADD",66,59,"2"],["B","ADD",65,59,"2"],["B","ADD",64,59,"2"],["B","ADD",63,59,"2"],["B","ADD",62,59,"2"],["B","ADD",61,59,"2"],["B","ADD",60,59,"2"],["B","ADD",56,58,"-2"],["B","ADD",54,58,"-2"],["B","ADD",52,58,"-2"],["B","ADD",50,58,"-2"],["B","ADD",48,58,"-2"],["B","ADD",46,58,"-2"],["B","ADD",44,58,"-2"],["B","ADD",42,58,"-2"],["B","ADD",40,58,"-2"],["B","SCALE",58,"-1"],["B","ADD",77,58,"-2"],["B","ADD",76,58,"-2"],["B","ADD",75,58,"-2"],["B","ADD",74,58,"-2"],["B","ADD",73,58,"-2"],["B","ADD",72,58,"-2"],["B","ADD",71,58,"-2"],["B","ADD",70,58,"-2"],["B","ADD",69,58,"-2"],["B","ADD",68,58,"-2"],["B","ADD",67,58,"-2"],["B","ADD",66,58,"-2"],["B","ADD",65,58,"-2"],["B","ADD",64,58,"-2"],["B","ADD",63,58,"-2"],["B","ADD",62,58,"-2"],["B","ADD",61,58,"-2"],["B","ADD",60,58,"-2"],["B","ADD",56,57,"2"],["B","ADD",54,57,"2"],["B","ADD",52,57,"2"],["B","ADD",50,57,"2"],["B","ADD",48,57,"2"],["B","ADD",46,57,"2"],["B","ADD",44,57,"2"],["B","ADD",42,57,"2"],["B","ADD",40,57,"2"],["B","ADD",77,57,"-2"],["B","ADD",76,57,"-2"],["B","ADD",75,57,"-2"],["B","ADD",74,57,"-2"],["B","ADD",73,57,"-2"],["B","ADD",72,57,"-2"],["B","ADD",71,57,"-2"],["B","ADD",70,57,"-2"],["B","ADD",69,57,"-2"],["B","ADD",68,57,"-2"],["B","ADD",67,57,"-2"],["B","ADD",66,57,"-2"],["B","ADD",65,57,"-2"],["B","ADD",64,57,"-2"],["B","ADD",63,57,"-2"],["B","ADD",62,57,"-2"],["B","ADD",61,57,"-2"],["B","ADD",60,57,"-2"],["B","ADD",58,57,"2"],["B","ADD",54,55,"-2"],["B","ADD",52,55,"-2"],["B","ADD",50,55,"-2"],["B","ADD",48,55,"-2"],["B","ADD",46,55,"-2"],["B","ADD",44,55,"-2"],["B","ADD",42,55,"-2"],["B","ADD",40,55,"-2"],["B","ADD",77,55,"2"],["B","ADD",76,55,"2"],["B","ADD",75,55,"2"],["B","ADD",74,55,"2"],["B","ADD",73,55,"2"],["B","ADD",72,55,"2"],["B","ADD",71,55,"2"],["B","ADD",70,55,"2"],["B","ADD",69,55,"2"],["B","ADD",68,55,"2"],["B","ADD",67,55,"2"],["B","ADD",66,55,"2"],["B","ADD",65,55,"2"],["B","ADD",64,55,"2"],["B","ADD",63,55,"2"],["B","ADD",62,55,"2"],["B","ADD",61,55,"2"],["B","ADD",60,55,"2"],["B","ADD",58,55,"-2"],["B","ADD",56,55,"-2"],["B","ADD",52,54,"-2"],["B","ADD",50,54,"-2"],["B","ADD",48,54,"-2"],["B","ADD",46,54,"-2"],["B","ADD",44,54,"-2"],["B","ADD",42,54,"-2"],["B","ADD",40,54,"-2"],["B","SCALE",54,"-1"],["B","ADD",77,54,"-2"],["B","ADD",76,54,"-2"],["B","ADD",75,54,"-2"],["B","ADD",74,54,"-2"],["B","ADD",73,54,"-2"],["B","ADD",72,54,"-2"],["B","ADD",71,54,"-2"],["B","ADD",70,54,"-2"],["B","ADD",69,54,"-2"],["B","ADD",68,54,"-2"],["B","ADD",67,54,"-2"],["B","ADD",66,54,"-2"],["B","ADD",65,54,"-2"],["B","ADD",64,54,"-2"],["B","ADD",63,54,"-2"],["B","ADD",62,54,"-2"],["B","ADD",61,54,"-2"],["B","ADD",60,54,"-2"],["B","ADD",58,54,"2"],["B","ADD",56,54,"2"],["B","ADD",52,53,"2"],["B","ADD",50,53,"2"],["B","ADD",48,53,"2"],["B","ADD",46,53,"2"],["B","ADD",44,53,"2"],["B","ADD",42,53,"2"],["B","ADD",40,53,"2"],["B","ADD",77,53,"-2"],["B","ADD",76,53,"-2"],["B","ADD",75,53,"-2"],["B","ADD",74,53,"-2"],["B","ADD",73,53,"-2"],["B","ADD",72,53,"-2"],["B","ADD",71,53,"-2"],["B","ADD",70,53,"-2"],["B","ADD",69,53,"-2"],["B","ADD",68,53,"-2"],["B","ADD",67,53,"-2"],["B","ADD",66,53,"-2"],["B","ADD",65,53,"-2"],["B","ADD",64,53,"-2"],["B","ADD",63,53,"-2"],["B","ADD",62,53,"-2"],["B","ADD",61,53,"-2"],["B","ADD",60,53,"-2"],["B","ADD",58,53,"2"],["B","ADD",56,53,"2"],["B","ADD",54,53,"2"],["B","ADD",50,51,"-2"],["B","ADD",48,51,"-2"],["B","ADD",46,51,"-2"],["B","ADD",44,51,"-2"],["B","ADD",42,51,"-2"],["B","ADD",40,51,"-2"],["B","ADD",77,51,"2"],["B","ADD",76,51,"2"],["B","ADD",75,51,"2"],["B","ADD",74,51,"2"],["B","ADD",73,51,"2"],["B","ADD",72,51,"2"],["B","ADD",71,51,"2"],["B","ADD",70,51,"2"],["B","ADD",69,51,"2"],["B","ADD",68,51,"2"],["B","ADD",67,51,"2"],["B","ADD",66,51,"2"],["B","ADD",65,51,"2"],["B","ADD",64,51,"2"],["B","ADD",63,51,"2"],["B","ADD",62,51,"2"],["B","ADD",61,51,"2"],["B","ADD",60,51,"2"],["B","ADD",58,51,"-2"],["B","ADD",56,51,"-2"],["B","ADD",54,51,"-2"],["B","ADD",52,51,"-2"],["B","ADD",48,50,"-2"],["B","ADD",46,50,"-2"],["B","ADD",44,50,"-2"],["B","ADD",42,50,"-2"],["B","ADD",40,50,"-2"],["B","SCALE",50,"-1"],["B","ADD",77,50,"-2"],["B","ADD",76,50,"-2"],["B","ADD",75,50,"-2"],["B","ADD",74,50,"-2"],["B","ADD",73,50,"-2"],["B","ADD",72,50,"-2"],["B","ADD",71,50,"-2"],["B","ADD",70,50,"-2"],["B","ADD",69,50,"-2"],["B","ADD",68,50,"-2"],["B","ADD",67,50,"-2"],["B","ADD",66,50,"-2"],["B","ADD",65,50,"-2"],["B","ADD",64,50,"-2"],["B","ADD",63,50,"-2"],["B","ADD",62,50,"-2"],["B","ADD",61,50,"-2"],["B","ADD",60,50,"-2"],["B","ADD",58,50,"2"],["B","ADD",56,50,"2"],["B","ADD",54,50,"2"],["B","ADD",52,50,"2"],["B","ADD",48,49,"2"],["B","ADD",46,49,"2"],["B","ADD",44,49,"2"],["B","ADD",42,49,"2"],["B","ADD",40,49,"2"],["B","ADD",77,49,"-2"],["B","ADD",76,49,"-2"],["B","ADD",75,49,"-2"],["B","ADD",74,49,"-2"],["B","ADD",73,49,"-2"],["B","ADD",72,49,"-2"],["B","ADD",71,49,"-2"],["B","ADD",70,49,"-2"],["B","ADD",69,49,"-2"],["B","ADD",68,49,"-2"],["B","ADD",67,49,"-2"],["B","ADD",66,49,"-2"],["B","ADD",65,49,"-2"],["B","ADD",64,49,"-2"],["B","ADD",63,49,"-2"],["B","ADD",62,49,"-2"],["B","ADD",61,49,"-2"],["B","ADD",60,49,"-2"],["B","ADD",58,49,"2"],["B","ADD",56,49,"2"],["B","ADD",54,49,"2"],["B","ADD",52,49,"2"],["B","ADD",50,49,"2"],["B","ADD",46,47,"-2"],["B","ADD",44,47,"-2"],["B","ADD",42,47,"-2"],["B","ADD",40,47,"-2"],["B","ADD",77,47,"2"],["B","ADD",76,47,"2"],["B","ADD",75,47,"2"],["B","ADD",74,47,"2"],["B","ADD",73,47,"2"],["B","ADD",72,47,"2"],["B","ADD",71,47,"2"],["B","ADD",70,47,"2"],["B","ADD",69,47,"2"],["B","ADD",68,47,"2"],["B","ADD",67,47,"2"],["B","ADD",66,47,"2"],["B","ADD",65,47,"2"],["B","ADD",64,47,"2"],["B","ADD",63,47,"2"],["B","ADD",62,47,"2"],["B","ADD",61,47,"2"],["B","ADD",60,47,"2"],["B","ADD",58,47,"-2"],["B","ADD",56,47,"-2"],["B","ADD",54,47,"-2"],["B","ADD",52,47,"-2"],["B","ADD",50,47,"-2"],["B","ADD",48,47,"-2"],["B","ADD",44,46,"-2"],["B","ADD",42,46,"-2"],["B","ADD",40,46,"-2"],["B","SCALE",46,"-1"],["B","ADD",77,46,"-2"],["B","ADD",76,46,"-2"],["B","ADD",75,46,"-2"],["B","ADD",74,46,"-2"],["B","ADD",73,46,"-2"],["B","ADD",72,46,"-2"],["B","ADD",71,46,"-2"],["B","ADD",70,46,"-2"],["B","ADD",69,46,"-2"],["B","ADD",68,46,"-2"],["B","ADD",67,46,"-2"],["B","ADD",66,46,"-2"],["B","ADD",65,46,"-2"],["B","ADD",64,46,"-2"],["B","ADD",63,46,"-2"],["B","ADD",62,46,"-2"],["B","ADD",61,46,"-2"],["B","ADD",60,46,"-2"],["B","ADD",58,46,"2"],["B","ADD",56,46,"2"],["B","ADD",54,46,"2"],["B","ADD",52,46,"2"],["B","ADD",50,46,"2"],["B","ADD",48,46,"2"],["B","ADD",44,45,"2"],["B","ADD",42,45,"2"],["B","ADD",40,45,"2"],["B","ADD",77,45,"-2"],["B","ADD",76,45,"-2"],["B","ADD",75,45,"-2"],["B","ADD",74,45,"-2"],["B","ADD",73,45,"-2"],["B","ADD",72,45,"-2"],["B","ADD",71,45,"-2"],["B","ADD",70,45,"-2"],["B","ADD",69,45,"-2"],["B","ADD",68,45,"-2"],["B","ADD",67,45,"-2"],["B","ADD",66,45,"-2"],["B","ADD",65,45,"-2"],["B","ADD",64,45,"-2"],["B","ADD",63,45,"-2"],["B","ADD",62,45,"-2"],["B","ADD",61,45,"-2"],["B","ADD",60,45,"-2"],["B","ADD",58,45,"2"],["B","ADD",56,45,"2"],["B","ADD",54,45,"2"],["B","ADD",52,45,"2"],["B","ADD",50,45,"2"],["B","ADD",48,45,"2"],["B","ADD",46,45,"2"],["B","ADD",42,43,"-2"],["B","ADD",40,43,"-2"],["B","ADD",77,43,"2"],["B","ADD",76,43,"2"],["B","ADD",75,43,"2"],["B","ADD",74,43,"2"],["B","ADD",73,43,"2"],["B","ADD",72,43,"2"],["B","ADD",71,43,"2"],["B","ADD",70,43,"2"],["B","ADD",69,43,"2"],["B","ADD",68,43,"2"],["B","ADD",67,43,"2"],["B","ADD",66,43,"2"],["B","ADD",65,43,"2"],["B","ADD",64,43,"2"],["B","ADD",63,43,"2"],["B","ADD",62,43,"2"],["B","ADD",61,43,"2"],["B","ADD",60,43,"2"],["B","ADD",58,43,"-2"],["B","ADD",56,43,"-2"],["B","ADD",54,43,"-2"],["B","ADD",52,43,"-2"],["B","ADD",50,43,"-2"],["B","ADD",48,43,"-2"],["B","ADD",46,43,"-2"],["B","ADD",44,43,"-2"],["B","ADD",40,42,"-2"],["B","SCALE",42,"-1"],["B","ADD",77,42,"-2"],["B","ADD",76,42,"-2"],["B","ADD",75,42,"-2"],["B","ADD",74,42,"-2"],["B","ADD",73,42,"-2"],["B","ADD",72,42,"-2"],["B","ADD",71,42,"-2"],["B","ADD",70,42,"-2"],["B","ADD",69,42,"-2"],["B","ADD",68,42,"-2"],["B","ADD",67,42,"-2"],["B","ADD",66,42,"-2"],["B","ADD",65,42,"-2"],["B","ADD",64,42,"-2"],["B","ADD",63,42,"-2"],["B","ADD",62,42,"-2"],["B","ADD",61,42,"-2"],["B","ADD",60,42,"-2"],["B","ADD",58,42,"2"],["B","ADD",56,42,"2"],["B","ADD",54,42,"2"],["B","ADD",52,42,"2"],["B","ADD",50,42,"2"],["B","ADD",48,42,"2"],["B","ADD",46,42,"2"],["B","ADD",44,42,"2"],["B","SCALE",41,"-1"],["B","ADD",77,41,"-2"],["B","ADD",76,41,"-2"],["B","ADD",75,41,"-2"],["B","ADD",74,41,"-2"],["B","ADD",73,41,"-2"],["B","ADD",72,41,"-2"],["B","ADD",71,41,"-2"],["B","ADD",70,41,"-2"],["B","ADD",69,41,"-2"],["B","ADD",68,41,"-2"],["B","ADD",67,41,"-2"],["B","ADD",66,41,"-2"],["B","ADD",65,41,"-2"],["B","ADD",64,41,"-2"],["B","ADD",63,41,"-2"],["B","ADD",62,41,"-2"],["B","ADD",61,41,"-2"],["B","ADD",60,41,"-2"],["B","SCALE",40,"1/2"],["B","ADD",77,40,"2"],["B","ADD",76,40,"2"],["B","ADD",75,40,"2"],["B","ADD",74,40,"2"],["B","ADD",73,40,"2"],["B","ADD",72,40,"2"],["B","ADD",71,40,"2"],["B","ADD",70,40,"2"],["B","ADD",69,40,"2"],["B","ADD",68,40,"2"],["B","ADD",67,40,"2"],["B","ADD",66,40,"2"],["B","ADD",65,40,"2"],["B","ADD",64,40,"2"],["B","ADD",63,40,"2"],["B","ADD",62,40,"2"],["B","ADD",61,40,"2"],["B","ADD",60,40,"2"],["B","ADD",58,40,"-2"],["B","ADD",56,40,"-2"],["B","ADD",54,40,"-2"],["B","ADD",52,40,"-2"],["B","ADD",50,40,"-2"],["B","ADD",48,40,"-2"],["B","ADD",46,40,"-2"],["B","ADD",44,40,"-2"],["B","ADD",42,40,"-2"],["B","SWAP",40,41],["B","LAMBDA",40,-1],["B","QUERY",40,41,-1],["B","LAMBDA",40,1],["B","ADD",40,41,"-1"],["B","ADD",41,77,"1"],["B","ADD",74,76,"-1"],["B","ADD",72,76,"-1"],["B","ADD",70,76,"-1"],["B","ADD",68,76,"-1"],["B","ADD",66,76,"-1"],["B","ADD",64,76,"-1"],["B","ADD",60,76,"-1/2"],["B","ADD",41,76,"1"],["B","SWAP",75,77],["B","ADD",41,74,"1"],["B","SWAP",74,76],["B","ADD",41,73,"-1"],["B","ADD",41,72,"1"],["B","ADD",41,70,"-1"],["B","ADD",41,69,"1"],["B","ADD",41,68,"-1"],["B","SWAP",67,71],["B","ADD",41,66,"1"],["B","SWAP",66,70],["B","ADD",41,65,"-1"],["B","SWAP",65,73],["B","ADD",41,64,"1"],["B","SWAP",64,72],["B","SWAP",63,77],["B","ADD",41,62,"-1"],["B","SWAP",62,76],["B","ADD",60,61,"-1"],["B","ADD",40,61,"1"],["B","SCALE",61,"-2"],["B","ADD",77,61,"1"],["B","ADD",76,61,"1"],["B","SWAP",61,75],["B","SCALE",60,"-2"],["B","ADD",74,60,"-1"],["B","ADD",72,60,"1"],["B","ADD",70,60,"1"],["B","ADD",68,60,"1"],["B","ADD",66,60,"1"],["B","ADD",64,60,"1"],["B","ADD",62,60,"1"],["B","ADD",41,59,"-1"],["B","ADD",41,58,"1"],["B","ADD",41,57,"-1"],["B","ADD",41,55,"1"],["B","ADD",41,54,"-1"],["B","ADD",41,53,"1"],["B","ADD",41,51,"-1"],["B","ADD",41,50,"1"],["B","ADD",41,49,"-1"],["B","ADD",41,47,"1"],["B","ADD",41,46,"-1"],["B","ADD",41,45,"1"],["B","ADD",41,43,"-1"],["B","ADD",41,42,"1"],["B","ADD",40,41,"1"],["B","SCALE",41,"-128"],["B","ADD",74,41,"1/64"],["B","ADD",72,41,"-1/64"],["B","ADD",70,41,"-1/64"],["B","ADD",68,41,"-1/64"],["B","ADD",66,41,"-1/64"],["B","ADD",64,41,"-1/64"],["B","ADD",62,41,"-1/64"],["B","ADD",60,41,"-1/64"],["B","SCALE",40,"128"],["B","ADD",77,40,"1/32"],["B","ADD",76,40,"1/64"],["B","ADD",75,40,"1/32"],["B","ADD",74,40,"-1/64"],["B","SWAP",40,41],["B","LAMBDA",40,-1],["J",10,[1,0,20,21],[41,40,"-1","1/2"]],["A","LAMBDA",20,-1],["A","SCALE",21,"-1"],["A","LAMBDA",0,1],["A","ADD",0,1,"-1"],["A","IDLE_ONE",2,[10]],["A","IDLE_ONE",3,[10,11]],["A","IDLE_ONE",4,[10,11,12]],["A","IDLE_ONE",5,[10,11,12,13]],["A","IDLE_ONE",6,[10,11,12,13,14]],["A","IDLE_ONE",7,[10,11,12,13,14,15]],["A","IDLE_ONE",8,[10,11,12,13,14,15,16]],["A","IDLE_ONE",9,[10,11,12,13,14,15,16,17]],["A","SWAP",17,18],["A","SWAP",16,18],["A","SWAP",15,18],["A","SWAP",14,18],["A","SWAP",13,18],["A","SWAP",12,18],["A","SWAP",11,18],["A","SWAP",10,18],["A","SWAP",9,18],["A","SWAP",8,18],["A","SWAP",7,18],["A","SWAP",6,18],["A","SWAP",5,18],["A","SWAP",4,18],["A","SWAP",3,18],["A","ADD",1,2,"-1"],["A","SCALE",2,"-1"],["A","SWAP",2,18],["A","SCALE",1,"-1"],["A","ADD",18,1,"2"],["A","ADD",18,0,"2"],["A","ADD",1,0,"1"],["A","SWAP",0,18],["A","LAMBDA",0,-1],["A","ADD",20,21,"-1"],["A","IDLE_ONE",22,[10]],["A","IDLE_ONE",23,[10,11]],["A","IDLE_ONE",24,[10,11,12]],["A","IDLE_ONE",25,[10,11,12,13]],["A","IDLE_ONE",26,[10,11,12,13,14]],["A","IDLE_ONE",27,[10,11,12,13,14,15]],["A","IDLE_ONE",28,[10,11,12,13,14,15,16]],["A","IDLE_ONE",29,[10,11,12,13,14,15,16,17]],["A","SWAP",37,38],["A","SWAP",36,38],["A","SWAP",35,38],["A","SWAP",34,38],["A","SWAP",33,38],["A","SWAP",32,38],["A","SWAP",31,38],["A","SWAP",30,38],["A","SWAP",29,38],["A","SWAP",28,38],["A","SWAP",27,38],["A","SWAP",26,38],["A","SWAP",25,38],["A","SWAP",24,38],["A","SWAP",23,38],["A","ADD",21,22,"-1"],["A","SCALE",22,"-1"],["A","SWAP",22,38],["A","ADD",38,21,"-2"],["A","ADD",38,20,"2"],["A","ADD",21,20,"-1"],["A","SWAP",20,38],["A","LAMBDA",20,1],["B","LAMBDA",40,1],["B","IDLE_ONE",60,[10,11,12,13,14,15,16,17]],["B","IDLE_ONE",61,[10,11,12,13,14,15,16,17]],["B","IDLE_ONE",62,[10,11,12,13,14,15,16]],["B","IDLE_ONE",63,[10,11,12,13,14,15,16]],["B","IDLE_ONE",64,[10,11,12,13,14,15]],["B","IDLE_ONE",65,[10,11,12,13,14,15]],["B","IDLE_ONE",66,[10,11,12,13,14]],["B","IDLE_ONE",67,[10,11,12,13,14]],["B","IDLE_ONE",68,[10,11,12,13]],["B","IDLE_ONE",69,[10,11,12,13]],["B","IDLE_ONE",70,[10,11,12]],["B","IDLE_ONE",71,[10,11,12]],["B","IDLE_ONE",72,[10,11]],["B","IDLE_ONE",73,[10,11]],["B","IDLE_ONE",74,[10]],["B","IDLE_ONE",75,[10]],["B","IDLE_ONE",76,[10]],["B","IDLE_ONE",77,[10]],["B","ADD",76,77,"-1/2"],["B","ADD",75,77,"-1"],["B","ADD",74,77,"1/2"],["B","ADD",41,77,"-64"],["B","SCALE",77,"1/4"],["B","ADD",74,76,"-2"],["B","SCALE",76,"2"],["B","ADD",77,76,"1/2"],["B","ADD",74,75,"3/2"],["B","ADD",41,75,"64"],["B","ADD",40,75,"64"],["B","SCALE",75,"2"],["B","ADD",77,75,"-5/8"],["B","ADD",76,75,"-3/2"],["B","SWAP",75,77],["B","ADD",40,74,"-64"],["B","ADD",76,74,"2"],["B","ADD",75,74,"3/2"],["B","SWAP",74,75],["B","SWAP",73,75],["B","SWAP",72,74],["B","SWAP",71,73],["B","SWAP",70,72],["B","SWAP",69,71],["B","SWAP",68,70],["B","SWAP",67,69],["B","SWAP",66,68],["B","SWAP",65,67],["B","SWAP",64,66],["B","SWAP",63,65],["B","SWAP",62,64],["B","SWAP",61,63],["B","SWAP",60,62],["B","ADD",40,41,"1/2"],["B","SCALE",41,"-1"],["B","ADD",77,41,"1/32"],["B","ADD",76,41,"-1/64"],["B","ADD",61,41,"1/64"],["B","ADD",60,41,"1/128"],["B","SCALE",40,"-1"],["B","ADD",77,40,"-1/32"],["B","ADD",61,40,"-1/64"],["B","ADD",60,40,"-1/64"],["B","ADD",41,40,"-1"],["B","LAMBDA",40,-1],["J",11,[1,0,20,21],[41,40,"-1","1/2"]],["A","LAMBDA",20,-1],["A","SCALE",21,"-1"],["A","LAMBDA",0,1],["A","SWAP",17,18],["A","SWAP",16,18],["A","SWAP",15,18],["A","SWAP",14,18],["A","SWAP",13,18],["A","SWAP",12,18],["A","SWAP",11,18],["A","SWAP",10,18],["A","SWAP",9,18],["A","SWAP",8,18],["A","SWAP",7,18],["A","SWAP",6,18],["A","SWAP",5,18],["A","SWAP",4,18],["A","SWAP",3,18],["A","ADD",1,2,"-1"],["A","ADD",0,2,"-1"],["A","SCALE",2,"-1"],["A","SWAP",2,18],["A","ADD",0,1,"-1"],["A","SCALE",1,"-1"],["A","ADD",18,1,"2"],["A","ADD",18,0,"2"],["A","ADD",1,0,"1"],["A","SWAP",0,18],["A","LAMBDA",0,-1],["A","SWAP",37,38],["A","SWAP",36,38],["A","SWAP",35,38],["A","SWAP",34,38],["A","SWAP",33,38],["A","SWAP",32,38],["A","SWAP",31,38],["A","SWAP",30,38],["A","SWAP",29,38],["A","SWAP",28,38],["A","SWAP",27,38],["A","SWAP",26,38],["A","SWAP",25,38],["A","SWAP",24,38],["A","SWAP",23,38],["A","ADD",21,22,"-1"],["A","ADD",20,22,"-1"],["A","SCALE",22,"-1"],["A","SWAP",22,38],["A","ADD",20,21,"-1"],["A","ADD",38,21,"-2"],["A","ADD",38,20,"2"],["A","ADD",21,20,"-1"],["A","SWAP",20,38],["A","LAMBDA",20,1],["B","LAMBDA",40,1],["B","IDLE_ONE",76,[11]],["B","IDLE_ONE",77,[11]],["B","ADD",76,77,"1"],["B","ADD",74,77,"-1/4"],["B","ADD",41,77,"-64"],["B","SCALE",77,"-1/2"],["B","ADD",75,76,"1/2"],["B","ADD",74,76,"1/2"],["B","ADD",41,76,"64"],["B","ADD",40,76,"32"],["B","SWAP",76,77],["B","ADD",74,75,"-1/2"],["B","ADD",41,75,"-128"],["B","SCALE",75,"-1"],["B","ADD",77,75,"2"],["B","ADD",76,75,"-1"],["B","ADD",40,74,"128"],["B","SCALE",74,"-2"],["B","ADD",76,74,"1"],["B","ADD",75,74,"1"],["B","SWAP",73,75],["B","SWAP",72,74],["B","SWAP",71,73],["B","SWAP",70,72],["B","SWAP",69,71],["B","SWAP",68,70],["B","SWAP",67,69],["B","SWAP",66,68],["B","SWAP",65,67],["B","SWAP",64,66],["B","SWAP",63,65],["B","SWAP",62,64],["B","ADD",40,41,"1/2"],["B","SCALE",41,"-1"],["B","ADD",77,41,"1/32"],["B","ADD",76,41,"-1/64"],["B","ADD",63,41,"1/64"],["B","ADD",62,41,"1/128"],["B","SCALE",40,"-1"],["B","ADD",77,40,"-1/32"],["B","ADD",63,40,"-1/64"],["B","ADD",62,40,"-1/64"],["B","ADD",41,40,"-1"],["B","LAMBDA",40,-1],["J",12,[1,0,20,21],[41,40,"-1","1/2"]],["A","LAMBDA",20,-1],["A","SCALE",21,"-1"],["A","LAMBDA",0,1],["A","SWAP",17,18],["A","SWAP",16,18],["A","SWAP",15,18],["A","SWAP",14,18],["A","SWAP",13,18],["A","SWAP",12,18],["A","SWAP",11,18],["A","SWAP",10,18],["A","SWAP",9,18],["A","SWAP",8,18],["A","SWAP",7,18],["A","SWAP",6,18],["A","SWAP",5,18],["A","SWAP",4,18],["A","SWAP",3,18],["A","ADD",1,2,"-1"],["A","ADD",0,2,"-1"],["A","SCALE",2,"-1"],["A","SWAP",2,18],["A","ADD",0,1,"-1"],["A","SCALE",1,"-1"],["A","ADD",18,1,"2"],["A","ADD",18,0,"2"],["A","ADD",1,0,"1"],["A","SWAP",0,18],["A","LAMBDA",0,-1],["A","SWAP",37,38],["A","SWAP",36,38],["A","SWAP",35,38],["A","SWAP",34,38],["A","SWAP",33,38],["A","SWAP",32,38],["A","SWAP",31,38],["A","SWAP",30,38],["A","SWAP",29,38],["A","SWAP",28,38],["A","SWAP",27,38],["A","SWAP",26,38],["A","SWAP",25,38],["A","SWAP",24,38],["A","SWAP",23,38],["A","ADD",21,22,"-1"],["A","ADD",20,22,"-1"],["A","SCALE",22,"-1"],["A","SWAP",22,38],["A","ADD",20,21,"-1"],["A","ADD",38,21,"-2"],["A","ADD",38,20,"2"],["A","ADD",21,20,"-1"],["A","SWAP",20,38],["A","LAMBDA",20,1],["B","LAMBDA",40,1],["B","IDLE_ONE",76,[12]],["B","IDLE_ONE",77,[12]],["B","ADD",76,77,"1"],["B","ADD",74,77,"-1/4"],["B","ADD",41,77,"-64"],["B","SCALE",77,"-1/2"],["B","ADD",75,76,"1/2"],["B","ADD",74,76,"1/2"],["B","ADD",41,76,"64"],["B","ADD",40,76,"32"],["B","SWAP",76,77],["B","ADD",74,75,"-1/2"],["B","ADD",41,75,"-128"],["B","SCALE",75,"-1"],["B","ADD",77,75,"2"],["B","ADD",76,75,"-1"],["B","ADD",40,74,"128"],["B","SCALE",74,"-2"],["B","ADD",76,74,"1"],["B","ADD",75,74,"1"],["B","SWAP",73,75],["B","SWAP",72,74],["B","SWAP",71,73],["B","SWAP",70,72],["B","SWAP",69,71],["B","SWAP",68,70],["B","SWAP",67,69],["B","SWAP",66,68],["B","SWAP",65,67],["B","SWAP",64,66],["B","ADD",40,41,"1/2"],["B","SCALE",41,"-1"],["B","ADD",77,41,"1/32"],["B","ADD",76,41,"-1/64"],["B","ADD",65,41,"1/64"],["B","ADD",64,41,"1/128"],["B","SCALE",40,"-1"],["B","ADD",77,40,"-1/32"],["B","ADD",65,40,"-1/64"],["B","ADD",64,40,"-1/64"],["B","ADD",41,40,"-1"],["B","LAMBDA",40,-1],["J",13,[1,0,20,21],[41,40,"-1","1/2"]],["A","LAMBDA",20,-1],["A","SCALE",21,"-1"],["A","LAMBDA",0,1],["A","SWAP",17,18],["A","SWAP",16,18],["A","SWAP",15,18],["A","SWAP",14,18],["A","SWAP",13,18],["A","SWAP",12,18],["A","SWAP",11,18],["A","SWAP",10,18],["A","SWAP",9,18],["A","SWAP",8,18],["A","SWAP",7,18],["A","SWAP",6,18],["A","SWAP",5,18],["A","SWAP",4,18],["A","SWAP",3,18],["A","ADD",1,2,"-1"],["A","ADD",0,2,"-1"],["A","SCALE",2,"-1"],["A","SWAP",2,18],["A","ADD",0,1,"-1"],["A","SCALE",1,"-1"],["A","ADD",18,1,"2"],["A","ADD",18,0,"2"],["A","ADD",1,0,"1"],["A","SWAP",0,18],["A","LAMBDA",0,-1],["A","SWAP",37,38],["A","SWAP",36,38],["A","SWAP",35,38],["A","SWAP",34,38],["A","SWAP",33,38],["A","SWAP",32,38],["A","SWAP",31,38],["A","SWAP",30,38],["A","SWAP",29,38],["A","SWAP",28,38],["A","SWAP",27,38],["A","SWAP",26,38],["A","SWAP",25,38],["A","SWAP",24,38],["A","SWAP",23,38],["A","ADD",21,22,"-1"],["A","ADD",20,22,"-1"],["A","SCALE",22,"-1"],["A","SWAP",22,38],["A","ADD",20,21,"-1"],["A","ADD",38,21,"-2"],["A","ADD",38,20,"2"],["A","ADD",21,20,"-1"],["A","SWAP",20,38],["A","LAMBDA",20,1],["B","LAMBDA",40,1],["B","IDLE_ONE",76,[13]],["B","IDLE_ONE",77,[13]],["B","ADD",76,77,"1"],["B","ADD",74,77,"-1/4"],["B","ADD",41,77,"-64"],["B","SCALE",77,"-1/2"],["B","ADD",75,76,"1/2"],["B","ADD",74,76,"1/2"],["B","ADD",41,76,"64"],["B","ADD",40,76,"32"],["B","SWAP",76,77],["B","ADD",74,75,"-1/2"],["B","ADD",41,75,"-128"],["B","SCALE",75,"-1"],["B","ADD",77,75,"2"],["B","ADD",76,75,"-1"],["B","ADD",40,74,"128"],["B","SCALE",74,"-2"],["B","ADD",76,74,"1"],["B","ADD",75,74,"1"],["B","SWAP",73,75],["B","SWAP",72,74],["B","SWAP",71,73],["B","SWAP",70,72],["B","SWAP",69,71],["B","SWAP",68,70],["B","SWAP",67,69],["B","SWAP",66,68],["B","ADD",40,41,"1/2"],["B","SCALE",41,"-1"],["B","ADD",77,41,"1/32"],["B","ADD",76,41,"-1/64"],["B","ADD",67,41,"1/64"],["B","ADD",66,41,"1/128"],["B","SCALE",40,"-1"],["B","ADD",77,40,"-1/32"],["B","ADD",67,40,"-1/64"],["B","ADD",66,40,"-1/64"],["B","ADD",41,40,"-1"],["B","LAMBDA",40,-1],["J",14,[1,0,20,21],[41,40,"-1","1/2"]],["A","LAMBDA",20,-1],["A","SCALE",21,"-1"],["A","LAMBDA",0,1],["A","SWAP",17,18],["A","SWAP",16,18],["A","SWAP",15,18],["A","SWAP",14,18],["A","SWAP",13,18],["A","SWAP",12,18],["A","SWAP",11,18],["A","SWAP",10,18],["A","SWAP",9,18],["A","SWAP",8,18],["A","SWAP",7,18],["A","SWAP",6,18],["A","SWAP",5,18],["A","SWAP",4,18],["A","SWAP",3,18],["A","ADD",1,2,"-1"],["A","ADD",0,2,"-1"],["A","SCALE",2,"-1"],["A","SWAP",2,18],["A","ADD",0,1,"-1"],["A","SCALE",1,"-1"],["A","ADD",18,1,"2"],["A","ADD",18,0,"2"],["A","ADD",1,0,"1"],["A","SWAP",0,18],["A","LAMBDA",0,-1],["A","SWAP",37,38],["A","SWAP",36,38],["A","SWAP",35,38],["A","SWAP",34,38],["A","SWAP",33,38],["A","SWAP",32,38],["A","SWAP",31,38],["A","SWAP",30,38],["A","SWAP",29,38],["A","SWAP",28,38],["A","SWAP",27,38],["A","SWAP",26,38],["A","SWAP",25,38],["A","SWAP",24,38],["A","SWAP",23,38],["A","ADD",21,22,"-1"],["A","ADD",20,22,"-1"],["A","SCALE",22,"-1"],["A","SWAP",22,38],["A","ADD",20,21,"-1"],["A","ADD",38,21,"-2"],["A","ADD",38,20,"2"],["A","ADD",21,20,"-1"],["A","SWAP",20,38],["A","LAMBDA",20,1],["B","LAMBDA",40,1],["B","IDLE_ONE",76,[14]],["B","IDLE_ONE",77,[14]],["B","ADD",76,77,"1"],["B","ADD",74,77,"-1/4"],["B","ADD",41,77,"-64"],["B","SCALE",77,"-1/2"],["B","ADD",75,76,"1/2"],["B","ADD",74,76,"1/2"],["B","ADD",41,76,"64"],["B","ADD",40,76,"32"],["B","SWAP",76,77],["B","ADD",74,75,"-1/2"],["B","ADD",41,75,"-128"],["B","SCALE",75,"-1"],["B","ADD",77,75,"2"],["B","ADD",76,75,"-1"],["B","ADD",40,74,"128"],["B","SCALE",74,"-2"],["B","ADD",76,74,"1"],["B","ADD",75,74,"1"],["B","SWAP",73,75],["B","SWAP",72,74],["B","SWAP",71,73],["B","SWAP",70,72],["B","SWAP",69,71],["B","SWAP",68,70],["B","ADD",40,41,"1/2"],["B","SCALE",41,"-1"],["B","ADD",77,41,"1/32"],["B","ADD",76,41,"-1/64"],["B","ADD",69,41,"1/64"],["B","ADD",68,41,"1/128"],["B","SCALE",40,"-1"],["B","ADD",77,40,"-1/32"],["B","ADD",69,40,"-1/64"],["B","ADD",68,40,"-1/64"],["B","ADD",41,40,"-1"],["B","LAMBDA",40,-1],["J",15,[1,0,20,21],[41,40,"-1","1/2"]],["A","LAMBDA",20,-1],["A","SCALE",21,"-1"],["A","LAMBDA",0,1],["A","SWAP",17,18],["A","SWAP",16,18],["A","SWAP",15,18],["A","SWAP",14,18],["A","SWAP",13,18],["A","SWAP",12,18],["A","SWAP",11,18],["A","SWAP",10,18],["A","SWAP",9,18],["A","SWAP",8,18],["A","SWAP",7,18],["A","SWAP",6,18],["A","SWAP",5,18],["A","SWAP",4,18],["A","SWAP",3,18],["A","ADD",1,2,"-1"],["A","ADD",0,2,"-1"],["A","SCALE",2,"-1"],["A","SWAP",2,18],["A","ADD",0,1,"-1"],["A","SCALE",1,"-1"],["A","ADD",18,1,"2"],["A","ADD",18,0,"2"],["A","ADD",1,0,"1"],["A","SWAP",0,18],["A","LAMBDA",0,-1],["A","SWAP",37,38],["A","SWAP",36,38],["A","SWAP",35,38],["A","SWAP",34,38],["A","SWAP",33,38],["A","SWAP",32,38],["A","SWAP",31,38],["A","SWAP",30,38],["A","SWAP",29,38],["A","SWAP",28,38],["A","SWAP",27,38],["A","SWAP",26,38],["A","SWAP",25,38],["A","SWAP",24,38],["A","SWAP",23,38],["A","ADD",21,22,"-1"],["A","ADD",20,22,"-1"],["A","SCALE",22,"-1"],["A","SWAP",22,38],["A","ADD",20,21,"-1"],["A","ADD",38,21,"-2"],["A","ADD",38,20,"2"],["A","ADD",21,20,"-1"],["A","SWAP",20,38],["A","LAMBDA",20,1],["B","LAMBDA",40,1],["B","IDLE_ONE",76,[15]],["B","IDLE_ONE",77,[15]],["B","ADD",76,77,"1"],["B","ADD",74,77,"-1/4"],["B","ADD",41,77,"-64"],["B","SCALE",77,"-1/2"],["B","ADD",75,76,"1/2"],["B","ADD",74,76,"1/2"],["B","ADD",41,76,"64"],["B","ADD",40,76,"32"],["B","SWAP",76,77],["B","ADD",74,75,"-1/2"],["B","ADD",41,75,"-128"],["B","SCALE",75,"-1"],["B","ADD",77,75,"2"],["B","ADD",76,75,"-1"],["B","ADD",40,74,"128"],["B","SCALE",74,"-2"],["B","ADD",76,74,"1"],["B","ADD",75,74,"1"],["B","SWAP",73,75],["B","SWAP",72,74],["B","SWAP",71,73],["B","SWAP",70,72],["B","ADD",40,41,"1/2"],["B","SCALE",41,"-1"],["B","ADD",77,41,"1/32"],["B","ADD",76,41,"-1/64"],["B","ADD",71,41,"1/64"],["B","ADD",70,41,"1/128"],["B","SCALE",40,"-1"],["B","ADD",77,40,"-1/32"],["B","ADD",71,40,"-1/64"],["B","ADD",70,40,"-1/64"],["B","ADD",41,40,"-1"],["B","LAMBDA",40,-1],["J",16,[1,0,20,21],[41,40,"-1","1/2"]],["A","LAMBDA",20,-1],["A","SCALE",21,"-1"],["A","LAMBDA",0,1],["A","SWAP",17,18],["A","SWAP",16,18],["A","SWAP",15,18],["A","SWAP",14,18],["A","SWAP",13,18],["A","SWAP",12,18],["A","SWAP",11,18],["A","SWAP",10,18],["A","SWAP",9,18],["A","SWAP",8,18],["A","SWAP",7,18],["A","SWAP",6,18],["A","SWAP",5,18],["A","SWAP",4,18],["A","SWAP",3,18],["A","ADD",1,2,"-1"],["A","ADD",0,2,"-1"],["A","SCALE",2,"-1"],["A","SWAP",2,18],["A","ADD",0,1,"-1"],["A","SCALE",1,"-1"],["A","ADD",18,1,"2"],["A","ADD",18,0,"2"],["A","ADD",1,0,"1"],["A","SWAP",0,18],["A","LAMBDA",0,-1],["A","SWAP",37,38],["A","SWAP",36,38],["A","SWAP",35,38],["A","SWAP",34,38],["A","SWAP",33,38],["A","SWAP",32,38],["A","SWAP",31,38],["A","SWAP",30,38],["A","SWAP",29,38],["A","SWAP",28,38],["A","SWAP",27,38],["A","SWAP",26,38],["A","SWAP",25,38],["A","SWAP",24,38],["A","SWAP",23,38],["A","ADD",21,22,"-1"],["A","ADD",20,22,"-1"],["A","SCALE",22,"-1"],["A","SWAP",22,38],["A","ADD",20,21,"-1"],["A","ADD",38,21,"-2"],["A","ADD",38,20,"2"],["A","ADD",21,20,"-1"],["A","SWAP",20,38],["A","LAMBDA",20,1],["B","LAMBDA",40,1],["B","IDLE_ONE",76,[16]],["B","IDLE_ONE",77,[16]],["B","ADD",76,77,"1"],["B","ADD",74,77,"-1/4"],["B","ADD",41,77,"-64"],["B","SCALE",77,"-1/2"],["B","ADD",75,76,"1/2"],["B","ADD",74,76,"1/2"],["B","ADD",41,76,"64"],["B","ADD",40,76,"32"],["B","SWAP",76,77],["B","ADD",74,75,"-1/2"],["B","ADD",41,75,"-128"],["B","SCALE",75,"-1"],["B","ADD",77,75,"2"],["B","ADD",76,75,"-1"],["B","ADD",40,74,"128"],["B","SCALE",74,"-2"],["B","ADD",76,74,"1"],["B","ADD",75,74,"1"],["B","SWAP",73,75],["B","SWAP",72,74],["B","ADD",40,41,"1/2"],["B","SCALE",41,"-1"],["B","ADD",77,41,"1/32"],["B","ADD",76,41,"-1/64"],["B","ADD",73,41,"1/64"],["B","ADD",72,41,"1/128"],["B","SCALE",40,"-1"],["B","ADD",77,40,"-1/32"],["B","ADD",73,40,"-1/64"],["B","ADD",72,40,"-1/64"],["B","ADD",41,40,"-1"],["B","LAMBDA",40,-1],["J",17,[1,0,20,21],[41,40,"-1","1/2"]],["A","LAMBDA",20,-1],["A","SCALE",21,"-1"],["A","LAMBDA",0,1],["A","SWAP",17,18],["A","SWAP",16,18],["A","SWAP",15,18],["A","SWAP",14,18],["A","SWAP",13,18],["A","SWAP",12,18],["A","SWAP",11,18],["A","SWAP",10,18],["A","SWAP",9,18],["A","SWAP",8,18],["A","SWAP",7,18],["A","SWAP",6,18],["A","SWAP",5,18],["A","SWAP",4,18],["A","SWAP",3,18],["A","ADD",1,2,"-1"],["A","ADD",0,2,"-1"],["A","SCALE",2,"-1"],["A","SWAP",2,18],["A","ADD",0,1,"-1"],["A","SCALE",1,"-1"],["A","ADD",18,1,"2"],["A","ADD",18,0,"2"],["A","ADD",1,0,"1"],["A","SWAP",0,18],["A","LAMBDA",0,-1],["A","SWAP",37,38],["A","SWAP",36,38],["A","SWAP",35,38],["A","SWAP",34,38],["A","SWAP",33,38],["A","SWAP",32,38],["A","SWAP",31,38],["A","SWAP",30,38],["A","SWAP",29,38],["A","SWAP",28,38],["A","SWAP",27,38],["A","SWAP",26,38],["A","SWAP",25,38],["A","SWAP",24,38],["A","SWAP",23,38],["A","ADD",21,22,"-1"],["A","ADD",20,22,"-1"],["A","SCALE",22,"-1"],["A","SWAP",22,38],["A","ADD",20,21,"-1"],["A","ADD",38,21,"-2"],["A","ADD",38,20,"2"],["A","ADD",21,20,"-1"],["A","SWAP",20,38],["A","LAMBDA",20,1],["B","LAMBDA",40,1],["B","IDLE_ONE",76,[17]],["B","IDLE_ONE",77,[17]],["B","ADD",76,77,"1"],["B","ADD",74,77,"-1/4"],["B","ADD",41,77,"-64"],["B","SCALE",77,"-1/4"],["B","ADD",75,76,"1/2"],["B","ADD",74,76,"1/2"],["B","ADD",41,76,"64"],["B","ADD",40,76,"32"],["B","SCALE",76,"1/2"],["B","SWAP",76,77],["B","ADD",74,75,"-1/2"],["B","ADD",41,75,"-128"],["B","SCALE",75,"-1"],["B","ADD",77,75,"1"],["B","ADD",76,75,"-1/2"],["B","ADD",40,74,"128"],["B","SCALE",74,"-2"],["B","ADD",76,74,"1/2"],["B","ADD",75,74,"1"],["B","ADD",40,41,"1/2"],["B","SCALE",41,"-1"],["B","ADD",77,41,"1/64"],["B","ADD",76,41,"-1/128"],["B","ADD",75,41,"1/64"],["B","ADD",74,41,"1/128"],["B","SCALE",40,"-1"],["B","ADD",77,40,"-1/64"],["B","ADD",75,40,"-1/64"],["B","ADD",74,40,"-1/64"],["B","ADD",41,40,"-1"],["B","LAMBDA",40,-1],["J",18,[1,0,20,21],[41,40,"-1","1/2"]],["A","LAMBDA",20,-1],["A","SCALE",21,"-1"],["A","LAMBDA",0,1],["A","SWAP",17,18],["A","SWAP",16,18],["A","SWAP",15,18],["A","SWAP",14,18],["A","SWAP",13,18],["A","SWAP",12,18],["A","SWAP",11,18],["A","SWAP",10,18],["A","SWAP",9,18],["A","SWAP",8,18],["A","SWAP",7,18],["A","SWAP",6,18],["A","SWAP",5,18],["A","SWAP",4,18],["A","SWAP",3,18],["A","SWAP",2,18],["A","ADD",0,1,"-2"],["A","SWAP",1,18],["A","SCALE",0,"-1"],["A","ADD",18,0,"-1"],["A","LAMBDA",0,-1],["A","LAMBDA",1,-1],["A","LAMBDA",2,-1],["A","LAMBDA",3,-1],["A","LAMBDA",4,-1],["A","LAMBDA",5,-1],["A","LAMBDA",6,-1],["A","LAMBDA",7,-1],["A","LAMBDA",8,-1],["A","LAMBDA",9,-1],["A","LAMBDA",10,-1],["A","LAMBDA",11,-1],["A","LAMBDA",12,-1],["A","LAMBDA",13,-1],["A","LAMBDA",14,-1],["A","LAMBDA",15,-1],["A","LAMBDA",16,-1],["A","LAMBDA",17,-1],["A","LAMBDA",18,-1],["A","LAMBDA",19,-1],["A","SWAP",37,38],["A","SWAP",36,38],["A","SWAP",35,38],["A","SWAP",34,38],["A","SWAP",33,38],["A","SWAP",32,38],["A","SWAP",31,38],["A","SWAP",30,38],["A","SWAP",29,38],["A","SWAP",28,38],["A","SWAP",27,38],["A","SWAP",26,38],["A","SWAP",25,38],["A","SWAP",24,38],["A","SWAP",23,38],["A","SWAP",22,38],["A","ADD",20,21,"-2"],["A","SWAP",21,38],["A","SCALE",20,"-1"],["A","ADD",38,20,"-1"],["A","LAMBDA",20,-1],["A","LAMBDA",21,-1],["A","LAMBDA",22,-1],["A","LAMBDA",23,-1],["A","LAMBDA",24,-1],["A","LAMBDA",25,-1],["A","LAMBDA",26,-1],["A","LAMBDA",27,-1],["A","LAMBDA",28,-1],["A","LAMBDA",29,-1],["A","LAMBDA",30,-1],["A","LAMBDA",31,-1],["A","LAMBDA",32,-1],["A","LAMBDA",33,-1],["A","LAMBDA",34,-1],["A","LAMBDA",35,-1],["A","LAMBDA",36,-1],["A","LAMBDA",37,-1],["A","LAMBDA",38,-1],["A","LAMBDA",39,-1],["B","LAMBDA",40,1],["B","IDLE_ONE",76,[18]],["B","IDLE_ONE",77,[18]],["B","ADD",41,77,"-128"],["B","ADD",40,77,"64"],["B","SCALE",77,"-1"],["B","ADD",40,76,"128"],["B","SCALE",76,"-1"],["B","ADD",77,76,"2"],["B","ADD",40,41,"1/2"],["B","SCALE",41,"1/128"],["B","ADD",77,41,"-2"],["B","ADD",76,41,"-1"],["B","SCALE",40,"1/128"],["B","ADD",77,40,"2"],["B","ADD",76,40,"2"],["B","SWAP",40,41],["B","LAMBDA",40,-1],["B","LAMBDA",41,-1],["B","LAMBDA",42,-1],["B","LAMBDA",43,-1],["B","LAMBDA",44,-1],["B","LAMBDA",45,-1],["B","LAMBDA",46,-1],["B","LAMBDA",47,-1],["B","LAMBDA",48,-1],["B","LAMBDA",49,-1],["B","LAMBDA",50,-1],["B","LAMBDA",51,-1],["B","LAMBDA",52,-1],["B","LAMBDA",53,-1],["B","LAMBDA",54,-1],["B","LAMBDA",55,-1],["B","LAMBDA",56,-1],["B","LAMBDA",57,-1],["B","LAMBDA",58,-1],["B","LAMBDA",59,-1],["B","LAMBDA",60,-1],["B","LAMBDA",61,-1],["B","LAMBDA",62,-1],["B","LAMBDA",63,-1],["B","LAMBDA",64,-1],["B","LAMBDA",65,-1],["B","LAMBDA",66,-1],["B","LAMBDA",67,-1],["B","LAMBDA",68,-1],["B","LAMBDA",69,-1],["B","LAMBDA",70,-1],["B","LAMBDA",71,-1],["B","LAMBDA",72,-1],["B","LAMBDA",73,-1],["B","LAMBDA",74,-1],["B","LAMBDA",75,-1],["B","LAMBDA",76,-1],["B","LAMBDA",77,-1]]} \ No newline at end of file diff --git a/research/odd-native-common-grid/source/data/word.json.gz b/research/odd-native-common-grid/source/data/word.json.gz new file mode 100644 index 0000000000..476c66170e Binary files /dev/null and b/research/odd-native-common-grid/source/data/word.json.gz differ diff --git a/research/odd-native-common-grid/verify.py b/research/odd-native-common-grid/verify.py new file mode 100644 index 0000000000..0d5862d041 --- /dev/null +++ b/research/odd-native-common-grid/verify.py @@ -0,0 +1,98 @@ +"""Source-authenticated dual-method replay; no native or supplier admission. + +Prepared for @CubeJerry with substantial OpenAI assistance. Apache-2.0. +""" +from __future__ import annotations + +import ast +from hashlib import sha256 +from pathlib import Path +import gzip +import json +import sys + +HERE = Path(__file__).resolve().parent +sys.path.insert(0, str(HERE)) +from audit_bounds import caller_bounds, ceil_log2, require, word_bounds +from audit_controls import controls, rejects +import independent_bounds as independent + + +def authenticate(): + manifest = json.loads((HERE / "SOURCE-BYTES.json").read_text()) + require(manifest["head"] == "4e13b7acdbea1c9f12aa88126435360eecea7401", "exact candidate head") + for entry in manifest["files"]: + raw = (HERE / entry["path"]).read_bytes() + require(len(raw) == entry["bytes"] and sha256(raw).hexdigest() == entry["sha256"], + "source bytes: " + entry["path"]) + raw = (HERE / "source/data/caller.json").read_bytes() + wanted = sha256(raw).hexdigest() + mutant = bytes([raw[0] ^ 1]) + raw[1:] + require(sha256(mutant).hexdigest() != wanted, "single-byte source corruption detected") + return manifest + + +def source_parameters(text): + # Only inspect literal declarations. Never execute the source check.py. + result = {} + for node in ast.parse(text).body: + if not isinstance(node, ast.Assign) or len(node.targets) != 1: + continue + target = node.targets[0] + if isinstance(target, ast.Tuple) and all(isinstance(x, ast.Name) for x in target.elts): + names = [x.id for x in target.elts] + if names == ["cutoff", "floor", "power", "offset"]: + require(isinstance(node.value, ast.Tuple), "literal source parameter tuple") + result.update(zip(names[:3], [ast.literal_eval(x) for x in node.value.elts[:3]])) + require(result == {"cutoff": 11, "floor": 12, "power": 1920}, "retained separation parameters") + return result + + +def main(): + source = authenticate() + word = json.loads(gzip.decompress((HERE / "source/data/word.json.gz").read_bytes())) + caller = json.loads((HERE / "source/data/caller.json").read_text()) + expected = json.loads((HERE / "EXPECTED-BOUNDS.json").read_text()) + bounds = {"word": word_bounds(word), "caller": caller_bounds(caller)} + require(json.dumps(bounds, sort_keys=True) == json.dumps(expected, sort_keys=True), + "complete exact source envelope receipt") + + # Independently authored fixed-grid integer and positive transfer-matrix + # engines, not a second invocation of the rational row interpreter. + iw, ic = independent.word_run(word), independent.caller_run(caller) + for key in ("dyadic_height", "maximum_scaled_mass", "coefficient_visits"): + require(iw[key] == bounds["word"][key], "independent word: " + key) + require(iw["odd_scale_lcm"] == 1125 and iw["numerator_bits"] == 24, "independent scale and numerator") + for key in ("maximum_mass", "denominator_height", "pre_joint_height"): + require(ic[key] == bounds["caller"][key], "independent caller: " + key) + from fractions import Fraction + require(ceil_log2(Fraction(ic["pre_joint_mass"])) == bounds["caller"]["pre_joint_mass_bits"], + "independent joint entrance mass") + rejected_scales = {str(scale): rejects(lambda s=scale: independent.word_run(word, scale=s), + "integer grid rejection at event " + str(event)) + for scale, event in ((225, 1101), (375, 36915))} + + threshold = independent.threshold_run() + params = source_parameters((HERE / "source/check.py").read_text()) + require(caller["ambient_rank"] == 153 and 153 < 2**8 + and 8*params["power"] < threshold["H"], "compiler carrier below fixed N") + A = max(bounds["caller"]["denominator_height"], + bounds["caller"]["pre_joint_height"] + bounds["word"]["dyadic_height"]) + B = max(bounds["caller"]["mass_bits"], + bounds["caller"]["pre_joint_mass_bits"] + bounds["word"]["scaled_mass_bits"]) + require((A, B) == (178, 161), "source-specific unfinished-context bounds") + require(2 * max(A, B) + 1 == 357, "same exact threshold coefficient") + c = controls(word, caller) + receipt = {"source_head": source["head"], "source_files": len(source["files"]), + "word_coefficient_visits": bounds["word"]["coefficient_visits"], + "caller_events": bounds["caller"]["events"], "independent_minimum_scale": iw["odd_scale_lcm"], + "A": A, "B": B, "threshold": threshold, + "per_caller_scale_scans": 2*bounds["word"]["public_fields"]*bounds["caller"]["operations"]["J"], + "rejected_scales": rejected_scales, "controls": c, + "native_endpoints_reproved": False, "full_supplier_admitted": False, "new_kappa": False} + require(receipt["per_caller_scale_scans"] == 52272, "complete per-call scale/unscale inventory") + print("PASS_ODD_NATIVE_COMMON_GRID " + json.dumps(receipt, sort_keys=True)) + + +if __name__ == "__main__": + main()