Skip to content

gf16.t27 (L6 ceiling): gf16_extract_exponent returns 0 for every input; 3 invariants false under execution #8519

Closed

Description

@github-actions

Re-filed from #6431. An attempt claimed that issue on 2026-10-05 and left an empty branch, and a dispatch row that has spent its retry ceiling keeps its issue for good - so no bee could take it again, however much the brief improved. The work below is carried over unchanged.


Problem

tri lab-exec specs/numeric/gf16.t27 (new on PR #5084: generate the Zig on the lab, zig test it -- invariants are comptime blocks, so a false claim is a compile error) reports three FALSE invariants in the numeric ceiling:

invariant why it fails
gf16_inf_exp_all_ones_mant_zero gf16_extract_exponent(x) = (x >> EXP_SHIFT) & EXP_MASK with EXP_MASK = 0x7E00 (in-place mask). After the shift the value is at most 0x3F, and 0x3F & 0x7E00 == 0: the extractor returns 0 for every input.
gf16_nan_exp_all_ones_mant_nonzero same extractor
gf16_identity_encoding asserts gf16_from_components(0, 0, 0) == 0x3C00. That is 0 by construction; 0x3C00 is IEEE binary16's 1.0 (bias 15). With GF16's BIAS = 31, 1.0 is exp field 31 -> 0x3E00. pow2_table[0] = 0x3C00 has the same binary16 origin.

specs/interop/gf_cross_language.t27:29 relies on gf16_extract_exponent(gf16_phi) > 0.

Original checks (kept for history; the Queen does not run these)

  • gf16_extract_exponent masks before shifting ((x & EXP_MASK) >> EXP_SHIFT) or uses a 6-bit mask after it.
  • The 1.0 encoding (and pow2_table) is stated in GF16's own bias, not binary16's, and agrees with conformance/FORMAT-SPEC-001.json.
  • tri lab-exec specs/numeric/gf16.t27 prints no FALSE line.

Original L6 note

specs/numeric/gf16.t27 is L6 CEILING (docs/T27-CONSTITUTION.md): the fix and its re-seal are the owner's decision. The autonomous loop did not edit it.

Evidence

Lab run at t27c 31ca24f / 18385ef, 2026-10-05. Same run found and fixed (on #5084): constants.t27 phi_golden_conjugate, three tokenizer invariants, phi_universal_attractor contraction claim, tf3_negate_zero_unchanged.

Generated with Claude Code


Queen-runnable restatement (2026-10-05)

The owner flagged this issue for action, so the L6 ceiling spec is edited here in t27; the fix is a .t27 edit plus whatever t27c gen regenerates. GF16 is 1 sign + 6 exponent + 9 mantissa with bias 31 (conformance/FORMAT-SPEC-001.json formats.GF16), so 1.0 is exponent field 31, raw 0x3E00; the binary16 value 0x3C00 (bias 15) is not 1.0 in GF16.

Boundary

  • specs/numeric/gf16.t27

User Scenarios & Testing

  • Given master, where gf16_extract_exponent computes (gf16 >> EXP_SHIFT) & EXP_MASK and so returns 0 for every input, when the fix lands, then it masks before shifting (or shifts then masks with EXP_MAX) and gf16_extract_exponent(GF16_INF_POS) equals EXP_MAX (63).
  • Given master, where invariant gf16_identity_encoding asserts gf16_from_components(0, 0, 0) == 0x3C00 (binary16 1.0), when the fix lands, then the 1.0 encoding is stated in GF16's own bias as gf16_from_components(0, 31, 0) == 0x3E00, and pow2_table starts at the GF16 encoding of 1.0, not 0x3C00.
  • Given the fixed spec, when tri lab-exec specs/numeric/gf16.t27 runs on the lab, then no invariant is reported FALSE (gf16_inf_exp_all_ones_mant_zero, gf16_nan_exp_all_ones_mant_nonzero, gf16_identity_encoding included).

Requirements

  • FR-001: The change MUST make gf16_extract_exponent return bits 14..9 of its input ((gf16 & EXP_MASK) >> EXP_SHIFT).
  • FR-002: The change MUST state the 1.0 encoding and pow2_table in GF16's bias 31, agreeing with conformance/FORMAT-SPEC-001.json, and MUST correct the tests that assert binary16 values (gf16_identity_encoding, gf16_exponent_extraction, gf16_pow2_table_consistency, gf16_from_components).
  • FR-003: The change MUST add an invariant gf16_one_encoding_bias31 asserting gf16_from_components(0, 31, 0) == 0x3E00.
  • FR-004: The change MUST keep specs/interop/gf_cross_language.t27 true (it relies on gf16_extract_exponent(gf16_phi) > 0).
  • FR-005: The change MUST NOT add or modify non-t27 hand-written code (specs/policy/own_language.t27) and MUST NOT touch FROZEN_HASH.

Success Criteria

  • grep -c '(gf16 >> EXP_SHIFT) & EXP_MASK' specs/numeric/gf16.t27 prints 0
  • grep -c 'gf16_from_components(0, 0, 0) == 0x3C00' specs/numeric/gf16.t27 prints 0
  • grep -c 'invariant gf16_one_encoding_bias31' specs/numeric/gf16.t27 prints 1
  • grep -c '^ 0x3C00, 0x3D00' specs/numeric/gf16.t27 prints 0
  • t27c spec-status specs/numeric/gf16.t27 prints IMPLEMENTED

The instruments

Every one of these reads and prints; none of them writes. Run them from the repository root, with <spec> replaced by the file in ## Boundary:

.t27 is not Rust and not Zig, and a bee fluent in either writes one by
accident. Measured 2026-09-20: a bee filled eight bodies in
specs/file/watcher.t27 with return Ok(());, Err(FileError::WatcherNotFound)
and for i in 0..watchers.length. The parse ratchet refused the whole file --
Unexpected token in expression: RParen, line 123 -- and a spec that does not
parse generates nothing, so every test it already carried stopped running.

At the top level the parser accepts exactly these eight forms, with an optional
pub, and no others:

const   var   fn   enum   struct   test   invariant   bench

There is no trait, no impl, no type X = ..., no generics, no macro. What
a bee reaches for from another language, and what happens:

  • Rust's result sugar (Ok(()), Err(E::V), ?) is not a construct here.
  • Rust macros (println!, format!, vec!) are not constructs here.
  • A range loop (for i in 0..n) is Rust and Zig, not this language.
  • Zig builtins (catch unreachable, @intCast, @constCast) are not constructs here.
  • Cross-module reuse (use other::fn;) parses and then generates a comment and an unqualified call, so the Zig fails with use of undeclared identifier (use a::b; generates no import, so no spec can reuse a function from another spec #4298). It does not work yet.

t27c parse <spec> answers in one line whether what you wrote is the language.
Run it before you report, every time.

  • t27c spec-status <spec> - the compiler's one-word verdict: IMPLEMENTED, PARTIAL, UNWRITTEN, NOPARSE, NOFN. Exit code is 0 whatever it says, so read the word.
  • t27c symbols <spec> - every name the file declares, with its kind. Answers "does this already exist here?" before you add it.
  • t27c outline <spec> - per function: its locals, what it calls, what it returns. The contract you are implementing against.
  • t27c coverage <spec> - which functions have a test and which do not. The issue asks for tests; this is how you check you wrote them.
  • t27c lint <spec> - style and shape warnings. It OVER-REPORTS has no test or invariant: measured 2026-09-20 over 60 specs it printed 677 of those where coverage found 190 untested functions, disagreeing on 59 of the 60 - it warns about bit_to_trit_pair in specs/base/ternary_encoding.t27, which test bit_to_trit_pair_zero calls on line 249. Read it as a hint; coverage is the answer.
  • t27c typecheck <spec> - types, before generation. Prints Typecheck OK (0 errors, 0 warnings) or the errors.
  • t27c test-report <spec> - builds this spec and runs its own tests, which is what the oracle does. BLOCKED means the generated Zig does not compile, with the error beside it.
  • python3 tools/dupe_scan.py --name <function> - where that function already lives, if it does. 576 of 4021 bodies here are byte-identical copies.

The rest of the toolbelt is in docs/BEE_TOOLBELT.md.

Activity

  1. added a commit that references this issue on Oct 10, 2026
    4206385
  2. gHashTag commented on Oct 12, 2026

    @gHashTag
    Owner

    All three defects are fixed on master: gf16_extract_exponent returns real exponents again (#6940; specs/numeric/gf16.t27:1014 tests extract(0x3C00) == 30), gf16_identity_encoding and gf16_one encoding assert 0x3E00 in GF16's own bias 31 (specs/numeric/gf16.t27:1357, :1210), and pow2_table's binary16 origin is gone (specs/numeric/gf16.t27:50). The false-invariant list is empty on current master runs.

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Metadata

Metadata

Assignees

No one assigned

    Labels

    No labels
    No labels

    Projects

    No projects

      Milestone

      No milestone

      Relationships

      None yet

      Development

      No branches or pull requests

      Issue actions