specs/numeric: GF8/20/24/32 invariants check concrete points instead of prose the parser drops

.trinity/seals/GF20.json

@@ -1,11 +1,14 @@
 {
-  "gen_hash_c": "sha256:8733c8dcfebe0845d7fc299f51971c0f5952dabdef26e62e240e4defa03b2b2d",
+  "gen_hash_c": "sha256:344c9156c81daa83be2fa71865eb546f2f08e5e5569b87695922c00a93866c4b",
   "gen_hash_rust": "sha256:3e41eb5b23ffb1aac262af09e4b7a41c560efc58e09550d9f48f5489ee3bff1d",
   "gen_hash_verilog": "sha256:b0b054b3c2e8b4a095568ec5242edbee786fabf0ac499cb6ee920228ee01f533",
-  "gen_hash_zig": "sha256:f91702e478f778da300a8acfd22d5c5b3996a40e28e727e23024c221980d4e35",
+  "gen_hash_zig": "sha256:f3c9ba9001ea7111ca4a52904fa4b71c856b4e1251d9a46315046c5d2f5e8260",
   "module": "GF20",
   "ring": 12,
-  "sealed_at": "2026-09-08T14:07:51Z",
-  "spec_hash": "sha256:9ec4b6bdfdd71d5d9e4e95513ab3bbc6ac8691ab2086dd1b4e0a2b681cf1b5f9",
-  "spec_path": "specs/numeric/gf20.t27"
+  "sealed_at": "2026-10-03T09:55:30Z",
+  "spec_hash": "sha256:fd492fcff3f39b20902af7b561ded6cf63507d879058c2027123cb9162094a78",
+  "spec_path": "specs/numeric/gf20.t27",
+  "tests": {
+    "blocked": "does not compile: /var/folders/jz/zcjlxjps7gs81jtkwvkbryzc0000gn/T/t27c-test-report-gf20-75779/spec.zig:176:25: error: unused capture"
+  }
 }

.trinity/seals/GF24.json

@@ -1,11 +1,14 @@
 {
-  "gen_hash_c": "sha256:71790015a90f4495ff71d8b799e98b3d2fb86ce080a0f7507f0530ac3029d20c",
+  "gen_hash_c": "sha256:7ac54bf5db56f41960e5cca4619804e95605dca9c80630d4f55767ecbe44089a",
   "gen_hash_rust": "sha256:df7678b000c10fedde6db8d5dfce3ce0b04d16908e102129a242dc5c3245ce9d",
   "gen_hash_verilog": "sha256:ec4e97cce598d924f2e159f0b3ca0014f2d4e97f4e9b15efdb063da78cd39551",
-  "gen_hash_zig": "sha256:603b80abe85f3b6ea8f59499be1fd1b45e67ad5c417f9985aaeb43c43e330085",
+  "gen_hash_zig": "sha256:458be730a91279d1843b56fb2efb8df2572f5bcfe9e3f751336bb79039b1af26",
   "module": "GF24",
   "ring": 12,
-  "sealed_at": "2026-09-08T14:07:51Z",
-  "spec_hash": "sha256:a10ca3fde42f89cdc371a5b78bce652bfdd697f2dbf85996b07ccc59e0a4076b",
-  "spec_path": "specs/numeric/gf24.t27"
+  "sealed_at": "2026-10-03T09:55:31Z",
+  "spec_hash": "sha256:3e9933f3374bdcc9bc90d19a08b90c325d5874f954c8ad4f7875a90c99c25bfc",
+  "spec_path": "specs/numeric/gf24.t27",
+  "tests": {
+    "blocked": "does not compile: /var/folders/jz/zcjlxjps7gs81jtkwvkbryzc0000gn/T/t27c-test-report-gf24-75791/spec.zig:176:25: error: unused capture"
+  }
 }

.trinity/seals/GF32.json

@@ -1,11 +1,14 @@
 {
-  "gen_hash_c": "sha256:4f3671aed9eb20a67aa52db73897081b8271c174468d5dbceb5e6cb7ec440e69",
+  "gen_hash_c": "sha256:5dd6d4b3ea5f3f5a99cbdbb6d55d7e51e071a61884c1991cf14fce715b03727a",
   "gen_hash_rust": "sha256:750c7bf550f4d03e147ee4faa739bfe442e04cda9ef65f93fc887bf5a4614272",
   "gen_hash_verilog": "sha256:bcaf267d10eebafcc5628136abbe047584ce08886a87b61bf361909e5730597b",
-  "gen_hash_zig": "sha256:c54d2d1ec4e5ebfbbe307244915b053ef8feb0e68bb723ac092b2a2fef7fdea0",
+  "gen_hash_zig": "sha256:d2c087b61ed650a37ba1e357ecec2ece94dd7274d8b3361d0217446d28f2dab1",
   "module": "GF32",
   "ring": 12,
-  "sealed_at": "2026-09-08T14:07:51Z",
-  "spec_hash": "sha256:2387a4d9b48f4cdbdcea0ac11b1a3e95b82a71b42f9967d7318bc838c899f333",
-  "spec_path": "specs/numeric/gf32.t27"
+  "sealed_at": "2026-10-03T09:55:31Z",
+  "spec_hash": "sha256:5006880d682eed6653a3ae5552c36aa56c1014c9ff6547937a7b5f4e26a63dd4",
+  "spec_path": "specs/numeric/gf32.t27",
+  "tests": {
+    "blocked": "does not compile: /var/folders/jz/zcjlxjps7gs81jtkwvkbryzc0000gn/T/t27c-test-report-gf32-75803/spec.zig:176:25: error: unused capture"
+  }
 }

.trinity/seals/GF8.json

@@ -1,11 +1,14 @@
 {
-  "gen_hash_c": "sha256:8bdf3c5d8b6d35a283370901d6db35de7d7de19bdfb04bd34cb0a85f5f010c04",
+  "gen_hash_c": "sha256:ede2ced17f3d07182f4ecfd50f4f0416e7c2fe4895b980fb76a07a6a12a909bc",
   "gen_hash_rust": "sha256:7d1f40246aec6b456a8b1fd0f4b36902296f458c7708019c088f456d00433e4b",
   "gen_hash_verilog": "sha256:9dbbbb42bf8f29550ecfa83e0519ddf277e2ec805786dff87bf61e4fe8316627",
-  "gen_hash_zig": "sha256:f2c89dc29ca982ec4ef5ac1153b07c39269c7ecd5dba2d1db14e1b4c43cd294f",
+  "gen_hash_zig": "sha256:1eae6734c496fc8cd6b5e80feeb0935859f15b67becc01eb266e54cb98b61389",
   "module": "GF8",
   "ring": 12,
-  "sealed_at": "2026-09-08T14:07:51Z",
-  "spec_hash": "sha256:d349676390480743109fe238f507d2d7df3d2acfc16b7b24c4c18079e9f77f95",
-  "spec_path": "specs/numeric/gf8.t27"
+  "sealed_at": "2026-10-03T09:55:30Z",
+  "spec_hash": "sha256:4683c0f77b752ec56b7b5a1d3786a2b7bddc67c20771bc000b3707677a63bd64",
+  "spec_path": "specs/numeric/gf8.t27",
+  "tests": {
+    "blocked": "does not compile: /var/folders/jz/zcjlxjps7gs81jtkwvkbryzc0000gn/T/t27c-test-report-gf8-75766/spec.zig:183:25: error: unused capture"
+  }
 }

.trinity/seals/numeric_GF20.json

@@ -1,12 +1,15 @@
 {
-  "gen_hash_c": "sha256:8733c8dcfebe0845d7fc299f51971c0f5952dabdef26e62e240e4defa03b2b2d",
+  "gen_hash_c": "sha256:344c9156c81daa83be2fa71865eb546f2f08e5e5569b87695922c00a93866c4b",
   "gen_hash_rust": "sha256:3e41eb5b23ffb1aac262af09e4b7a41c560efc58e09550d9f48f5489ee3bff1d",
   "gen_hash_verilog": "sha256:b0b054b3c2e8b4a095568ec5242edbee786fabf0ac499cb6ee920228ee01f533",
-  "gen_hash_zig": "sha256:f91702e478f778da300a8acfd22d5c5b3996a40e28e727e23024c221980d4e35",
+  "gen_hash_zig": "sha256:f3c9ba9001ea7111ca4a52904fa4b71c856b4e1251d9a46315046c5d2f5e8260",
   "module": "GF20",
   "ring": 12,
-  "sealed_at": "2026-09-08T14:07:51Z",
-  "sealed_by": "t27c-bootstrap@0.2.0",
-  "spec_hash": "sha256:9ec4b6bdfdd71d5d9e4e95513ab3bbc6ac8691ab2086dd1b4e0a2b681cf1b5f9",
-  "spec_path": "specs/numeric/gf20.t27"
+  "sealed_at": "2026-10-03T09:55:30Z",
+  "sealed_by": "t27c-bootstrap@0.4.0",
+  "spec_hash": "sha256:fd492fcff3f39b20902af7b561ded6cf63507d879058c2027123cb9162094a78",
+  "spec_path": "specs/numeric/gf20.t27",
+  "tests": {
+    "blocked": "does not compile: /var/folders/jz/zcjlxjps7gs81jtkwvkbryzc0000gn/T/t27c-test-report-gf20-75779/spec.zig:176:25: error: unused capture"
+  }
 }

.trinity/seals/numeric_GF24.json

@@ -1,12 +1,15 @@
 {
-  "gen_hash_c": "sha256:71790015a90f4495ff71d8b799e98b3d2fb86ce080a0f7507f0530ac3029d20c",
+  "gen_hash_c": "sha256:7ac54bf5db56f41960e5cca4619804e95605dca9c80630d4f55767ecbe44089a",
   "gen_hash_rust": "sha256:df7678b000c10fedde6db8d5dfce3ce0b04d16908e102129a242dc5c3245ce9d",
   "gen_hash_verilog": "sha256:ec4e97cce598d924f2e159f0b3ca0014f2d4e97f4e9b15efdb063da78cd39551",
-  "gen_hash_zig": "sha256:603b80abe85f3b6ea8f59499be1fd1b45e67ad5c417f9985aaeb43c43e330085",
+  "gen_hash_zig": "sha256:458be730a91279d1843b56fb2efb8df2572f5bcfe9e3f751336bb79039b1af26",
   "module": "GF24",
   "ring": 12,
-  "sealed_at": "2026-09-08T14:07:51Z",
-  "sealed_by": "t27c-bootstrap@0.2.0",
-  "spec_hash": "sha256:a10ca3fde42f89cdc371a5b78bce652bfdd697f2dbf85996b07ccc59e0a4076b",
-  "spec_path": "specs/numeric/gf24.t27"
+  "sealed_at": "2026-10-03T09:55:31Z",
+  "sealed_by": "t27c-bootstrap@0.4.0",
+  "spec_hash": "sha256:3e9933f3374bdcc9bc90d19a08b90c325d5874f954c8ad4f7875a90c99c25bfc",
+  "spec_path": "specs/numeric/gf24.t27",
+  "tests": {
+    "blocked": "does not compile: /var/folders/jz/zcjlxjps7gs81jtkwvkbryzc0000gn/T/t27c-test-report-gf24-75791/spec.zig:176:25: error: unused capture"
+  }
 }

.trinity/seals/numeric_GF32.json

@@ -1,12 +1,15 @@
 {
-  "gen_hash_c": "sha256:4f3671aed9eb20a67aa52db73897081b8271c174468d5dbceb5e6cb7ec440e69",
+  "gen_hash_c": "sha256:5dd6d4b3ea5f3f5a99cbdbb6d55d7e51e071a61884c1991cf14fce715b03727a",
   "gen_hash_rust": "sha256:750c7bf550f4d03e147ee4faa739bfe442e04cda9ef65f93fc887bf5a4614272",
   "gen_hash_verilog": "sha256:bcaf267d10eebafcc5628136abbe047584ce08886a87b61bf361909e5730597b",
-  "gen_hash_zig": "sha256:c54d2d1ec4e5ebfbbe307244915b053ef8feb0e68bb723ac092b2a2fef7fdea0",
+  "gen_hash_zig": "sha256:d2c087b61ed650a37ba1e357ecec2ece94dd7274d8b3361d0217446d28f2dab1",
   "module": "GF32",
   "ring": 12,
-  "sealed_at": "2026-09-08T14:07:51Z",
-  "sealed_by": "t27c-bootstrap@0.2.0",
-  "spec_hash": "sha256:2387a4d9b48f4cdbdcea0ac11b1a3e95b82a71b42f9967d7318bc838c899f333",
-  "spec_path": "specs/numeric/gf32.t27"
+  "sealed_at": "2026-10-03T09:55:31Z",
+  "sealed_by": "t27c-bootstrap@0.4.0",
+  "spec_hash": "sha256:5006880d682eed6653a3ae5552c36aa56c1014c9ff6547937a7b5f4e26a63dd4",
+  "spec_path": "specs/numeric/gf32.t27",
+  "tests": {
+    "blocked": "does not compile: /var/folders/jz/zcjlxjps7gs81jtkwvkbryzc0000gn/T/t27c-test-report-gf32-75803/spec.zig:176:25: error: unused capture"
+  }
 }

.trinity/seals/numeric_GF8.json

@@ -1,12 +1,15 @@
 {
-  "gen_hash_c": "sha256:8bdf3c5d8b6d35a283370901d6db35de7d7de19bdfb04bd34cb0a85f5f010c04",
+  "gen_hash_c": "sha256:ede2ced17f3d07182f4ecfd50f4f0416e7c2fe4895b980fb76a07a6a12a909bc",
   "gen_hash_rust": "sha256:7d1f40246aec6b456a8b1fd0f4b36902296f458c7708019c088f456d00433e4b",
   "gen_hash_verilog": "sha256:9dbbbb42bf8f29550ecfa83e0519ddf277e2ec805786dff87bf61e4fe8316627",
-  "gen_hash_zig": "sha256:f2c89dc29ca982ec4ef5ac1153b07c39269c7ecd5dba2d1db14e1b4c43cd294f",
+  "gen_hash_zig": "sha256:1eae6734c496fc8cd6b5e80feeb0935859f15b67becc01eb266e54cb98b61389",
   "module": "GF8",
   "ring": 12,
-  "sealed_at": "2026-09-08T14:07:51Z",
-  "sealed_by": "t27c-bootstrap@0.2.0",
-  "spec_hash": "sha256:d349676390480743109fe238f507d2d7df3d2acfc16b7b24c4c18079e9f77f95",
-  "spec_path": "specs/numeric/gf8.t27"
+  "sealed_at": "2026-10-03T09:55:30Z",
+  "sealed_by": "t27c-bootstrap@0.4.0",
+  "spec_hash": "sha256:4683c0f77b752ec56b7b5a1d3786a2b7bddc67c20771bc000b3707677a63bd64",
+  "spec_path": "specs/numeric/gf8.t27",
+  "tests": {
+    "blocked": "does not compile: /var/folders/jz/zcjlxjps7gs81jtkwvkbryzc0000gn/T/t27c-test-report-gf8-75766/spec.zig:183:25: error: unused capture"
+  }
 }

docs/now/2026-10-03-gf-invariants-say-what-they-check.md

@@ -0,0 +1,18 @@
+# NOW -- GF invariants say what they check (2026-10-03)
+
+## What was read
+
+- `t27c parse-complete` on master 8fdf7155: `specs/numeric/gf8.t27` discarded 37 top-level tokens; gf20, gf24 and gf32 discarded 31 each.
+- `--show` named them: three prose invariants in each spec (`for all positive x`, `for all valid x`, `== i32 for all f32 x`) and `PHI_DISTANCE == 0.132 within 0.001` in gf8. Each invariant kept its name, so it read as checked while its body was gone.
+
+## What changed
+
+- Each prose claim is checked at concrete points: `pow(x, 0.0) == 1` and `pow(x, 1.0) == x` at 0.5, 2.5 and 7.0; "floor returns a whole number" as `floor(floor(x)) == floor(x)` at 3.7 and -3.2; the gf8 phi distance as `abs(PHI_DISTANCE - 0.132) < 0.001`.
+- No `as i32` from a float: the Zig emitter lowers it as `@intCast`, which does not compile for a float.
+- The eight seals of the four specs were regenerated with the t27c built from this tree (`seal --verify`: all hashes MATCH).
+
+## Not verified
+
+- `t27c test-report` is BLOCKED on all four specs on master and here alike: the generated Zig has an `unused capture` at the same line (`for (0..k) |i|`, 3 errors before and after). The new checks are in the Zig output, but none of them ran.
+
+Closes #5698

docs/reports/suite_expectations.json

@@ -2,7 +2,7 @@
   "schema_version": 1,
   "generated_by": "t27c suite --bless-expectations",
   "max_gate_failures": 2,
-  "max_entries": 134,
+  "max_entries": 130,
   "entries": [
     {
       "path": "specs/api/sdk_contract.t27",
@@ -837,51 +837,6 @@
         "bdd-block-fallback": 31
       }
     },
-    {
-      "path": "specs/numeric/gf20.t27",
-      "phase": "parse-no-discard",
-      "reason": "parser reaches EOF but DISCARDS top-level tokens; newly visible now that the parenthesised range for parses",
-      "issue": 2474,
-      "expires": "2026-11-30",
-      "discard_tokens": 31,
-      "discard_by_channel": {
-        "bdd-block-fallback": 31
-      }
-    },
-    {
-      "path": "specs/numeric/gf24.t27",
-      "phase": "parse-no-discard",
-      "reason": "parser reaches EOF but DISCARDS top-level tokens; newly visible now that the parenthesised range for parses",
-      "issue": 2474,
-      "expires": "2026-11-30",
-      "discard_tokens": 31,
-      "discard_by_channel": {
-        "bdd-block-fallback": 31
-      }
-    },
-    {
-      "path": "specs/numeric/gf32.t27",
-      "phase": "parse-no-discard",
-      "reason": "parser reaches EOF but DISCARDS top-level tokens; newly visible now that the parenthesised range for parses",
-      "issue": 2474,
-      "expires": "2026-11-30",
-      "discard_tokens": 31,
-      "discard_by_channel": {
-        "bdd-block-fallback": 31
-      }
-    },
-    {
-      "path": "specs/numeric/gf8.t27",
-      "phase": "parse-no-discard",
-      "reason": "parser reaches EOF but DISCARDS top-level tokens; newly visible now that the parenthesised range for parses",
-      "issue": 2474,
-      "expires": "2026-11-30",
-      "discard_tokens": 37,
-      "discard_by_channel": {
-        "bdd-block-fallback": 31,
-        "top-level-resync": 6
-      }
-    },
     {
       "path": "specs/numeric/gft1024.t27",
       "phase": "typecheck",

specs/numeric/gf20.t27

@@ -424,18 +424,29 @@ module GF20 {
         then abs(result - 5.0) < 1e-6
 
     invariant gf20_pow_zero_exponent_identity
-        assert pow(x, 0.0) == 1.0 for all positive x
+        // For every positive x; checked at three points, one on each side of 1.
+        given x1 = 0.5
+        and x2 = 2.5
+        and x3 = 7.0
+        assert abs(pow(x1, 0.0) - 1.0) < 1e-6 and abs(pow(x2, 0.0) - 1.0) < 1e-6 and abs(pow(x3, 0.0) - 1.0) < 1e-6
 
     invariant gf20_pow_one_exponent_identity
-        assert pow(x, 1.0) == x for all valid x
+        // For every valid x; checked at three points.
+        given x1 = 0.5
+        and x2 = 2.5
+        and x3 = 7.0
+        assert abs(pow(x1, 1.0) - x1) < 1e-5 and abs(pow(x2, 1.0) - x2) < 1e-5 and abs(pow(x3, 1.0) - x3) < 1e-5
 
     invariant gf20_ln_exp_inversion
         given x = 2.0
         and y = ln_approx(x)
         then abs(exp_approx(y) - x) < 0.01
 
     invariant gf20_floor_returns_integer
-        assert floor(x) == i32 for all f32 x
+        // floor returns a whole number, and the floor of a whole number is itself.
+        given r1 = floor(3.7)
+        and r2 = floor(-3.2)
+        assert abs(floor(r1) - r1) < 1e-6 and abs(floor(r2) - r2) < 1e-6
 
     invariant gf20_floor_monotonic
         given x1 = 2.5

specs/numeric/gf24.t27

@@ -424,18 +424,29 @@ module GF24 {
         then abs(result - 5.0) < 1e-6
 
     invariant gf24_pow_zero_exponent_identity
-        assert pow(x, 0.0) == 1.0 for all positive x
+        // For every positive x; checked at three points, one on each side of 1.
+        given x1 = 0.5
+        and x2 = 2.5
+        and x3 = 7.0
+        assert abs(pow(x1, 0.0) - 1.0) < 1e-6 and abs(pow(x2, 0.0) - 1.0) < 1e-6 and abs(pow(x3, 0.0) - 1.0) < 1e-6
 
     invariant gf24_pow_one_exponent_identity
-        assert pow(x, 1.0) == x for all valid x
+        // For every valid x; checked at three points.
+        given x1 = 0.5
+        and x2 = 2.5
+        and x3 = 7.0
+        assert abs(pow(x1, 1.0) - x1) < 1e-5 and abs(pow(x2, 1.0) - x2) < 1e-5 and abs(pow(x3, 1.0) - x3) < 1e-5
 
     invariant gf24_ln_exp_inversion
         given x = 2.0
         and y = ln_approx(x)
         then abs(exp_approx(y) - x) < 0.01
 
     invariant gf24_floor_returns_integer
-        assert floor(x) == i32 for all f32 x
+        // floor returns a whole number, and the floor of a whole number is itself.
+        given r1 = floor(3.7)
+        and r2 = floor(-3.2)
+        assert abs(floor(r1) - r1) < 1e-6 and abs(floor(r2) - r2) < 1e-6
 
     invariant gf24_floor_monotonic
         given x1 = 2.5

specs/numeric/gf32.t27

@@ -435,18 +435,29 @@ module GF32 {
         then abs(result - 5.0) < 1e-6
 
     invariant gf32_pow_zero_exponent_identity
-        assert pow(x, 0.0) == 1.0 for all positive x
+        // For every positive x; checked at three points, one on each side of 1.
+        given x1 = 0.5
+        and x2 = 2.5
+        and x3 = 7.0
+        assert abs(pow(x1, 0.0) - 1.0) < 1e-6 and abs(pow(x2, 0.0) - 1.0) < 1e-6 and abs(pow(x3, 0.0) - 1.0) < 1e-6
 
     invariant gf32_pow_one_exponent_identity
-        assert pow(x, 1.0) == x for all valid x
+        // For every valid x; checked at three points.
+        given x1 = 0.5
+        and x2 = 2.5
+        and x3 = 7.0
+        assert abs(pow(x1, 1.0) - x1) < 1e-5 and abs(pow(x2, 1.0) - x2) < 1e-5 and abs(pow(x3, 1.0) - x3) < 1e-5
 
     invariant gf32_ln_exp_inversion
         given x = 2.0
         and y = ln_approx(x)
         then abs(exp_approx(y) - x) < 0.01
 
     invariant gf32_floor_returns_integer
-        assert floor(x) == i32 for all f32 x
+        // floor returns a whole number, and the floor of a whole number is itself.
+        given r1 = floor(3.7)
+        and r2 = floor(-3.2)
+        assert abs(floor(r1) - r1) < 1e-6 and abs(floor(r2) - r2) < 1e-6
 
     invariant gf32_floor_monotonic
         given x1 = 2.5

specs/numeric/gf8.t27

@@ -453,10 +453,18 @@ module GF8 {
         then abs(result - 5.0) < 1e-6
 
     invariant gf8_pow_zero_exponent_identity
-        assert pow(x, 0.0) == 1.0 for all positive x
+        // For every positive x; checked at three points, one on each side of 1.
+        given x1 = 0.5
+        and x2 = 2.5
+        and x3 = 7.0
+        assert abs(pow(x1, 0.0) - 1.0) < 1e-6 and abs(pow(x2, 0.0) - 1.0) < 1e-6 and abs(pow(x3, 0.0) - 1.0) < 1e-6
 
     invariant gf8_pow_one_exponent_identity
-        assert pow(x, 1.0) == x for all valid x
+        // For every valid x; checked at three points.
+        given x1 = 0.5
+        and x2 = 2.5
+        and x3 = 7.0
+        assert abs(pow(x1, 1.0) - x1) < 1e-5 and abs(pow(x2, 1.0) - x2) < 1e-5 and abs(pow(x3, 1.0) - x3) < 1e-5
 
     invariant gf8_pow_multiply_exponents
         given a = 2.0
@@ -474,7 +482,10 @@ module GF8 {
         then abs(ln_approx(y) - x) < 0.01
 
     invariant gf8_floor_returns_integer
-        assert floor(x) == i32 for all f32 x
+        // floor returns a whole number, and the floor of a whole number is itself.
+        given r1 = floor(3.7)
+        and r2 = floor(-3.2)
+        assert abs(floor(r1) - r1) < 1e-6 and abs(floor(r2) - r2) < 1e-6
 
     invariant gf8_floor_monotonic
         given x1 = 2.5
@@ -516,6 +527,6 @@ module GF8 {
 
     // Invariant: GF8 phi_distance
     invariant gf8_phi_distance
-        assert PHI_DISTANCE == 0.132 within 0.001
+        assert abs(PHI_DISTANCE - 0.132) < 0.001
         // Rationale: exp/mant = 3/4 = 0.75, phi_distance = |0.75 - 0.618| = 0.132
 }