Skip to content

Three spec lines written in notation the language does not have #2791

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Merged
gHashTag merged 2 commits into from
Aug 29, 2026
Merged

Three spec lines written in notation the language does not have #2791

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
2 commits
Select commit Hold shift + click to select a range
d6f2d1e
fix(specs): three lines written in notation the language does not have
gHashTag Aug 29, 2026
d1e450d
merge master into w702-spec-notation
gHashTag Aug 29, 2026
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
6 changes: 3 additions & 3 deletions .trinity/seals/Constants.json
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -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"
}
6 changes: 3 additions & 3 deletions .trinity/seals/JonesPolynomial.json
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -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"
}
6 changes: 3 additions & 3 deletions .trinity/seals/RadixEconomy.json
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -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"
}
11 changes: 6 additions & 5 deletions .trinity/seals/math_Constants.json
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -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"
}
}
11 changes: 6 additions & 5 deletions .trinity/seals/math_RadixEconomy.json
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -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"
}
}
8 changes: 4 additions & 4 deletions .trinity/seals/vsa_JonesPolynomial.json
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -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"
}
8 changes: 8 additions & 0 deletions docs/now/2026-08-29-three-spec-lines-and-the-idiom-i-validated-against-a-broken.md
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -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
12 changes: 6 additions & 6 deletions docs/reports/suite_expectations.json
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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
}
},
Expand Down Expand Up @@ -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
}
},
{
Expand Down Expand Up @@ -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
}
Expand Down
2 changes: 1 addition & 1 deletion specs/math/constants.t27
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand Down
2 changes: 1 addition & 1 deletion specs/math/radix_economy.t27
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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

// ═══════════════════════════════════════════════════════════════════════════
Expand Down
2 changes: 1 addition & 1 deletion specs/vsa/jones_polynomial.t27
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand Down
Loading