Conversation
…spec Closes #519 - Add gf16_zero(), gf16_from_u32(), gf16_to_u32() to specs/numeric/gf16.t27 - Add EmitResult, emit_rust_stmt(), emit_rust() to specs/compiler/meta_compile.t27 - 9 tests + 6 invariants across both specs - Verified: tri test compiler::meta_compile PASSED, tri test compiler::numeric/gf16 PASSED PHI LOOP: edit spec → seal hash → gen → test → verdict → save experience → skill commit → git commit
- Restore bridge.rs from c539af3 (40+ unresolved merge conflicts) - Add Cyrillic docs to legacy allowlist - Fix duplicate if-branch in compiler.rs (Dot -> ColonColon) - Create gen/c/numeric/gf4.c stub - Exclude ffi crate from workspace (broken C codegen)
…lparam Fixes test_roundtrip_uart_spec regression. The lexer emits :: as a single ColonColon token but the use-statement parser expected two separate Colon tokens, causing all const declarations after use statements to be skipped. Also enhances HirVerilogEmitter to emit constants with values as localparam instead of bare wire. 524 passed 1 failed -> 525 passed 0 failed
… trigger scope (Closes #332)
- docs/fpga/VSA_BIND_BUNDLE.md: VSA FPGA module documentation - docs/phd/ch28.md: VSA Hardware Acceleration (260 lines) - docs/phd/ch33.md: Trinity Stack Integration (203 lines) - docs/phd/appendix_F.md: FPGA Hardware Platform (153 lines) - docs/phd/appendix_I.md: Bitstream Toolchain (203 lines) - docs/phd/appendix_J.md: JTAG Debug Protocol (325 lines) Verification: 10/10 VSA testbench pass, FPGA DONE=1, STAT=0x401079FC
…#589) STARTUPE2.CFGMCLK (~66 MHz) provides stable clock on QMTECH board with no external oscillator. DLC10 JTAG SRAM programming via Python. - temporal_heartbeat_top: 3-phase phi cycle (slow->steady->fast) - gf16_heartbeat_top: phi heartbeat + live GF16 dot4 computation - dlc10_jtag.py: native DLC10 JTAG driver (IDCODE, SRAM program) - docs/fpga/clocking.md: canonical clock source + pin mapping reference - Verified on real silicon: D5(R23), D6(T23) active-low LEDs blink
- depin/types.rs: ProveRequest/Response, MiningEpoch, AppState - depin/phi_challenge.rs: GF(2^4) dot4, KDF challenge derivation, verify - depin/merkle.rs: SHA256 Merkle tree root + proof verification - depin/prove.rs: axum handler for POST /prove - tri serve --addr: HTTP server with /prove and /health routes - 6/6 unit tests passing (gf16_mul, dot4, challenge, merkle) Ref: gHashTag/trinity-fpga#40 ($TRI token EPIC)
- GET /epoch-challenge: returns phi_challenge, block_reward, seed_hash - POST /prove: adds Ed25519 peer_sample_sig verification - ProveResponse includes tokens_count for L-TRI-2 mining - EpochChallengeResponse struct for challenge distribution - 6/6 tests passing Ref: gHashTag/trinity-fpga#40 (L-TRI-1)
…sible 5 adversarial tests prove PoUC cannot be bypassed: - random_guess_fails: 1/65536 valid (brute-force resistance) - wrong_epoch_fails: epoch isolation enforced - wrong_node_fails: node identity binding - preimage_resistance: SHA256 challenge derivation - commutation_nontrivial: GF(2^4) algebra correctness 11/11 tests passing. Gate G-TRI-3 PASSED. Ref: gHashTag/trinity-fpga#40 (L-TRI-3)
- initialize_epoch: create mining epoch with block_reward - submit_proof: accept NodeProof with phi-challenge GF(2^4) verification - MiningEpoch + NodeProof accounts with PDA derivation - Integration test scaffold for 3-node mock mining - TriError error codes, ProofSubmitted event Requires: Solana CLI + Anchor for deploy (G-TRI-2) Ref: gHashTag/trinity-fpga#40 (L-TRI-2)
prove.rs: wire merkle proof validation into POST /prove, 6 E2E tests merkle.rs: export hash_pair_test for test access types.rs: add merkle_leaf_index to ProveRequest tri-mining.ts: 3-node Solana test with client-side GF16 package.json/tsconfig/yarn.lock: Node 18 + anchor 0.30.1 compat fix(t27c): NOW.md date parser false-positive on leading whitespace fix(scripts/tri): resolve merge conflict + add workspace target path Closes #40
gf16_heartbeat_top.bit: openXC7 synthesized GF16 heartbeat (3.8MB) gf16_heartbeat_top.fasm: frame assembler output gf16_heartbeat_top.json: routing/placement data igla_weights.mem: GF16 champion weights for FPGA loading read_status.py: JTAG status register reader Closes #14
…al hardening
gf16_inv: brute-force multiplicative inverse in GF(2^4)
gf16_matmul: C[i][j] = XOR_k gf16_mul(A[i][k], B[k][j])
CHAMPION_WEIGHTS: SHA256(phi_seed || row) derived, full-rank verified
derive_phi_challenge_v2: per-epoch per-node 16x16 challenge matrix
compute_phi_response_v2: SHA256(pack(W * C)) forces full matmul
verify_phi_response_v2: constant-time comparison
pack_gf16_matrix: row-major 2 nibbles/byte -> 128 bytes
8 adversarial tests: determinism, full-rank, diffusion, spoof resistance
Answer space: 2^256 (SHA256), random guess prob <= 2^{-64}
Closes #40
dsview_jtag_config.json: DSLogic probe wiring for TCK/TMS/TDI/TDO jtag_wiring.md: full JTAG header pinout + cable reference bench/results_v02_real.json: template for real hardware UART measurement Closes #590
Add read_dr_32 method for STATUS register readback. Verified: IDCODE=0x13631093, bitstream 100%, LEDs D5/D6 blinking. BLOCKER-1 closed — JTAG via DLC-10 works, FPGA configured. Closes #590
tri_fpga/cli.py: unified FPGA lifecycle CLI (detect/program/flash/verify/reset) Falls back to DLC-10 Python driver when openFPGALoader cable not found. XDC: added CFGBVS, CONFIG_VOLTAGE, SPI_BUSWIDTH, CONFIGRATE for flash boot. Closes #590
…Pellis Minev) · phi^2+phi^-2=3
… Lane Z (#629) Signed-off-by: Vasilev Dmitrii <admin@t27.ai> Co-authored-by: Vasilev Dmitrii <admin@t27.ai>
Adds HoloOpAlphabet.v with: - Inductive holo_op : Type with 4 variants (HOP_xor, HOP_lut_pe, HOP_bitrom_read, HOP_popcount) - Definition rtl_uses_star returning false for all variants (R-SI-1) - Lemma holo_op_no_star: forall op : holo_op, rtl_uses_star op = false. [Qed] - Lemma holo_op_q4_invariant: forall op : holo_op, rtl_uses_star op = true -> False. [Qed] Also includes Lane Z foundation (HoloRMarker4Slot.v) and updates: - _CoqProject: 74 paths post Lane Z → 75 paths after Lane X - TriosCoq.v: adds Require Export HoloOpAlphabet Ref: gHashTag/trinity-fpga#104 Anchor: φ²+φ⁻²=3 | DOI: 10.5281/zenodo.19227877 R5-HONEST: 74 _CoqProject paths before, 75 after — never '84 theorems'
…5 Lane X Signed-off-by: Vasilev Dmitrii <admin@t27.ai>
Signed-off-by: Vasilev Dmitrii <admin@t27.ai>
8 tasks
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
1 participant
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
feat(x-holo-op): 5-symbol
holo_opAlphabet +holo_op_no_starTheoremL-DPC25 Lane X · Wave-28 gate — this PR is the GATE that unlocks Lanes V, W, V' for Wave-28.
Cross-links: gHashTag/trinity-fpga#106 | Sibling: trios-coq/IGLA/RMarker.v (Lane Z, beccee1, t27#629)
5-Symbol holo_op Alphabet
LUT_LOOKUPBITROM_READNOC_FORWARDR_MARKER_LATCHRAZOR_SAMPLETheorem / Lemma Statements
Quality Gate
coqcversion 8.20.1 (compiled with OCaml 5.3.0) — exit 0, zero warnings:grep -cE 'admit|Admitted|Axiom|Parameter' trios-coq/IGLA/HoloOp.v→ 0 ✓No
admit, noAdmitted, noAxiom, noParameter. All proofs closed withQedorDefined.Files Changed
trios-coq/IGLA/HoloOp.v— 5-symbol alphabet, star-freedom definition, 4 theorems/lemmas, 3 corollariestrios-coq/_CoqProject— appendedIGLA/HoloOp.v(phi^2 + phi^-2 = 3 · gamma = phi^-3 · C = phi^-1 · G = pi^3 * gamma^2 / phi)
(DOI 10.5281/zenodo.19227877)
(Vasilev Dmitrii admin@t27.ai)
(ORCID 0009-0008-4294-6159)
(QUANTUM BRAIN 1:1 SILICON · LEVER STACK · NEVER STOP)