diff --git a/sonnet/README.md b/sonnet/README.md index 9d20f909..a72307e6 100644 --- a/sonnet/README.md +++ b/sonnet/README.md @@ -83,6 +83,7 @@ deferred until its next oracle/evidence gate is affordable. | [`pcr3bp-history-cost/`](pcr3bp-history-cost/) | Phases 0–1 complete; Phase 2 frozen | lifted topology and scale-jet reconstruction separate word, clock, deck, and hyperbolic costs; no Bellman/Huffman source is yet justified | [Phase-2 contract](pcr3bp-history-cost/02-return-partition-holonomy-contract.md); next run the frozen two-gate covariance and convergence gates | | [`am-conformal-chart-normal-forms/`](am-conformal-chart-normal-forms/) | T0/T1; Phase 1 mechanism calibrated | exact Riccati lift, Möbius covariance, scalar-gauge invariance, cubic no-go, and eight-axis Pareto accounting; no discovery or economy theorem | [Phase-1 results](am-conformal-chart-normal-forms/02-phase1-riccati-results.md); next freeze a blind low-height grammar and run bounded recovery | | [`effective-scale-carrier-ladder/`](effective-scale-carrier-ladder/) | T1 / NARROW | finite syntax decision eliminates a surreal runtime; symbolic height is a real C2 obstruction, but semantic evaluation and C3/C4 separation remain open | [results](effective-scale-carrier-ladder/01-results.md), [compiler](../workstreams/carrier_ladder/compiler/), and [commit--reveal audit](../workstreams/carrier_ladder/redteam/); next implement an effective normalized hyperiteration fragment, not a general surreal runtime | +| [`am-power-weight-compiler/`](am-power-weight-compiler/) | T1 / EXPAND | 12/12 frozen public cases and nonce-protected held-out pass with exact replay; sparse distant readout shows a 2-weight versus 33-weight window advantage, but no general performance or surreal claim | [results](am-power-weight-compiler/01-results.md), [compiler](../workstreams/am_weight_compiler/), and [commit--reveal audit](../workstreams/am_weight_compiler/HELD_OUT_REVEAL.json); next freeze a separate AM goal front-end and transport corpus | | [`s6-complex-arithmetic-tower/`](s6-complex-arithmetic-tower/) | T0 initialization | auditable two-question research contract only; neither the manuscript nor an arithmetic interface is verified | [problem frontier](s6-complex-arithmetic-tower/00-problem-frontier.md); next archive/checksum the source and reproduce its matrix/topology certificate | | [`boltzmann-bbgky-h-theorem/`](boltzmann-bbgky-h-theorem/) | Phase 1I charted fibre-response calibration passed | 47 exact certificates through Phases 1C and 1E–1I; target Lyapunov decrease need not survive continued fibre response; contrast/odds expose a chart-relative dynamics/composition tradeoff; no continuum response theorem, fibre objectification, or generic entropy claim | [Phase 1I result](boltzmann-bbgky-h-theorem/18-phase1i-charted-fibre-calculus-results.md); next run the separate finite collision-covector and continuum fibre-response gates | diff --git a/sonnet/am-power-weight-compiler/00-problem-frontier.md b/sonnet/am-power-weight-compiler/00-problem-frontier.md new file mode 100644 index 00000000..cfdbf9a6 --- /dev/null +++ b/sonnet/am-power-weight-compiler/00-problem-frontier.md @@ -0,0 +1,123 @@ +# Completed AM power--weight compiler + +## Problem and task + +Can the native Addition/Multiplication affine function language be made into +an exact, replayable coefficient compiler whose semantic carrier is the +power--weight algebra and its observer-directed completion, rather than an +ordinary polynomial, matrix, jet, or generic computer-algebra series? + +The primitive continuous processes are + +\[ +T_t(a,v)=(a+t,v), +\qquad +S_s(a,v)=(e^s a,v+s), +\] + +with finite and infinitesimal laws + +\[ +S_sT_t=T_{e^st}S_s, +\qquad +[A,M]=A. +\] + +The native basis is + +\[ +\Phi_{\nu,w}=a^\nu e^{(w-\nu)v}, +\] + +not the polynomial calibration module `span(1,a,...,a^n)`. Literal ordered +process words, their symbolic action, and observer coefficient readouts remain +separately typed. + +## Primitive audit + +- **base coefficient domain:** exact rationals; +- **constant readout extension:** finite rational linear combinations of + formal `exp(q)` atoms, with `exp(q)exp(r)=exp(q+r)`; +- **power degree:** integer `nu`; +- **exponential character:** rational `lambda = w - nu`; +- **M-weight:** rational `w`; +- **base algebra:** finite support in `(nu,w)`; +- **completion:** allowed only along a declared positive rational weight cone; +- **task:** one exact target weight or bounded weight band; +- **residual:** all weights strictly above the observer horizon; +- **resonance:** a typed extension, never a silent base-algebra element. + +The finite-LE chart from issue #144 is not identified with the native AM +frame. Any later bridge must be an explicit task-relative adapter. + +## Construction and laws + +Multiplication is sparse convolution on the power--weight lattice. The native +operators satisfy + +\[ +M\Phi_{\nu,w}=w\Phi_{\nu,w}, +\qquad +A\Phi_{\nu,w}=\nu\Phi_{\nu-1,w-1}, +\] + +and replay must verify + +\[ +M^nA^m=A^m(M-m)^n. +\] + +`ExpPositive` and `LogOnePlusPositive` denote elements of the declared +completion. They must answer a finite observer by dependency-directed exact +coefficient extraction. Neither compiler nor replay may call a generic +`limit()` or unrestricted `series()` oracle. + +At `nu=-1`, an Addition primitive requires the positive-real logarithmic +extension; at `w=0`, a Multiplication primitive requires the `v` Jordan +extension. With `ordinary-only` policy those inputs fail closed. + +## Solver plan + +- research-local Python implementation with `Fraction` and a small exact + formal exponential-constant algebra; +- strict JSON corpus and canonical digests; +- memoized coefficient dependency evaluation; +- specialized monomial coefficient rules where independently replayable; +- compact certificate containing source/context digests, requested and + visited weights, operator laws, extensions, failures, costs, and claim scope; +- replay from source and context, not from a stored expansion trace; +- same-information SymPy baseline kept non-authoritative; +- seconds-scale unit, corpus, tamper, manifest, and default-CI bridge tests. + +## Cost axes + +Compilation, coefficient operations, visited weights, maximum live support, +certificate bytes, replay operations, baseline wall time, and baseline peak +support are reported separately. Shorter syntax or a correct coefficient does +not establish economy. + +## Evidence firewall + +Grammar, coefficient domain, positive-cone semantics, operator laws, +completion rules, resonance policy, budgets, public controls, scoring, and one +self-committed held-out payload freeze before evaluator source. The hidden +payload receives generalization evidence but no independent-discovery credit. + +## Claim boundary + +The maximum positive claim is a reusable exact compiler for the frozen +rank-one rational AM power--weight fragment. This is pressure on U2 and E, not +evidence for multivariable AM, V5 analytic closure, transseries, hyperseries, +surreal arithmetic, symbolic-height iteration, or Arithmetic Universality. +Mathematical Core, Engineering Architecture, Theory Map, and Public API remain +unchanged at creation. + +## Kill conditions + +Publish `STOP` if the result requires answer storage, unrestricted series or +limit calls, post-reveal grammar/scoring changes, or full expansion traces. +Publish `ELIMINATE` if it adds no semantic or material software capability +beyond a certificate wrapper around the baseline. Publish `NARROW` if native +laws work but completion/transport is not reusable. Publish `EXPAND` only if +the frozen task family gains replayable semantics or a material measured +dependency/support/certificate advantage. diff --git a/sonnet/am-power-weight-compiler/01-results.md b/sonnet/am-power-weight-compiler/01-results.md new file mode 100644 index 00000000..844189bd --- /dev/null +++ b/sonnet/am-power-weight-compiler/01-results.md @@ -0,0 +1,147 @@ +# Completed AM power--weight compiler: first results + +Status: T1 / `EXPAND` within a strict rank-one rational claim ceiling. + +Issue: [#146](https://github.com/mountain/process-geometry/issues/146) +Draft implementation: [#147](https://github.com/mountain/process-geometry/pull/147) + +## 1. Result + +The first executable completed AM carrier now exists as a research-local +compiler. Its native terms are + +\[ +\Phi_{\nu,w}=a^\nu e^{(w-\nu)v}, +\qquad \nu\in\mathbb Z, +\qquad w\in\mathbb Q, +\] + +with exact product and generator actions + +\[ +\Phi_{\nu,w}\Phi_{\mu,z}=\Phi_{\nu+\mu,w+z}, +\qquad +A\Phi_{\nu,w}=\nu\Phi_{\nu-1,w-1}, +\qquad +M\Phi_{\nu,w}=w\Phi_{\nu,w}. +\] + +The completion does not construct a full coefficient window. After an +observer declares one target weight, the compiler recursively requests only +the dependencies needed for that readout. Exact coefficients live in the +finite group algebra + +\[ +\mathbb Q[\exp(\mathbb Q)], +\qquad +\exp(q)\exp(r)=\exp(q+r). +\] + +This is a power--weight/exponential-polynomial carrier. A jet or matrix may be +an observer product, but neither receives semantic-carrier credit. + +## 2. Frozen public gate + +All 12 preimplementation cases passed and replayed: + +- the product, `A`, `M`, PBW identity, and finite affine relation are exact; +- `power-weight` and `power-character` encodings canonicalize to the same term; +- positive-cone `exp` and `log1p` completion produces exact target weights; +- the `A` resonance produces typed `log-a` with the witness `a>0`; +- the `M` resonance produces typed `v-jordan`; +- missing positivity, negative completion input, excessive lattice + denominator, excessive target weight, ordinary-only resonance, and symbolic + height all fail closed with the frozen taxonomy. + +The two public completion probes were: + +| Case | Exact readout | Dependency requests | Distinct weights | Exact coefficient operations | Certificate | +|---|---:|---:|---:|---:|---:| +| weight-32 log cancellation | `-1/32` | 4 | 2 | 3 | 864 B | +| nested completed exponential | `exp(2)` | 8 | 2 | 7 | 863 B | + +The first case is the clearest observer-directed result: it asks directly for +weight 32 of a monomial logarithm and the cancelling finite term, rather than +constructing weights 0 through 32. + +## 3. Commit--reveal result + +The hidden payload was committed before implementation by + +`d578b7ed9f5193cc5b0a0212c3edad025a3b2cee4cf3f90885dd95a412ce5597`. + +The evaluator and replay were then remotely frozen at + +`a4cd0a7918b4d79ea049852bb829e0feb92d5e2f`. + +Only afterwards was the payload revealed: + +\[ +[x^0]\,x^{-7}\left( +\exp\!\left(\log(1+2x)+x^2\right) +-\left(1+2x+x^2+2x^3+\frac{x^4}{2}+x^5+\frac{x^6}{6}\right) +\right). +\] + +The compiler returned + +\[ +\boxed{\frac13}. +\] + +The commitment verified exactly. The certificate used 29 dependency requests +over weights 0 through 7, 111 exact coefficient operations, and 888 bytes; a +fresh semantic replay reproduced the same certificate digest. + +This is generalization evidence, not independent-discovery evidence: the +held-out was a nonce-protected preimplementation self-commit. + +## 4. Same-information baseline + +The declared SymPy baseline obtained all three exact readouts. It was allowed +to materialize a truncated coefficient window but received no credit for AM +carrier semantics, completion-domain witnesses, resonance typing, or replay. + +| Case | Baseline window | AM distinct weights | SymPy median | AM median | Interpretation | +|---|---:|---:|---:|---:|---| +| weight-32 cancellation | 33 | 2 | 19.76 ms | 0.37 ms | material support advantage | +| nested exponential | 2 | 2 | 14.46 ms | 0.17 ms | same weight span | +| held-out weight 7 | 8 | 8 | 13.63 ms | 0.76 ms | same weight span | + +Timing is a warm, local microbenchmark and is explicitly non-authoritative. +It is not a performance theorem. The defensible economy claim is narrower: +observer-directed extraction avoids a full intervening window on sparse, +distant readouts such as the weight-32 cancellation probe. The other two +cases demonstrate exact semantics and replay, not reduced weight support. + +## 5. Evaluation + +The frozen scoring rule gives `EXPAND`, for two reasons: + +1. a reusable completed-AM task family now has executable, replayable + semantics rather than only a matrix or polynomial proxy; +2. one frozen workload demonstrates a material dependency-window advantage. + +This does **not** establish a general computational advantage over SymPy, a +general AM function theory, multivariable completion, or any surreal-number +runtime claim. In fact, the result sharpens the surreal assessment: no surreal +object was needed for this bounded rational-rank AM layer. Surreal height may +become relevant only at a later rank/iteration boundary; importing it here +would have added ontology without adding capability. + +## 6. Next gate + +Freeze a separate AM goal front-end and transport corpus. Its job is to map +existing mathematical vignettes and tests into the validated carrier, for +example a future textual request of the form + +```text +\goal coefficient weight=7 of exp(log1p(2*x)+x^2) +``` + +without changing the now-tested evaluator. The front-end must preserve exact +source/context digests, reject ambiguous coordinate identifications, and +compare each transported task with its same-information baseline. + +The current implementation consumes the frozen JSON AST; the textual +`\goal` form above is a next-stage interface proposal, not current syntax. diff --git a/tests/test_am_weight_compiler_workstream.py b/tests/test_am_weight_compiler_workstream.py new file mode 100644 index 00000000..379a2043 --- /dev/null +++ b/tests/test_am_weight_compiler_workstream.py @@ -0,0 +1,19 @@ +from __future__ import annotations + +from pathlib import Path +import sys + + +WORKSTREAM = Path(__file__).resolve().parents[1] / "workstreams" / "am_weight_compiler" +sys.path.insert(0, str(WORKSTREAM)) + +from am_weight_compiler.corpus import run_corpus # noqa: E402 + + +def test_am_weight_compiler_public_gate() -> None: + result = run_corpus( + WORKSTREAM / "PUBLIC_CORPUS.json", + WORKSTREAM / "FROZEN_CONTRACT.json", + ) + assert result["passed"] is True + assert result["pass_count"] == result["case_count"] == 12 diff --git a/workstreams/am_weight_compiler/BASELINE_CONTRACT.json b/workstreams/am_weight_compiler/BASELINE_CONTRACT.json new file mode 100644 index 00000000..a16f4753 --- /dev/null +++ b/workstreams/am_weight_compiler/BASELINE_CONTRACT.json @@ -0,0 +1,25 @@ +{ + "schema": "process-geometry/am-weight-baseline-contract/v0", + "engine": "SymPy", + "same_information": true, + "authority": "non-authoritative", + "allowed": [ + "expand or series in the baseline only", + "exact coefficient extraction", + "wall-time and expression-support measurement" + ], + "forbidden_credit": [ + "semantic carrier", + "completion proof", + "branch or resonance proof", + "replay certificate" + ], + "comparison": [ + "exact readout equality", + "source support", + "visited/dependency weights", + "certificate bytes", + "coefficient operations", + "wall time as non-authoritative" + ] +} diff --git a/workstreams/am_weight_compiler/FROZEN_CONTRACT.json b/workstreams/am_weight_compiler/FROZEN_CONTRACT.json new file mode 100644 index 00000000..409cd6b8 --- /dev/null +++ b/workstreams/am_weight_compiler/FROZEN_CONTRACT.json @@ -0,0 +1,62 @@ +{ + "schema": "process-geometry/am-weight-contract/v0", + "issue": 146, + "claim_mode": "exact-symbolic", + "native_frame": { + "finite_law": "S_s T_t = T_(exp(s)*t) S_s", + "infinitesimal_law": "[A,M]=A", + "basis": "Phi_(nu,w)=a^nu*exp((w-nu)*v)", + "power_degrees": "integers", + "weights": "finitely generated rational rank-one lattice" + }, + "coefficient_domain": { + "base": "Q", + "readout": "finite Q-linear combinations of formal exp(q), q in Q", + "law": "exp(q)*exp(r)=exp(q+r)" + }, + "completion": { + "cone": "positive normalized integer weights", + "exp": "argument has no negative weight and has a rational constant coefficient", + "log1p": "argument has strictly positive weight", + "observer": "one exact target weight or finite band", + "residual": "all weights above the observer horizon", + "semantic_carrier": "completed AM power-weight algebra; generated matrices or jets have no carrier credit" + }, + "resonance": { + "A": "nu=-1 forces a positive-real log(a) extension", + "M": "w=0 forces a v Jordan extension", + "ordinary_only": "fail closed at either resonance" + }, + "grammar": [ + "native-power-weight", + "native-power-character", + "finite-weight-series", + "add", + "multiply", + "scale", + "weight-shift", + "exp-positive", + "log-one-plus-positive", + "primitive-request", + "symbolic-height-negative-control" + ], + "budgets": { + "max_nodes": 1024, + "max_lattice_denominator": 24, + "max_abs_power": 256, + "max_target_weight": 256, + "max_coefficient_operations": 100000, + "max_certificate_bytes": 65536 + }, + "forbidden": [ + "generic limit call in compiler or replay", + "generic unrestricted series call in compiler or replay", + "stored expected answer", + "stored full expansion trace", + "post-reveal grammar or scoring change", + "identifying a jet or matrix window as the semantic carrier", + "silently identifying the finite-LE N/t chart with native AM coordinates" + ], + "dispositions": ["EXPAND", "NARROW", "ELIMINATE", "STOP"], + "claim_ceiling": "exact observer-directed coefficient semantics for the frozen rank-one rational completed AM power-weight fragment" +} diff --git a/workstreams/am_weight_compiler/HELD_OUT_COMMITMENT.json b/workstreams/am_weight_compiler/HELD_OUT_COMMITMENT.json new file mode 100644 index 00000000..f019fe62 --- /dev/null +++ b/workstreams/am_weight_compiler/HELD_OUT_COMMITMENT.json @@ -0,0 +1,8 @@ +{ + "schema": "process-geometry/am-weight-heldout-commitment/v0", + "scheme": "sha256(canonical-json-with-256-bit-nonce)", + "payload_sha256": "d578b7ed9f5193cc5b0a0212c3edad025a3b2cee4cf3f90885dd95a412ce5597", + "reveal_rule": "Reveal only after grammar, coefficient domain, completion rules, resonance policy, budgets, evaluator source, replay, and scoring are publicly frozen.", + "anti_bruteforce": "The payload includes a random 256-bit nonce.", + "independence_boundary": "This is a preimplementation self-commit, not an independent-agent held-out; it receives generalization evidence but no independent-discovery credit." +} diff --git a/workstreams/am_weight_compiler/HELD_OUT_RESULT.json b/workstreams/am_weight_compiler/HELD_OUT_RESULT.json new file mode 100644 index 00000000..5ef463dd --- /dev/null +++ b/workstreams/am_weight_compiler/HELD_OUT_RESULT.json @@ -0,0 +1,63 @@ +{ + "case_id": "heldout-mixed-log-exp-weight7", + "certificate": { + "case_id": "heldout-mixed-log-exp-weight7", + "certificate_digest": "e2c43ede3614378731d7912372f0caf898b99bd28b3adca9ab8ce18cce746ad4", + "claim_scope": "frozen-rank-one-rational-completed-am-fragment", + "context_digest": "68afe2f989d0ad11054607890d6dd35172deb72016d0587466c6f2adada06f93", + "costs": { + "compilation": { + "lattice_denominator": 1, + "nodes": 9 + }, + "evaluation": { + "coefficient_operations": 111 + }, + "storage": { + "certificate_bytes": 888, + "source_bytes": 656 + } + }, + "dependencies": { + "request_count": 29, + "weight_count": 8, + "weights": [ + "0", + "1", + "2", + "3", + "4", + "5", + "6", + "7" + ] + }, + "kind": "coefficient", + "observer": { + "residual": "weights-above-observer-horizon", + "target_weight": "0" + }, + "result": { + "coefficient": "1/3" + }, + "schema": "process-geometry/am-weight-certificate/v0", + "semantic_carrier": "completed-am-power-weight/rank-one-rational/v0", + "source_digest": "9a2d378cd8d4bf338273d26c691702667cac95659793e5d1b7da51213045a3f0", + "status": "evaluated" + }, + "commitment_verified": true, + "passed": true, + "payload_digest": "d578b7ed9f5193cc5b0a0212c3edad025a3b2cee4cf3f90885dd95a412ce5597", + "pre_reveal_source_commit": "a4cd0a7918b4d79ea049852bb829e0feb92d5e2f", + "replay": { + "certificate_digest": "e2c43ede3614378731d7912372f0caf898b99bd28b3adca9ab8ce18cce746ad4", + "costs": { + "coefficient_operations": 111, + "dependency_requests": 29 + }, + "recomputed_digest": "e2c43ede3614378731d7912372f0caf898b99bd28b3adca9ab8ce18cce746ad4", + "replay_digest": "58cc54cd10452ebae2fe423281b72088975e5a9c09649f86babaae0ecb201d7c", + "status": "verified" + }, + "schema": "process-geometry/am-weight-heldout-result/v0" +} diff --git a/workstreams/am_weight_compiler/HELD_OUT_REVEAL.json b/workstreams/am_weight_compiler/HELD_OUT_REVEAL.json new file mode 100644 index 00000000..2185e151 --- /dev/null +++ b/workstreams/am_weight_compiler/HELD_OUT_REVEAL.json @@ -0,0 +1,103 @@ +{ + "schema": "process-geometry/am-weight-heldout-reveal/v0", + "commitment_algorithm": "sha256(canonical-json(payload))", + "commitment": "d578b7ed9f5193cc5b0a0212c3edad025a3b2cee4cf3f90885dd95a412ce5597", + "pre_reveal_source_commit": "a4cd0a7918b4d79ea049852bb829e0feb92d5e2f", + "pre_reveal_source_tree": "b8bece048e6f1803afbb328be72413fb08fee159", + "payload": { + "cases": [ + { + "expected": "1/3", + "id": "heldout-mixed-log-exp-weight7", + "source": "x^-7*(exp(log(1+2*x)+x^2)-(1+2*x+x^2+2*x^3+x^4/2+x^5+x^6/6))", + "task": "compute exact zero-weight readout and replay dependency slice" + } + ], + "nonce": "2f16bb4cce712b7237726d1fc876c3f2efcffa7b2236ce3a1dd074234af9a2a9", + "schema_version": "am-weight-heldout-v1" + }, + "executable_case": { + "id": "heldout-mixed-log-exp-weight7", + "kind": "coefficient", + "target_weight": "0", + "expression": { + "op": "shift", + "by": "-7", + "argument": { + "op": "add", + "arguments": [ + { + "op": "exp", + "argument": { + "op": "add", + "arguments": [ + { + "op": "log1p", + "argument": { + "op": "finite", + "terms": [ + { + "weight": "1", + "coefficient": "2" + } + ] + } + }, + { + "op": "finite", + "terms": [ + { + "weight": "2", + "coefficient": "1" + } + ] + } + ] + } + }, + { + "op": "scale", + "coefficient": "-1", + "argument": { + "op": "finite", + "terms": [ + { + "weight": "0", + "coefficient": "1" + }, + { + "weight": "1", + "coefficient": "2" + }, + { + "weight": "2", + "coefficient": "1" + }, + { + "weight": "3", + "coefficient": "2" + }, + { + "weight": "4", + "coefficient": "1/2" + }, + { + "weight": "5", + "coefficient": "1" + }, + { + "weight": "6", + "coefficient": "1/6" + } + ] + } + } + ] + } + }, + "expected": { + "status": "evaluated", + "coefficient": "1/3" + } + } +} diff --git a/workstreams/am_weight_compiler/OBSERVED_BASELINES.json b/workstreams/am_weight_compiler/OBSERVED_BASELINES.json new file mode 100644 index 00000000..2daf6a5e --- /dev/null +++ b/workstreams/am_weight_compiler/OBSERVED_BASELINES.json @@ -0,0 +1,229 @@ +{ + "cases": [ + { + "candidate": { + "certificate_digest": "88f325cd067bf587cb91d78c3809467ae28f442b01d01bd6ff79b2b6c4fae91a", + "coefficient": "-1/32", + "costs": { + "compilation": { + "lattice_denominator": 1, + "nodes": 5 + }, + "evaluation": { + "coefficient_operations": 3 + }, + "storage": { + "certificate_bytes": 864, + "source_bytes": 1409 + } + }, + "dependencies": { + "request_count": 4, + "weight_count": 2, + "weights": [ + "0", + "32" + ] + }, + "replay_status": "verified", + "status": "evaluated", + "wall_time_ms": { + "authority": "non-authoritative", + "evaluation_median": 0.367427, + "evaluation_samples": [ + 0.800185, + 0.367427, + 0.390012, + 0.350352, + 0.340708 + ], + "replay_median": 0.411535, + "replay_samples": [ + 0.411535, + 0.358484, + 0.460118, + 0.346737, + 0.443814 + ] + } + }, + "case_id": "p2-weight32-log-cancellation", + "coefficient": "-1/32", + "expanded_term_count": 1, + "materialized_window": { + "maximum_source_weight": 32, + "minimum_weight": 0, + "weight_count": 33 + }, + "method": "same-information-truncated-series-window", + "semantic_or_certificate_credit": false, + "source": { + "finite_terms": 32, + "nodes": 5 + }, + "status": "evaluated", + "wall_time_ms": { + "authority": "non-authoritative", + "median": 19.762397, + "samples": [ + 345.114878, + 19.762397, + 19.523384 + ] + } + }, + { + "candidate": { + "certificate_digest": "767f31f7a7db9a34007d26f1bc975284971c94072712d049a6a8257ff507aff2", + "coefficient": "exp(2)", + "costs": { + "compilation": { + "lattice_denominator": 1, + "nodes": 6 + }, + "evaluation": { + "coefficient_operations": 7 + }, + "storage": { + "certificate_bytes": 863, + "source_bytes": 321 + } + }, + "dependencies": { + "request_count": 8, + "weight_count": 2, + "weights": [ + "0", + "1" + ] + }, + "replay_status": "verified", + "status": "evaluated", + "wall_time_ms": { + "authority": "non-authoritative", + "evaluation_median": 0.171601, + "evaluation_samples": [ + 0.372665, + 0.176819, + 0.171601, + 0.15775, + 0.158731 + ], + "replay_median": 0.183619, + "replay_samples": [ + 0.212974, + 0.183619, + 0.170439, + 0.166212, + 0.215077 + ] + } + }, + "case_id": "p3-completed-exp-composition", + "coefficient": "exp(2)", + "expanded_term_count": 1, + "materialized_window": { + "maximum_source_weight": 1, + "minimum_weight": 0, + "weight_count": 2 + }, + "method": "same-information-truncated-series-window", + "semantic_or_certificate_credit": false, + "source": { + "finite_terms": 2, + "nodes": 6 + }, + "status": "evaluated", + "wall_time_ms": { + "authority": "non-authoritative", + "median": 14.457141, + "samples": [ + 38.627462, + 14.161853, + 14.457141 + ] + } + }, + { + "candidate": { + "certificate_digest": "e2c43ede3614378731d7912372f0caf898b99bd28b3adca9ab8ce18cce746ad4", + "coefficient": "1/3", + "costs": { + "compilation": { + "lattice_denominator": 1, + "nodes": 9 + }, + "evaluation": { + "coefficient_operations": 111 + }, + "storage": { + "certificate_bytes": 888, + "source_bytes": 656 + } + }, + "dependencies": { + "request_count": 29, + "weight_count": 8, + "weights": [ + "0", + "1", + "2", + "3", + "4", + "5", + "6", + "7" + ] + }, + "replay_status": "verified", + "status": "evaluated", + "wall_time_ms": { + "authority": "non-authoritative", + "evaluation_median": 0.756729, + "evaluation_samples": [ + 0.942271, + 0.79688, + 0.756729, + 0.714055, + 0.685521 + ], + "replay_median": 0.757601, + "replay_samples": [ + 0.757601, + 0.873737, + 0.706223, + 0.727485, + 0.83628 + ] + } + }, + "case_id": "heldout-mixed-log-exp-weight7", + "coefficient": "1/3", + "expanded_term_count": 1, + "materialized_window": { + "maximum_source_weight": 7, + "minimum_weight": 0, + "weight_count": 8 + }, + "method": "same-information-truncated-series-window", + "semantic_or_certificate_credit": false, + "source": { + "finite_terms": 9, + "nodes": 9 + }, + "status": "evaluated", + "wall_time_ms": { + "authority": "non-authoritative", + "median": 13.626651, + "samples": [ + 115.991861, + 13.02016, + 13.626651 + ] + } + } + ], + "contract": "BASELINE_CONTRACT.json", + "engine": "SymPy 1.14.0", + "schema": "process-geometry/am-weight-observed-baselines/v0" +} diff --git a/workstreams/am_weight_compiler/POST_REVEAL_MANIFEST.sha256 b/workstreams/am_weight_compiler/POST_REVEAL_MANIFEST.sha256 new file mode 100644 index 00000000..bfe393d7 --- /dev/null +++ b/workstreams/am_weight_compiler/POST_REVEAL_MANIFEST.sha256 @@ -0,0 +1,12 @@ +9c5a5c9b0a35e945f00de2a59de4a320b57cd7dced2d28e1f201832b90317ccb PRE_REVEAL_SOURCE_MANIFEST.sha256 +7aa05505f23d457839f2d0d5b87237334b723df61e8b4a0375368c1dad9f1ddc HELD_OUT_REVEAL.json +54ec807fb6f5a69fd2376d6e62cbbcfc21b1578341219189d2cb8a844e64c0b1 HELD_OUT_RESULT.json +6b9e55f3c3dcbce7cea8fbba13a39b63467a7981c0203fdf8e9970bef279b237 PUBLIC_RESULT.json +b46ef0831c0c22212eb26286ccb26cda9ebd80ba9b5318a172bdefcb5678fc33 OBSERVED_BASELINES.json +5d94207ba90fd0984a8bd84d3babaa4a8c488fc0c81150558637337a7e0e475f RESEARCH_DISPOSITION.json +f4ccc7da845ac09e98690a7ab23571608250b01a177d5bb9180d47fcaee729ba run_heldout.py +08820feebb2957d454356b059cf6b5a7a69ca5bdf5fcda649b8c3ac7794e6809 run_baselines.py +aaf489f618e9556abba5bb4c76fa7def5709e251e26a5c755ae10bab5c1e76f9 tests/test_heldout_reveal.py +74310197bf17b71bba4b07a18e198b69cfee9f72723dc079a124ea7194358dcc tests/test_stored_results.py +d0aca46d0f1b04a5cfc96c7de0fdcbb2d4e03114330e0b110fe12840974efe21 ../../sonnet/am-power-weight-compiler/01-results.md +23a7862672dcb702c6ab8451bf611444b8693939c9cdf485c2492d84ff26dbbf ../../sonnet/README.md diff --git a/workstreams/am_weight_compiler/PRE_REVEAL_SOURCE_MANIFEST.sha256 b/workstreams/am_weight_compiler/PRE_REVEAL_SOURCE_MANIFEST.sha256 new file mode 100644 index 00000000..b3a839c8 --- /dev/null +++ b/workstreams/am_weight_compiler/PRE_REVEAL_SOURCE_MANIFEST.sha256 @@ -0,0 +1,18 @@ +c66853b705acc3d73d8da9b8f0ffb323f5269b87514b849c7d91aedd6783c0a8 FROZEN_CONTRACT.json +243320c2b2f29101435fb69099277e67a72c1c2ff52a1499a6a1386b7d8ee337 PUBLIC_CORPUS.json +342c159f372272f72879cd9e4160526a95eb459b2483b1ba02c12a8065665345 SCORING.json +f426853b2b1da5d5f2e874c6d5ebdc19bd9b014ea80f0fbd7081747d1847ea83 BASELINE_CONTRACT.json +aa013e9cf5d9731f46ad21fa14cad51b3357b51456aa8a00cc77b47390a2b70f HELD_OUT_COMMITMENT.json +e1d3c828c6c854448a5d19e4731fff68a403812f8103065c7509a50918b6e9b9 README.md +8c0e9cacf11a6706f04e8b1481bfc400808d575eca227dad9239ecde8ef9953e pyproject.toml +6bf30ffd028c75394b5cd0d5f3e06497f4a4c7f43f5a0929a71afea500c8517c run_corpus.py +24c6fc66e11303f52727737670fe827219d46ab71a7ce4fac7a6c21e9cc43dfb am_weight_compiler/__init__.py +15807c7c65b078d38012dab90682d6388abf3be2c870fa5c8aeb8ca6d813834d am_weight_compiler/model.py +e1b731e5c0d75211eaceb308492a370269c3cee9ba6af1aae766d6aea619d6c0 am_weight_compiler/native.py +935054aef927b123bd4ab058871d317e337190e050da2533e09d3fa82c74a7f3 am_weight_compiler/coefficients.py +af0db89afee801fe60b85d8e18e375e6714466a927d25d1580934f05e6553dbb am_weight_compiler/evaluator.py +704ed359b4a80a9ccedb79ea28ed8367c2a5bbde95a7a10e8ccd07a6e63ad365 am_weight_compiler/replay.py +236bf5327a3d57f7382a0c695cc4f783d68cddc8b11b4de1a35bf5de672d708b am_weight_compiler/corpus.py +fdca0d1d42f97ead54fe41a8fd9137f3972af43eb4cc0e78bd902b23784f9ac9 tests/test_compiler.py +ea988aaa40c05b7f53e3c4cafe9b7e9bd66d1ac3c244276f6d705c21383efd74 tests/test_corpus.py +3ead22aa6ac7b35f71bd3300da9ab8d1050d4a2a393c2101bdae249505d3cd2c ../../tests/test_am_weight_compiler_workstream.py diff --git a/workstreams/am_weight_compiler/PUBLIC_CORPUS.json b/workstreams/am_weight_compiler/PUBLIC_CORPUS.json new file mode 100644 index 00000000..1ebe2913 --- /dev/null +++ b/workstreams/am_weight_compiler/PUBLIC_CORPUS.json @@ -0,0 +1,427 @@ +{ + "schema": "process-geometry/am-weight-corpus/v0", + "context": { + "lattice_step": "1", + "positive_cone": true, + "coefficient_domain": "Q[exp(Q)]" + }, + "cases": [ + { + "id": "p1-native-am-laws", + "kind": "native-laws", + "left": { + "basis": "power-weight", + "nu": 3, + "weight": "5", + "coefficient": "2" + }, + "right": { + "basis": "power-weight", + "nu": -1, + "weight": "2", + "coefficient": "3" + }, + "pbw": { + "source": { + "basis": "power-weight", + "nu": 4, + "weight": "7", + "coefficient": "1" + }, + "m": 2, + "n": 3 + }, + "finite_relation": { + "translation": "2", + "scale": "3" + }, + "expected": { + "status": "evaluated", + "product": { + "nu": 2, + "weight": "7", + "coefficient": "6" + }, + "A_left": { + "nu": 2, + "weight": "4", + "coefficient": "6" + }, + "M_left": { + "nu": 3, + "weight": "5", + "coefficient": "10" + }, + "pbw": true, + "finite_relation": true + } + }, + { + "id": "p2-weight32-log-cancellation", + "kind": "coefficient", + "target_weight": "0", + "expression": { + "op": "shift", + "by": "-32", + "argument": { + "op": "add", + "arguments": [ + { + "op": "log1p", + "argument": { + "op": "finite", + "terms": [ + { + "weight": "1", + "coefficient": "1" + } + ] + } + }, + { + "op": "finite", + "terms": [ + { + "weight": "1", + "coefficient": "-1" + }, + { + "weight": "2", + "coefficient": "1/2" + }, + { + "weight": "3", + "coefficient": "-1/3" + }, + { + "weight": "4", + "coefficient": "1/4" + }, + { + "weight": "5", + "coefficient": "-1/5" + }, + { + "weight": "6", + "coefficient": "1/6" + }, + { + "weight": "7", + "coefficient": "-1/7" + }, + { + "weight": "8", + "coefficient": "1/8" + }, + { + "weight": "9", + "coefficient": "-1/9" + }, + { + "weight": "10", + "coefficient": "1/10" + }, + { + "weight": "11", + "coefficient": "-1/11" + }, + { + "weight": "12", + "coefficient": "1/12" + }, + { + "weight": "13", + "coefficient": "-1/13" + }, + { + "weight": "14", + "coefficient": "1/14" + }, + { + "weight": "15", + "coefficient": "-1/15" + }, + { + "weight": "16", + "coefficient": "1/16" + }, + { + "weight": "17", + "coefficient": "-1/17" + }, + { + "weight": "18", + "coefficient": "1/18" + }, + { + "weight": "19", + "coefficient": "-1/19" + }, + { + "weight": "20", + "coefficient": "1/20" + }, + { + "weight": "21", + "coefficient": "-1/21" + }, + { + "weight": "22", + "coefficient": "1/22" + }, + { + "weight": "23", + "coefficient": "-1/23" + }, + { + "weight": "24", + "coefficient": "1/24" + }, + { + "weight": "25", + "coefficient": "-1/25" + }, + { + "weight": "26", + "coefficient": "1/26" + }, + { + "weight": "27", + "coefficient": "-1/27" + }, + { + "weight": "28", + "coefficient": "1/28" + }, + { + "weight": "29", + "coefficient": "-1/29" + }, + { + "weight": "30", + "coefficient": "1/30" + }, + { + "weight": "31", + "coefficient": "-1/31" + } + ] + } + ] + } + }, + "expected": { + "status": "evaluated", + "coefficient": "-1/32", + "maximum_visited_weights": 8 + } + }, + { + "id": "p3-completed-exp-composition", + "kind": "coefficient", + "target_weight": "0", + "expression": { + "op": "exp", + "argument": { + "op": "shift", + "by": "-1", + "argument": { + "op": "add", + "arguments": [ + { + "op": "exp", + "argument": { + "op": "finite", + "terms": [ + { + "weight": "1", + "coefficient": "2" + } + ] + } + }, + { + "op": "finite", + "terms": [ + { + "weight": "0", + "coefficient": "-1" + } + ] + } + ] + } + } + }, + "expected": { + "status": "evaluated", + "coefficient": "exp(2)", + "maximum_visited_weights": 12 + } + }, + { + "id": "p4-A-resonance-extension", + "kind": "primitive", + "generator": "A", + "term": { + "basis": "power-weight", + "nu": -1, + "weight": "2", + "coefficient": "1" + }, + "extension_policy": "allow-typed", + "expected": { + "status": "evaluated", + "extension": "log-a", + "domain_witness": "a>0" + } + }, + { + "id": "p4-M-resonance-extension", + "kind": "primitive", + "generator": "M", + "term": { + "basis": "power-weight", + "nu": 2, + "weight": "0", + "coefficient": "1" + }, + "extension_policy": "allow-typed", + "expected": { + "status": "evaluated", + "extension": "v-jordan" + } + }, + { + "id": "p5-paired-basis-canonicalization", + "kind": "paired", + "left": { + "basis": "power-weight", + "nu": 3, + "weight": "5", + "coefficient": "7/2" + }, + "right": { + "basis": "power-character", + "nu": 3, + "character": "2", + "coefficient": "7/2" + }, + "expected": { + "status": "evaluated", + "same_canonical_term": true + } + }, + { + "id": "n1-completion-without-cone", + "kind": "coefficient", + "target_weight": "1", + "context_override": { + "positive_cone": false + }, + "expression": { + "op": "log1p", + "argument": { + "op": "finite", + "terms": [ + { + "weight": "1", + "coefficient": "1" + } + ] + } + }, + "expected": { + "status": "unsupported", + "failure": "positive-cone-required" + } + }, + { + "id": "n2-negative-completion-input", + "kind": "coefficient", + "target_weight": "1", + "expression": { + "op": "log1p", + "argument": { + "op": "finite", + "terms": [ + { + "weight": "-1", + "coefficient": "1" + } + ] + } + }, + "expected": { + "status": "unsupported", + "failure": "completion-input-not-positive" + } + }, + { + "id": "n3-lattice-denominator-budget", + "kind": "coefficient", + "target_weight": "1", + "expression": { + "op": "finite", + "terms": [ + { + "weight": "1/29", + "coefficient": "1" + } + ] + }, + "expected": { + "status": "resource_exceeded", + "failure": "lattice-denominator-budget-exceeded" + } + }, + { + "id": "n4-target-weight-budget", + "kind": "coefficient", + "target_weight": "300", + "expression": { + "op": "finite", + "terms": [ + { + "weight": "1", + "coefficient": "1" + } + ] + }, + "expected": { + "status": "resource_exceeded", + "failure": "target-weight-budget-exceeded" + } + }, + { + "id": "n5-resonance-ordinary-only", + "kind": "primitive", + "generator": "A", + "term": { + "basis": "power-weight", + "nu": -1, + "weight": "2", + "coefficient": "1" + }, + "extension_policy": "ordinary-only", + "expected": { + "status": "unsupported", + "failure": "resonance-extension-required" + } + }, + { + "id": "n6-symbolic-height", + "kind": "coefficient", + "target_weight": "0", + "expression": { + "op": "symbolic-iterate", + "function": "exp", + "height_symbol": "h" + }, + "expected": { + "status": "unsupported", + "failure": "symbolic-height-outside-am-fragment" + } + } + ] +} diff --git a/workstreams/am_weight_compiler/PUBLIC_RESULT.json b/workstreams/am_weight_compiler/PUBLIC_RESULT.json new file mode 100644 index 00000000..dfa4e846 --- /dev/null +++ b/workstreams/am_weight_compiler/PUBLIC_RESULT.json @@ -0,0 +1,602 @@ +{ + "case_count": 12, + "corpus_schema": "process-geometry/am-weight-corpus/v0", + "pass_count": 12, + "passed": true, + "rows": [ + { + "case_id": "p1-native-am-laws", + "certificate": { + "case_id": "p1-native-am-laws", + "certificate_digest": "e1495534ffafbe12bd898d05b46b42194523a8b05fa62b1b34867db841032544", + "claim_scope": "frozen-rank-one-rational-completed-am-fragment", + "context_digest": "68afe2f989d0ad11054607890d6dd35172deb72016d0587466c6f2adada06f93", + "costs": { + "compilation": { + "lattice_denominator": 1, + "nodes": 4 + }, + "evaluation": { + "coefficient_operations": 0 + }, + "storage": { + "certificate_bytes": 944, + "source_bytes": 331 + } + }, + "dependencies": { + "request_count": 0, + "weight_count": 0, + "weights": [] + }, + "kind": "native-laws", + "observer": null, + "result": { + "A_left": { + "coefficient": "6", + "nu": 2, + "weight": "4" + }, + "M_left": { + "coefficient": "10", + "nu": 3, + "weight": "5" + }, + "finite_relation": true, + "pbw": true, + "product": { + "coefficient": "6", + "nu": 2, + "weight": "7" + } + }, + "schema": "process-geometry/am-weight-certificate/v0", + "semantic_carrier": "completed-am-power-weight/rank-one-rational/v0", + "source_digest": "1059eb117546ace735e9df37c1c90b499cf3930daefc5085252c71f615e32a9b", + "status": "evaluated" + }, + "passed": true, + "replay": { + "certificate_digest": "e1495534ffafbe12bd898d05b46b42194523a8b05fa62b1b34867db841032544", + "costs": { + "coefficient_operations": 0, + "dependency_requests": 0 + }, + "recomputed_digest": "e1495534ffafbe12bd898d05b46b42194523a8b05fa62b1b34867db841032544", + "replay_digest": "1d21332977a1601d15882f5f3df462ae71d25fa390f7e27c6752e4e232a6c2c4", + "status": "verified" + } + }, + { + "case_id": "p2-weight32-log-cancellation", + "certificate": { + "case_id": "p2-weight32-log-cancellation", + "certificate_digest": "88f325cd067bf587cb91d78c3809467ae28f442b01d01bd6ff79b2b6c4fae91a", + "claim_scope": "frozen-rank-one-rational-completed-am-fragment", + "context_digest": "68afe2f989d0ad11054607890d6dd35172deb72016d0587466c6f2adada06f93", + "costs": { + "compilation": { + "lattice_denominator": 1, + "nodes": 5 + }, + "evaluation": { + "coefficient_operations": 3 + }, + "storage": { + "certificate_bytes": 864, + "source_bytes": 1409 + } + }, + "dependencies": { + "request_count": 4, + "weight_count": 2, + "weights": [ + "0", + "32" + ] + }, + "kind": "coefficient", + "observer": { + "residual": "weights-above-observer-horizon", + "target_weight": "0" + }, + "result": { + "coefficient": "-1/32" + }, + "schema": "process-geometry/am-weight-certificate/v0", + "semantic_carrier": "completed-am-power-weight/rank-one-rational/v0", + "source_digest": "3e36909bb3104d49f4734ba69cbbdae526611d4ffcbf98b5c571cd035b140e76", + "status": "evaluated" + }, + "passed": true, + "replay": { + "certificate_digest": "88f325cd067bf587cb91d78c3809467ae28f442b01d01bd6ff79b2b6c4fae91a", + "costs": { + "coefficient_operations": 3, + "dependency_requests": 4 + }, + "recomputed_digest": "88f325cd067bf587cb91d78c3809467ae28f442b01d01bd6ff79b2b6c4fae91a", + "replay_digest": "3c96431c123c2949d11d471b0416ec48ba8015c13dcfe62d712d7de74ffd2263", + "status": "verified" + } + }, + { + "case_id": "p3-completed-exp-composition", + "certificate": { + "case_id": "p3-completed-exp-composition", + "certificate_digest": "767f31f7a7db9a34007d26f1bc975284971c94072712d049a6a8257ff507aff2", + "claim_scope": "frozen-rank-one-rational-completed-am-fragment", + "context_digest": "68afe2f989d0ad11054607890d6dd35172deb72016d0587466c6f2adada06f93", + "costs": { + "compilation": { + "lattice_denominator": 1, + "nodes": 6 + }, + "evaluation": { + "coefficient_operations": 7 + }, + "storage": { + "certificate_bytes": 863, + "source_bytes": 321 + } + }, + "dependencies": { + "request_count": 8, + "weight_count": 2, + "weights": [ + "0", + "1" + ] + }, + "kind": "coefficient", + "observer": { + "residual": "weights-above-observer-horizon", + "target_weight": "0" + }, + "result": { + "coefficient": "exp(2)" + }, + "schema": "process-geometry/am-weight-certificate/v0", + "semantic_carrier": "completed-am-power-weight/rank-one-rational/v0", + "source_digest": "2bf105bcf6b202f3d01f11dfd722111fdb08a8fa8704afe290ff79873a976617", + "status": "evaluated" + }, + "passed": true, + "replay": { + "certificate_digest": "767f31f7a7db9a34007d26f1bc975284971c94072712d049a6a8257ff507aff2", + "costs": { + "coefficient_operations": 7, + "dependency_requests": 8 + }, + "recomputed_digest": "767f31f7a7db9a34007d26f1bc975284971c94072712d049a6a8257ff507aff2", + "replay_digest": "b1b1e285987a338347dc450388b073f02fed459dd54023d05242cba0d1691336", + "status": "verified" + } + }, + { + "case_id": "p4-A-resonance-extension", + "certificate": { + "case_id": "p4-A-resonance-extension", + "certificate_digest": "5ff981a955d485bf19142626108512efa4cd32baeb7399273cc775047d529b83", + "claim_scope": "frozen-rank-one-rational-completed-am-fragment", + "context_digest": "68afe2f989d0ad11054607890d6dd35172deb72016d0587466c6f2adada06f93", + "costs": { + "compilation": { + "lattice_denominator": 1, + "nodes": 1 + }, + "evaluation": { + "coefficient_operations": 0 + }, + "storage": { + "certificate_bytes": 809, + "source_bytes": 172 + } + }, + "dependencies": { + "request_count": 0, + "weight_count": 0, + "weights": [] + }, + "kind": "primitive", + "observer": null, + "result": { + "domain_witness": "a>0", + "extension": "log-a" + }, + "schema": "process-geometry/am-weight-certificate/v0", + "semantic_carrier": "completed-am-power-weight/rank-one-rational/v0", + "source_digest": "f348dbc1a1fa2e60aa55eb23419186ac60622b9180dd957bac009989ff5d74e4", + "status": "evaluated" + }, + "passed": true, + "replay": { + "certificate_digest": "5ff981a955d485bf19142626108512efa4cd32baeb7399273cc775047d529b83", + "costs": { + "coefficient_operations": 0, + "dependency_requests": 0 + }, + "recomputed_digest": "5ff981a955d485bf19142626108512efa4cd32baeb7399273cc775047d529b83", + "replay_digest": "4c6a4d6c3c8dda037fe63ed49c5de32c35328a248ccb17cc18c1f69b4d117fce", + "status": "verified" + } + }, + { + "case_id": "p4-M-resonance-extension", + "certificate": { + "case_id": "p4-M-resonance-extension", + "certificate_digest": "d9892e4de1769a860b2e007cbcaba8d24da454f18e96277518ef245ec26d8b83", + "claim_scope": "frozen-rank-one-rational-completed-am-fragment", + "context_digest": "68afe2f989d0ad11054607890d6dd35172deb72016d0587466c6f2adada06f93", + "costs": { + "compilation": { + "lattice_denominator": 1, + "nodes": 1 + }, + "evaluation": { + "coefficient_operations": 0 + }, + "storage": { + "certificate_bytes": 789, + "source_bytes": 171 + } + }, + "dependencies": { + "request_count": 0, + "weight_count": 0, + "weights": [] + }, + "kind": "primitive", + "observer": null, + "result": { + "extension": "v-jordan" + }, + "schema": "process-geometry/am-weight-certificate/v0", + "semantic_carrier": "completed-am-power-weight/rank-one-rational/v0", + "source_digest": "34e8526792b39c7bcdda5e316280b7f1151c71ca1125eded85dd2f827b02e5ff", + "status": "evaluated" + }, + "passed": true, + "replay": { + "certificate_digest": "d9892e4de1769a860b2e007cbcaba8d24da454f18e96277518ef245ec26d8b83", + "costs": { + "coefficient_operations": 0, + "dependency_requests": 0 + }, + "recomputed_digest": "d9892e4de1769a860b2e007cbcaba8d24da454f18e96277518ef245ec26d8b83", + "replay_digest": "bab4b31b4e48ae37f3e698567fb5baf7cdd783f5498d1c1b8e16b4c573769b0c", + "status": "verified" + } + }, + { + "case_id": "p5-paired-basis-canonicalization", + "certificate": { + "case_id": "p5-paired-basis-canonicalization", + "certificate_digest": "7b7a97a0ec0e7679aa0dcf96ede00602122adf1b9f1464abbea3dc065ee86194", + "claim_scope": "frozen-rank-one-rational-completed-am-fragment", + "context_digest": "68afe2f989d0ad11054607890d6dd35172deb72016d0587466c6f2adada06f93", + "costs": { + "compilation": { + "lattice_denominator": 1, + "nodes": 2 + }, + "evaluation": { + "coefficient_operations": 0 + }, + "storage": { + "certificate_bytes": 798, + "source_bytes": 208 + } + }, + "dependencies": { + "request_count": 0, + "weight_count": 0, + "weights": [] + }, + "kind": "paired", + "observer": null, + "result": { + "same_canonical_term": true + }, + "schema": "process-geometry/am-weight-certificate/v0", + "semantic_carrier": "completed-am-power-weight/rank-one-rational/v0", + "source_digest": "321119011741d148619abc25bbf5d1e6fb0d1e09a636ba48d8b1c855c97a10d0", + "status": "evaluated" + }, + "passed": true, + "replay": { + "certificate_digest": "7b7a97a0ec0e7679aa0dcf96ede00602122adf1b9f1464abbea3dc065ee86194", + "costs": { + "coefficient_operations": 0, + "dependency_requests": 0 + }, + "recomputed_digest": "7b7a97a0ec0e7679aa0dcf96ede00602122adf1b9f1464abbea3dc065ee86194", + "replay_digest": "1bc93f037046d905697b019ccbccb8dfbd28a84c71149d8f41922f4e9f09a5cc", + "status": "verified" + } + }, + { + "case_id": "n1-completion-without-cone", + "certificate": { + "case_id": "n1-completion-without-cone", + "certificate_digest": "e286792fa7185023f7550ddd74945364d33dbea8c37c823979c1c956335e0638", + "claim_scope": "frozen-rank-one-rational-completed-am-fragment", + "context_digest": "7d6df28354fb4a5dc34d991c992884d4f857deada5ca34f7df0f3c2fde7b9cc7", + "costs": { + "compilation": { + "lattice_denominator": 1, + "nodes": 0 + }, + "evaluation": { + "coefficient_operations": 0 + }, + "storage": { + "certificate_bytes": 807, + "source_bytes": 217 + } + }, + "dependencies": { + "request_count": 0, + "weight_count": 0, + "weights": [] + }, + "kind": "coefficient", + "observer": null, + "result": { + "failure": "positive-cone-required" + }, + "schema": "process-geometry/am-weight-certificate/v0", + "semantic_carrier": "completed-am-power-weight/rank-one-rational/v0", + "source_digest": "4281c3daf9204738b0f8af29ac421e96ac9d5382c09901e5d4f393b10277c7ee", + "status": "unsupported" + }, + "passed": true, + "replay": { + "certificate_digest": "e286792fa7185023f7550ddd74945364d33dbea8c37c823979c1c956335e0638", + "costs": { + "coefficient_operations": 0, + "dependency_requests": 0 + }, + "recomputed_digest": "e286792fa7185023f7550ddd74945364d33dbea8c37c823979c1c956335e0638", + "replay_digest": "607fe5be7967c3bf4eaea6ab10aa2979371018420f95e23ebca0583ce5eaca17", + "status": "verified" + } + }, + { + "case_id": "n2-negative-completion-input", + "certificate": { + "case_id": "n2-negative-completion-input", + "certificate_digest": "154b80a467582d2b19a42b31b12010ccbe305d676100b1abc105bbb3b2ed4e8f", + "claim_scope": "frozen-rank-one-rational-completed-am-fragment", + "context_digest": "68afe2f989d0ad11054607890d6dd35172deb72016d0587466c6f2adada06f93", + "costs": { + "compilation": { + "lattice_denominator": 1, + "nodes": 0 + }, + "evaluation": { + "coefficient_operations": 0 + }, + "storage": { + "certificate_bytes": 816, + "source_bytes": 177 + } + }, + "dependencies": { + "request_count": 0, + "weight_count": 0, + "weights": [] + }, + "kind": "coefficient", + "observer": null, + "result": { + "failure": "completion-input-not-positive" + }, + "schema": "process-geometry/am-weight-certificate/v0", + "semantic_carrier": "completed-am-power-weight/rank-one-rational/v0", + "source_digest": "fa1ea4d7f3aa636e3d95677cee953b2541626fcf1bf798292d8951c42b62d10d", + "status": "unsupported" + }, + "passed": true, + "replay": { + "certificate_digest": "154b80a467582d2b19a42b31b12010ccbe305d676100b1abc105bbb3b2ed4e8f", + "costs": { + "coefficient_operations": 0, + "dependency_requests": 0 + }, + "recomputed_digest": "154b80a467582d2b19a42b31b12010ccbe305d676100b1abc105bbb3b2ed4e8f", + "replay_digest": "8e499b17d97ef50b6c67d59f2a43f82507178434e01c11f868dd5ff57da11f57", + "status": "verified" + } + }, + { + "case_id": "n3-lattice-denominator-budget", + "certificate": { + "case_id": "n3-lattice-denominator-budget", + "certificate_digest": "ae99481cf7a3618ef6c87aff3402fba51e611dc776036b4540a0f74eaa1e2ae0", + "claim_scope": "frozen-rank-one-rational-completed-am-fragment", + "context_digest": "68afe2f989d0ad11054607890d6dd35172deb72016d0587466c6f2adada06f93", + "costs": { + "compilation": { + "lattice_denominator": 1, + "nodes": 0 + }, + "evaluation": { + "coefficient_operations": 0 + }, + "storage": { + "certificate_bytes": 829, + "source_bytes": 154 + } + }, + "dependencies": { + "request_count": 0, + "weight_count": 0, + "weights": [] + }, + "kind": "coefficient", + "observer": null, + "result": { + "failure": "lattice-denominator-budget-exceeded" + }, + "schema": "process-geometry/am-weight-certificate/v0", + "semantic_carrier": "completed-am-power-weight/rank-one-rational/v0", + "source_digest": "8f278f223561b44d47edc50a6a30fd15b1b521c5c0936cc5fedca037082a7dad", + "status": "resource_exceeded" + }, + "passed": true, + "replay": { + "certificate_digest": "ae99481cf7a3618ef6c87aff3402fba51e611dc776036b4540a0f74eaa1e2ae0", + "costs": { + "coefficient_operations": 0, + "dependency_requests": 0 + }, + "recomputed_digest": "ae99481cf7a3618ef6c87aff3402fba51e611dc776036b4540a0f74eaa1e2ae0", + "replay_digest": "1af829ab153aab0ec169c1a8c541f96f07d1a6037913b95777fae247a604c2d6", + "status": "verified" + } + }, + { + "case_id": "n4-target-weight-budget", + "certificate": { + "case_id": "n4-target-weight-budget", + "certificate_digest": "be95eeef35675c4244cd1d1304b1f639a68fc32facb3dab4b49ebe3834cd3fb8", + "claim_scope": "frozen-rank-one-rational-completed-am-fragment", + "context_digest": "68afe2f989d0ad11054607890d6dd35172deb72016d0587466c6f2adada06f93", + "costs": { + "compilation": { + "lattice_denominator": 1, + "nodes": 0 + }, + "evaluation": { + "coefficient_operations": 0 + }, + "storage": { + "certificate_bytes": 817, + "source_bytes": 147 + } + }, + "dependencies": { + "request_count": 0, + "weight_count": 0, + "weights": [] + }, + "kind": "coefficient", + "observer": null, + "result": { + "failure": "target-weight-budget-exceeded" + }, + "schema": "process-geometry/am-weight-certificate/v0", + "semantic_carrier": "completed-am-power-weight/rank-one-rational/v0", + "source_digest": "1333dfb3832577e8047a7a710da312221213d75c1215138e7a859acdda61a8c7", + "status": "resource_exceeded" + }, + "passed": true, + "replay": { + "certificate_digest": "be95eeef35675c4244cd1d1304b1f639a68fc32facb3dab4b49ebe3834cd3fb8", + "costs": { + "coefficient_operations": 0, + "dependency_requests": 0 + }, + "recomputed_digest": "be95eeef35675c4244cd1d1304b1f639a68fc32facb3dab4b49ebe3834cd3fb8", + "replay_digest": "9a30cdbbb911a6d90169850cc7ad25dada0ae77b478d235f4a1a189430c497df", + "status": "verified" + } + }, + { + "case_id": "n5-resonance-ordinary-only", + "certificate": { + "case_id": "n5-resonance-ordinary-only", + "certificate_digest": "cbe7cbc546f53d714596a3bed40a704998ca545a542430af60f499099c2fac62", + "claim_scope": "frozen-rank-one-rational-completed-am-fragment", + "context_digest": "68afe2f989d0ad11054607890d6dd35172deb72016d0587466c6f2adada06f93", + "costs": { + "compilation": { + "lattice_denominator": 1, + "nodes": 0 + }, + "evaluation": { + "coefficient_operations": 0 + }, + "storage": { + "certificate_bytes": 811, + "source_bytes": 176 + } + }, + "dependencies": { + "request_count": 0, + "weight_count": 0, + "weights": [] + }, + "kind": "primitive", + "observer": null, + "result": { + "failure": "resonance-extension-required" + }, + "schema": "process-geometry/am-weight-certificate/v0", + "semantic_carrier": "completed-am-power-weight/rank-one-rational/v0", + "source_digest": "19d4623a753ee9c2cf605699303092e78fc8f4023493ab4c64bda4c57b9eb60a", + "status": "unsupported" + }, + "passed": true, + "replay": { + "certificate_digest": "cbe7cbc546f53d714596a3bed40a704998ca545a542430af60f499099c2fac62", + "costs": { + "coefficient_operations": 0, + "dependency_requests": 0 + }, + "recomputed_digest": "cbe7cbc546f53d714596a3bed40a704998ca545a542430af60f499099c2fac62", + "replay_digest": "d589c7b897fd916697bfbfff0dc68e3f2ec04b7a6de27ba6982f86f6ca9be29a", + "status": "verified" + } + }, + { + "case_id": "n6-symbolic-height", + "certificate": { + "case_id": "n6-symbolic-height", + "certificate_digest": "1cb9d266425af8e3872511065f786481109cc513e5f1c055e68d4a1dee97865c", + "claim_scope": "frozen-rank-one-rational-completed-am-fragment", + "context_digest": "68afe2f989d0ad11054607890d6dd35172deb72016d0587466c6f2adada06f93", + "costs": { + "compilation": { + "lattice_denominator": 1, + "nodes": 0 + }, + "evaluation": { + "coefficient_operations": 0 + }, + "storage": { + "certificate_bytes": 812, + "source_bytes": 144 + } + }, + "dependencies": { + "request_count": 0, + "weight_count": 0, + "weights": [] + }, + "kind": "coefficient", + "observer": null, + "result": { + "failure": "symbolic-height-outside-am-fragment" + }, + "schema": "process-geometry/am-weight-certificate/v0", + "semantic_carrier": "completed-am-power-weight/rank-one-rational/v0", + "source_digest": "538c3db4138ea37487f5ea255cdf2e8b87ec2ffb7f849ac8c9cbefd389b32d58", + "status": "unsupported" + }, + "passed": true, + "replay": { + "certificate_digest": "1cb9d266425af8e3872511065f786481109cc513e5f1c055e68d4a1dee97865c", + "costs": { + "coefficient_operations": 0, + "dependency_requests": 0 + }, + "recomputed_digest": "1cb9d266425af8e3872511065f786481109cc513e5f1c055e68d4a1dee97865c", + "replay_digest": "ded372b8ceb0ed49cebd5c274347f9c0b17c6b184fe165bb501f723663546f6b", + "status": "verified" + } + } + ], + "schema": "process-geometry/am-weight-corpus-result/v0" +} diff --git a/workstreams/am_weight_compiler/README.md b/workstreams/am_weight_compiler/README.md new file mode 100644 index 00000000..2588de58 --- /dev/null +++ b/workstreams/am_weight_compiler/README.md @@ -0,0 +1,38 @@ +# AM weight compiler workstream + +Research-local implementation for issue #146. + +This workstream treats the completed AM power--weight algebra as the semantic +carrier. Finite coefficient windows, matrices, or jets may be generated only +after an observer is declared. The native AM frame is not identified with the +finite-LE `N/t` chart. + +The contract, public corpus, budgets, baseline, scoring, and hidden commitment +freeze before compiler source. No general `series()` or `limit()` call is +allowed in compiler or replay. + +No multivariable AM, higher arithmetic rank, transseries, hyperseries, +surreal, symbolic-height, Public API, Core, or Theory Map promotion is +authorized. + +## Executable gate + +The research-local package implements: + +- exact native `power-weight` and `power-character` canonicalization; +- the product, `A`, `M`, PBW, and finite affine laws; +- exact coefficients in the finite group algebra `Q[exp(Q)]`; +- observer-directed `add`, `multiply`, `scale`, `shift`, `exp`, and `log1p`; +- typed `log-a` and `v-jordan` resonance witnesses; +- compact deterministic certificates and full semantic replay. + +Run the frozen public gate with: + +```console +python run_corpus.py +python -m pytest -q +``` + +The evaluator deliberately records dependency slices rather than completed +series windows. SymPy is reserved for the separately declared, +non-authoritative same-information baseline. diff --git a/workstreams/am_weight_compiler/RESEARCH_DISPOSITION.json b/workstreams/am_weight_compiler/RESEARCH_DISPOSITION.json new file mode 100644 index 00000000..feeb1737 --- /dev/null +++ b/workstreams/am_weight_compiler/RESEARCH_DISPOSITION.json @@ -0,0 +1,21 @@ +{ + "schema": "process-geometry/am-weight-disposition/v0", + "disposition": "EXPAND", + "basis": [ + "all 12 frozen public cases pass and replay", + "the precommitted held-out payload verifies and returns the exact coefficient 1/3", + "the held-out certificate replays with 29 dependency requests over 8 weights and 111 exact coefficient operations", + "the weight-32 cancellation case reads 2 weights versus the baseline's declared 33-weight materialized window", + "native AM laws, paired encodings, completion domains, and both typed resonances have executable semantics" + ], + "claim_allowed": "The frozen rank-one rational completed AM fragment has exact observer-directed coefficient semantics with deterministic replay.", + "claims_forbidden": [ + "general computational advantage over computer algebra systems", + "a general AM function theory", + "multivariable or higher-rank AM completion", + "a surreal or transseries runtime result", + "an identification of jets or matrices with the semantic carrier" + ], + "economy_assessment": "Workload-specific dependency advantage is demonstrated for sparse distant readout; P3 and the held-out case materialize the same number of distinct weights as the declared baseline. Wall-time measurements are non-authoritative.", + "next_gate": "Freeze a separate AM goal front-end and transport corpus that translates existing mathematical vignettes into this carrier without changing the validated evaluator." +} diff --git a/workstreams/am_weight_compiler/SCORING.json b/workstreams/am_weight_compiler/SCORING.json new file mode 100644 index 00000000..f054d0af --- /dev/null +++ b/workstreams/am_weight_compiler/SCORING.json @@ -0,0 +1,25 @@ +{ + "schema": "process-geometry/am-weight-scoring/v0", + "acceptance": [ + "all native AM laws replay exactly", + "P2 and P3 use observer-directed dependencies without generic series or limit", + "both resonance extensions are typed", + "paired encodings canonicalize", + "all negatives fail closed", + "held-out passes after remote source freeze", + "default CI remains seconds-scale" + ], + "dispositions": { + "EXPAND": "reusable AM weight task family gains replayable semantics or a material dependency/support/certificate advantage", + "NARROW": "native laws work but completion or transport remains too restricted", + "ELIMINATE": "no capability beyond a certificate wrapper around the same-information baseline", + "STOP": "answer leakage, opaque oracle, post-reveal change, or uneconomic full traces" + }, + "economy_claim_requires": [ + "declared workload", + "same-information baseline", + "compilation and replay costs", + "support and certificate measurements", + "reproducible material advantage" + ] +} diff --git a/workstreams/am_weight_compiler/am_weight_compiler/__init__.py b/workstreams/am_weight_compiler/am_weight_compiler/__init__.py new file mode 100644 index 00000000..21c35f5e --- /dev/null +++ b/workstreams/am_weight_compiler/am_weight_compiler/__init__.py @@ -0,0 +1,14 @@ +"""Research-local completed AM power-weight compiler.""" + +from .corpus import run_corpus +from .evaluator import evaluate_case +from .model import Budgets, ExpQCoefficient +from .replay import replay_certificate + +__all__ = [ + "Budgets", + "ExpQCoefficient", + "evaluate_case", + "replay_certificate", + "run_corpus", +] diff --git a/workstreams/am_weight_compiler/am_weight_compiler/coefficients.py b/workstreams/am_weight_compiler/am_weight_compiler/coefficients.py new file mode 100644 index 00000000..ec2a0a14 --- /dev/null +++ b/workstreams/am_weight_compiler/am_weight_compiler/coefficients.py @@ -0,0 +1,324 @@ +from __future__ import annotations + +from fractions import Fraction +from math import factorial +from typing import Any, Mapping, Sequence + +from .model import ( + Budgets, + EvaluationFailure, + ExpQCoefficient, + Meter, + digest_json, + lcm, + parse_fraction, +) + + +Expr = Mapping[str, Any] + + +class WeightEvaluator: + """Demand-driven exact coefficients in one normalized rational weight lattice.""" + + def __init__( + self, + expression: Expr, + target: Fraction, + context: Mapping[str, object], + budgets: Budgets, + ) -> None: + self.expression = expression + self.target = target + self.context = context + self.budgets = budgets + self.meter = Meter(budgets) + self._keys: dict[int, str] = {} + self._minimum_cache: dict[int, Fraction] = {} + self._coefficient_cache: dict[tuple[int, Fraction], ExpQCoefficient] = {} + self._validate_syntax(expression) + self.lattice_denominator = self._lattice_denominator(expression, target) + if self.lattice_denominator > budgets.max_lattice_denominator: + raise EvaluationFailure( + "resource_exceeded", "lattice-denominator-budget-exceeded" + ) + if abs(target) > budgets.max_target_weight: + raise EvaluationFailure("resource_exceeded", "target-weight-budget-exceeded") + + def coefficient(self) -> ExpQCoefficient: + return self._coefficient(self.expression, self.target) + + def _node_key(self, node: Expr) -> str: + identity = id(node) + if identity not in self._keys: + self._keys[identity] = digest_json(node)[:16] + return self._keys[identity] + + def _validate_syntax(self, node: Expr) -> None: + self.meter.nodes += 1 + if self.meter.nodes > self.budgets.max_nodes: + raise EvaluationFailure("resource_exceeded", "node-budget-exceeded") + op = node.get("op") + if op == "finite": + terms = node.get("terms") + if not isinstance(terms, list): + raise EvaluationFailure("unsupported", "malformed-finite-series") + for term in terms: + if not isinstance(term, dict): + raise EvaluationFailure("unsupported", "malformed-finite-series") + parse_fraction(term.get("weight"), field="weight") + parse_fraction(term.get("coefficient"), field="coefficient") + return + if op in {"add", "multiply"}: + arguments = node.get("arguments") + if not isinstance(arguments, list) or len(arguments) < 2: + raise EvaluationFailure("unsupported", f"malformed-{op}") + for argument in arguments: + if not isinstance(argument, dict): + raise EvaluationFailure("unsupported", f"malformed-{op}") + self._validate_syntax(argument) + return + if op in {"shift", "scale"}: + argument = node.get("argument") + if not isinstance(argument, dict): + raise EvaluationFailure("unsupported", f"malformed-{op}") + parse_fraction(node.get("by" if op == "shift" else "coefficient")) + self._validate_syntax(argument) + return + if op in {"exp", "log1p"}: + argument = node.get("argument") + if not isinstance(argument, dict): + raise EvaluationFailure("unsupported", f"malformed-{op}") + self._validate_syntax(argument) + return + if op == "symbolic-iterate": + raise EvaluationFailure("unsupported", "symbolic-height-outside-am-fragment") + raise EvaluationFailure("unsupported", "unknown-expression-operation") + + def _collect_weights(self, node: Expr, weights: list[Fraction]) -> None: + op = node["op"] + if op == "finite": + weights.extend(parse_fraction(term["weight"]) for term in node["terms"]) + elif op in {"add", "multiply"}: + for argument in node["arguments"]: + self._collect_weights(argument, weights) + elif op == "shift": + weights.append(parse_fraction(node["by"])) + self._collect_weights(node["argument"], weights) + elif op in {"scale", "exp", "log1p"}: + self._collect_weights(node["argument"], weights) + + def _lattice_denominator(self, node: Expr, target: Fraction) -> int: + weights = [target] + self._collect_weights(node, weights) + denominator = 1 + for weight in weights: + denominator = lcm(denominator, weight.denominator) + return denominator + + def _index(self, weight: Fraction) -> int: + value = weight * self.lattice_denominator + if value.denominator != 1: + raise EvaluationFailure("unsupported", "weight-outside-normalized-lattice") + return value.numerator + + def _weight(self, index: int) -> Fraction: + return Fraction(index, self.lattice_denominator) + + def _minimum(self, node: Expr) -> Fraction: + identity = id(node) + cached = self._minimum_cache.get(identity) + if cached is not None: + return cached + op = node["op"] + if op == "finite": + nonzero = [ + parse_fraction(term["weight"]) + for term in node["terms"] + if parse_fraction(term["coefficient"]) + ] + value = min(nonzero) if nonzero else Fraction(0) + elif op == "add": + structural = min(self._minimum(argument) for argument in node["arguments"]) + start = self._index(structural) + horizon = start + self.budgets.max_target_weight * self.lattice_denominator + value = structural + for index in range(start, horizon + 1): + candidate = self._weight(index) + if not self._coefficient(node, candidate).is_zero: + value = candidate + break + elif op == "multiply": + value = sum((self._minimum(argument) for argument in node["arguments"]), Fraction(0)) + elif op == "scale": + scalar = parse_fraction(node["coefficient"]) + value = self._minimum(node["argument"]) if scalar else Fraction(0) + elif op == "shift": + value = parse_fraction(node["by"]) + self._minimum(node["argument"]) + elif op == "exp": + value = Fraction(0) + elif op == "log1p": + value = self._minimum(node["argument"]) + else: + raise EvaluationFailure("unsupported", "unknown-expression-operation") + self._minimum_cache[identity] = value + return value + + def _require_completion(self, node: Expr, *, strict: bool) -> None: + if not bool(self.context.get("positive_cone")): + raise EvaluationFailure("unsupported", "positive-cone-required") + minimum = self._minimum(node) + if minimum < 0 or (strict and minimum <= 0): + raise EvaluationFailure("unsupported", "completion-input-not-positive") + + def _finite_monomial(self, node: Expr) -> tuple[Fraction, Fraction] | None: + if node.get("op") != "finite": + return None + combined: dict[Fraction, Fraction] = {} + for term in node["terms"]: + weight = parse_fraction(term["weight"]) + coefficient = parse_fraction(term["coefficient"]) + combined[weight] = combined.get(weight, Fraction(0)) + coefficient + nonzero = [(weight, coefficient) for weight, coefficient in combined.items() if coefficient] + if len(nonzero) == 1 and nonzero[0][0] > 0: + return nonzero[0] + return None + + def _coefficient(self, node: Expr, weight: Fraction) -> ExpQCoefficient: + cache_key = (id(node), weight) + cached = self._coefficient_cache.get(cache_key) + if cached is not None: + return cached + self.meter.visit(self._node_key(node), weight) + op = node["op"] + if op == "finite": + total = Fraction(0) + for term in node["terms"]: + if parse_fraction(term["weight"]) == weight: + total += parse_fraction(term["coefficient"]) + self.meter.bump_operation() + result = ExpQCoefficient.rational(total) + elif op == "add": + result = ExpQCoefficient.zero() + for argument in node["arguments"]: + result = result + self._coefficient(argument, weight) + self.meter.bump_operation() + elif op == "scale": + result = self._coefficient(node["argument"], weight).scale_rational( + parse_fraction(node["coefficient"]) + ) + self.meter.bump_operation() + elif op == "shift": + result = self._coefficient( + node["argument"], weight - parse_fraction(node["by"]) + ) + elif op == "multiply": + result = self._product_coefficient(node["arguments"], weight) + elif op == "exp": + result = self._exp_coefficient(node["argument"], weight) + elif op == "log1p": + result = self._log1p_coefficient(node["argument"], weight) + else: + raise EvaluationFailure("unsupported", "unknown-expression-operation") + self._coefficient_cache[cache_key] = result + return result + + def _product_coefficient( + self, arguments: Sequence[Expr], target: Fraction + ) -> ExpQCoefficient: + if len(arguments) == 1: + return self._coefficient(arguments[0], target) + first = arguments[0] + rest = arguments[1:] + first_min = self._minimum(first) + rest_min = sum((self._minimum(argument) for argument in rest), Fraction(0)) + start = self._index(first_min) + stop = self._index(target - rest_min) + if stop < start: + return ExpQCoefficient.zero() + total = ExpQCoefficient.zero() + for index in range(start, stop + 1): + left_weight = self._weight(index) + left = self._coefficient(first, left_weight) + if left.is_zero: + continue + right = self._product_coefficient(rest, target - left_weight) + total = total + left * right + self.meter.bump_operation(2) + return total + + def _exp_coefficient(self, argument: Expr, weight: Fraction) -> ExpQCoefficient: + self._require_completion(argument, strict=False) + index = self._index(weight) + if index < 0: + return ExpQCoefficient.zero() + monomial = self._finite_monomial(argument) + if monomial is not None: + mono_weight, coefficient = monomial + mono_index = self._index(mono_weight) + if index % mono_index: + return ExpQCoefficient.zero() + exponent = index // mono_index + self.meter.bump_operation() + return ExpQCoefficient.rational(coefficient**exponent / factorial(exponent)) + constant = self._coefficient(argument, Fraction(0)) + if not constant.is_rational: + raise EvaluationFailure("unsupported", "non-rational-exp-constant") + if index == 0: + return ExpQCoefficient.exp_atom(constant.rational_value()) + total = ExpQCoefficient.zero() + for k in range(1, index + 1): + source = self._coefficient(argument, self._weight(k)) + if source.is_zero: + continue + prior = self._coefficient_for_exp(argument, index - k) + total = total + source.scale_rational(k) * prior + self.meter.bump_operation(3) + return total.divide_rational(index) + + def _coefficient_for_exp(self, argument: Expr, index: int) -> ExpQCoefficient: + key = (id(argument), "exp", index) + cached = getattr(self, "_exp_cache", {}).get(key) + if cached is not None: + return cached + if not hasattr(self, "_exp_cache"): + self._exp_cache: dict[tuple[object, ...], ExpQCoefficient] = {} + result = self._exp_coefficient(argument, self._weight(index)) + self._exp_cache[key] = result + return result + + def _log1p_coefficient(self, argument: Expr, weight: Fraction) -> ExpQCoefficient: + self._require_completion(argument, strict=True) + index = self._index(weight) + if index <= 0: + return ExpQCoefficient.zero() + monomial = self._finite_monomial(argument) + if monomial is not None: + mono_weight, coefficient = monomial + mono_index = self._index(mono_weight) + if index % mono_index: + return ExpQCoefficient.zero() + exponent = index // mono_index + sign = Fraction(1 if exponent % 2 else -1) + self.meter.bump_operation() + return ExpQCoefficient.rational(sign * coefficient**exponent / exponent) + total = self._coefficient(argument, weight).scale_rational(index) + for k in range(1, index): + source = self._coefficient(argument, self._weight(index - k)) + if source.is_zero: + continue + prior = self._coefficient_for_log1p(argument, k) + total = total - prior.scale_rational(k) * source + self.meter.bump_operation(3) + return total.divide_rational(index) + + def _coefficient_for_log1p(self, argument: Expr, index: int) -> ExpQCoefficient: + key = (id(argument), "log1p", index) + cached = getattr(self, "_log_cache", {}).get(key) + if cached is not None: + return cached + if not hasattr(self, "_log_cache"): + self._log_cache: dict[tuple[object, ...], ExpQCoefficient] = {} + result = self._log1p_coefficient(argument, self._weight(index)) + self._log_cache[key] = result + return result diff --git a/workstreams/am_weight_compiler/am_weight_compiler/corpus.py b/workstreams/am_weight_compiler/am_weight_compiler/corpus.py new file mode 100644 index 00000000..8a65d036 --- /dev/null +++ b/workstreams/am_weight_compiler/am_weight_compiler/corpus.py @@ -0,0 +1,57 @@ +from __future__ import annotations + +import json +from pathlib import Path +from typing import Any, Mapping + +from .evaluator import evaluate_case +from .model import Budgets +from .replay import replay_certificate + + +def _expected_matches(expected: Mapping[str, Any], certificate: Mapping[str, Any]) -> bool: + if certificate["status"] != expected["status"]: + return False + result = certificate["result"] + if "failure" in expected: + return result.get("failure") == expected["failure"] + for key, value in expected.items(): + if key in {"status", "maximum_visited_weights"}: + continue + if result.get(key) != value: + return False + maximum = expected.get("maximum_visited_weights") + if maximum is not None and certificate["dependencies"]["request_count"] > maximum: + return False + return True + + +def run_corpus( + corpus_path: Path, + contract_path: Path, +) -> dict[str, Any]: + corpus = json.loads(corpus_path.read_text(encoding="utf-8")) + contract = json.loads(contract_path.read_text(encoding="utf-8")) + budgets = Budgets.from_mapping(contract["budgets"]) + rows = [] + for case in corpus["cases"]: + certificate = evaluate_case(case, corpus["context"], budgets) + replay = replay_certificate(case, corpus["context"], budgets, certificate) + passed = _expected_matches(case["expected"], certificate) + passed = passed and replay["status"] == "verified" + rows.append( + { + "case_id": case["id"], + "passed": passed, + "certificate": certificate, + "replay": replay, + } + ) + return { + "schema": "process-geometry/am-weight-corpus-result/v0", + "corpus_schema": corpus["schema"], + "passed": all(row["passed"] for row in rows), + "pass_count": sum(bool(row["passed"]) for row in rows), + "case_count": len(rows), + "rows": rows, + } diff --git a/workstreams/am_weight_compiler/am_weight_compiler/evaluator.py b/workstreams/am_weight_compiler/am_weight_compiler/evaluator.py new file mode 100644 index 00000000..c2005b24 --- /dev/null +++ b/workstreams/am_weight_compiler/am_weight_compiler/evaluator.py @@ -0,0 +1,134 @@ +from __future__ import annotations + +from copy import deepcopy +from fractions import Fraction +from typing import Any, Mapping + +from .coefficients import WeightEvaluator +from .model import ( + Budgets, + EvaluationFailure, + canonical_json, + digest_json, + fraction_text, + parse_fraction, + without_expected, +) +from .native import AMTerm, finite_affine_relation, pbw_identity, primitive + + +SEMANTIC_CARRIER = "completed-am-power-weight/rank-one-rational/v0" + + +def _with_certificate_size(certificate: dict[str, Any], budgets: Budgets) -> None: + storage = certificate["costs"]["storage"] + previous = -1 + while storage["certificate_bytes"] != previous: + previous = storage["certificate_bytes"] + storage["certificate_bytes"] = len(canonical_json(certificate).encode("utf-8")) + if storage["certificate_bytes"] > budgets.max_certificate_bytes: + raise EvaluationFailure("resource_exceeded", "certificate-budget-exceeded") + + +def _seal(certificate: dict[str, Any], budgets: Budgets) -> dict[str, Any]: + certificate["certificate_digest"] = "0" * 64 + _with_certificate_size(certificate, budgets) + unsigned = {key: value for key, value in certificate.items() if key != "certificate_digest"} + certificate["certificate_digest"] = digest_json(unsigned) + return certificate + + +def _base_certificate( + case: Mapping[str, Any], context: Mapping[str, object], budgets: Budgets +) -> dict[str, Any]: + source = without_expected(case) + return { + "schema": "process-geometry/am-weight-certificate/v0", + "case_id": case.get("id"), + "kind": case.get("kind"), + "semantic_carrier": SEMANTIC_CARRIER, + "claim_scope": "frozen-rank-one-rational-completed-am-fragment", + "source_digest": digest_json(source), + "context_digest": digest_json({"context": context, "budgets": budgets.as_dict()}), + "status": "evaluated", + "result": {}, + "observer": None, + "dependencies": {"request_count": 0, "weight_count": 0, "weights": []}, + "costs": { + "compilation": {"nodes": 0, "lattice_denominator": 1}, + "evaluation": {"coefficient_operations": 0}, + "storage": { + "source_bytes": len(canonical_json(source).encode("utf-8")), + "certificate_bytes": 0, + }, + }, + } + + +def evaluate_case( + case: Mapping[str, Any], + corpus_context: Mapping[str, object], + budgets: Budgets, +) -> dict[str, Any]: + context = deepcopy(dict(corpus_context)) + context.update(case.get("context_override", {})) + certificate = _base_certificate(case, context, budgets) + try: + kind = case.get("kind") + if kind == "native-laws": + left = AMTerm.decode(case["left"], max_abs_power=budgets.max_abs_power) + right = AMTerm.decode(case["right"], max_abs_power=budgets.max_abs_power) + pbw_source = AMTerm.decode( + case["pbw"]["source"], max_abs_power=budgets.max_abs_power + ) + relation = case["finite_relation"] + certificate["result"] = { + "product": left.multiply(right).as_dict(), + "A_left": left.apply_A().as_dict(), + "M_left": left.apply_M().as_dict(), + "pbw": pbw_identity( + pbw_source, int(case["pbw"]["m"]), int(case["pbw"]["n"]) + ), + "finite_relation": finite_affine_relation( + parse_fraction(relation["translation"]), + parse_fraction(relation["scale"]), + ), + } + certificate["costs"]["compilation"]["nodes"] = 4 + elif kind == "primitive": + term = AMTerm.decode(case["term"], max_abs_power=budgets.max_abs_power) + certificate["result"] = primitive( + term, str(case["generator"]), str(case["extension_policy"]) + ) + certificate["costs"]["compilation"]["nodes"] = 1 + elif kind == "paired": + left = AMTerm.decode(case["left"], max_abs_power=budgets.max_abs_power) + right = AMTerm.decode(case["right"], max_abs_power=budgets.max_abs_power) + certificate["result"] = {"same_canonical_term": left == right} + certificate["costs"]["compilation"]["nodes"] = 2 + elif kind == "coefficient": + target = parse_fraction(case["target_weight"], field="target_weight") + evaluator = WeightEvaluator(case["expression"], target, context, budgets) + coefficient = evaluator.coefficient() + certificate["result"] = {"coefficient": coefficient.to_text()} + certificate["observer"] = { + "target_weight": fraction_text(target), + "residual": "weights-above-observer-horizon", + } + certificate["dependencies"] = evaluator.meter.dependency_summary() + certificate["costs"]["compilation"] = { + "nodes": evaluator.meter.nodes, + "lattice_denominator": evaluator.lattice_denominator, + } + certificate["costs"]["evaluation"] = { + "coefficient_operations": evaluator.meter.coefficient_operations + } + else: + raise EvaluationFailure("unsupported", "unknown-case-kind") + except EvaluationFailure as exc: + certificate["status"] = exc.status + certificate["result"] = {"failure": exc.code} + except (KeyError, TypeError, ValueError) as exc: + certificate["status"] = "unsupported" + certificate["result"] = {"failure": "malformed-case", "detail": str(exc)} + return _seal(certificate, budgets) diff --git a/workstreams/am_weight_compiler/am_weight_compiler/model.py b/workstreams/am_weight_compiler/am_weight_compiler/model.py new file mode 100644 index 00000000..7941d60e --- /dev/null +++ b/workstreams/am_weight_compiler/am_weight_compiler/model.py @@ -0,0 +1,182 @@ +from __future__ import annotations + +from dataclasses import dataclass +from fractions import Fraction +import hashlib +import json +from math import gcd +from typing import Any, Iterable, Mapping + + +def parse_fraction(value: object, *, field: str = "value") -> Fraction: + if isinstance(value, bool): + raise ValueError(f"{field} must be rational") + if isinstance(value, int): + return Fraction(value) + if isinstance(value, str): + try: + return Fraction(value) + except (ValueError, ZeroDivisionError) as exc: + raise ValueError(f"{field} must be rational") from exc + raise ValueError(f"{field} must be rational") + + +def fraction_text(value: Fraction) -> str: + if value.denominator == 1: + return str(value.numerator) + return f"{value.numerator}/{value.denominator}" + + +def canonical_json(value: object) -> str: + return json.dumps(value, sort_keys=True, separators=(",", ":"), ensure_ascii=False) + + +def digest_json(value: object) -> str: + return hashlib.sha256(canonical_json(value).encode("utf-8")).hexdigest() + + +def lcm(left: int, right: int) -> int: + return abs(left * right) // gcd(left, right) if left and right else 0 + + +@dataclass(frozen=True) +class ExpQCoefficient: + """An exact finite sum of rational multiples of formal exp(q) atoms.""" + + terms: tuple[tuple[Fraction, Fraction], ...] + + @classmethod + def from_items( + cls, items: Iterable[tuple[Fraction, Fraction]] + ) -> "ExpQCoefficient": + combined: dict[Fraction, Fraction] = {} + for exponent, coefficient in items: + combined[exponent] = combined.get(exponent, Fraction(0)) + coefficient + return cls(tuple(sorted((q, c) for q, c in combined.items() if c))) + + @classmethod + def zero(cls) -> "ExpQCoefficient": + return cls(()) + + @classmethod + def rational(cls, value: Fraction | int) -> "ExpQCoefficient": + coefficient = Fraction(value) + return cls(()) if not coefficient else cls(((Fraction(0), coefficient),)) + + @classmethod + def exp_atom(cls, exponent: Fraction) -> "ExpQCoefficient": + return cls(((exponent, Fraction(1)),)) + + @property + def is_zero(self) -> bool: + return not self.terms + + @property + def is_rational(self) -> bool: + return not self.terms or all(exponent == 0 for exponent, _ in self.terms) + + def rational_value(self) -> Fraction: + if not self.is_rational: + raise ValueError("coefficient is not rational") + return self.terms[0][1] if self.terms else Fraction(0) + + def __add__(self, other: "ExpQCoefficient") -> "ExpQCoefficient": + return self.from_items((*self.terms, *other.terms)) + + def __neg__(self) -> "ExpQCoefficient": + return self.from_items((q, -c) for q, c in self.terms) + + def __sub__(self, other: "ExpQCoefficient") -> "ExpQCoefficient": + return self + (-other) + + def __mul__(self, other: "ExpQCoefficient") -> "ExpQCoefficient": + return self.from_items( + (left_q + right_q, left_c * right_c) + for left_q, left_c in self.terms + for right_q, right_c in other.terms + ) + + def divide_rational(self, divisor: Fraction | int) -> "ExpQCoefficient": + divisor = Fraction(divisor) + if not divisor: + raise ZeroDivisionError("coefficient division by zero") + return self.from_items((q, c / divisor) for q, c in self.terms) + + def scale_rational(self, scalar: Fraction | int) -> "ExpQCoefficient": + scalar = Fraction(scalar) + return self.from_items((q, scalar * c) for q, c in self.terms) + + def to_text(self) -> str: + if not self.terms: + return "0" + pieces: list[str] = [] + for exponent, coefficient in self.terms: + if exponent == 0: + term = fraction_text(abs(coefficient)) + else: + atom = f"exp({fraction_text(exponent)})" + magnitude = abs(coefficient) + term = atom if magnitude == 1 else f"{fraction_text(magnitude)}*{atom}" + if not pieces: + pieces.append(f"-{term}" if coefficient < 0 else term) + else: + pieces.append((" - " if coefficient < 0 else " + ") + term) + return "".join(pieces) + + +@dataclass(frozen=True) +class Budgets: + max_nodes: int = 1024 + max_lattice_denominator: int = 24 + max_abs_power: int = 256 + max_target_weight: int = 256 + max_coefficient_operations: int = 100_000 + max_certificate_bytes: int = 65_536 + + @classmethod + def from_mapping(cls, data: Mapping[str, object]) -> "Budgets": + values = {name: int(data[name]) for name in cls.__dataclass_fields__} + return cls(**values) + + def as_dict(self) -> dict[str, int]: + return { + name: getattr(self, name) + for name in self.__dataclass_fields__ + } + + +class EvaluationFailure(Exception): + def __init__(self, status: str, code: str): + super().__init__(code) + self.status = status + self.code = code + + +class Meter: + def __init__(self, budgets: Budgets): + self.budgets = budgets + self.nodes = 0 + self.coefficient_operations = 0 + self.dependencies: set[tuple[str, Fraction]] = set() + + def bump_operation(self, amount: int = 1) -> None: + self.coefficient_operations += amount + if self.coefficient_operations > self.budgets.max_coefficient_operations: + raise EvaluationFailure( + "resource_exceeded", "coefficient-operation-budget-exceeded" + ) + + def visit(self, node_key: str, weight: Fraction) -> None: + self.dependencies.add((node_key, weight)) + + def dependency_summary(self) -> dict[str, object]: + weights = sorted({weight for _, weight in self.dependencies}) + return { + "request_count": len(self.dependencies), + "weight_count": len(weights), + "weights": [fraction_text(weight) for weight in weights], + } + + +def without_expected(case: Mapping[str, Any]) -> dict[str, Any]: + return {key: value for key, value in case.items() if key != "expected"} diff --git a/workstreams/am_weight_compiler/am_weight_compiler/native.py b/workstreams/am_weight_compiler/am_weight_compiler/native.py new file mode 100644 index 00000000..197c273a --- /dev/null +++ b/workstreams/am_weight_compiler/am_weight_compiler/native.py @@ -0,0 +1,120 @@ +from __future__ import annotations + +from dataclasses import dataclass +from fractions import Fraction +from math import prod +from typing import Mapping + +from .model import ExpQCoefficient, EvaluationFailure, fraction_text, parse_fraction + + +@dataclass(frozen=True) +class AMTerm: + nu: int + weight: Fraction + coefficient: Fraction + + @classmethod + def decode(cls, value: Mapping[str, object], *, max_abs_power: int) -> "AMTerm": + nu_value = value.get("nu") + if isinstance(nu_value, bool) or not isinstance(nu_value, int): + raise ValueError("nu must be an integer") + if abs(nu_value) > max_abs_power: + raise EvaluationFailure("resource_exceeded", "power-budget-exceeded") + basis = value.get("basis") + if basis == "power-weight": + weight = parse_fraction(value.get("weight"), field="weight") + elif basis == "power-character": + character = parse_fraction(value.get("character"), field="character") + weight = Fraction(nu_value) + character + else: + raise EvaluationFailure("unsupported", "unknown-am-basis") + return cls( + nu=nu_value, + weight=weight, + coefficient=parse_fraction(value.get("coefficient"), field="coefficient"), + ) + + @property + def character(self) -> Fraction: + return self.weight - self.nu + + def multiply(self, other: "AMTerm") -> "AMTerm": + return AMTerm( + nu=self.nu + other.nu, + weight=self.weight + other.weight, + coefficient=self.coefficient * other.coefficient, + ) + + def apply_A(self) -> "AMTerm": + return AMTerm( + nu=self.nu - 1, + weight=self.weight - 1, + coefficient=self.coefficient * self.nu, + ) + + def apply_M(self) -> "AMTerm": + return AMTerm( + nu=self.nu, + weight=self.weight, + coefficient=self.coefficient * self.weight, + ) + + def as_dict(self) -> dict[str, object]: + return { + "nu": self.nu, + "weight": fraction_text(self.weight), + "coefficient": fraction_text(self.coefficient), + } + + +def falling(value: Fraction | int, length: int) -> Fraction: + return prod((Fraction(value) - offset for offset in range(length)), start=Fraction(1)) + + +def pbw_identity(term: AMTerm, a_power: int, m_power: int) -> bool: + """Check A^m M^n = (M+m)^n A^m on one exact weight vector.""" + + left = falling(term.nu, a_power) * term.weight**m_power + lowered_weight = term.weight - a_power + right = falling(term.nu, a_power) * (lowered_weight + a_power) ** m_power + return left == right + + +def finite_affine_relation(translation: Fraction, scale: Fraction) -> bool: + """Check normal forms for S_s T_t = T_(exp(s)t) S_s.""" + + left_translation = ExpQCoefficient.exp_atom(scale).scale_rational(translation) + right_translation = ExpQCoefficient.rational(translation) * ExpQCoefficient.exp_atom(scale) + return left_translation == right_translation + + +def primitive(term: AMTerm, generator: str, extension_policy: str) -> dict[str, object]: + allow_typed = extension_policy == "allow-typed" + if generator == "A": + if term.nu == -1: + if not allow_typed: + raise EvaluationFailure("unsupported", "resonance-extension-required") + return {"extension": "log-a", "domain_witness": "a>0"} + return { + "extension": "ordinary-power-weight", + "term": AMTerm( + nu=term.nu + 1, + weight=term.weight + 1, + coefficient=term.coefficient / (term.nu + 1), + ).as_dict(), + } + if generator == "M": + if term.weight == 0: + if not allow_typed: + raise EvaluationFailure("unsupported", "resonance-extension-required") + return {"extension": "v-jordan"} + return { + "extension": "ordinary-power-weight", + "term": AMTerm( + nu=term.nu, + weight=term.weight, + coefficient=term.coefficient / term.weight, + ).as_dict(), + } + raise EvaluationFailure("unsupported", "unknown-primitive-generator") diff --git a/workstreams/am_weight_compiler/am_weight_compiler/replay.py b/workstreams/am_weight_compiler/am_weight_compiler/replay.py new file mode 100644 index 00000000..10b86d3e --- /dev/null +++ b/workstreams/am_weight_compiler/am_weight_compiler/replay.py @@ -0,0 +1,36 @@ +from __future__ import annotations + +from typing import Any, Mapping + +from .evaluator import evaluate_case +from .model import Budgets, digest_json + + +def replay_certificate( + case: Mapping[str, Any], + corpus_context: Mapping[str, object], + budgets: Budgets, + certificate: Mapping[str, Any], +) -> dict[str, object]: + recomputed = evaluate_case(case, corpus_context, budgets) + supplied = dict(certificate) + verified = recomputed == supplied + return { + "status": "verified" if verified else "rejected", + "certificate_digest": supplied.get("certificate_digest"), + "recomputed_digest": recomputed.get("certificate_digest"), + "replay_digest": digest_json( + { + "source_digest": recomputed["source_digest"], + "certificate_digest": supplied.get("certificate_digest"), + "recomputed_digest": recomputed.get("certificate_digest"), + "verified": verified, + } + ), + "costs": { + "coefficient_operations": recomputed["costs"]["evaluation"][ + "coefficient_operations" + ], + "dependency_requests": recomputed["dependencies"]["request_count"], + }, + } diff --git a/workstreams/am_weight_compiler/pyproject.toml b/workstreams/am_weight_compiler/pyproject.toml new file mode 100644 index 00000000..6cb95bca --- /dev/null +++ b/workstreams/am_weight_compiler/pyproject.toml @@ -0,0 +1,13 @@ +[build-system] +requires = ["setuptools>=70"] +build-backend = "setuptools.build_meta" + +[project] +name = "am-power-weight-compiler" +version = "0.1.0" +description = "Research-local observer-directed completed AM coefficients" +requires-python = ">=3.10" + +[tool.pytest.ini_options] +testpaths = ["tests"] +addopts = "-q" diff --git a/workstreams/am_weight_compiler/run_baselines.py b/workstreams/am_weight_compiler/run_baselines.py new file mode 100644 index 00000000..ad599827 --- /dev/null +++ b/workstreams/am_weight_compiler/run_baselines.py @@ -0,0 +1,178 @@ +from __future__ import annotations + +from fractions import Fraction +import json +from pathlib import Path +from statistics import median +from time import perf_counter_ns +from typing import Any, Mapping + +import sympy as sp + +from am_weight_compiler.evaluator import evaluate_case +from am_weight_compiler.model import Budgets +from am_weight_compiler.replay import replay_certificate + + +x = sp.Symbol("x", positive=True) + + +def rational(value: object) -> sp.Rational: + parsed = Fraction(str(value)) + return sp.Rational(parsed.numerator, parsed.denominator) + + +def to_sympy(node: Mapping[str, Any]) -> sp.Expr: + op = node["op"] + if op == "finite": + return sum( + ( + rational(term["coefficient"]) * x ** rational(term["weight"]) + for term in node["terms"] + ), + sp.S.Zero, + ) + if op == "add": + return sum((to_sympy(argument) for argument in node["arguments"]), sp.S.Zero) + if op == "multiply": + return sp.prod(to_sympy(argument) for argument in node["arguments"]) + if op == "scale": + return rational(node["coefficient"]) * to_sympy(node["argument"]) + if op == "shift": + return x ** rational(node["by"]) * to_sympy(node["argument"]) + if op == "exp": + return sp.exp(to_sympy(node["argument"])) + if op == "log1p": + return sp.log(1 + to_sympy(node["argument"])) + raise ValueError(f"baseline does not support {op}") + + +def source_horizon(node: Mapping[str, Any], target: int) -> int: + op = node["op"] + if op == "shift": + shift = Fraction(str(node["by"])) + if shift.denominator != 1: + raise ValueError("baseline window only reports integer weights") + return source_horizon(node["argument"], target - shift.numerator) + if op in {"add", "multiply"}: + return max(source_horizon(argument, target) for argument in node["arguments"]) + if op in {"scale", "exp", "log1p"}: + return source_horizon(node["argument"], target) + return target + + +def source_measure(node: Mapping[str, Any]) -> tuple[int, int]: + op = node["op"] + if op == "finite": + return 1, len(node["terms"]) + if op in {"add", "multiply"}: + children = [source_measure(argument) for argument in node["arguments"]] + return 1 + sum(item[0] for item in children), sum(item[1] for item in children) + if op in {"scale", "shift", "exp", "log1p"}: + nodes, terms = source_measure(node["argument"]) + return nodes + 1, terms + raise ValueError(f"baseline does not support {op}") + + +def benchmark_case(case: Mapping[str, Any], repetitions: int = 3) -> dict[str, object]: + target = Fraction(str(case["target_weight"])) + if target.denominator != 1: + raise ValueError("baseline benchmark cases use integer target weights") + expression = to_sympy(case["expression"]) + target_int = target.numerator + samples: list[float] = [] + coefficient = None + expanded = None + for _ in range(repetitions): + started = perf_counter_ns() + expanded = sp.series(expression, x, 0, target_int + 1).removeO().expand() + coefficient = expanded.coeff(x, target_int) + samples.append((perf_counter_ns() - started) / 1_000_000) + assert coefficient is not None and expanded is not None + nodes, finite_terms = source_measure(case["expression"]) + horizon = source_horizon(case["expression"], target_int) + return { + "case_id": case["id"], + "status": "evaluated", + "coefficient": str(coefficient), + "method": "same-information-truncated-series-window", + "source": {"nodes": nodes, "finite_terms": finite_terms}, + "materialized_window": { + "minimum_weight": 0, + "maximum_source_weight": horizon, + "weight_count": horizon + 1, + }, + "expanded_term_count": len(sp.Add.make_args(expanded)), + "wall_time_ms": { + "samples": [round(value, 6) for value in samples], + "median": round(median(samples), 6), + "authority": "non-authoritative", + }, + "semantic_or_certificate_credit": False, + } + + +def benchmark_candidate( + case: Mapping[str, Any], + context: Mapping[str, object], + budgets: Budgets, + repetitions: int = 5, +) -> dict[str, object]: + evaluation_samples: list[float] = [] + replay_samples: list[float] = [] + certificate = None + replay = None + for _ in range(repetitions): + started = perf_counter_ns() + certificate = evaluate_case(case, context, budgets) + evaluation_samples.append((perf_counter_ns() - started) / 1_000_000) + started = perf_counter_ns() + replay = replay_certificate(case, context, budgets, certificate) + replay_samples.append((perf_counter_ns() - started) / 1_000_000) + assert certificate is not None and replay is not None + return { + "status": certificate["status"], + "coefficient": certificate["result"].get("coefficient"), + "dependencies": certificate["dependencies"], + "costs": certificate["costs"], + "certificate_digest": certificate["certificate_digest"], + "replay_status": replay["status"], + "wall_time_ms": { + "evaluation_samples": [round(value, 6) for value in evaluation_samples], + "evaluation_median": round(median(evaluation_samples), 6), + "replay_samples": [round(value, 6) for value in replay_samples], + "replay_median": round(median(replay_samples), 6), + "authority": "non-authoritative", + }, + } + + +def load_cases(root: Path) -> list[Mapping[str, Any]]: + public = json.loads((root / "PUBLIC_CORPUS.json").read_text(encoding="utf-8")) + reveal = json.loads((root / "HELD_OUT_REVEAL.json").read_text(encoding="utf-8")) + selected = [ + case + for case in public["cases"] + if case["id"] in {"p2-weight32-log-cancellation", "p3-completed-exp-composition"} + ] + return [*selected, reveal["executable_case"]] + + +if __name__ == "__main__": + root = Path(__file__).resolve().parent + contract_data = json.loads((root / "FROZEN_CONTRACT.json").read_text(encoding="utf-8")) + public_data = json.loads((root / "PUBLIC_CORPUS.json").read_text(encoding="utf-8")) + budgets = Budgets.from_mapping(contract_data["budgets"]) + cases = load_cases(root) + rows = [] + for case in cases: + row = benchmark_case(case) + row["candidate"] = benchmark_candidate(case, public_data["context"], budgets) + rows.append(row) + result = { + "schema": "process-geometry/am-weight-observed-baselines/v0", + "engine": f"SymPy {sp.__version__}", + "contract": "BASELINE_CONTRACT.json", + "cases": rows, + } + print(json.dumps(result, indent=2, sort_keys=True)) diff --git a/workstreams/am_weight_compiler/run_corpus.py b/workstreams/am_weight_compiler/run_corpus.py new file mode 100644 index 00000000..c2cd1018 --- /dev/null +++ b/workstreams/am_weight_compiler/run_corpus.py @@ -0,0 +1,13 @@ +from __future__ import annotations + +import json +from pathlib import Path + +from am_weight_compiler.corpus import run_corpus + + +if __name__ == "__main__": + root = Path(__file__).resolve().parent + result = run_corpus(root / "PUBLIC_CORPUS.json", root / "FROZEN_CONTRACT.json") + print(json.dumps(result, indent=2, sort_keys=True)) + raise SystemExit(0 if result["passed"] else 1) diff --git a/workstreams/am_weight_compiler/run_heldout.py b/workstreams/am_weight_compiler/run_heldout.py new file mode 100644 index 00000000..8b382776 --- /dev/null +++ b/workstreams/am_weight_compiler/run_heldout.py @@ -0,0 +1,51 @@ +from __future__ import annotations + +import json +from pathlib import Path + +from am_weight_compiler.evaluator import evaluate_case +from am_weight_compiler.model import Budgets, digest_json +from am_weight_compiler.replay import replay_certificate + + +def run(root: Path) -> dict[str, object]: + reveal = json.loads((root / "HELD_OUT_REVEAL.json").read_text(encoding="utf-8")) + commitment = json.loads( + (root / "HELD_OUT_COMMITMENT.json").read_text(encoding="utf-8") + ) + contract = json.loads((root / "FROZEN_CONTRACT.json").read_text(encoding="utf-8")) + public = json.loads((root / "PUBLIC_CORPUS.json").read_text(encoding="utf-8")) + + payload_digest = digest_json(reveal["payload"]) + commitment_verified = ( + payload_digest == reveal["commitment"] == commitment["payload_sha256"] + ) + if not commitment_verified: + raise SystemExit("held-out commitment mismatch") + + case = reveal["executable_case"] + budgets = Budgets.from_mapping(contract["budgets"]) + certificate = evaluate_case(case, public["context"], budgets) + replay = replay_certificate(case, public["context"], budgets, certificate) + expected = case["expected"] + passed = ( + certificate["status"] == expected["status"] + and certificate["result"].get("coefficient") == expected["coefficient"] + and replay["status"] == "verified" + ) + return { + "schema": "process-geometry/am-weight-heldout-result/v0", + "case_id": case["id"], + "commitment_verified": commitment_verified, + "payload_digest": payload_digest, + "pre_reveal_source_commit": reveal["pre_reveal_source_commit"], + "passed": passed, + "certificate": certificate, + "replay": replay, + } + + +if __name__ == "__main__": + result = run(Path(__file__).resolve().parent) + print(json.dumps(result, indent=2, sort_keys=True)) + raise SystemExit(0 if result["passed"] else 1) diff --git a/workstreams/am_weight_compiler/tests/test_compiler.py b/workstreams/am_weight_compiler/tests/test_compiler.py new file mode 100644 index 00000000..000124c9 --- /dev/null +++ b/workstreams/am_weight_compiler/tests/test_compiler.py @@ -0,0 +1,90 @@ +from __future__ import annotations + +from copy import deepcopy +from fractions import Fraction +import json +from pathlib import Path + +from am_weight_compiler.coefficients import WeightEvaluator +from am_weight_compiler.evaluator import evaluate_case +from am_weight_compiler.model import Budgets, ExpQCoefficient +from am_weight_compiler.replay import replay_certificate + + +ROOT = Path(__file__).resolve().parents[1] +CONTRACT = json.loads((ROOT / "FROZEN_CONTRACT.json").read_text(encoding="utf-8")) +CORPUS = json.loads((ROOT / "PUBLIC_CORPUS.json").read_text(encoding="utf-8")) +BUDGETS = Budgets.from_mapping(CONTRACT["budgets"]) +CONTEXT = CORPUS["context"] + + +def finite(*terms: tuple[str, str]) -> dict[str, object]: + return { + "op": "finite", + "terms": [ + {"weight": weight, "coefficient": coefficient} + for weight, coefficient in terms + ], + } + + +def test_exp_q_coefficient_is_exact_group_algebra() -> None: + left = ExpQCoefficient.exp_atom(Fraction(2, 3)).scale_rational(3) + right = ExpQCoefficient.exp_atom(Fraction(1, 3)).scale_rational(2) + assert (left * right).to_text() == "6*exp(1)" + assert (left + (-left)).to_text() == "0" + + +def test_generic_exp_log_recurrence_uses_only_requested_weight() -> None: + expression = { + "op": "exp", + "argument": { + "op": "add", + "arguments": [ + {"op": "log1p", "argument": finite(("1", "1"))}, + finite(("2", "1")), + ], + }, + } + evaluator = WeightEvaluator(expression, Fraction(5), CONTEXT, BUDGETS) + assert evaluator.coefficient().to_text() == "1/2" + assert evaluator.meter.coefficient_operations < 100 + + +def test_rational_lattice_and_multiplication() -> None: + expression = { + "op": "multiply", + "arguments": [ + {"op": "exp", "argument": finite(("1/2", "2"))}, + finite(("1/2", "3")), + ], + } + evaluator = WeightEvaluator(expression, Fraction(3, 2), CONTEXT, BUDGETS) + assert evaluator.lattice_denominator == 2 + assert evaluator.coefficient().to_text() == "6" + + +def test_replay_rejects_certificate_tampering() -> None: + case = next(case for case in CORPUS["cases"] if case["id"] == "p3-completed-exp-composition") + certificate = evaluate_case(case, CONTEXT, BUDGETS) + tampered = deepcopy(certificate) + tampered["result"]["coefficient"] = "exp(3)" + assert replay_certificate(case, CONTEXT, BUDGETS, certificate)["status"] == "verified" + assert replay_certificate(case, CONTEXT, BUDGETS, tampered)["status"] == "rejected" + + +def test_expected_field_has_no_semantic_effect() -> None: + case = deepcopy(next(case for case in CORPUS["cases"] if case["id"] == "p2-weight32-log-cancellation")) + first = evaluate_case(case, CONTEXT, BUDGETS) + case["expected"]["coefficient"] = "999" + second = evaluate_case(case, CONTEXT, BUDGETS) + assert first == second + + +def test_source_firewall_excludes_generic_oracles() -> None: + source = "\n".join( + path.read_text(encoding="utf-8") + for path in (ROOT / "am_weight_compiler").glob("*.py") + ) + assert ".series(" not in source + assert ".limit(" not in source diff --git a/workstreams/am_weight_compiler/tests/test_corpus.py b/workstreams/am_weight_compiler/tests/test_corpus.py new file mode 100644 index 00000000..2a947bdc --- /dev/null +++ b/workstreams/am_weight_compiler/tests/test_corpus.py @@ -0,0 +1,15 @@ +from __future__ import annotations + +from pathlib import Path + +from am_weight_compiler.corpus import run_corpus + + +ROOT = Path(__file__).resolve().parents[1] + + +def test_frozen_public_corpus_and_replay() -> None: + result = run_corpus(ROOT / "PUBLIC_CORPUS.json", ROOT / "FROZEN_CONTRACT.json") + assert result["passed"] is True + assert result["pass_count"] == result["case_count"] == 12 + assert all(row["replay"]["status"] == "verified" for row in result["rows"]) diff --git a/workstreams/am_weight_compiler/tests/test_heldout_reveal.py b/workstreams/am_weight_compiler/tests/test_heldout_reveal.py new file mode 100644 index 00000000..7fa3d5d0 --- /dev/null +++ b/workstreams/am_weight_compiler/tests/test_heldout_reveal.py @@ -0,0 +1,30 @@ +from __future__ import annotations + +import json +from pathlib import Path + +from run_heldout import run + + +ROOT = Path(__file__).resolve().parents[1] + + +def test_committed_heldout_reveals_and_replays() -> None: + result = run(ROOT) + assert result["commitment_verified"] is True + assert result["passed"] is True + assert result["certificate"]["result"]["coefficient"] == "1/3" + assert result["replay"]["status"] == "verified" + stored = json.loads((ROOT / "HELD_OUT_RESULT.json").read_text(encoding="utf-8")) + assert result == stored + + +def test_observed_baselines_agree_without_semantic_credit() -> None: + observed = json.loads( + (ROOT / "OBSERVED_BASELINES.json").read_text(encoding="utf-8") + ) + assert len(observed["cases"]) == 3 + for row in observed["cases"]: + assert row["coefficient"] == row["candidate"]["coefficient"] + assert row["semantic_or_certificate_credit"] is False + assert row["candidate"]["replay_status"] == "verified" diff --git a/workstreams/am_weight_compiler/tests/test_stored_results.py b/workstreams/am_weight_compiler/tests/test_stored_results.py new file mode 100644 index 00000000..ffd6c2c1 --- /dev/null +++ b/workstreams/am_weight_compiler/tests/test_stored_results.py @@ -0,0 +1,15 @@ +from __future__ import annotations + +import json +from pathlib import Path + +from am_weight_compiler.corpus import run_corpus + + +ROOT = Path(__file__).resolve().parents[1] + + +def test_stored_public_result_is_reproducible() -> None: + result = run_corpus(ROOT / "PUBLIC_CORPUS.json", ROOT / "FROZEN_CONTRACT.json") + stored = json.loads((ROOT / "PUBLIC_RESULT.json").read_text(encoding="utf-8")) + assert result == stored