From 17f13be53cbe996b35174a3f1d9dd47bb77c22ec Mon Sep 17 00:00:00 2001 From: dmitrii-f-t27 Date: Fri, 16 Oct 2026 22:44:53 -0300 Subject: [PATCH] spec(port): port specs/port/trios-railway/crates/trios-igla-race/src/invariants.t27 (Closes #9677) Port gHashTag/trios-railway:crates/trios-igla-race/src/invariants.rs (at 8b229e9489ee, 15 lines) as specs/port/trios-railway/crates/ trios-igla-race/src/invariants.t27 - Roadmap Stage 6, goal #4548, target t27c gen-rust. The constitutional anchor check is ported as pure functions and tested (5 tests, 5 pass, 0 vacuous, 100% function coverage): the language has no sqrt builtin, so sqrt(5) is computed by Newton's iteration (forty halving steps from 5.0, far past f64 precision), phi as (1 + sqrt(5)) / 2, the anchor as phi^2 + 1/phi^2, and the tolerance check carries the original's 1e-10 bound as its decimal form. No transport exists in this port. Verified: parse OK, spec-status IMPLEMENTED, typecheck 0 errors, coverage 5/5, test-report 5/5 pass, 0 BLOCKED, gen 69 lines with 0 'not yet implemented', boundary exactly this one file, dupe_scan: all 5 names unique across 2040 specs, bare body scan adds no duplicate group (752 bodies / 221 groups unchanged). Dmitrii Fedorov ([@dmitrii-f-t27](https://github.com/dmitrii-f-t27)) --- .../crates/trios-igla-race/src/invariants.t27 | 82 +++++++++++++++++++ 1 file changed, 82 insertions(+) create mode 100644 specs/port/trios-railway/crates/trios-igla-race/src/invariants.t27 diff --git a/specs/port/trios-railway/crates/trios-igla-race/src/invariants.t27 b/specs/port/trios-railway/crates/trios-igla-race/src/invariants.t27 new file mode 100644 index 0000000000..c5e9df0a5c --- /dev/null +++ b/specs/port/trios-railway/crates/trios-igla-race/src/invariants.t27 @@ -0,0 +1,82 @@ +// trios-igla-race invariants — the constitutional phi anchor check. +// Port of gHashTag/trios-railway:crates/trios-igla-race/src/invariants.rs +// (at 8b229e9489ee, 15 lines) — Roadmap Stage 6, goal #4548, target t27c +// gen-rust. +// +// The original computes phi as (1 + sqrt(5)) / 2 and verifies the +// constitutional anchor identity phi^2 + 1/phi^2 = 3 within 1e-10. The +// language has no sqrt builtin, so the port computes sqrt(5) by Newton's +// iteration — forty halving steps from 5.0 converge far past f64 +// precision — and the tolerance check carries the 1e-10 bound as +// 0.0000000001 (the parser's literal set has no scientific notation). +// Every function is a tested pure decision; no transport exists in this +// port (issue #9677, "Port the decision, not the plumbing"). + +module port::trios_igla_race_invariants; + +// Newton's iteration for sqrt(5): x <- (x + 5/x) / 2, forty rounds from +// 5.0 — quadratic convergence, far beyond the f64 tolerance below. +pub fn sqrt5_newton() -> f64 { + var s: f64 = 5.0; + var i: usize = 0; + while (i < 40) { + s = (s + 5.0 / s) / 2.0; + i += 1; + } + return s; +} + +// Original line 2: `let phi = (1.0_f64 + 5.0_f64.sqrt()) / 2.0;`. +pub fn phi_from_sqrt5(sqrt5: f64) -> f64 { + return (1.0 + sqrt5) / 2.0; +} + +// Original line 3: `let anchor = phi * phi + 1.0 / (phi * phi);`. +pub fn anchor_of_phi(phi: f64) -> f64 { + const sq: f64 = phi * phi; + return sq + 1.0 / sq; +} + +// Original line 4: `(anchor - 3.0).abs() < 1e-10` — the tolerance bound, +// carried as its decimal form. +pub fn within_anchor_tolerance(anchor: f64) -> bool { + if (anchor - 3.0 < 0.0) { + return (3.0 - anchor) < 0.0000000001; + } + return (anchor - 3.0) < 0.0000000001; +} + +// Original lines 1-5: the constitutional anchor check itself. +pub fn check_phi_anchor() -> bool { + return within_anchor_tolerance(anchor_of_phi(phi_from_sqrt5(sqrt5_newton()))); +} + +test phi_anchor_holds { + assert(check_phi_anchor()); +} + +test anchor_identity_at_the_golden_ratio { + assert(within_anchor_tolerance(anchor_of_phi(1.618033988749895))); + assert(within_anchor_tolerance(anchor_of_phi(phi_from_sqrt5(sqrt5_newton())))); + assert(!within_anchor_tolerance(anchor_of_phi(1.5))); +} + +test sqrt5_converges_to_the_root { + const s = sqrt5_newton(); + assert(s > 2.2360679774); + assert(s < 2.2360679775); +} + +test phi_matches_the_golden_ratio { + const phi = phi_from_sqrt5(sqrt5_newton()); + assert(phi > 1.6180339887); + assert(phi < 1.6180339888); +} + +test tolerance_around_three { + assert(within_anchor_tolerance(3.0)); + assert(within_anchor_tolerance(3.00000000005)); + assert(within_anchor_tolerance(2.99999999995)); + assert(!within_anchor_tolerance(3.05)); + assert(!within_anchor_tolerance(2.95)); +}