From d6f2d1e4c75a4f97c93f5e2432344c8bed9f8e44 Mon Sep 17 00:00:00 2001 From: Vasilev Dmitrii Date: Sat, 29 Aug 2026 14:57:14 +0700 Subject: [PATCH] fix(specs): three lines written in notation the language does not have Spec-side, not parser-side. Of the eight lines using a single `=` where t27 needs `==`, three can be repaired without inventing meaning: assert G_MEASURED = 6.67430e-11 +/- 1.5e-15 -> assert abs(G_MEASURED - 6.67430e-11) < 1.5e-15 assert LOG3_2 * LOG2_3 = 1.0 within 1e-6 -> assert abs(LOG3_2 * LOG2_3 - 1.0) < 1e-6 assert BRACKET_UNKNOT = 1.0 -> assert BRACKET_UNKNOT == 1.0 AND I VALIDATED THE FIRST TWO AGAINST A BROKEN LINE. My first rewrite used `assert |x - y| < tol`, because specs/vsa/jones_polynomial.t27:318 writes it that way -- and that line is itself one of the discarding ones. The parser has no vertical-bar absolute value. Measured: the rewrite moved 2 tokens. `abs(...)` is the corpus's actual idiom; specs/math/radix_economy.t27 uses it four times in clauses that lower cleanly. With it: discarded tokens 23644 -> 23624 constants 11 -> 10 fallback events radix_economy 5 -> 4 jones_polynomial 4 -> 3 all three still generate with every backend THE OTHER FIVE ARE NOT MECHANICAL, and are left alone: * three carry quantifier prose (`for all positive integer n`, `for any a, b in {1, -1}`) and belong to #2774 * `assert E_OPTIMAL = 1/e` references an `e` the spec never defines; the constant's own definition line says `= 0.36787944117144233; // 1/e`, so the assertion is a restatement of the definition and needs an author, not an edit * `assert jones_polynomial(...) = jones_polynomial(...)` is followed by `when bracket1 and bracket2 are related by Reidemeister moves` -- an English sentence, not a clause suite --ratchet RATCHET: CLEAN, three entries re-blessed check_specs_generate.py / check_seal_coverage.py / check_elab_ratchet.py exit 0 Refs #2754 Co-Authored-By: Claude Opus 5 --- .trinity/seals/Constants.json | 6 +++--- .trinity/seals/JonesPolynomial.json | 6 +++--- .trinity/seals/RadixEconomy.json | 6 +++--- .trinity/seals/math_Constants.json | 11 ++++++----- .trinity/seals/math_RadixEconomy.json | 11 ++++++----- .trinity/seals/vsa_JonesPolynomial.json | 8 ++++---- ...nes-and-the-idiom-i-validated-against-a-broken.md | 8 ++++++++ docs/reports/suite_expectations.json | 12 ++++++------ specs/math/constants.t27 | 2 +- specs/math/radix_economy.t27 | 2 +- specs/vsa/jones_polynomial.t27 | 2 +- 11 files changed, 42 insertions(+), 32 deletions(-) create mode 100644 docs/now/2026-08-29-three-spec-lines-and-the-idiom-i-validated-against-a-broken.md diff --git a/.trinity/seals/Constants.json b/.trinity/seals/Constants.json index fafe396ab3..ec0e343a9b 100644 --- a/.trinity/seals/Constants.json +++ b/.trinity/seals/Constants.json @@ -1,11 +1,11 @@ { - "gen_hash_c": "sha256:bf197b0bf0a1b90dcbd106eb143ab41b1457cf5e053dfc45a3dfddd53ed56a6c", + "gen_hash_c": "sha256:890c041564d28bc5359e61804f69e171220914ee44812065e28fed818f5b45ff", "gen_hash_rust": "sha256:8af3c35dea0a81b70a47a79041faabf9e9dd12237d13a450ed4c2c112f84605b", "gen_hash_verilog": "sha256:44f1589ebe0f5e4b6f5ee6a7703a07396631386783041fe6d79786d0766270b0", - "gen_hash_zig": "sha256:acbbe7a4d0c7261b7dc61b952b0b5d2428e939b6d3cc4c558e5028b314e3fa2a", + "gen_hash_zig": "sha256:4c234f381187460730e2dc1f31664b0e2bfb6d8487a983fb5b3802b099bf3c4e", "module": "Constants", "ring": 12, "sealed_at": "2026-08-28T00:21:37Z", - "spec_hash": "sha256:a2dd3a0fd05206b5075f2370c675551288975fdfb9a3054a10373aeccaaa52f4", + "spec_hash": "sha256:03eefe082ee54a6ca22094e90aca020dbec9bee84f0e0b2f3402b98451405dc5", "spec_path": "specs/math/constants.t27" } diff --git a/.trinity/seals/JonesPolynomial.json b/.trinity/seals/JonesPolynomial.json index 12bd756132..01a9199c15 100644 --- a/.trinity/seals/JonesPolynomial.json +++ b/.trinity/seals/JonesPolynomial.json @@ -1,11 +1,11 @@ { - "gen_hash_c": "sha256:c286be618ed78366c1df1dd44cb15c1e6fd57fa37bf557b03be11b0bb8f854af", + "gen_hash_c": "sha256:abfcdc86d40a1e73979dd0abc348327fa321e11e11e68231e0630fe2791d247b", "gen_hash_rust": "sha256:2dd52a6bc47b88e5ea49fff38bbe9937fa3b3e87e8d104e6314091c94d3e1d3f", "gen_hash_verilog": "sha256:644d8c5309231400b435250fd966219bd5b5b28c9ae8732a5a48884088072fa0", - "gen_hash_zig": "sha256:1c78dfad02821454197755756ccc61755626a4f901350aa8be5c14395c06fef3", + "gen_hash_zig": "sha256:8c6168bc7c86c23fea148565c0c2859d5adcc3b5456b08e5a0d35796564bbb36", "module": "JonesPolynomial", "ring": 12, "sealed_at": "2026-08-28T00:21:37Z", - "spec_hash": "sha256:b1ff39e967bed28b4fd7033a0368f00b9a8b395d16dc4d7b62759e27feab3834", + "spec_hash": "sha256:cc960e5ccb68352c21b7479e7f775cc698d4a8fec103c05683cc962e5107b86a", "spec_path": "specs/vsa/jones_polynomial.t27" } diff --git a/.trinity/seals/RadixEconomy.json b/.trinity/seals/RadixEconomy.json index 966252e210..282e57e464 100644 --- a/.trinity/seals/RadixEconomy.json +++ b/.trinity/seals/RadixEconomy.json @@ -1,11 +1,11 @@ { - "gen_hash_c": "sha256:5034d9dee38f5bade874474c3a070a04ec77797de81affaff171fc5761043210", + "gen_hash_c": "sha256:3cf28e50da39cd58fdd5c925169d328130d434aa6e9f1d8f66a2dbab8c806f54", "gen_hash_rust": "sha256:e938fb541ee7f6cdc99b74fbfe39c0a4770f927c5a2484af198e078273b9c6db", "gen_hash_verilog": "sha256:06739f7f1fa4d30f335d4f83560a9855b839d294f0f2add07c3b1898b888fc01", - "gen_hash_zig": "sha256:a4c43c252dee914a92045fead2af6119f765680cac40bb6e5d8cfc4f0fbf3fd2", + "gen_hash_zig": "sha256:74377556b80975876f9c08c33db08de3d9713a3af008721e8014ef407647f1a2", "module": "RadixEconomy", "ring": 12, "sealed_at": "2026-08-28T00:21:37Z", - "spec_hash": "sha256:01c5e5ec04877472db2072daa8f53206eb910d29c515c4677fb322b203d5f374", + "spec_hash": "sha256:be8b3a944add54031ff82e824411ad3bfcfaed42a8150b3131649cf1d3080a92", "spec_path": "specs/math/radix_economy.t27" } diff --git a/.trinity/seals/math_Constants.json b/.trinity/seals/math_Constants.json index fafe396ab3..fd643a4689 100644 --- a/.trinity/seals/math_Constants.json +++ b/.trinity/seals/math_Constants.json @@ -1,11 +1,12 @@ { - "gen_hash_c": "sha256:bf197b0bf0a1b90dcbd106eb143ab41b1457cf5e053dfc45a3dfddd53ed56a6c", + "gen_hash_c": "sha256:890c041564d28bc5359e61804f69e171220914ee44812065e28fed818f5b45ff", "gen_hash_rust": "sha256:8af3c35dea0a81b70a47a79041faabf9e9dd12237d13a450ed4c2c112f84605b", "gen_hash_verilog": "sha256:44f1589ebe0f5e4b6f5ee6a7703a07396631386783041fe6d79786d0766270b0", - "gen_hash_zig": "sha256:acbbe7a4d0c7261b7dc61b952b0b5d2428e939b6d3cc4c558e5028b314e3fa2a", + "gen_hash_zig": "sha256:4c234f381187460730e2dc1f31664b0e2bfb6d8487a983fb5b3802b099bf3c4e", "module": "Constants", "ring": 12, - "sealed_at": "2026-08-28T00:21:37Z", - "spec_hash": "sha256:a2dd3a0fd05206b5075f2370c675551288975fdfb9a3054a10373aeccaaa52f4", + "sealed_at": "2026-08-29T07:56:35Z", + "sealed_by": "t27c-bootstrap@0.2.0", + "spec_hash": "sha256:03eefe082ee54a6ca22094e90aca020dbec9bee84f0e0b2f3402b98451405dc5", "spec_path": "specs/math/constants.t27" -} +} \ No newline at end of file diff --git a/.trinity/seals/math_RadixEconomy.json b/.trinity/seals/math_RadixEconomy.json index 966252e210..9baef28eda 100644 --- a/.trinity/seals/math_RadixEconomy.json +++ b/.trinity/seals/math_RadixEconomy.json @@ -1,11 +1,12 @@ { - "gen_hash_c": "sha256:5034d9dee38f5bade874474c3a070a04ec77797de81affaff171fc5761043210", + "gen_hash_c": "sha256:3cf28e50da39cd58fdd5c925169d328130d434aa6e9f1d8f66a2dbab8c806f54", "gen_hash_rust": "sha256:e938fb541ee7f6cdc99b74fbfe39c0a4770f927c5a2484af198e078273b9c6db", "gen_hash_verilog": "sha256:06739f7f1fa4d30f335d4f83560a9855b839d294f0f2add07c3b1898b888fc01", - "gen_hash_zig": "sha256:a4c43c252dee914a92045fead2af6119f765680cac40bb6e5d8cfc4f0fbf3fd2", + "gen_hash_zig": "sha256:74377556b80975876f9c08c33db08de3d9713a3af008721e8014ef407647f1a2", "module": "RadixEconomy", "ring": 12, - "sealed_at": "2026-08-28T00:21:37Z", - "spec_hash": "sha256:01c5e5ec04877472db2072daa8f53206eb910d29c515c4677fb322b203d5f374", + "sealed_at": "2026-08-29T07:56:35Z", + "sealed_by": "t27c-bootstrap@0.2.0", + "spec_hash": "sha256:be8b3a944add54031ff82e824411ad3bfcfaed42a8150b3131649cf1d3080a92", "spec_path": "specs/math/radix_economy.t27" -} +} \ No newline at end of file diff --git a/.trinity/seals/vsa_JonesPolynomial.json b/.trinity/seals/vsa_JonesPolynomial.json index a5c9b73878..a40a493834 100644 --- a/.trinity/seals/vsa_JonesPolynomial.json +++ b/.trinity/seals/vsa_JonesPolynomial.json @@ -1,12 +1,12 @@ { - "gen_hash_c": "sha256:c286be618ed78366c1df1dd44cb15c1e6fd57fa37bf557b03be11b0bb8f854af", + "gen_hash_c": "sha256:abfcdc86d40a1e73979dd0abc348327fa321e11e11e68231e0630fe2791d247b", "gen_hash_rust": "sha256:2dd52a6bc47b88e5ea49fff38bbe9937fa3b3e87e8d104e6314091c94d3e1d3f", "gen_hash_verilog": "sha256:644d8c5309231400b435250fd966219bd5b5b28c9ae8732a5a48884088072fa0", - "gen_hash_zig": "sha256:1c78dfad02821454197755756ccc61755626a4f901350aa8be5c14395c06fef3", + "gen_hash_zig": "sha256:8c6168bc7c86c23fea148565c0c2859d5adcc3b5456b08e5a0d35796564bbb36", "module": "JonesPolynomial", "ring": 12, - "sealed_at": "2026-08-29T04:46:46Z", + "sealed_at": "2026-08-29T07:56:35Z", "sealed_by": "t27c-bootstrap@0.2.0", - "spec_hash": "sha256:b1ff39e967bed28b4fd7033a0368f00b9a8b395d16dc4d7b62759e27feab3834", + "spec_hash": "sha256:cc960e5ccb68352c21b7479e7f775cc698d4a8fec103c05683cc962e5107b86a", "spec_path": "specs/vsa/jones_polynomial.t27" } \ No newline at end of file diff --git a/docs/now/2026-08-29-three-spec-lines-and-the-idiom-i-validated-against-a-broken.md b/docs/now/2026-08-29-three-spec-lines-and-the-idiom-i-validated-against-a-broken.md new file mode 100644 index 0000000000..c1d67a461f --- /dev/null +++ b/docs/now/2026-08-29-three-spec-lines-and-the-idiom-i-validated-against-a-broken.md @@ -0,0 +1,8 @@ +# NOW -- Three spec lines, and the idiom I validated against a broken line (2026-08-29) + +## Three spec lines, and the idiom I validated against a broken line (Refs #2754) + +- assert X = Y uses a single = where t27 needs ==; assert |x - y| < tol uses vertical bars the parser does not have +- I first wrote |...| because a line in the corpus uses it -- that line is itself one of the failing ones. abs(...) is the real idiom, and radix_economy already uses it four times in clauses that work +- 23644 -> 23624 tokens; constants 11 -> 10, radix_economy 5 -> 4, jones 4 -> 3 fallback events; all three still generate +- five of the eight single-= lines are NOT mechanical: three carry quantifier prose (#2774), one references an undefined e, one is followed by an English when-clause diff --git a/docs/reports/suite_expectations.json b/docs/reports/suite_expectations.json index 03f94048f6..13b9615aa8 100644 --- a/docs/reports/suite_expectations.json +++ b/docs/reports/suite_expectations.json @@ -891,9 +891,9 @@ "reason": "parser reaches EOF but DISCARDS top-level tokens (forall-quantified properties)", "issue": 2474, "expires": "2026-11-30", - "discard_tokens": 159, + "discard_tokens": 151, "discard_by_channel": { - "bdd-block-fallback": 151, + "bdd-block-fallback": 143, "top-level-resync": 8 } }, @@ -934,9 +934,9 @@ "reason": "parser reaches EOF but DISCARDS top-level tokens (forall-quantified properties)", "issue": 2474, "expires": "2026-11-30", - "discard_tokens": 63, + "discard_tokens": 55, "discard_by_channel": { - "bdd-block-fallback": 63 + "bdd-block-fallback": 55 } }, { @@ -1502,9 +1502,9 @@ "reason": "parser reaches EOF but DISCARDS top-level tokens (forall-quantified properties)", "issue": 2474, "expires": "2026-11-30", - "discard_tokens": 69, + "discard_tokens": 65, "discard_by_channel": { - "bdd-block-fallback": 56, + "bdd-block-fallback": 52, "brace-body/in-fallback": 4, "top-level-resync": 9 } diff --git a/specs/math/constants.t27 b/specs/math/constants.t27 index 769760f6c3..47a2a12c45 100644 --- a/specs/math/constants.t27 +++ b/specs/math/constants.t27 @@ -316,7 +316,7 @@ module Constants { // Rationale: e is proven to be irrational (Euler, 1737) invariant codata_gravitational_constant - assert G_MEASURED = 6.67430e-11 +/- 1.5e-15 + assert abs(G_MEASURED - 6.67430e-11) < 1.5e-15 // Rationale: CODATA 2022 measured value with uncertainty invariant cosmological_constant_positive diff --git a/specs/math/radix_economy.t27 b/specs/math/radix_economy.t27 index 88b7b17ef8..5c5b6f2446 100644 --- a/specs/math/radix_economy.t27 +++ b/specs/math/radix_economy.t27 @@ -305,7 +305,7 @@ module RadixEconomy { // Rationale: 3^18 ≈ 3.9e8, 2^28 ≈ 2.7e8, 2^29 ≈ 5.4e8 invariant log_reciprocal_identity - assert LOG3_2 * LOG2_3 = 1.0 within 1e-6 + assert abs(LOG3_2 * LOG2_3 - 1.0) < 1e-6 // Rationale: log_a(b) * log_b(a) = 1 for any valid bases // ═══════════════════════════════════════════════════════════════════════════ diff --git a/specs/vsa/jones_polynomial.t27 b/specs/vsa/jones_polynomial.t27 index 870b15da4d..dce4911d5c 100644 --- a/specs/vsa/jones_polynomial.t27 +++ b/specs/vsa/jones_polynomial.t27 @@ -322,7 +322,7 @@ module JonesPolynomial { // Rationale: writhe is linear sum of crossing signs invariant bracket_unknot_normalization - assert BRACKET_UNKNOT = 1.0 + assert BRACKET_UNKNOT == 1.0 // Rationale: Kauffman bracket of unknot is 1 (definition) invariant jones_polynomial_invariance