diff --git a/.github/workflows/ci.yml b/.github/workflows/ci.yml index 92feb4c22..16a75c271 100644 --- a/.github/workflows/ci.yml +++ b/.github/workflows/ci.yml @@ -191,7 +191,7 @@ jobs: if: steps.classify.outputs.docs_only != 'true' run: | python3 -m pip install --user -r scripts/conway/requirements.txt \ - python-flint==0.9.0 sympy==1.14.0 gmpy2 cypari2 conway-polynomials matplotlib==3.11.1 + python-flint==0.9.0 z3-solver==4.15.4.0 sympy==1.14.0 gmpy2 cypari2 conway-polynomials matplotlib==3.11.1 python3 -m unittest scripts/oracle/test_hermite_bench_drivers.py python3 -m unittest scripts/oracle/test_matrix_carriers.py scripts/oracle/test_rank_bench.py scripts/oracle/test_rank_stages.py python3 -m unittest scripts/bench/test_rank_measure.py scripts/bench/test_rank_analyze.py diff --git a/HexSignDet/README.md b/HexSignDet/README.md index 06d1ee24e..da84560ef 100644 --- a/HexSignDet/README.md +++ b/HexSignDet/README.md @@ -216,8 +216,30 @@ performance milestone is claimed here. See the [specification](SPEC/hex-sign-det for the complete contract and [#10377](https://github.com/kim-em/hex-dev/issues/10377) for the remaining assignment. +The extension conformance target uses the existing `RationalFn Rat` and +`RationalFn (RationalFn Rat)` coefficient fields with explicit exact signs at +successive positive infinitesimals. Its independent oracle is pinned to +`z3-solver==4.15.4.0` and numeric runtime version `(4, 15, 4, 0)`; +its RCF API constructs roots and compares them exactly. Every fixture records the ordered +coefficient levels and starts a fresh oracle context. The corrected +`(εx²−1)(εx³−1)` example exercises the two positive partial descriptors, +completion, root order, selected signs and cross-polynomial re-encoding without +a rational separator. Two-level fixtures isolate `δ` from `ε` and `ε+δ` using +an endpoint `2δ`. Both coefficient levels reject changed context, head and +derivative-query bindings, and reject a multi-query table presented as a leaf. +These leaf-arity checks do not test an identity-preserving incomplete support +forgery. The oracle enforces each case’s coefficient depth and the corrected +Passmore polynomial, and checks all five descriptor-error reasons. It separately +rejects forged counts, reordered roots, altered encodings and context metadata. +These test-only sign callbacks do not implement the ordered-function provider; +tower-generated coefficient proofs, nested semantic replay, literal DAG +serialization and all Phase-4 measurements remain required. + Build the library and its regression target with: ```sh -lake build HexSignDet +HexSignDet.Conformance +lake build HexSignDet +HexSignDet.Conformance hexsigndet_emit_infinitesimal +.lake/build/bin/hexsigndet_emit_infinitesimal > conformance-fixtures/HexSignDet/infinitesimal.jsonl +python3 scripts/oracle/sign_det_z3.py --check +python3 -m unittest scripts.oracle.test_sign_det_z3 ``` diff --git a/conformance-fixtures/HexSignDet/README.md b/conformance-fixtures/HexSignDet/README.md index 282cbcfbe..47eb9a9f0 100644 --- a/conformance-fixtures/HexSignDet/README.md +++ b/conformance-fixtures/HexSignDet/README.md @@ -1,4 +1,4 @@ -# Rational sign-table and descriptor fixtures +# Exact sign-table and descriptor fixtures `sign_det.jsonl` contains 101 cases emitted by `hexsigndet_emit_fixtures`. The 59 table records include ascending rational polynomial coefficients as exact @@ -52,7 +52,29 @@ python3 scripts/oracle/sign_det_flint.py --check python3 -m unittest scripts.oracle.test_sign_det_flint ``` -These fixtures validate rational sign tables and the implemented descriptor -operations, including cross-polynomial comparison and re-encoding. -Extension-field and nested-context conformance remain required. None of these fixtures proves general -root-sum/Thom semantics or supplies Phase-4 performance evidence. +`infinitesimal.jsonl` contains 29 cases emitted by `hexsigndet_emit_infinitesimal` +using the existing rational-function fields over one and two positive +infinitesimals. The independent Z3 RCF oracle requires `z3-solver==4.15.4.0` +and numeric runtime version `(4, 15, 4, 0)`. Each record creates a fresh context +and reconstructs the serialized coefficients with exact arithmetic. The oracle +enforces the coefficient depth of each case and the corrected Passmore +polynomial `(εx²−1)(εx³−1)`, then computes roots, signs and order independently. +The cases cover sign tables, invalid domains, all five descriptor-error reasons, +completion, selected signs, comparisons and re-encoding. Negative replay checks +change context, head and derivative-query bindings or present a multi-query +table as a leaf; the latter checks leaf arity, not identity-preserving incomplete +support. The 16 adversarial Python tests also reject substituted case inputs, +omitted support with preserved totals, wrong root order and version drift. + +```sh +lake build hexsigndet_emit_infinitesimal +.lake/build/bin/hexsigndet_emit_infinitesimal > conformance-fixtures/HexSignDet/infinitesimal.jsonl +python3 scripts/oracle/sign_det_z3.py --check +python3 -m unittest scripts.oracle.test_sign_det_z3 +``` + +These fixtures validate rational and nested-infinitesimal sign tables and the +implemented descriptor operations, including comparison and re-encoding. +The infinitesimal sign callbacks are test providers. General coefficient +interpretation, nested semantic replay and root-sum/Thom correspondence proofs +remain required. None of these fixtures supplies Phase-4 performance evidence. diff --git a/conformance-fixtures/HexSignDet/infinitesimal.jsonl b/conformance-fixtures/HexSignDet/infinitesimal.jsonl new file mode 100644 index 000000000..502865cd2 --- /dev/null +++ b/conformance-fixtures/HexSignDet/infinitesimal.jsonl @@ -0,0 +1,29 @@ +{"kind":"result","lib":"HexSignDet","case":"infinitesimal/passmore/whole","op":"table","value":{"coefficientContext":{"id":10377,"levels":["epsilon1"],"order":"each-new-level-smaller-than-positive-base-elements"},"data":{"direct":{"missingSupportReplay":null,"replay":true,"staleChildReplay":false,"status":"ok","table":[{"count":1,"signs":[-1]},{"count":2,"signs":[1]}]},"head":[{"den":[[1,1]],"num":[[1,1]]},{"den":[[1,1]],"num":[]},{"den":[[1,1]],"num":[[0,1],[-1,1]]},{"den":[[1,1]],"num":[[0,1],[-1,1]]},{"den":[[1,1]],"num":[]},{"den":[[1,1]],"num":[[0,1],[0,1],[1,1]]}],"lower":"-inf","queries":[[{"den":[[1,1]],"num":[[0,1],[-6,1]]},{"den":[[1,1]],"num":[]},{"den":[[1,1]],"num":[[0,1],[0,1],[60,1]]}]],"reduced":{"missingSupportReplay":null,"replay":true,"staleChildReplay":false,"status":"ok","table":[{"count":1,"signs":[-1]},{"count":2,"signs":[1]}]},"reference":{"replay":true,"status":"ok","table":[{"count":1,"signs":[-1]},{"count":2,"signs":[1]}]},"schema":1,"upper":"+inf"}}} +{"kind":"result","lib":"HexSignDet","case":"infinitesimal/passmore/positive","op":"table","value":{"coefficientContext":{"id":10377,"levels":["epsilon1"],"order":"each-new-level-smaller-than-positive-base-elements"},"data":{"direct":{"missingSupportReplay":null,"replay":true,"staleChildReplay":false,"status":"ok","table":[{"count":1,"signs":[-1]},{"count":1,"signs":[1]}]},"head":[{"den":[[1,1]],"num":[[1,1]]},{"den":[[1,1]],"num":[]},{"den":[[1,1]],"num":[[0,1],[-1,1]]},{"den":[[1,1]],"num":[[0,1],[-1,1]]},{"den":[[1,1]],"num":[]},{"den":[[1,1]],"num":[[0,1],[0,1],[1,1]]}],"lower":{"den":[[1,1]],"num":[]},"queries":[[{"den":[[1,1]],"num":[[0,1],[-6,1]]},{"den":[[1,1]],"num":[]},{"den":[[1,1]],"num":[[0,1],[0,1],[60,1]]}]],"reduced":{"missingSupportReplay":null,"replay":true,"staleChildReplay":false,"status":"ok","table":[{"count":1,"signs":[-1]},{"count":1,"signs":[1]}]},"reference":{"replay":true,"status":"ok","table":[{"count":1,"signs":[-1]},{"count":1,"signs":[1]}]},"schema":1,"upper":"+inf"}}} +{"kind":"result","lib":"HexSignDet","case":"infinitesimal/passmore/empty","op":"table","value":{"coefficientContext":{"id":10377,"levels":["epsilon1"],"order":"each-new-level-smaller-than-positive-base-elements"},"data":{"direct":{"missingSupportReplay":null,"replay":true,"staleChildReplay":false,"status":"ok","table":[{"count":2,"signs":[]}]},"head":[{"den":[[1,1]],"num":[[1,1]]},{"den":[[1,1]],"num":[]},{"den":[[1,1]],"num":[[0,1],[-1,1]]},{"den":[[1,1]],"num":[[0,1],[-1,1]]},{"den":[[1,1]],"num":[]},{"den":[[1,1]],"num":[[0,1],[0,1],[1,1]]}],"lower":{"den":[[1,1]],"num":[]},"queries":[],"reduced":{"missingSupportReplay":null,"replay":true,"staleChildReplay":false,"status":"ok","table":[{"count":2,"signs":[]}]},"reference":{"replay":true,"status":"ok","table":[{"count":2,"signs":[]}]},"schema":1,"upper":"+inf"}}} +{"kind":"result","lib":"HexSignDet","case":"infinitesimal/descriptor/passmore/cubic","op":"descriptor","value":{"coefficientContext":{"id":10377,"levels":["epsilon1"],"order":"each-new-level-smaller-than-positive-base-elements"},"data":{"context":10377,"head":[{"den":[[1,1]],"num":[[1,1]]},{"den":[[1,1]],"num":[]},{"den":[[1,1]],"num":[[0,1],[-1,1]]},{"den":[[1,1]],"num":[[0,1],[-1,1]]},{"den":[[1,1]],"num":[]},{"den":[[1,1]],"num":[[0,1],[0,1],[1,1]]}],"indices":[3],"lower":{"den":[[1,1]],"num":[]},"queries":[[{"den":[[1,1]],"num":[[0,1],[-6,1]]},{"den":[[1,1]],"num":[]},{"den":[[1,1]],"num":[[0,1],[0,1],[60,1]]}],[{"den":[[1,1]],"num":[]},{"den":[[1,1]],"num":[[1,1]]}],[{"den":[[1,1]],"num":[[1,1]]},{"den":[[1,1]],"num":[]},{"den":[[1,1]],"num":[[0,1],[-1,1]]},{"den":[[1,1]],"num":[[0,1],[-1,1]]},{"den":[[1,1]],"num":[]},{"den":[[1,1]],"num":[[0,1],[0,1],[1,1]]}]],"roots":{"roots":[{"indices":[1,2,3,4,5],"replay":true,"signs":[-1,-1,-1,1,1]},{"indices":[1,2,3,4,5],"replay":true,"signs":[1,1,1,1,1]}],"status":"ok"},"schema":1,"signs":[-1],"upper":"+inf","validation":{"changedHeadReplay":false,"completion":{"bindings":true,"copiedQueriesReplay":false,"indices":[1,2,3,4,5],"replay":true,"signs":[-1,-1,-1,1,1],"status":"ok"},"replay":true,"selected":{"replay":true,"signs":[-1,1,0],"status":"ok"},"staleContextReplay":false,"status":"ok"}}}} +{"kind":"result","lib":"HexSignDet","case":"infinitesimal/descriptor/passmore/square","op":"descriptor","value":{"coefficientContext":{"id":10377,"levels":["epsilon1"],"order":"each-new-level-smaller-than-positive-base-elements"},"data":{"context":10377,"head":[{"den":[[1,1]],"num":[[1,1]]},{"den":[[1,1]],"num":[]},{"den":[[1,1]],"num":[[0,1],[-1,1]]},{"den":[[1,1]],"num":[[0,1],[-1,1]]},{"den":[[1,1]],"num":[]},{"den":[[1,1]],"num":[[0,1],[0,1],[1,1]]}],"indices":[3],"lower":{"den":[[1,1]],"num":[]},"queries":[[{"den":[[1,1]],"num":[[0,1],[-6,1]]},{"den":[[1,1]],"num":[]},{"den":[[1,1]],"num":[[0,1],[0,1],[60,1]]}],[{"den":[[1,1]],"num":[]},{"den":[[1,1]],"num":[[1,1]]}],[{"den":[[1,1]],"num":[[1,1]]},{"den":[[1,1]],"num":[]},{"den":[[1,1]],"num":[[0,1],[-1,1]]},{"den":[[1,1]],"num":[[0,1],[-1,1]]},{"den":[[1,1]],"num":[]},{"den":[[1,1]],"num":[[0,1],[0,1],[1,1]]}]],"roots":{"roots":[{"indices":[1,2,3,4,5],"replay":true,"signs":[-1,-1,-1,1,1]},{"indices":[1,2,3,4,5],"replay":true,"signs":[1,1,1,1,1]}],"status":"ok"},"schema":1,"signs":[1],"upper":"+inf","validation":{"changedHeadReplay":false,"completion":{"bindings":true,"copiedQueriesReplay":false,"indices":[1,2,3,4,5],"replay":true,"signs":[1,1,1,1,1],"status":"ok"},"replay":true,"selected":{"replay":true,"signs":[1,1,0],"status":"ok"},"staleContextReplay":false,"status":"ok"}}}} +{"kind":"result","lib":"HexSignDet","case":"infinitesimal/descriptor/passmore/ambiguous","op":"descriptor","value":{"coefficientContext":{"id":10377,"levels":["epsilon1"],"order":"each-new-level-smaller-than-positive-base-elements"},"data":{"context":10377,"head":[{"den":[[1,1]],"num":[[1,1]]},{"den":[[1,1]],"num":[]},{"den":[[1,1]],"num":[[0,1],[-1,1]]},{"den":[[1,1]],"num":[[0,1],[-1,1]]},{"den":[[1,1]],"num":[]},{"den":[[1,1]],"num":[[0,1],[0,1],[1,1]]}],"indices":[],"lower":{"den":[[1,1]],"num":[]},"queries":[],"roots":{"roots":[{"indices":[1,2,3,4,5],"replay":true,"signs":[-1,-1,-1,1,1]},{"indices":[1,2,3,4,5],"replay":true,"signs":[1,1,1,1,1]}],"status":"ok"},"schema":1,"signs":[],"upper":"+inf","validation":{"reason":"ambiguous","status":"invalid-descriptor"}}}} +{"kind":"result","lib":"HexSignDet","case":"infinitesimal/descriptor/passmore/absent","op":"descriptor","value":{"coefficientContext":{"id":10377,"levels":["epsilon1"],"order":"each-new-level-smaller-than-positive-base-elements"},"data":{"context":10377,"head":[{"den":[[1,1]],"num":[[1,1]]},{"den":[[1,1]],"num":[]},{"den":[[1,1]],"num":[[0,1],[-1,1]]},{"den":[[1,1]],"num":[[0,1],[-1,1]]},{"den":[[1,1]],"num":[]},{"den":[[1,1]],"num":[[0,1],[0,1],[1,1]]}],"indices":[3],"lower":{"den":[[1,1]],"num":[]},"queries":[],"roots":{"roots":[{"indices":[1,2,3,4,5],"replay":true,"signs":[-1,-1,-1,1,1]},{"indices":[1,2,3,4,5],"replay":true,"signs":[1,1,1,1,1]}],"status":"ok"},"schema":1,"signs":[0],"upper":"+inf","validation":{"reason":"absent","status":"invalid-descriptor"}}}} +{"kind":"result","lib":"HexSignDet","case":"infinitesimal/descriptor/passmore/malformed","op":"descriptor","value":{"coefficientContext":{"id":10377,"levels":["epsilon1"],"order":"each-new-level-smaller-than-positive-base-elements"},"data":{"context":10377,"head":[{"den":[[1,1]],"num":[[1,1]]},{"den":[[1,1]],"num":[]},{"den":[[1,1]],"num":[[0,1],[-1,1]]},{"den":[[1,1]],"num":[[0,1],[-1,1]]},{"den":[[1,1]],"num":[]},{"den":[[1,1]],"num":[[0,1],[0,1],[1,1]]}],"indices":[9],"lower":{"den":[[1,1]],"num":[]},"queries":[],"roots":{"roots":[{"indices":[1,2,3,4,5],"replay":true,"signs":[-1,-1,-1,1,1]},{"indices":[1,2,3,4,5],"replay":true,"signs":[1,1,1,1,1]}],"status":"ok"},"schema":1,"signs":[-1],"upper":"+inf","validation":{"reason":"malformed","status":"invalid-descriptor"}}}} +{"kind":"result","lib":"HexSignDet","case":"infinitesimal/compare/passmore/order","op":"compare","value":{"coefficientContext":{"id":10377,"levels":["epsilon1"],"order":"each-new-level-smaller-than-positive-base-elements"},"data":{"left":{"context":10377,"head":[{"den":[[1,1]],"num":[[1,1]]},{"den":[[1,1]],"num":[]},{"den":[[1,1]],"num":[[0,1],[-1,1]]},{"den":[[1,1]],"num":[[0,1],[-1,1]]},{"den":[[1,1]],"num":[]},{"den":[[1,1]],"num":[[0,1],[0,1],[1,1]]}],"indices":[3],"lower":{"den":[[1,1]],"num":[]},"signs":[-1],"upper":"+inf"},"result":{"commonHead":[{"den":[[1,1]],"num":[[1,1]]},{"den":[[1,1]],"num":[]},{"den":[[1,1]],"num":[[0,1],[-1,1]]},{"den":[[1,1]],"num":[[0,1],[-1,1]]},{"den":[[1,1]],"num":[]},{"den":[[1,1]],"num":[[0,1],[0,1],[1,1]]}],"commonReplay":true,"leftReplay":true,"leftSigns":[-1,-1,-1,1,1],"order":"lt","rightReplay":true,"rightSigns":[1,1,1,1,1],"status":"ok"},"right":{"context":10377,"head":[{"den":[[1,1]],"num":[[1,1]]},{"den":[[1,1]],"num":[]},{"den":[[1,1]],"num":[[0,1],[-1,1]]},{"den":[[1,1]],"num":[[0,1],[-1,1]]},{"den":[[1,1]],"num":[]},{"den":[[1,1]],"num":[[0,1],[0,1],[1,1]]}],"indices":[3],"lower":{"den":[[1,1]],"num":[]},"signs":[1],"upper":"+inf"},"schema":1}}} +{"kind":"result","lib":"HexSignDet","case":"infinitesimal/reencode/passmore/reencode","op":"reencode","value":{"coefficientContext":{"id":10377,"levels":["epsilon1"],"order":"each-new-level-smaller-than-positive-base-elements"},"data":{"head":[{"den":[[1,1]],"num":[[-1,1]]},{"den":[[1,1]],"num":[]},{"den":[[1,1]],"num":[]},{"den":[[1,1]],"num":[[0,1],[1,1]]}],"lower":"-inf","result":{"indices":[1,2,3],"replay":true,"signs":[1,1,1],"status":"ok"},"schema":1,"source":{"context":10377,"head":[{"den":[[1,1]],"num":[[1,1]]},{"den":[[1,1]],"num":[]},{"den":[[1,1]],"num":[[0,1],[-1,1]]},{"den":[[1,1]],"num":[[0,1],[-1,1]]},{"den":[[1,1]],"num":[]},{"den":[[1,1]],"num":[[0,1],[0,1],[1,1]]}],"indices":[3],"lower":{"den":[[1,1]],"num":[]},"signs":[-1],"upper":"+inf"},"upper":"+inf"}}} +{"kind":"result","lib":"HexSignDet","case":"infinitesimal/square/zero-repeat","op":"table","value":{"coefficientContext":{"id":10377,"levels":["epsilon1"],"order":"each-new-level-smaller-than-positive-base-elements"},"data":{"direct":{"missingSupportReplay":false,"replay":true,"staleChildReplay":false,"status":"ok","table":[{"count":1,"signs":[0,-1,-1,0]},{"count":1,"signs":[0,1,1,0]}]},"head":[{"den":[[1,1]],"num":[[0,1],[-1,1]]},{"den":[[1,1]],"num":[]},{"den":[[1,1]],"num":[[1,1]]}],"lower":"-inf","queries":[[],[{"den":[[1,1]],"num":[]},{"den":[[1,1]],"num":[[1,1]]}],[{"den":[[1,1]],"num":[]},{"den":[[1,1]],"num":[[1,1]]}],[{"den":[[1,1]],"num":[[0,1],[-1,1]]},{"den":[[1,1]],"num":[]},{"den":[[1,1]],"num":[[1,1]]}]],"reduced":{"missingSupportReplay":false,"replay":true,"staleChildReplay":false,"status":"ok","table":[{"count":1,"signs":[0,-1,-1,0]},{"count":1,"signs":[0,1,1,0]}]},"reference":{"replay":true,"status":"ok","table":[{"count":1,"signs":[0,-1,-1,0]},{"count":1,"signs":[0,1,1,0]}]},"schema":1,"upper":"+inf"}}} +{"kind":"result","lib":"HexSignDet","case":"infinitesimal/square/negative-scale","op":"table","value":{"coefficientContext":{"id":10377,"levels":["epsilon1"],"order":"each-new-level-smaller-than-positive-base-elements"},"data":{"direct":{"missingSupportReplay":null,"replay":true,"staleChildReplay":false,"status":"ok","table":[{"count":1,"signs":[-1]},{"count":1,"signs":[1]}]},"head":[{"den":[[1,1]],"num":[[0,1],[1,1]]},{"den":[[1,1]],"num":[]},{"den":[[1,1]],"num":[[-1,1]]}],"lower":"-inf","queries":[[{"den":[[1,1]],"num":[]},{"den":[[1,1]],"num":[[1,1]]}]],"reduced":{"missingSupportReplay":null,"replay":true,"staleChildReplay":false,"status":"ok","table":[{"count":1,"signs":[-1]},{"count":1,"signs":[1]}]},"reference":{"replay":true,"status":"ok","table":[{"count":1,"signs":[-1]},{"count":1,"signs":[1]}]},"schema":1,"upper":"+inf"}}} +{"kind":"result","lib":"HexSignDet","case":"infinitesimal/descriptor/square/negative-head","op":"descriptor","value":{"coefficientContext":{"id":10377,"levels":["epsilon1"],"order":"each-new-level-smaller-than-positive-base-elements"},"data":{"context":10377,"head":[{"den":[[1,1]],"num":[[0,1],[1,1]]},{"den":[[1,1]],"num":[]},{"den":[[1,1]],"num":[[-1,1]]}],"indices":[1],"lower":"-inf","queries":[[{"den":[[1,1]],"num":[]},{"den":[[1,1]],"num":[[1,1]]}],[{"den":[[1,1]],"num":[[0,1],[-1,1]]},{"den":[[1,1]],"num":[]},{"den":[[1,1]],"num":[[1,1]]}]],"roots":{"roots":[{"indices":[1,2],"replay":true,"signs":[1,-1]},{"indices":[1,2],"replay":true,"signs":[-1,-1]}],"status":"ok"},"schema":1,"signs":[-1],"upper":"+inf","validation":{"changedHeadReplay":false,"completion":{"bindings":true,"copiedQueriesReplay":false,"indices":[1,2],"replay":true,"signs":[-1,-1],"status":"ok"},"replay":true,"selected":{"replay":true,"signs":[1,0],"status":"ok"},"staleContextReplay":false,"status":"ok"}}}} +{"kind":"result","lib":"HexSignDet","case":"infinitesimal/compare/square/scaled-equal","op":"compare","value":{"coefficientContext":{"id":10377,"levels":["epsilon1"],"order":"each-new-level-smaller-than-positive-base-elements"},"data":{"left":{"context":10377,"head":[{"den":[[1,1]],"num":[[0,1],[-1,1]]},{"den":[[1,1]],"num":[]},{"den":[[1,1]],"num":[[1,1]]}],"indices":[1],"lower":"-inf","signs":[1],"upper":"+inf"},"result":{"commonHead":[{"den":[[1,1]],"num":[[0,1],[-1,1]]},{"den":[[1,1]],"num":[]},{"den":[[1,1]],"num":[[1,1]]}],"commonReplay":true,"leftReplay":true,"leftSigns":[1,1],"order":"eq","rightReplay":true,"rightSigns":[1,1],"status":"ok"},"right":{"context":10377,"head":[{"den":[[1,1]],"num":[[0,1],[0,1],[1,1]]},{"den":[[1,1]],"num":[]},{"den":[[1,1]],"num":[[0,1],[-1,1]]}],"indices":[1],"lower":"-inf","signs":[-1],"upper":"+inf"},"schema":1}}} +{"kind":"result","lib":"HexSignDet","case":"infinitesimal/compare/passmore/shared-cubic","op":"compare","value":{"coefficientContext":{"id":10377,"levels":["epsilon1"],"order":"each-new-level-smaller-than-positive-base-elements"},"data":{"left":{"context":10377,"head":[{"den":[[1,1]],"num":[[1,1]]},{"den":[[1,1]],"num":[]},{"den":[[1,1]],"num":[[0,1],[-1,1]]},{"den":[[1,1]],"num":[[0,1],[-1,1]]},{"den":[[1,1]],"num":[]},{"den":[[1,1]],"num":[[0,1],[0,1],[1,1]]}],"indices":[3],"lower":{"den":[[1,1]],"num":[]},"signs":[-1],"upper":"+inf"},"result":{"commonHead":[{"den":[[1,1]],"num":[[1,1]]},{"den":[[1,1]],"num":[]},{"den":[[1,1]],"num":[[0,1],[-1,1]]},{"den":[[1,1]],"num":[[0,1],[-1,1]]},{"den":[[1,1]],"num":[]},{"den":[[1,1]],"num":[[0,1],[0,1],[1,1]]}],"commonReplay":true,"leftReplay":true,"leftSigns":[-1,-1,-1,1,1],"order":"eq","rightReplay":true,"rightSigns":[-1,-1,-1,1,1],"status":"ok"},"right":{"context":10377,"head":[{"den":[[1,1]],"num":[[-1,1]]},{"den":[[1,1]],"num":[]},{"den":[[1,1]],"num":[]},{"den":[[1,1]],"num":[[0,1],[1,1]]}],"indices":[1],"lower":{"den":[[1,1]],"num":[]},"signs":[1],"upper":"+inf"},"schema":1}}} +{"kind":"result","lib":"HexSignDet","case":"infinitesimal/square/zero-root","op":"table","value":{"coefficientContext":{"id":10377,"levels":["epsilon1"],"order":"each-new-level-smaller-than-positive-base-elements"},"data":{"direct":{"missingSupportReplay":false,"replay":true,"staleChildReplay":false,"status":"ok","table":[{"count":1,"signs":[0,0]}]},"head":[{"den":[[1,1]],"num":[]},{"den":[[1,1]],"num":[[1,1]]}],"lower":"-inf","queries":[[{"den":[[1,1]],"num":[]},{"den":[[1,1]],"num":[[1,1]]}],[]],"reduced":{"missingSupportReplay":false,"replay":true,"staleChildReplay":false,"status":"ok","table":[{"count":1,"signs":[0,0]}]},"reference":{"replay":true,"status":"ok","table":[{"count":1,"signs":[0,0]}]},"schema":1,"upper":"+inf"}}} +{"kind":"result","lib":"HexSignDet","case":"infinitesimal/square/constant","op":"table","value":{"coefficientContext":{"id":10377,"levels":["epsilon1"],"order":"each-new-level-smaller-than-positive-base-elements"},"data":{"direct":{"missingSupportReplay":null,"replay":true,"staleChildReplay":false,"status":"ok","table":[]},"head":[{"den":[[1,1]],"num":[[0,1],[1,1]]}],"lower":"-inf","queries":[],"reduced":{"missingSupportReplay":null,"replay":true,"staleChildReplay":false,"status":"ok","table":[]},"reference":{"replay":true,"status":"ok","table":[]},"schema":1,"upper":"+inf"}}} +{"kind":"result","lib":"HexSignDet","case":"infinitesimal/square/root-free","op":"table","value":{"coefficientContext":{"id":10377,"levels":["epsilon1"],"order":"each-new-level-smaller-than-positive-base-elements"},"data":{"direct":{"missingSupportReplay":null,"replay":true,"staleChildReplay":false,"status":"ok","table":[]},"head":[{"den":[[1,1]],"num":[[0,1],[1,1]]},{"den":[[1,1]],"num":[]},{"den":[[1,1]],"num":[[1,1]]}],"lower":"-inf","queries":[],"reduced":{"missingSupportReplay":null,"replay":true,"staleChildReplay":false,"status":"ok","table":[]},"reference":{"replay":true,"status":"ok","table":[]},"schema":1,"upper":"+inf"}}} +{"kind":"result","lib":"HexSignDet","case":"infinitesimal/square/repeated","op":"table","value":{"coefficientContext":{"id":10377,"levels":["epsilon1"],"order":"each-new-level-smaller-than-positive-base-elements"},"data":{"direct":{"status":"invalid-domain"},"head":[{"den":[[1,1]],"num":[[0,1],[0,1],[1,1]]},{"den":[[1,1]],"num":[]},{"den":[[1,1]],"num":[[0,1],[-2,1]]},{"den":[[1,1]],"num":[]},{"den":[[1,1]],"num":[[1,1]]}],"lower":"-inf","queries":[],"reduced":{"status":"invalid-domain"},"reference":{"status":"invalid-domain"},"schema":1,"upper":"+inf"}}} +{"kind":"result","lib":"HexSignDet","case":"infinitesimal/square/root-endpoint","op":"table","value":{"coefficientContext":{"id":10377,"levels":["epsilon1"],"order":"each-new-level-smaller-than-positive-base-elements"},"data":{"direct":{"status":"invalid-domain"},"head":[{"den":[[1,1]],"num":[[0,1],[-1,1]]},{"den":[[1,1]],"num":[[1,1]]}],"lower":{"den":[[1,1]],"num":[[0,1],[1,1]]},"queries":[],"reduced":{"status":"invalid-domain"},"reference":{"status":"invalid-domain"},"schema":1,"upper":"+inf"}}} +{"kind":"result","lib":"HexSignDet","case":"infinitesimal/square/cancelled","op":"table","value":{"coefficientContext":{"id":10377,"levels":["epsilon1"],"order":"each-new-level-smaller-than-positive-base-elements"},"data":{"direct":{"status":"invalid-domain"},"head":[],"lower":"-inf","queries":[],"reduced":{"status":"invalid-domain"},"reference":{"status":"invalid-domain"},"schema":1,"upper":"+inf"}}} +{"kind":"result","lib":"HexSignDet","case":"infinitesimal/nested/whole","op":"table","value":{"coefficientContext":{"id":10377,"levels":["epsilon1","epsilon2"],"order":"each-new-level-smaller-than-positive-base-elements"},"data":{"direct":{"missingSupportReplay":false,"replay":true,"staleChildReplay":false,"status":"ok","table":[{"count":1,"signs":[0,-1,0]},{"count":1,"signs":[1,0,0]},{"count":1,"signs":[1,1,0]}]},"head":[{"den":[{"den":[[1,1]],"num":[[1,1]]}],"num":[{"den":[[1,1]],"num":[]},{"den":[[1,1]],"num":[[0,1],[0,1],[-1,1]]},{"den":[[1,1]],"num":[[0,1],[-1,1]]}]},{"den":[{"den":[[1,1]],"num":[[1,1]]}],"num":[{"den":[[1,1]],"num":[[0,1],[0,1],[1,1]]},{"den":[[1,1]],"num":[[0,1],[3,1]]},{"den":[[1,1]],"num":[[1,1]]}]},{"den":[{"den":[[1,1]],"num":[[1,1]]}],"num":[{"den":[[1,1]],"num":[[0,1],[-2,1]]},{"den":[[1,1]],"num":[[-2,1]]}]},{"den":[{"den":[[1,1]],"num":[[1,1]]}],"num":[{"den":[[1,1]],"num":[[1,1]]}]}],"lower":"-inf","queries":[[{"den":[{"den":[[1,1]],"num":[[1,1]]}],"num":[{"den":[[1,1]],"num":[]},{"den":[[1,1]],"num":[[-1,1]]}]},{"den":[{"den":[[1,1]],"num":[[1,1]]}],"num":[{"den":[[1,1]],"num":[[1,1]]}]}],[{"den":[{"den":[[1,1]],"num":[[1,1]]}],"num":[{"den":[[1,1]],"num":[[0,1],[-1,1]]}]},{"den":[{"den":[[1,1]],"num":[[1,1]]}],"num":[{"den":[[1,1]],"num":[[1,1]]}]}],[]],"reduced":{"missingSupportReplay":false,"replay":true,"staleChildReplay":false,"status":"ok","table":[{"count":1,"signs":[0,-1,0]},{"count":1,"signs":[1,0,0]},{"count":1,"signs":[1,1,0]}]},"reference":{"replay":true,"status":"ok","table":[{"count":1,"signs":[0,-1,0]},{"count":1,"signs":[1,0,0]},{"count":1,"signs":[1,1,0]}]},"schema":1,"upper":"+inf"}}} +{"kind":"result","lib":"HexSignDet","case":"infinitesimal/nested/singleton","op":"table","value":{"coefficientContext":{"id":10377,"levels":["epsilon1","epsilon2"],"order":"each-new-level-smaller-than-positive-base-elements"},"data":{"direct":{"missingSupportReplay":null,"replay":true,"staleChildReplay":false,"status":"ok","table":[{"count":1,"signs":[]}]},"head":[{"den":[{"den":[[1,1]],"num":[[1,1]]}],"num":[{"den":[[1,1]],"num":[]},{"den":[[1,1]],"num":[[0,1],[0,1],[-1,1]]},{"den":[[1,1]],"num":[[0,1],[-1,1]]}]},{"den":[{"den":[[1,1]],"num":[[1,1]]}],"num":[{"den":[[1,1]],"num":[[0,1],[0,1],[1,1]]},{"den":[[1,1]],"num":[[0,1],[3,1]]},{"den":[[1,1]],"num":[[1,1]]}]},{"den":[{"den":[[1,1]],"num":[[1,1]]}],"num":[{"den":[[1,1]],"num":[[0,1],[-2,1]]},{"den":[[1,1]],"num":[[-2,1]]}]},{"den":[{"den":[[1,1]],"num":[[1,1]]}],"num":[{"den":[[1,1]],"num":[[1,1]]}]}],"lower":{"den":[{"den":[[1,1]],"num":[[1,1]]}],"num":[]},"queries":[],"reduced":{"missingSupportReplay":null,"replay":true,"staleChildReplay":false,"status":"ok","table":[{"count":1,"signs":[]}]},"reference":{"replay":true,"status":"ok","table":[{"count":1,"signs":[]}]},"schema":1,"upper":{"den":[{"den":[[1,1]],"num":[[1,1]]}],"num":[{"den":[[1,1]],"num":[]},{"den":[[1,1]],"num":[[2,1]]}]}}}} +{"kind":"result","lib":"HexSignDet","case":"infinitesimal/nested/reversed","op":"table","value":{"coefficientContext":{"id":10377,"levels":["epsilon1","epsilon2"],"order":"each-new-level-smaller-than-positive-base-elements"},"data":{"direct":{"status":"invalid-domain"},"head":[{"den":[{"den":[[1,1]],"num":[[1,1]]}],"num":[{"den":[[1,1]],"num":[]},{"den":[[1,1]],"num":[[0,1],[0,1],[-1,1]]},{"den":[[1,1]],"num":[[0,1],[-1,1]]}]},{"den":[{"den":[[1,1]],"num":[[1,1]]}],"num":[{"den":[[1,1]],"num":[[0,1],[0,1],[1,1]]},{"den":[[1,1]],"num":[[0,1],[3,1]]},{"den":[[1,1]],"num":[[1,1]]}]},{"den":[{"den":[[1,1]],"num":[[1,1]]}],"num":[{"den":[[1,1]],"num":[[0,1],[-2,1]]},{"den":[[1,1]],"num":[[-2,1]]}]},{"den":[{"den":[[1,1]],"num":[[1,1]]}],"num":[{"den":[[1,1]],"num":[[1,1]]}]}],"lower":{"den":[{"den":[[1,1]],"num":[[1,1]]}],"num":[{"den":[[1,1]],"num":[[0,1],[1,1]]}]},"queries":[],"reduced":{"status":"invalid-domain"},"reference":{"status":"invalid-domain"},"schema":1,"upper":{"den":[{"den":[[1,1]],"num":[[1,1]]}],"num":[{"den":[[1,1]],"num":[]},{"den":[[1,1]],"num":[[2,1]]}]}}}} +{"kind":"result","lib":"HexSignDet","case":"infinitesimal/nested/root-endpoint","op":"table","value":{"coefficientContext":{"id":10377,"levels":["epsilon1","epsilon2"],"order":"each-new-level-smaller-than-positive-base-elements"},"data":{"direct":{"status":"invalid-domain"},"head":[{"den":[{"den":[[1,1]],"num":[[1,1]]}],"num":[{"den":[[1,1]],"num":[]},{"den":[[1,1]],"num":[[0,1],[0,1],[-1,1]]},{"den":[[1,1]],"num":[[0,1],[-1,1]]}]},{"den":[{"den":[[1,1]],"num":[[1,1]]}],"num":[{"den":[[1,1]],"num":[[0,1],[0,1],[1,1]]},{"den":[[1,1]],"num":[[0,1],[3,1]]},{"den":[[1,1]],"num":[[1,1]]}]},{"den":[{"den":[[1,1]],"num":[[1,1]]}],"num":[{"den":[[1,1]],"num":[[0,1],[-2,1]]},{"den":[[1,1]],"num":[[-2,1]]}]},{"den":[{"den":[[1,1]],"num":[[1,1]]}],"num":[{"den":[[1,1]],"num":[[1,1]]}]}],"lower":{"den":[{"den":[[1,1]],"num":[[1,1]]}],"num":[{"den":[[1,1]],"num":[]},{"den":[[1,1]],"num":[[1,1]]}]},"queries":[],"reduced":{"status":"invalid-domain"},"reference":{"status":"invalid-domain"},"schema":1,"upper":"+inf"}}} +{"kind":"result","lib":"HexSignDet","case":"infinitesimal/descriptor/nested/singleton","op":"descriptor","value":{"coefficientContext":{"id":10377,"levels":["epsilon1","epsilon2"],"order":"each-new-level-smaller-than-positive-base-elements"},"data":{"context":10377,"head":[{"den":[{"den":[[1,1]],"num":[[1,1]]}],"num":[{"den":[[1,1]],"num":[]},{"den":[[1,1]],"num":[[0,1],[0,1],[-1,1]]},{"den":[[1,1]],"num":[[0,1],[-1,1]]}]},{"den":[{"den":[[1,1]],"num":[[1,1]]}],"num":[{"den":[[1,1]],"num":[[0,1],[0,1],[1,1]]},{"den":[[1,1]],"num":[[0,1],[3,1]]},{"den":[[1,1]],"num":[[1,1]]}]},{"den":[{"den":[[1,1]],"num":[[1,1]]}],"num":[{"den":[[1,1]],"num":[[0,1],[-2,1]]},{"den":[[1,1]],"num":[[-2,1]]}]},{"den":[{"den":[[1,1]],"num":[[1,1]]}],"num":[{"den":[[1,1]],"num":[[1,1]]}]}],"indices":[],"lower":{"den":[{"den":[[1,1]],"num":[[1,1]]}],"num":[]},"queries":[[{"den":[{"den":[[1,1]],"num":[[1,1]]}],"num":[{"den":[[1,1]],"num":[]},{"den":[[1,1]],"num":[[-1,1]]}]},{"den":[{"den":[[1,1]],"num":[[1,1]]}],"num":[{"den":[[1,1]],"num":[[1,1]]}]}],[{"den":[{"den":[[1,1]],"num":[[1,1]]}],"num":[{"den":[[1,1]],"num":[[0,1],[-1,1]]}]},{"den":[{"den":[[1,1]],"num":[[1,1]]}],"num":[{"den":[[1,1]],"num":[[1,1]]}]}]],"roots":{"roots":[{"indices":[1,2,3],"replay":true,"signs":[1,-1,1]}],"status":"ok"},"schema":1,"signs":[],"upper":{"den":[{"den":[[1,1]],"num":[[1,1]]}],"num":[{"den":[[1,1]],"num":[]},{"den":[[1,1]],"num":[[2,1]]}]},"validation":{"changedHeadReplay":false,"completion":{"bindings":true,"copiedQueriesReplay":false,"indices":[1,2,3],"replay":true,"signs":[1,-1,1],"status":"ok"},"replay":true,"selected":{"replay":true,"signs":[0,-1],"status":"ok"},"staleContextReplay":false,"status":"ok"}}}} +{"kind":"result","lib":"HexSignDet","case":"infinitesimal/descriptor/nested/reversed","op":"descriptor","value":{"coefficientContext":{"id":10377,"levels":["epsilon1","epsilon2"],"order":"each-new-level-smaller-than-positive-base-elements"},"data":{"context":10377,"head":[{"den":[{"den":[[1,1]],"num":[[1,1]]}],"num":[{"den":[[1,1]],"num":[]},{"den":[[1,1]],"num":[[0,1],[0,1],[-1,1]]},{"den":[[1,1]],"num":[[0,1],[-1,1]]}]},{"den":[{"den":[[1,1]],"num":[[1,1]]}],"num":[{"den":[[1,1]],"num":[[0,1],[0,1],[1,1]]},{"den":[[1,1]],"num":[[0,1],[3,1]]},{"den":[[1,1]],"num":[[1,1]]}]},{"den":[{"den":[[1,1]],"num":[[1,1]]}],"num":[{"den":[[1,1]],"num":[[0,1],[-2,1]]},{"den":[[1,1]],"num":[[-2,1]]}]},{"den":[{"den":[[1,1]],"num":[[1,1]]}],"num":[{"den":[[1,1]],"num":[[1,1]]}]}],"indices":[],"lower":{"den":[{"den":[[1,1]],"num":[[1,1]]}],"num":[{"den":[[1,1]],"num":[[0,1],[1,1]]}]},"queries":[],"roots":{"status":"invalid-domain"},"schema":1,"signs":[],"upper":{"den":[{"den":[[1,1]],"num":[[1,1]]}],"num":[{"den":[[1,1]],"num":[]},{"den":[[1,1]],"num":[[2,1]]}]},"validation":{"reason":"domain","status":"invalid-descriptor"}}}} +{"kind":"result","lib":"HexSignDet","case":"infinitesimal/descriptor/nested/stale-context","op":"descriptor","value":{"coefficientContext":{"id":10377,"levels":["epsilon1","epsilon2"],"order":"each-new-level-smaller-than-positive-base-elements"},"data":{"context":10378,"head":[{"den":[{"den":[[1,1]],"num":[[1,1]]}],"num":[{"den":[[1,1]],"num":[]},{"den":[[1,1]],"num":[[0,1],[0,1],[-1,1]]},{"den":[[1,1]],"num":[[0,1],[-1,1]]}]},{"den":[{"den":[[1,1]],"num":[[1,1]]}],"num":[{"den":[[1,1]],"num":[[0,1],[0,1],[1,1]]},{"den":[[1,1]],"num":[[0,1],[3,1]]},{"den":[[1,1]],"num":[[1,1]]}]},{"den":[{"den":[[1,1]],"num":[[1,1]]}],"num":[{"den":[[1,1]],"num":[[0,1],[-2,1]]},{"den":[[1,1]],"num":[[-2,1]]}]},{"den":[{"den":[[1,1]],"num":[[1,1]]}],"num":[{"den":[[1,1]],"num":[[1,1]]}]}],"indices":[],"lower":{"den":[{"den":[[1,1]],"num":[[1,1]]}],"num":[]},"queries":[],"roots":{"roots":[{"indices":[1,2,3],"replay":true,"signs":[1,-1,1]}],"status":"ok"},"schema":1,"signs":[],"upper":{"den":[{"den":[[1,1]],"num":[[1,1]]}],"num":[{"den":[[1,1]],"num":[]},{"den":[[1,1]],"num":[[2,1]]}]},"validation":{"reason":"context","status":"invalid-descriptor"}}}} +{"kind":"result","lib":"HexSignDet","case":"infinitesimal/reencode/nested/reencode","op":"reencode","value":{"coefficientContext":{"id":10377,"levels":["epsilon1","epsilon2"],"order":"each-new-level-smaller-than-positive-base-elements"},"data":{"head":[{"den":[{"den":[[1,1]],"num":[[1,1]]}],"num":[{"den":[[1,1]],"num":[]},{"den":[[1,1]],"num":[[-1,1]]}]},{"den":[{"den":[[1,1]],"num":[[1,1]]}],"num":[{"den":[[1,1]],"num":[[1,1]]}]}],"lower":"-inf","result":{"indices":[1],"replay":true,"signs":[1],"status":"ok"},"schema":1,"source":{"context":10377,"head":[{"den":[{"den":[[1,1]],"num":[[1,1]]}],"num":[{"den":[[1,1]],"num":[]},{"den":[[1,1]],"num":[[0,1],[0,1],[-1,1]]},{"den":[[1,1]],"num":[[0,1],[-1,1]]}]},{"den":[{"den":[[1,1]],"num":[[1,1]]}],"num":[{"den":[[1,1]],"num":[[0,1],[0,1],[1,1]]},{"den":[[1,1]],"num":[[0,1],[3,1]]},{"den":[[1,1]],"num":[[1,1]]}]},{"den":[{"den":[[1,1]],"num":[[1,1]]}],"num":[{"den":[[1,1]],"num":[[0,1],[-2,1]]},{"den":[[1,1]],"num":[[-2,1]]}]},{"den":[{"den":[[1,1]],"num":[[1,1]]}],"num":[{"den":[[1,1]],"num":[[1,1]]}]}],"indices":[],"lower":{"den":[{"den":[[1,1]],"num":[[1,1]]}],"num":[]},"signs":[],"upper":{"den":[{"den":[[1,1]],"num":[[1,1]]}],"num":[{"den":[[1,1]],"num":[]},{"den":[[1,1]],"num":[[2,1]]}]}},"upper":"+inf"}}} diff --git a/conformance/HexSignDet/EmitInfinitesimal.lean b/conformance/HexSignDet/EmitInfinitesimal.lean new file mode 100644 index 000000000..389b9b52c --- /dev/null +++ b/conformance/HexSignDet/EmitInfinitesimal.lean @@ -0,0 +1,217 @@ +/- +Copyright (c) 2026 Lean FRO, LLC. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Kim Morrison +-/ +import HexSignDet.Infinitesimal +import HexSignDet.Compare +import Hex.Conformance.Emit +import Lean.Data.Json + +/-! Exact rational-function coefficient fixtures for the pinned Z3 RCF oracle. +The order of infinitesimal introduction is part of every input record. -/ +namespace Hex.SignDet.EmitInfinitesimal +open Lean Infinitesimal + +variable {E : Type} [Lean.Grind.Field E] [DecidableEq E] [NatCast E] + +private def rat (q : Rat) : Json := toJson #[q.num, (q.den : Int)] +private def poly (coeff : E → Json) (p : DensePoly E) : Json := Json.arr (p.toArray.map coeff) +private def fraction (coeff : E → Json) (q : RationalFn E) : Json := + Json.mkObj [("num", poly coeff q.num), ("den", poly coeff q.den)] +private def first : First → Json := fraction rat +private def second : Second → Json := fraction first + +private def endpoint (coeff : E → Json) : Endpoint E → Json + | .negInf => toJson "-inf" + | .posInf => toJson "+inf" + | .finite q => coeff q + +private def emit (depth : Nat) (name op : String) (data : Json) : IO Unit := + let context := Json.mkObj [("id", toJson (10377 : Nat)), + ("levels", toJson ((List.range depth).map fun i => s!"epsilon{i + 1}")), + ("order", toJson "each-new-level-smaller-than-positive-base-elements")] + Hex.Conformance.Emit.emitResult "HexSignDet" ("infinitesimal/" ++ name) op + (Json.mkObj [("coefficientContext", context), ("data", data)]).compress + +/-- Refine the context in a descendant while retaining all parent certificates. -/ +private def staleChild : Replay E Nat → Replay E Nat + | .leaf n => .leaf { n with context := 10378 } + | .split n l r => .split n (staleChild l) r + +private def row (signs : List Int) (count : Nat) : Json := + Json.mkObj [("signs", toJson signs), ("count", toJson count)] + +private def table {r : Nat} (s : System r) : Json := + toJson (s.positive.map fun i => row s.columns[i] s.counts[i].toNat) + +private def result (t : Json) (replay : Bool) : Json := + Json.mkObj [("status", toJson "ok"), ("table", t), ("replay", toJson replay)] + +private def failure (error : BuildError) : Json := + Json.mkObj [("status", toJson "error"), ("error", toJson (reprStr error))] + +private def produced (sign : E → Int) (domain : Sturm.PreparedDomain E) (qs : List (DensePoly E)) + (reduced : Bool) : Json := + match buildPrepared (10377 : Nat) domain qs reduced with + | .error error => failure error + | .ok t => Json.mkObj [("status", toJson "ok"), ("table", table t.val.node.system), + ("replay", toJson (t.val.check sign 10377 domain.head domain.lower domain.upper qs)), + ("staleChildReplay", toJson ((staleChild t.val).check sign 10377 + domain.head domain.lower domain.upper qs)), + ("missingSupportReplay", if qs.length > 1 then toJson + ((Replay.leaf t.val.node).check sign 10377 domain.head domain.lower domain.upper qs) + else Json.null)] + +private def reference (sign : E → Int) (domain : Sturm.PreparedDomain E) (qs : List (DensePoly E)) : Json := + match referencePrepared (10377 : Nat) domain qs with + | .error error => failure error + | .ok n => result (table n.system) + (n.check sign 10377 domain.head domain.lower domain.upper qs) + +private def descriptorResult (sign : E → Int) (raw : RawDescriptor E Nat) (qs : List (DensePoly E)) : Json := + match Descriptor.build sign 10377 raw with + | .error err => failure err + | .ok (.error reason) => Json.mkObj [("status", toJson "invalid-descriptor"), + ("reason", toJson (match reason with + | .context => "context" | .malformed => "malformed" | .domain => "domain" + | .absent => "absent" | .ambiguous => "ambiguous"))] + | .ok (.ok d) => + let completion := match d.buildCompletion with + | .error err => failure err + | .ok c => Json.mkObj [("status", toJson "ok"), ("indices", toJson c.descriptor.raw.indices), + ("signs", toJson c.descriptor.raw.signs), + ("replay", toJson (c.descriptor.raw.check sign 10377 c.descriptor.evidence)), + ("bindings", toJson (d.raw.completes c.descriptor.raw)), + ("copiedQueriesReplay", toJson (c.descriptor.evidence.check sign 10377 + raw.head raw.lower raw.upper (c.descriptor.raw.queries.map fun _ => 0)))] + let selected := match d.buildSigns qs with + | .error err => failure err + | .ok s => Json.mkObj [("status", toJson "ok"), ("signs", toJson s.values.toList), + ("replay", toJson (d.checkSigns qs s.values s.evidence))] + Json.mkObj [("status", toJson "ok"), ("replay", toJson (raw.check sign 10377 d.evidence)), + ("completion", completion), ("selected", selected), + ("staleContextReplay", toJson (raw.check sign 10378 d.evidence)), + ("changedHeadReplay", toJson ({raw with head := -raw.head}.check sign 10377 d.evidence))] + +private def rootsResult (sign : E → Int) (raw : RawDescriptor E Nat) : Json := + match Descriptor.buildRoots sign 10377 raw.head raw.lower raw.upper with + | .error err => failure err + | .ok none => Json.mkObj [("status", toJson "invalid-domain")] + | .ok (some roots) => Json.mkObj [("status", toJson "ok"), ("roots", toJson (roots.map fun d => + Json.mkObj [("indices", toJson d.raw.indices), ("signs", toJson d.raw.signs), + ("replay", toJson (d.raw.check sign 10377 d.evidence))]))] + +private def emitDescriptor (coeff : E → Json) (sign : E → Int) (depth : Nat) (name : String) (raw : RawDescriptor E Nat) + (qs : List (DensePoly E)) : IO Unit := + emit depth ("descriptor/" ++ name) "descriptor" + (Json.mkObj [("schema", toJson (1 : Nat)), ("head", poly coeff raw.head), + ("lower", endpoint coeff raw.lower), ("upper", endpoint coeff raw.upper), + ("context", toJson raw.context), ("indices", toJson raw.indices), ("signs", toJson raw.signs), + ("queries", toJson (qs.map (poly coeff))), ("validation", descriptorResult sign raw qs), + ("roots", rootsResult sign raw)]) + +private def rawJson (coeff : E → Json) (raw : RawDescriptor E Nat) : Json := + Json.mkObj [("head", poly coeff raw.head), ("lower", endpoint coeff raw.lower), ("upper", endpoint coeff raw.upper), + ("context", toJson raw.context), ("indices", toJson raw.indices), ("signs", toJson raw.signs)] + +private def emitComparison (coeff : E → Json) (sign : E → Int) (depth : Nat) (name : String) (left right : RawDescriptor E Nat) : IO Unit := do + let output := match Descriptor.build sign 10377 left, + Descriptor.build sign 10377 right with + | .ok (.ok l), .ok (.ok r) => match l.buildComparison r with + | .error err => failure err + | .ok c => Json.mkObj [("status", toJson "ok"), ("commonHead", poly coeff c.common.head), + ("order", toJson (match c.order with | .lt => "lt" | .eq => "eq" | .gt => "gt")), + ("leftSigns", toJson c.leftEncoding.target.raw.signs), + ("rightSigns", toJson c.rightEncoding.target.raw.signs), + ("commonReplay", toJson (c.common.check 10377 left.head right.head)), + ("leftReplay", toJson (l.checkReencoding c.leftEncoding.target c.common.head + .negInf .posInf c.leftEncoding.evidence)), + ("rightReplay", toJson (r.checkReencoding c.rightEncoding.target c.common.head + .negInf .posInf c.rightEncoding.evidence))] + | _, _ => Json.mkObj [("status", toJson "invalid-input")] + emit depth ("compare/" ++ name) "compare" + (Json.mkObj [("schema", toJson (1 : Nat)), ("left", rawJson coeff left), + ("right", rawJson coeff right), ("result", output)]) + +private def emitReencoding (coeff : E → Json) (sign : E → Int) (depth : Nat) (name : String) (raw : RawDescriptor E Nat) + (head : DensePoly E) (a b : Endpoint E) : IO Unit := do + let output := match Descriptor.build sign 10377 raw with + | .ok (.ok d) => match d.buildReencoding head a b with + | .error err => failure err + | .ok none => Json.mkObj [("status", toJson "none")] + | .ok (some r) => Json.mkObj [("status", toJson "ok"), + ("signs", toJson r.target.raw.signs), ("indices", toJson r.target.raw.indices), + ("replay", toJson (d.checkReencoding r.target head a b r.evidence))] + | _ => Json.mkObj [("status", toJson "invalid-input")] + emit depth ("reencode/" ++ name) "reencode" + (Json.mkObj [("schema", toJson (1 : Nat)), ("source", rawJson coeff raw), + ("head", poly coeff head), ("lower", endpoint coeff a), ("upper", endpoint coeff b), + ("result", output)]) + +private def emitTable (coeff : E → Json) (sign : E → Int) (depth : Nat) + (name : String) (p : DensePoly E) (qs : List (DensePoly E)) + (lower : Endpoint E := .negInf) (upper : Endpoint E := .posInf) : IO Unit := do + let input := [("schema", toJson (1 : Nat)), ("head", poly coeff p), + ("queries", toJson (qs.map (poly coeff))), + ("lower", endpoint coeff lower), ("upper", endpoint coeff upper)] + let fields := match Sturm.prepare sign p lower upper with + | none => + let invalid := Json.mkObj [("status", toJson "invalid-domain")] + [("reduced", invalid), ("direct", invalid), ("reference", invalid)] + | some domain => + [("reduced", produced sign domain qs true), ("direct", produced sign domain qs false)] ++ + (if qs.length ≤ 4 then [("reference", reference sign domain qs)] else []) + emit depth name "table" (Json.mkObj (input ++ fields)) + +def run : IO Unit := do + let p := passmore + let third := p.derivative.derivative.derivative + emitTable first firstSign 1 "passmore/whole" p [third] + emitTable first firstSign 1 "passmore/positive" p [third] (.finite 0) .posInf + emitTable first firstSign 1 "passmore/empty" p [] (.finite 0) .posInf + let raw : RawDescriptor First Nat := ⟨10377, p, .finite 0, .posInf, [3], [-1]⟩ + emitDescriptor first firstSign 1 "passmore/cubic" raw [third, x, p] + emitDescriptor first firstSign 1 "passmore/square" {raw with signs := [1]} [third, x, p] + emitDescriptor first firstSign 1 "passmore/ambiguous" {raw with indices := [], signs := []} [] + emitDescriptor first firstSign 1 "passmore/absent" {raw with signs := [0]} [] + emitDescriptor first firstSign 1 "passmore/malformed" {raw with indices := [9]} [] + emitComparison first firstSign 1 "passmore/order" raw {raw with signs := [1]} + emitReencoding first firstSign 1 "passmore/reencode" raw + (DensePoly.C epsilon * x.natPow 3 - 1) .negInf .posInf + let q : DensePoly First := x.natPow 2 - DensePoly.C epsilon + emitTable first firstSign 1 "square/zero-repeat" q [0, x, x, q] + emitTable first firstSign 1 "square/negative-scale" (-q) [x] + let qr : RawDescriptor First Nat := ⟨10377, q, .negInf, .posInf, [1], [1]⟩ + emitDescriptor first firstSign 1 "square/negative-head" + {qr with head := -q, signs := [-1]} [x, q] + emitComparison first firstSign 1 "square/scaled-equal" qr + {qr with head := DensePoly.C (-epsilon) * q, signs := [-1]} + emitComparison first firstSign 1 "passmore/shared-cubic" raw + {raw with head := DensePoly.C epsilon * x.natPow 3 - 1, indices := [1], signs := [1]} + emitTable first firstSign 1 "square/zero-root" x [x, 0] + emitTable first firstSign 1 "square/constant" (DensePoly.C epsilon) [] + emitTable first firstSign 1 "square/root-free" (x.natPow 2 + DensePoly.C epsilon) [] + emitTable first firstSign 1 "square/repeated" (q * q) [] + emitTable first firstSign 1 "square/root-endpoint" (x - DensePoly.C epsilon) [] + (.finite epsilon) .posInf + emitTable first firstSign 1 "square/cancelled" (q - q) [] + let n := nested + emitTable second secondSign 2 "nested/whole" n + [x - DensePoly.C delta, x - DensePoly.C (lift epsilon), 0] + emitTable second secondSign 2 "nested/singleton" n [] (.finite 0) (.finite (2 * delta)) + emitTable second secondSign 2 "nested/reversed" n [] + (.finite (lift epsilon)) (.finite (2 * delta)) + emitTable second secondSign 2 "nested/root-endpoint" n [] (.finite delta) .posInf + let nr : RawDescriptor Second Nat := ⟨10377, n, .finite 0, .finite (2 * delta), [], []⟩ + emitDescriptor second secondSign 2 "nested/singleton" nr + [x - DensePoly.C delta, x - DensePoly.C (lift epsilon)] + emitDescriptor second secondSign 2 "nested/reversed" + {nr with lower := .finite (lift epsilon)} [] + emitDescriptor second secondSign 2 "nested/stale-context" {nr with context := 10378} [] + emitReencoding second secondSign 2 "nested/reencode" nr + (x - DensePoly.C delta) .negInf .posInf + +end Hex.SignDet.EmitInfinitesimal + +def main : IO Unit := Hex.SignDet.EmitInfinitesimal.run diff --git a/conformance/HexSignDet/Infinitesimal.lean b/conformance/HexSignDet/Infinitesimal.lean new file mode 100644 index 000000000..476859865 --- /dev/null +++ b/conformance/HexSignDet/Infinitesimal.lean @@ -0,0 +1,63 @@ +/- +Copyright (c) 2026 Lean FRO, LLC. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Kim Morrison +-/ +module + +public import HexSignDet +public import HexRationalFn +public meta import HexRationalFn + +public section + +/-! Test coefficient providers for exact infinitesimal conformance. The outer +indeterminate is positive and smaller than every positive base-field element. +These use the existing rational-function field operations, with an explicit +sign callback. They do not register ordered-function or real-closure providers. -/ +namespace Hex.SignDet.Infinitesimal + +/-- The first nonzero coefficient determines a polynomial's sign at a positive +infinitesimal. The base callback is itself exact, including at nested levels. -/ +def lowestSign {K : Type} [Zero K] [DecidableEq K] + (sign : K → Int) (p : DensePoly K) : Int := + match p.toArray.toList.find? (fun c => c != 0) with + | none => 0 + | some c => sign c + +/-- A fraction's sign is the product of its numerator and denominator signs. -/ +def sign {K : Type} [Lean.Grind.Field K] [DecidableEq K] + (baseSign : K → Int) (f : RationalFn K) : Int := + lowestSign baseSign f.num * lowestSign baseSign f.den + +abbrev First := RationalFn Rat +abbrev Second := RationalFn First + +def firstSign : First → Int := sign Sturm.orderSign +def secondSign : Second → Int := sign firstSign + +def epsilon : First := RationalFn.X +def delta : Second := RationalFn.X +def lift (a : First) : Second := RationalFn.C a + +def x {K : Type} [Zero K] [One K] [DecidableEq K] : DensePoly K := + DensePoly.ofCoeffs #[0, 1] + +/-- The corrected de Moura–Passmore example. -/ +def passmore : DensePoly First := + (DensePoly.C epsilon * x.natPow 2 - 1) * (DensePoly.C epsilon * x.natPow 3 - 1) + +/-- Three nested-level roots, in the order δ, ε, ε+δ. -/ +def nested : DensePoly Second := + (x - DensePoly.C delta) * (x - DensePoly.C (lift epsilon)) * + (x - DensePoly.C (lift epsilon + delta)) + +#guard firstSign 0 = 0 +#guard firstSign (epsilon - 1) = -1 +#guard firstSign (epsilon / (epsilon - 1)) = -1 +#guard firstSign ((epsilon * epsilon - 1) / (epsilon - 1)) = 1 +#guard firstSign (epsilon - epsilon) = 0 +#guard secondSign (lift epsilon - delta) = 1 +#guard secondSign (delta - lift (epsilon * epsilon)) = -1 + +end Hex.SignDet.Infinitesimal diff --git a/lakefile.lean b/lakefile.lean index 5ff753bdb..a436d8c48 100644 --- a/lakefile.lean +++ b/lakefile.lean @@ -1005,7 +1005,7 @@ lean_lib HexConformance where ++ #[`HexReflect.TestProviders, `HexReflect.Conformance, `HexReflect.ScopeConformance, `HexReflect.ResidueConformance].map Glob.one - ++ #[`HexSignDet.Conformance, `HexSignDetMathlib.Conformance].map Glob.one + ++ #[`HexSignDet.Conformance, `HexSignDet.Infinitesimal, `HexSignDetMathlib.Conformance].map Glob.one ++ #[`HexSturm.Fixtures, `HexSturm.Conformance, `HexSturmMathlib.Conformance].map Glob.one ++ #[.submodules `HexSturmMathlib.Replay] @@ -1350,6 +1350,10 @@ lean_exe hexsigndet_emit_fixtures where srcDir := "conformance" root := `HexSignDet.EmitFixtures +lean_exe hexsigndet_emit_infinitesimal where + srcDir := "conformance" + root := `HexSignDet.EmitInfinitesimal + lean_exe hexrealformula_emit_fixtures where srcDir := "conformance" root := `HexRealFormula.EmitFixtures diff --git a/scripts/bench/proof_only_runtime_exemptions/lakefile-lean-327c99ca-a436d8c4.json b/scripts/bench/proof_only_runtime_exemptions/lakefile-lean-327c99ca-a436d8c4.json new file mode 100644 index 000000000..deaabd9a3 --- /dev/null +++ b/scripts/bench/proof_only_runtime_exemptions/lakefile-lean-327c99ca-a436d8c4.json @@ -0,0 +1,6 @@ +{ + "path": "lakefile.lean", + "baseline_blob": "327c99cacafccb757254a4ec924e9b7f90d3b9e3", + "current_blob": "a436d8c48bbb464e7d4680c0c083b2df06ef6d16", + "reason": "The only changed hexbz_factor_service-relevant declaration enables precompileModules on HexBasic. The measured native executable already links compiled HexBasic code; its Lean sources, executable declaration, C/object compilation options and runtime call graph are unchanged. This adds elaborator-loadable dynlibs, not a different native factorization implementation. Other changes register independent libraries, conformance modules, proof probes and executables, including hexsigndet_emit_fixtures; these targets are not dependencies of the measured factorization service. The HexPrimality/HexIntFactor producer flags and ECM diagnostic registrations do not reach that polynomial-factor service. This exemption makes no runtime-neutral claim about those separate construction paths. Relative to the already audited 5ff753bdb0c9985510f510f39e6e6eb465e98371 blob, this adds only HexSignDet.Infinitesimal to HexConformance and the hexsigndet_emit_infinitesimal executable. Comparing parsed Lake blocks finds no other change. Neither new conformance module belongs to the factorization service runtime import closure." +} diff --git a/scripts/ci/run_oracles.sh b/scripts/ci/run_oracles.sh index a6e2ef0df..452b4f255 100755 --- a/scripts/ci/run_oracles.sh +++ b/scripts/ci/run_oracles.sh @@ -59,6 +59,8 @@ ORACLES=( "HexRCF|hexrcf_emit_fixtures|scripts/oracle/rcf_flint.py|conformance-fixtures/HexRCF/rcf.jsonl" "HexRoots|hexroots_emit_fixtures|scripts/oracle/roots_flint.py|conformance-fixtures/HexRoots/roots.jsonl" "HexRealAlgebraic|hexrealalgebraic_emit_fixtures|scripts/oracle/real_algebraic_flint.py|conformance-fixtures/HexRealAlgebraic/real_algebraic.jsonl" + # Pinned Z3 RCF, exact nested-infinitesimal roots + "HexSignDet|hexsigndet_emit_infinitesimal|scripts/oracle/sign_det_z3.py|conformance-fixtures/HexSignDet/infinitesimal.jsonl" # SymPy backed "HexKronecker|hexkronecker_emit_fixtures|scripts/oracle/kronecker_sympy.py|conformance-fixtures/HexKronecker/identities.jsonl" "HexPolyDet|hexpolydet_emit_fixtures|scripts/oracle/matrix_carriers.py|conformance-fixtures/HexPolyDet/det.jsonl" @@ -128,6 +130,7 @@ import flint import cypari2 import conway_polynomials import sympy +import z3 PY then echo "FAIL: required oracle dependencies are unavailable" >&2 @@ -204,13 +207,20 @@ run_tuple() { fi fi - if [ "$lib" = "HexSignDet" ]; then + if [ "$oracle" = "scripts/oracle/sign_det_flint.py" ]; then if ! python3 -m unittest scripts.oracle.test_sign_det_flint; then echo "FAIL: $lib :: oracle rejection checks failed" return 1 fi fi + if [ "$oracle" = "scripts/oracle/sign_det_z3.py" ]; then + if ! python3 -m unittest scripts.oracle.test_sign_det_z3; then + echo "FAIL: $lib :: infinitesimal oracle rejection checks failed" + return 1 + fi + fi + local oracle_args=() case "$oracle" in *primality_pari.py) diff --git a/scripts/oracle/sign_det_common.py b/scripts/oracle/sign_det_common.py new file mode 100644 index 000000000..670ae152e --- /dev/null +++ b/scripts/oracle/sign_det_common.py @@ -0,0 +1,52 @@ +"""Serialization checks shared by independent exact sign/root oracles. + +This module contains no polynomial arithmetic or expected-root computation. +""" +from typing import Any + +from scripts.oracle.common import OracleMismatch + + +def require(condition: bool, message: str) -> None: + if not condition: + raise OracleMismatch(message) + + +def check_output(output: Any, expected: list[dict[str, Any]] | None, arity: int) -> None: + require(isinstance(output, dict), "missing constructor result") + if expected is None: + require(output == {"status": "invalid-domain"}, "invalid domain was accepted") + return + require(output.get("status") == "ok", f"valid-domain construction failed: {output!r}") + require(output.get("replay") is True, "produced replay did not pass its checker") + check_table(output.get("table"), expected, arity) + + +def check_table(table: Any, expected: list[dict[str, Any]], arity: int) -> None: + require(isinstance(table, list), "missing sparse sign table") + seen = set() + for row in table: + require(isinstance(row, dict) and set(row) == {"signs", "count"}, "malformed table row") + signs, count = row["signs"], row["count"] + require(isinstance(signs, list) and len(signs) == arity and + all(type(s) is int and s in (-1, 0, 1) for s in signs), "malformed sign condition") + require(type(count) is int and count > 0, "sparse counts must be positive integers") + key = tuple(signs) + require(key not in seen, "duplicate sign condition") + seen.add(key) + require(table == sorted(table, key=lambda row: row["signs"]), + "produced table rows are not in the serialization order") + require(table == expected, f"complete sign table differs: Lean={table!r}, oracle={expected!r}") + + +def sign_vector(value: Any, size: int) -> bool: + return (isinstance(value, list) and len(value) == size and + all(type(v) is int and v in (-1, 0, 1) for v in value)) + + +def check_encoding(value: Any, degree: int) -> None: + require(isinstance(value, dict) and isinstance(value.get("indices"), list) and + all(type(i) is int for i in value["indices"]) and + value["indices"] == list(range(1, degree + 1)) and + sign_vector(value.get("signs"), degree) and value.get("replay") is True, + "malformed or unchecked full root encoding") diff --git a/scripts/oracle/sign_det_flint.py b/scripts/oracle/sign_det_flint.py index c6032350d..1c11e3fbd 100644 --- a/scripts/oracle/sign_det_flint.py +++ b/scripts/oracle/sign_det_flint.py @@ -22,6 +22,7 @@ sys.path.insert(0, str(ROOT)) from scripts.oracle.common import OracleMismatch, read_fixtures, write_failure +from scripts.oracle.sign_det_common import require, check_output, check_table, sign_vector, check_encoding from scripts.oracle.real_algebraic_qqbar import QQBar, Unavailable, VERSION DEFAULT_FIXTURE = ROOT / "conformance-fixtures/HexSignDet/sign_det.jsonl" @@ -49,11 +50,6 @@ } -def require(condition: bool, message: str) -> None: - if not condition: - raise OracleMismatch(message) - - def rational(value: Any) -> Fraction: require(isinstance(value, list) and len(value) == 2 and all(type(x) is int for x in value) and value[1] > 0, @@ -127,33 +123,6 @@ def expected_table(data: dict[str, Any]) -> list[dict[str, Any]] | None: return [{"signs": list(signs), "count": count} for signs, count in sorted(counts.items())] -def check_output(output: Any, expected: list[dict[str, Any]] | None, arity: int) -> None: - require(isinstance(output, dict), "missing constructor result") - if expected is None: - require(output == {"status": "invalid-domain"}, "invalid domain was accepted") - return - require(output.get("status") == "ok", f"valid-domain construction failed: {output!r}") - require(output.get("replay") is True, "produced replay did not pass its checker") - check_table(output.get("table"), expected, arity) - - -def check_table(table: Any, expected: list[dict[str, Any]], arity: int) -> None: - require(isinstance(table, list), "missing sparse sign table") - seen = set() - for row in table: - require(isinstance(row, dict) and set(row) == {"signs", "count"}, "malformed table row") - signs, count = row["signs"], row["count"] - require(isinstance(signs, list) and len(signs) == arity and - all(type(s) is int and s in (-1, 0, 1) for s in signs), "malformed sign condition") - require(type(count) is int and count > 0, "sparse counts must be positive integers") - key = tuple(signs) - require(key not in seen, "duplicate sign condition") - seen.add(key) - require(table == sorted(table, key=lambda row: row["signs"]), - "produced table rows are not in the serialization order") - require(table == expected, f"complete sign table differs: Lean={table!r}, FLINT={expected!r}") - - def derivative_queries(head: Any) -> list[list[list[int]]]: coefficients = polynomial(head) while coefficients and coefficients[-1] == 0: @@ -165,19 +134,6 @@ def derivative_queries(head: Any) -> list[list[list[int]]]: return derivatives -def sign_vector(value: Any, size: int) -> bool: - return (isinstance(value, list) and len(value) == size and - all(type(v) is int and v in (-1, 0, 1) for v in value)) - - -def check_encoding(value: Any, degree: int) -> None: - require(isinstance(value, dict) and isinstance(value.get("indices"), list) and - all(type(i) is int for i in value["indices"]) and - value["indices"] == list(range(1, degree + 1)) and - sign_vector(value.get("signs"), degree) and value.get("replay") is True, - "malformed or unchecked full root encoding") - - def check_descriptor(data: dict[str, Any]) -> None: require(type(data["context"]) is int and data["context"] >= 0, "malformed descriptor context") derivatives = derivative_queries(data["head"]) diff --git a/scripts/oracle/sign_det_z3.py b/scripts/oracle/sign_det_z3.py new file mode 100644 index 000000000..b2562b04a --- /dev/null +++ b/scripts/oracle/sign_det_z3.py @@ -0,0 +1,331 @@ +#!/usr/bin/env python3 +"""Exact Z3 RCF oracle for sign determination over nested infinitesimals. + +Pin: z3-solver 4.15.4.0 and numeric runtime version (4, 15, 4, 0). +Each record gets a fresh RCF context; +each successive infinitesimal is smaller than positive base-field elements. +Roots, signs and comparisons use exact RCF operations, never decimal output. +""" +from __future__ import annotations + +import argparse +from collections import Counter +from importlib.metadata import version +from pathlib import Path +import sys +from typing import Any + +ROOT = Path(__file__).resolve().parents[2] +sys.path.insert(0, str(ROOT)) + +from scripts.oracle.common import OracleMismatch, read_fixtures, write_failure +from scripts.oracle.sign_det_common import require, check_encoding, check_output, sign_vector + +VERSION = "z3-solver 4.15.4.0" +DEFAULT_FIXTURE = ROOT / "conformance-fixtures/HexSignDet/infinitesimal.jsonl" +REQUIRED_CASES = {"infinitesimal/" + name for name in ( + "passmore/whole", "passmore/positive", "passmore/empty", "descriptor/passmore/cubic", + "descriptor/passmore/square", "descriptor/passmore/ambiguous", "compare/passmore/order", + "reencode/passmore/reencode", "square/zero-repeat", "square/negative-scale", + "square/repeated", "square/root-endpoint", "square/cancelled", "nested/whole", + "nested/singleton", "descriptor/nested/singleton", "descriptor/nested/stale-context", + "reencode/nested/reencode", "descriptor/square/negative-head", "compare/square/scaled-equal", + "compare/passmore/shared-cubic", "square/zero-root", "square/constant", "square/root-free", + "nested/reversed", "nested/root-endpoint", "descriptor/passmore/absent", + "descriptor/passmore/malformed", "descriptor/nested/reversed", +)} + + +def check_version() -> None: + import z3 + require(version("z3-solver") == "4.15.4.0" and z3.get_version()[:4] == (4, 15, 4, 0), + "the exact pinned z3-solver 4.15.4.0 is required") + + +class RCF: + """An independent exact root oracle for one serialized coefficient context.""" + + def __init__(self, context: Any): + import z3 + from z3 import z3rcf + require(isinstance(context, dict) and set(context) == {"id", "levels", "order"}, + "malformed coefficient context") + levels = context["levels"] + require(type(context["id"]) is int and context["id"] == 10377 and + isinstance(levels, list) and 1 <= len(levels) <= 2 and + levels == [f"epsilon{i + 1}" for i in range(len(levels))] and + context["order"] == "each-new-level-smaller-than-positive-base-elements", + "foreign, reordered or incomplete coefficient context") + self.context = z3.Context() + self.api = z3rcf + self.levels = [z3rcf.MkInfinitesimal(name, self.context) for name in levels] + self.zero = z3rcf.RCFNum(0, self.context) + self.one = z3rcf.RCFNum(1, self.context) + + def coeff(self, value: Any, depth: int | None = None): + if depth is None: + depth = len(self.levels) + if depth == 0: + require(isinstance(value, list) and len(value) == 2 and + all(type(v) is int for v in value) and value[1] > 0, + "malformed exact rational coefficient") + return self.api.RCFNum(f"{value[0]}/{value[1]}", self.context) + require(isinstance(value, dict) and set(value) == {"num", "den"} and + isinstance(value["num"], list) and isinstance(value["den"], list), + "malformed rational-function coefficient") + point = self.levels[depth - 1] + num = self.eval([self.coeff(c, depth - 1) for c in value["num"]], point) + den = self.eval([self.coeff(c, depth - 1) for c in value["den"]], point) + require(den != 0, "zero coefficient denominator") + # This pinned Python API exposes __div__, not Python 3 __truediv__. + return num.__div__(den) + + def poly(self, value: Any): + require(isinstance(value, list), "polynomial coefficients must be a list") + return self.trim([self.coeff(c) for c in value]) + + @staticmethod + def trim(p): + while p and p[-1] == 0: + p.pop() + return p + + def eval(self, p, x): + result = self.zero + for c in reversed(p): + result = result * x + c + return result + + def derivative(self, p): + return self.trim([c * i for i, c in enumerate(p)][1:]) + + def derivatives(self, p): + result = [] + for _ in range(len(p) - 1): + p = self.derivative(p) + result.append(p) + return result + + def remainder(self, p, q): + require(bool(q), "polynomial division by zero") + p = p.copy() + while len(p) >= len(q): + offset = len(p) - len(q) + scale = p[-1].__div__(q[-1]) + for i, c in enumerate(q): + p[offset + i] = p[offset + i] - scale * c + self.trim(p) + return p + + def squarefree(self, p): + if not p: + return False + q = self.derivative(p) + while q: + p, q = q, self.remainder(p, q) + return len(p) == 1 + + def endpoint(self, value): + if value == "-inf": + return (0, self.zero) + if value == "+inf": + return (2, self.zero) + return (1, self.coeff(value)) + + def domain(self, raw): + p = self.poly(raw["head"]) + a, b = self.endpoint(raw["lower"]), self.endpoint(raw["upper"]) + if not self.squarefree(p) or not a < b: + return p, None + if any(tag == 1 and self.eval(p, x) == 0 for tag, x in (a, b)): + return p, None + roots = sorted(self.api.MkRoots(p, self.context)) if len(p) > 1 else [] + require(all(x < y for x, y in zip(roots, roots[1:])), "oracle returned duplicate roots") + return p, [x for x in roots if (a[0] == 0 or a[1] < x) and (b[0] == 2 or x < b[1])] + + def signs(self, queries, root): + return [1 if (v := self.eval(q, root)) > 0 else -1 if v < 0 else 0 for q in queries] + + def table(self, data): + _, roots = self.domain(data) + queries = [self.poly(q) for q in data["queries"]] + if roots is None: + return None + counts = Counter(tuple(self.signs(queries, root)) for root in roots) + return [{"signs": list(signs), "count": count} for signs, count in sorted(counts.items())] + + def selection(self, raw, p, roots): + indices, signs = raw["indices"], raw["signs"] + require(type(raw["context"]) is int and raw["context"] >= 0 and + isinstance(indices, list) and isinstance(signs, list), "malformed descriptor input") + if raw["context"] != 10377: + return "context", [] + if roots is None: + return "domain", [] + n = len(p) - 1 + if (n <= 0 or any(type(i) is not int or not 1 <= i <= n for i in indices) or + len(indices) != len(set(indices)) or not sign_vector(signs, len(indices))): + return "malformed", [] + derivatives = self.derivatives(p) + selected = [r for r in roots if self.signs([derivatives[i - 1] for i in indices], r) == signs] + return (None if len(selected) == 1 else "absent" if not selected else "ambiguous"), selected + + def descriptor(self, data): + p, roots = self.domain(data) + derivatives = self.derivatives(p) + n = len(derivatives) + actual_roots = data["roots"] + if roots is None: + require(actual_roots == {"status": "invalid-domain"}, "invalid root-list domain accepted") + else: + require(isinstance(actual_roots, dict) and isinstance(actual_roots.get("roots"), list), + "missing root list") + for encoding in actual_roots["roots"]: + check_encoding(encoding, n) + expected = [{"indices": list(range(1, n + 1)), "signs": self.signs(derivatives, r), + "replay": True} for r in roots] + require(actual_roots == {"status": "ok", "roots": expected}, + "full encodings differ from exact increasing Z3 roots") + reason, selected = self.selection(data, p, roots) + actual = data["validation"] + if reason is not None: + require(actual == {"status": "invalid-descriptor", "reason": reason}, + f"invalid descriptor reason differs: {reason}") + return + require(actual.get("status") == "ok" and actual.get("replay") is True, + "valid descriptor construction/replay failed") + require(actual.get("staleContextReplay") is False and + actual.get("changedHeadReplay") is False, "stale descriptor evidence accepted") + check_encoding(actual.get("completion"), n) + require(isinstance(actual.get("selected"), dict) and + sign_vector(actual["selected"].get("signs"), len(data["queries"])), + "malformed selected query signs") + expected = {"status": "ok", "indices": list(range(1, n + 1)), + "signs": self.signs(derivatives, selected[0]), "replay": True, "bindings": True, + "copiedQueriesReplay": False} + require(actual["completion"] == expected, "completion changes selected root") + require(actual.get("selected") == {"status": "ok", "replay": True, + "signs": self.signs([self.poly(q) for q in data["queries"]], selected[0])}, + "selected query signs differ from exact Z3 evaluation") + + def selected(self, raw): + p, roots = self.domain(raw) + reason, selected = self.selection(raw, p, roots) + require(reason is None, f"invalid comparison/re-encoding source: {reason}") + return p, selected[0] + + def comparison(self, data): + left, a = self.selected(data["left"]) + right, b = self.selected(data["right"]) + out = data["result"] + require(out.get("status") == "ok" and all(out.get(flag) is True for flag in + ("commonReplay", "leftReplay", "rightReplay")), "unchecked comparison") + head = self.poly(out["commonHead"]) + product = [self.zero] * (len(left) + len(right) - 1) + for i, x in enumerate(left): + for j, y in enumerate(right): + product[i + j] = product[i + j] + x * y + require(self.squarefree(head) and not self.remainder(product, head) and + not self.remainder(head, left) and not self.remainder(head, right), + "common head is not a squarefree root union") + require(out.get("order") == ("lt" if a < b else "gt" if a > b else "eq"), + "comparison differs from exact Z3 root order") + derivatives = self.derivatives(head) + require(sign_vector(out.get("leftSigns"), len(derivatives)) and + sign_vector(out.get("rightSigns"), len(derivatives)), "malformed common-root encodings") + require(out.get("leftSigns") == self.signs(derivatives, a) and + out.get("rightSigns") == self.signs(derivatives, b), "wrong common-root encodings") + + def reencoding(self, data): + _, root = self.selected(data["source"]) + p, roots = self.domain(data) + out = data["result"] + if roots is None or not any(root == r for r in roots): + require(out == {"status": "none"}, "re-encoding accepted an absent root") + return + derivatives = self.derivatives(p) + check_encoding(out, len(derivatives)) + require(out == {"status": "ok", "indices": list(range(1, len(derivatives) + 1)), + "signs": self.signs(derivatives, root), "replay": True}, "re-encoding changes root") + + +def check_record(record): + require(record.get("kind") == "result" and record.get("lib") == "HexSignDet" and + record.get("op") in ("table", "descriptor", "compare", "reencode"), + "unexpected infinitesimal fixture record") + payload = record["value"] + context = payload["coefficientContext"] + oracle = RCF(context) + parts = record["case"].split("/") + require(len(oracle.levels) == (2 if "nested" in parts else 1), + "case has the wrong coefficient depth") + data = payload["data"] + require(isinstance(data, dict) and type(data.get("schema")) is int and data["schema"] == 1, + "unsupported infinitesimal fixture schema") + operation = record["op"] + if "passmore" in parts: + raw = data["source"] if operation == "reencode" else data["left"] if operation == "compare" else data + epsilon = oracle.levels[0] + require(oracle.poly(raw["head"]) == + [oracle.one, oracle.zero, -epsilon, -epsilon, oracle.zero, epsilon * epsilon], + "case does not contain the required Passmore polynomial") + if operation == "table": + expected = oracle.table(data) + for mode in ("reduced", "direct"): + check_output(data[mode], expected, len(data["queries"])) + if expected is not None: + require(data[mode].get("staleChildReplay") is False, "stale child evidence accepted") + if len(data["queries"]) > 1: + require(data[mode].get("missingSupportReplay") is False, + "multi-query table accepted as a leaf") + else: + require(data[mode].get("missingSupportReplay", "missing") is None, + "unexpected missing-support test for a leaf") + if len(data["queries"]) <= 4: + require("reference" in data, "small fixture lacks full-ternary reference") + if "reference" in data: + check_output(data["reference"], expected, len(data["queries"])) + else: + getattr(oracle, {"compare": "comparison", "reencode": "reencoding"}.get(operation, operation))(data) + + +def check(source, failure_dir, profile, seed): + seen = set() + failures = 0 + for record in read_fixtures(source): + case = record["case"] + try: + require(case not in seen, "duplicate case") + seen.add(case) + check_record(record) + except (OracleMismatch, KeyError, TypeError, ValueError, ArithmeticError) as exc: + failures += 1 + write_failure(failure_dir, library="HexSignDet", profile=profile, seed=seed, + case_id=case, kind="infinitesimal", input_record=record, + lean_output=record.get("value"), oracle_output=None, + oracle_name="Z3 RCF", oracle_version=VERSION, diff=str(exc)) + print(f"FAIL {case}: {exc}", file=sys.stderr) + require(REQUIRED_CASES <= seen, f"missing infinitesimal cases: {sorted(REQUIRED_CASES - seen)}") + print(f"HexSignDet: {len(seen)} exact infinitesimal cases, {failures} failures ({VERSION})") + return int(failures != 0) + + +def main(): + parser = argparse.ArgumentParser(description=__doc__) + parser.add_argument("source", nargs="?") + parser.add_argument("--check", action="store_true") + parser.add_argument("--profile", choices=("ci", "local"), default="ci") + parser.add_argument("--seed", type=int, default=10377) + parser.add_argument("--failure-dir", type=Path, default=ROOT / "conformance-failures") + args = parser.parse_args() + try: + check_version() + return check(args.source or (DEFAULT_FIXTURE if args.check else None), + args.failure_dir, args.profile, args.seed) + except (OracleMismatch, OSError, ImportError) as exc: + print(f"FAIL HexSignDet Z3 oracle: {exc}", file=sys.stderr) + return 1 + + +if __name__ == "__main__": + raise SystemExit(main()) diff --git a/scripts/oracle/test_sign_det_z3.py b/scripts/oracle/test_sign_det_z3.py new file mode 100644 index 000000000..095b1b8c5 --- /dev/null +++ b/scripts/oracle/test_sign_det_z3.py @@ -0,0 +1,186 @@ +"""Adversarial checks of the exact nested-infinitesimal oracle.""" +import copy +import json +import unittest +from unittest.mock import patch + +from scripts.oracle import sign_det_z3 as oracle +from scripts.oracle.common import OracleMismatch + + +class InfinitesimalOracle(unittest.TestCase): + @classmethod + def setUpClass(cls): + oracle.check_version() + cls.records = {r["case"].removeprefix("infinitesimal/"): r + for line in oracle.DEFAULT_FIXTURE.read_text().splitlines() + if (r := json.loads(line))} + + def record(self, name): + return copy.deepcopy(self.records[name]) + + def reject(self, record): + with self.assertRaises(OracleMismatch): + oracle.check_record(record) + + def test_exact_passmore_signs(self): + for name, expected in (("passmore/whole", [([-1], 1), ([1], 2)]), + ("passmore/positive", [([-1], 1), ([1], 1)]), + ("passmore/empty", [([], 2)])): + record = self.record(name) + rcf = oracle.RCF(record["value"]["coefficientContext"]) + self.assertEqual(rcf.table(record["value"]["data"]), + [{"signs": s, "count": c} for s, c in expected]) + oracle.check_record(record) + + def test_omitted_support_with_correct_total(self): + for mode in ("reduced", "direct", "reference"): + record = self.record("passmore/positive") + record["value"]["data"][mode]["table"] = [{"signs": [1], "count": 2}] + self.reject(record) + + def test_each_replay_and_reference_required(self): + for mode in ("reduced", "direct", "reference"): + record = self.record("passmore/positive") + record["value"]["data"][mode]["replay"] = False + self.reject(record) + record = self.record("passmore/positive") + del record["value"]["data"]["reference"] + self.reject(record) + + def test_stale_child_and_missing_support_checks(self): + for name in ("square/zero-repeat", "nested/whole"): + for mode in ("reduced", "direct"): + for key in ("staleChildReplay", "missingSupportReplay"): + record = self.record(name) + record["value"]["data"][mode][key] = True + self.reject(record) + + def test_nested_order_and_fresh_context(self): + context = self.record("nested/whole")["value"]["coefficientContext"] + rcf = oracle.RCF(context) + epsilon, delta = rcf.levels + self.assertTrue(0 < delta < epsilon ** 20) + for _ in range(3): + oracle.check_record(self.record("nested/whole")) + oracle.check_record(self.record("passmore/positive")) + + def test_coefficient_context_binding(self): + for key, value in (("id", 10378), ("id", True), ("levels", ["epsilon2", "epsilon1"]), + ("levels", ["epsilon1"]), ("order", "reverse")): + record = self.record("nested/whole") + record["value"]["coefficientContext"][key] = value + self.reject(record) + + def test_required_case_inputs(self): + for original, replacement, message in ( + ("nested/whole", "square/zero-repeat", "coefficient depth"), + ("descriptor/nested/singleton", "descriptor/square/negative-head", "coefficient depth"), + ("reencode/nested/reencode", "reencode/passmore/reencode", "coefficient depth"), + ("square/zero-repeat", "nested/whole", "coefficient depth"), + ("passmore/whole", "square/zero-repeat", "Passmore polynomial"), + ("descriptor/passmore/cubic", "descriptor/square/negative-head", "Passmore polynomial"), + ("compare/passmore/order", "compare/square/scaled-equal", "Passmore polynomial")): + record = self.record(replacement) + record["case"] = "infinitesimal/" + original + with self.assertRaisesRegex(OracleMismatch, message): + oracle.check_record(record) + record = self.record("reencode/passmore/reencode") + record["value"]["data"]["source"]["head"] = self.record( + "square/zero-repeat")["value"]["data"]["head"] + with self.assertRaisesRegex(OracleMismatch, "Passmore polynomial"): + oracle.check_record(record) + + def test_descriptor_error_reasons(self): + for name, reason in (("passmore/absent", "absent"), ("passmore/malformed", "malformed"), + ("nested/reversed", "domain")): + record = self.record("descriptor/" + name) + self.assertEqual(record["value"]["data"]["validation"], + {"status": "invalid-descriptor", "reason": reason}) + oracle.check_record(record) + record["value"]["data"]["validation"]["reason"] = "ambiguous" + self.reject(record) + + def test_bad_coefficient_denominator(self): + record = self.record("passmore/whole") + record["value"]["data"]["head"][0]["den"] = [] + self.reject(record) + + def test_domain_rejections(self): + for name in ("square/repeated", "square/root-endpoint", "square/cancelled", + "nested/reversed", "nested/root-endpoint"): + record = self.record(name) + oracle.check_record(record) + record["value"]["data"]["reduced"] = {"status": "ok", "table": [], "replay": True} + self.reject(record) + + def test_completion_root_order_and_selected_signs(self): + for name in ("descriptor/passmore/cubic", "descriptor/passmore/square", + "descriptor/nested/singleton", "descriptor/square/negative-head"): + record = self.record(name) + oracle.check_record(record) + for key in ("completion", "selected"): + bad = copy.deepcopy(record) + signs = bad["value"]["data"]["validation"][key]["signs"] + signs[0] = 1 if signs[0] != 1 else -1 + self.reject(bad) + record = self.record("descriptor/passmore/cubic") + record["value"]["data"]["roots"]["roots"].reverse() + self.reject(record) + + def test_booleans_are_not_signs_or_counts(self): + record = self.record("passmore/positive") + record["value"]["data"]["reduced"]["table"][0]["count"] = True + self.reject(record) + record = self.record("descriptor/passmore/cubic") + record["value"]["data"]["roots"]["roots"][0]["signs"][-1] = True + self.reject(record) + record = self.record("descriptor/passmore/square") + record["value"]["data"]["validation"]["selected"]["signs"][0] = True + self.reject(record) + + def test_stale_descriptor_and_changed_queries(self): + for name in ("descriptor/passmore/cubic", "descriptor/nested/singleton"): + for key in ("staleContextReplay", "changedHeadReplay"): + record = self.record(name) + record["value"]["data"]["validation"][key] = True + self.reject(record) + record = self.record(name) + record["value"]["data"]["validation"]["completion"]["copiedQueriesReplay"] = True + self.reject(record) + record = self.record("descriptor/nested/stale-context") + record["value"]["data"]["validation"]["reason"] = "ambiguous" + self.reject(record) + + def test_empty_partial_descriptor_is_ambiguous(self): + record = self.record("descriptor/passmore/ambiguous") + oracle.check_record(record) + record["value"]["data"]["validation"]["reason"] = "absent" + self.reject(record) + + def test_comparison_and_reencoding(self): + for name in ("compare/passmore/order", "compare/square/scaled-equal", + "compare/passmore/shared-cubic"): + record = self.record(name) + oracle.check_record(record) + record["value"]["data"]["result"]["order"] = "gt" + self.reject(record) + for name in ("reencode/passmore/reencode", "reencode/nested/reencode"): + record = self.record(name) + oracle.check_record(record) + record["value"]["data"]["result"]["signs"][0] *= -1 + self.reject(record) + + def test_version_pin(self): + with patch.object(oracle, "version", return_value="4.15.3.0"): + with self.assertRaises(OracleMismatch): + oracle.check_version() + with patch("z3.get_version", return_value=(4, 15, 3, 0)): + with self.assertRaises(OracleMismatch): + oracle.check_version() + with patch("z3.get_full_version", return_value="Z3 4.15.4.0 custom build"): + oracle.check_version() + + +if __name__ == "__main__": + unittest.main()