Skip to content

feat(ring-1): lex all 28 specs without errors [SEED-1] - #9

Merged
gHashTag merged 1 commit into
masterfrom
ring/1-lex-all-specs
Apr 4, 2026
Merged

gHashTag merged 1 commit into
masterfrom
ring/1-lex-all-specs

Conversation

@gHashTag

@gHashTag gHashTag commented Apr 4, 2026

Copy link
Copy Markdown
Owner

Closes #4

Summary

  • All 27 spec files in specs/ now parse successfully with t27c
  • All 15 compiler spec files in compiler/ also parse successfully
  • Single file changed: bootstrap/src/compiler.rs (+273, -51)

Changes

  • Brace-style modules: module Name { ... } (was only module name;)
  • Arrow return types: fn foo() -> Type { ... }
  • Generic returns: Option<T>, [][]const u8, !void
  • var declarations: at module level
  • Keyword-style blocks: test name given ... when ... then ...
  • Block comments: /* ... */
  • Dotted fn names: Parser.new(...)
  • Error union returns: !void, !Type
  • Const qualifier on fn: fn foo() const { ... }

Test plan

  • 27/27 spec files parse without errors
  • 15/15 compiler spec files parse without errors
  • cargo test passes (0 regressions)
  • Ring-0 functionality preserved

φ² + 1/φ² = 3 | TRINITY

All spec files in specs/ and compiler/ now parse successfully with t27c.

Fixes:
- Brace-style module declarations (module Name { ... })
- Arrow return types (fn foo() -> Type)
- Generic return types (Option<T>)
- Slice/const return types ([]const u8, [][]const u8)
- Error union return types (!void, !Type)
- var declarations at module level
- const qualifier on fn bodies
- Keyword-style test/invariant/bench blocks (given/when/then)
- Dotted function names (Parser.new)
- Block comments (/* ... */)
- Nested brackets/parens in skip-to-semicolon
- Pointer return types (*Type)

Results: 27/27 spec files PASS, 15/15 compiler specs PASS

Closes #4

Co-Authored-By: Claude Opus 4.6 <noreply@anthropic.com>
@gHashTag
gHashTag merged commit 41516f2 into master Apr 4, 2026
1 check passed
@gHashTag
gHashTag deleted the ring/1-lex-all-specs branch April 4, 2026 09:50
gHashTag added a commit that referenced this pull request May 15, 2026
…xt (#649)

Extends holo_op alphabet in coq/IGLA/RMarker.v with OP_LUT_NPU
(TRI-27 ISA 0xE3, Lever #9 LUT-NPU 81-entry hardware port of
Microsoft bitnet.cpp lookup table for b1.58 ternary inference).

New trios-coq/IGLA/LutNpu.v proves depth-6 alphabet chain via
Theorem lut_npu_safe (Forall rtl_uses_star=false), plus 11 spot
lemmas (length, head, last, membership, distinctness, extension
of W33 TENET chain).

Total 16 new Qed accepted by coqc 8.20.1 (W35-G2 >= 10):
- RMarker.v: lut_npu_no_star + 3 distinctness lemmas
- LutNpu.v: lut_npu_safe theorem + 11 spot lemmas

Projection: x1.20 TOPS/W -> 270 TOPS/W on TTIHP27a generic synth
(W34 baseline 225). Area cost +0.18 mm^2, power +6 mW.

R-SI-1 preserved: OP_LUT_NPU enumerated as rtl_uses_star = false.
R7 falsifier W-104-A: BitNet b1.58-3B Trinity-loss sparsity >= 50%.

Closes #649
Refs trinity-fpga#120

Anchor: phi^2 + phi^-2 = 3 . DOI 10.5281/zenodo.19227877
gHashTag added a commit that referenced this pull request May 15, 2026
…xt (#649) (#651)

Extends holo_op alphabet in coq/IGLA/RMarker.v with OP_LUT_NPU
(TRI-27 ISA 0xE3, Lever #9 LUT-NPU 81-entry hardware port of
Microsoft bitnet.cpp lookup table for b1.58 ternary inference).

New trios-coq/IGLA/LutNpu.v proves depth-6 alphabet chain via
Theorem lut_npu_safe (Forall rtl_uses_star=false), plus 11 spot
lemmas (length, head, last, membership, distinctness, extension
of W33 TENET chain).

Total 16 new Qed accepted by coqc 8.20.1 (W35-G2 >= 10):
- RMarker.v: lut_npu_no_star + 3 distinctness lemmas
- LutNpu.v: lut_npu_safe theorem + 11 spot lemmas

Projection: x1.20 TOPS/W -> 270 TOPS/W on TTIHP27a generic synth
(W34 baseline 225). Area cost +0.18 mm^2, power +6 mW.

R-SI-1 preserved: OP_LUT_NPU enumerated as rtl_uses_star = false.
R7 falsifier W-104-A: BitNet b1.58-3B Trinity-loss sparsity >= 50%.

Closes #649
Refs trinity-fpga#120

Anchor: phi^2 + phi^-2 = 3 . DOI 10.5281/zenodo.19227877

Co-authored-by: Vasilev Dmitrii <admin@t27.ai>
gHashTag added a commit that referenced this pull request May 22, 2026
…ernary logic) (Closes #735) (#736)

- ring-097-rust: bounded proof trace + K3 ternary logic mirroring specs/ar/proof_trace.t27 byte-for-byte

- 823 LOC, 29 tests, all green on Rust 1.83.0

- Cross-kernel anchor #9: cot_phi_identity routes phi^2 + 1/phi^2 = 3 through 6-step proof trace + pow_u64 numeric witness + phi^2/phi^-2 mass-conservation

- LOC correction: claimed 624 -> actual 823 (R5-HONEST)

Closes #735

Co-authored-by: Trinity Agent <agent@trinity-s3ai.local>
gHashTag added a commit that referenced this pull request Jun 1, 2026
feat(ring-1): lex all 28 specs without errors [SEED-1]
gHashTag added a commit that referenced this pull request Jun 1, 2026
…xt (#649) (#651)

Extends holo_op alphabet in coq/IGLA/RMarker.v with OP_LUT_NPU
(TRI-27 ISA 0xE3, Lever #9 LUT-NPU 81-entry hardware port of
Microsoft bitnet.cpp lookup table for b1.58 ternary inference).

New trios-coq/IGLA/LutNpu.v proves depth-6 alphabet chain via
Theorem lut_npu_safe (Forall rtl_uses_star=false), plus 11 spot
lemmas (length, head, last, membership, distinctness, extension
of W33 TENET chain).

Total 16 new Qed accepted by coqc 8.20.1 (W35-G2 >= 10):
- RMarker.v: lut_npu_no_star + 3 distinctness lemmas
- LutNpu.v: lut_npu_safe theorem + 11 spot lemmas

Projection: x1.20 TOPS/W -> 270 TOPS/W on TTIHP27a generic synth
(W34 baseline 225). Area cost +0.18 mm^2, power +6 mW.

R-SI-1 preserved: OP_LUT_NPU enumerated as rtl_uses_star = false.
R7 falsifier W-104-A: BitNet b1.58-3B Trinity-loss sparsity >= 50%.

Closes #649
Refs trinity-fpga#120

Anchor: phi^2 + phi^-2 = 3 . DOI 10.5281/zenodo.19227877

Co-authored-by: Vasilev Dmitrii <admin@t27.ai>
gHashTag added a commit that referenced this pull request Jun 1, 2026
…ernary logic) (Closes #735) (#736)

- ring-097-rust: bounded proof trace + K3 ternary logic mirroring specs/ar/proof_trace.t27 byte-for-byte

- 823 LOC, 29 tests, all green on Rust 1.83.0

- Cross-kernel anchor #9: cot_phi_identity routes phi^2 + 1/phi^2 = 3 through 6-step proof trace + pow_u64 numeric witness + phi^2/phi^-2 mass-conservation

- LOC correction: claimed 624 -> actual 823 (R5-HONEST)

Closes #735

Co-authored-by: Trinity Agent <agent@trinity-s3ai.local>
gHashTag added a commit that referenced this pull request Jun 1, 2026
…xt (#649) (#651)

Extends holo_op alphabet in coq/IGLA/RMarker.v with OP_LUT_NPU
(TRI-27 ISA 0xE3, Lever #9 LUT-NPU 81-entry hardware port of
Microsoft bitnet.cpp lookup table for b1.58 ternary inference).

New trios-coq/IGLA/LutNpu.v proves depth-6 alphabet chain via
Theorem lut_npu_safe (Forall rtl_uses_star=false), plus 11 spot
lemmas (length, head, last, membership, distinctness, extension
of W33 TENET chain).

Total 16 new Qed accepted by coqc 8.20.1 (W35-G2 >= 10):
- RMarker.v: lut_npu_no_star + 3 distinctness lemmas
- LutNpu.v: lut_npu_safe theorem + 11 spot lemmas

Projection: x1.20 TOPS/W -> 270 TOPS/W on TTIHP27a generic synth
(W34 baseline 225). Area cost +0.18 mm^2, power +6 mW.

R-SI-1 preserved: OP_LUT_NPU enumerated as rtl_uses_star = false.
R7 falsifier W-104-A: BitNet b1.58-3B Trinity-loss sparsity >= 50%.

Closes #649
Refs trinity-fpga#120

Anchor: phi^2 + phi^-2 = 3 . DOI 10.5281/zenodo.19227877

Co-authored-by: Vasilev Dmitrii <admin@t27.ai>
gHashTag added a commit that referenced this pull request Jun 1, 2026
…ernary logic) (Closes #735) (#736)

- ring-097-rust: bounded proof trace + K3 ternary logic mirroring specs/ar/proof_trace.t27 byte-for-byte

- 823 LOC, 29 tests, all green on Rust 1.83.0

- Cross-kernel anchor #9: cot_phi_identity routes phi^2 + 1/phi^2 = 3 through 6-step proof trace + pow_u64 numeric witness + phi^2/phi^-2 mass-conservation

- LOC correction: claimed 624 -> actual 823 (R5-HONEST)

Closes #735

Co-authored-by: Trinity Agent <agent@trinity-s3ai.local>
gHashTag added a commit that referenced this pull request Jun 17, 2026
…: SGUP-600cell competitor intel

- VcdRecorder::record: value: u32 → u64 (#971.1). Fixes silent truncation for
  signals wider than 32 bits (ternary regfile = 54 bits).
- TbConfig::new: add clock_period_ns parameter; compute timeout_ns from
  max_cycles * clock_period_ns instead of hardcoded *10 (#971.2). Eliminates
  timeout/SIM PASSED race for non-default clock periods.
- COMPETITIVE_POSITIONING.md: add SGUP-600cell (Zenodo:19927449) entry #9
  with explicit spectral mass formula m_k = m₀ exp[β_k csc(π α_k / 53)].
- WAVE_LOOP_68_REPORT.md + PLAN.md with metrics and 3 cooperation variants.
- Suite 548/548 PASS, cargo test 534/534 PASS.

Closes #971 (sub-issues 1 and 2)
gHashTag added a commit that referenced this pull request Aug 7, 2026
…t depth (Refs #1764) (#1904)

Variant 1 RTL prototype. Ruled out yosys auto-retiming (57->51, too weak).
Built two 2-stage GftSmul prototypes (cut after product; cut mid-RNE), both
bit-exact to the combinational core over ~40k random operands, but ltp rose
44->49/50: a register dropped into the generated combinational function
defeats yosys cross-function optimization and the RNE/accumulator depth does
not split there. Implication: the pipeline must be a spec-level on_clock where
the compiler co-optimizes stages (multiply becomes a real pipelined
primitive), not a hand-inserted register. Depth reduction is secondary anyway
-- the untested lever is mid-cloud resync, and since the microsequencer waits
settle >> 1 a latency-1 core needs no sequencer change. Added ruled-out items
#8 (auto-retime) and #9 (dropped-in register).

Refs #1764

Co-authored-by: Claude Opus 4.8 <noreply@anthropic.com>
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

None yet

Projects

None yet

Development

Successfully merging this pull request may close these issues.

[SEED-1] Ring-1: All immediates — lex all 28 specs without errors

2 participants