Skip to content

feat(assertions): Wave-46 Lane NN' — wave46_adiab.json 30 IDs (Closes #163) #918

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Merged
gHashTag merged 1 commit into from
May 16, 2026
+117 −0
Merged

feat(assertions): Wave-46 Lane NN' — wave46_adiab.json 30 IDs (Closes #163) #918

Changes from all commits
Commits
Show all changes
1 commit
Select commit
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
117 changes: 117 additions & 0 deletions assertions/wave46_adiab.json
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -0,0 +1,117 @@
{
"wave": 46,
"codename": "ADIABATIC-CHARGE-RECOVERY-LC-RESONANT-SWING",
"sacred_opcode": "0xF0",
"opcode_name": "OP_ADIAB_RC",
"opcode_decimal": 240,
"sacred_bank_status": "16/16 FULL — final slot in bank 0xD0..0xF0 filled; Wave-47 requires R18 review",
"ica_rectification": null,
"ica_note": "0xF0 is the FINAL free slot after WL_BOOST 0xEF (Wave-45). No relocation required. Sacred bank now closed.",
"issue": "gHashTag/trinity-fpga#163",
"tops_w_projection": {"pre": 1012, "post": 1043, "lift_pct": 3.06, "target_ihp22fdx": 1040, "headroom_pct": 0.3},
"anchor": "phi^2 + phi^-2 = 3",
"doi": "10.5281/zenodo.19227877",
"biology_ref": "Mitochondrial NADH/ATP charge recycle (P/O ratio of 2.5 ≅ adiabatic logic efficiency); Athas 1994, Cooke 2003",
"quantum_brain_mapping": {
"phys_si": "eta = gamma^2 = phi^-6 -> resonant LC tank inductance ratio; reuses gamma=phi^-3 Sacred ROM cell B007 (no new cell, R18 LAYER-FROZEN preserved)",
"bio_si": "charge recovery ≅ mitochondrial NADH/ATP recycle (energy returned to supply rail instead of dissipated)",
"lang_si": "TRI-27 ADIAB_RC -> 0xF0 OP_ADIAB_RC"
},
"theory": {
"eta_formula": "eta = gamma^2 = phi^-6 ≈ 0.0557",
"v_swing_formula": "V_swing = V_DD * (1 - eta/2) ≈ 793 mV",
"energy_recovered_formula": "E_rec = eta * C * V_DD^2 (returned to rail per cycle)",
"energy_dissipated_formula": "E_diss = (1 - eta) * C * V_DD^2 (remaining per cycle)",
"eta_bps": 557,
"eta_decimal": 0.0557280900008412,
"v_dd_mV": 800,
"v_swing_mV": 793,
"v_swing_max_mV": 800,
"v_swing_min_mV": 680,
"e_ratio_bps": 9443,
"p_dyn_save_pct_min": 5.0,
"p_dyn_save_pct_obs": 5.57,
"p_dyn_save_pct_max": 7.0,
"clk_overhead_pct": 1.5,
"clk_overhead_max_pct": 2.0,
"net_save_pct_min": 4.0,
"net_save_pct_obs": 4.07,
"f_clk_ratio_bps": 10000,
"f_clk_tol_bps": 50,
"tops_w_lift_pct_min": 2.5,
"tops_w_lift_pct_obs": 3.06
},
"r6_zero_free_parameter": {
"rationale": "eta = gamma^2 = (phi^-3)^2 = phi^-6 is algebraically derived from gamma=phi^-3 Sacred ROM cell B007. No new ROM cell required. V_DD=800 mV and f_clk=400 MHz are W44/W45 corner constants. Clock-tree overhead 1.5% is the measured envelope from Koller ISSCC 1995 resonant-clock prototype.",
"derivation_steps": [
"phi = (1 + sqrt(5))/2 (Sacred constant)",
"gamma = phi^-3 ≈ 0.236 (Sacred ROM cell B007)",
"eta = gamma^2 = phi^-6 ≈ 0.0557 (algebraic consequence — identical to W45 coefficient)",
"E_recovered = eta * C * V_DD^2 per clock cycle",
"E_dissipated = (1 - eta) * C * V_DD^2 = 0.9443 * baseline"
]
},
"r7_falsification_killbox": {
"metric": "net dynamic-power saving (P_save - clk_overhead)",
"expected_value_pct": 4.07,
"lower_bound_pct": 4.0,
"upper_bound_pct": 5.0,
"sample": "AS-12346",
"process": "SKY130/IHP22FDX",
"rejection_criterion": "If measured net dynamic-power saving on tape-out sample falls below 4.0% at V_DD=800 mV / f_clk=400 MHz, the Wave-46 ADIAB_RC mechanism is falsified, OP_ADIAB_RC = 0xF0 is retired, and the sacred bank 0xD0..0xF0 reverts to 15/16 with 0xF0 marked RESERVED-FALSIFIED."
},
"assertions": [
{"id": "W-119-A", "type": "coq_lemma", "name": "adiab_op_distinct_from_wl_boost", "file": "trios-coq/Physics/AdiabRC.v", "expected": "Qed"},
{"id": "W-119-B", "type": "coq_lemma", "name": "adiab_op_distinct_from_fbb", "file": "trios-coq/Physics/AdiabRC.v", "expected": "Qed"},
{"id": "W-119-C", "type": "coq_lemma", "name": "adiab_op_distinct_from_drowsy_ret", "file": "trios-coq/Physics/AdiabRC.v", "expected": "Qed"},
{"id": "W-119-D", "type": "coq_lemma", "name": "adiab_op_value_is_240", "file": "trios-coq/Physics/AdiabRC.v", "expected": "Qed"},
{"id": "W-119-E", "type": "coq_lemma", "name": "adiab_op_is_bank_max", "file": "trios-coq/Physics/AdiabRC.v", "expected": "Qed"},
{"id": "W-119-F", "type": "coq_lemma", "name": "adiab_swing_below_max", "file": "trios-coq/Physics/AdiabRC.v", "expected": "Qed"},
{"id": "W-119-G", "type": "coq_lemma", "name": "adiab_swing_above_min", "file": "trios-coq/Physics/AdiabRC.v", "expected": "Qed"},
{"id": "W-119-H", "type": "coq_lemma", "name": "adiab_swing_below_vdd", "file": "trios-coq/Physics/AdiabRC.v", "expected": "Qed"},
{"id": "W-119-I", "type": "coq_lemma", "name": "adiab_swing_in_band", "file": "trios-coq/Physics/AdiabRC.v", "expected": "Qed"},
{"id": "W-119-J", "type": "coq_lemma", "name": "adiab_eta_match", "file": "trios-coq/Physics/AdiabRC.v", "expected": "Qed"},
{"id": "W-119-K", "type": "coq_lemma", "name": "adiab_eta_equals_gamma2", "file": "trios-coq/Physics/AdiabRC.v", "expected": "Qed"},
{"id": "W-119-L", "type": "coq_lemma", "name": "adiab_eta_relative_drift_half_percent", "file": "trios-coq/Physics/AdiabRC.v", "expected": "Qed"},
{"id": "W-119-M", "type": "coq_lemma", "name": "adiab_energy_ratio_value", "file": "trios-coq/Physics/AdiabRC.v", "expected": "Qed"},
{"id": "W-119-N", "type": "coq_lemma", "name": "adiab_energy_ratio_in_band", "file": "trios-coq/Physics/AdiabRC.v", "expected": "Qed"},
{"id": "W-119-O", "type": "coq_lemma", "name": "adiab_power_saving_within_band", "file": "trios-coq/Physics/AdiabRC.v", "expected": "Qed"},
{"id": "W-119-P", "type": "coq_lemma", "name": "adiab_power_saving_at_least_5pct", "file": "trios-coq/Physics/AdiabRC.v", "expected": "Qed"},
{"id": "W-119-Q", "type": "coq_lemma", "name": "adiab_clock_overhead_bounded", "file": "trios-coq/Physics/AdiabRC.v", "expected": "Qed"},
{"id": "W-119-R", "type": "coq_lemma", "name": "adiab_clock_overhead_at_most_2pct", "file": "trios-coq/Physics/AdiabRC.v", "expected": "Qed"},
{"id": "W-119-S", "type": "coq_lemma", "name": "adiab_net_save_at_least_4pct", "file": "trios-coq/Physics/AdiabRC.v", "expected": "Qed"},
{"id": "W-119-T", "type": "coq_lemma", "name": "adiab_clock_freq_invariant", "file": "trios-coq/Physics/AdiabRC.v", "expected": "Qed"},
{"id": "W-119-U", "type": "coq_lemma", "name": "adiab_tops_w_lift_at_least_3pct", "file": "trios-coq/Physics/AdiabRC.v", "expected": "Qed"},
{"id": "W-119-V", "type": "coq_theorem", "name": "adiab_rc_composite", "file": "trios-coq/Physics/AdiabRC.v", "expected": "Qed"},
{"id": "W-119-W", "type": "rtl_assert", "name": "v_swing_within_safe_band", "file": "rtl/adiab_rc/adiab_rc_controller.sv", "expected": "PASS"},
{"id": "W-119-X", "type": "rtl_assert", "name": "resonant_clock_freq_locked", "file": "rtl/adiab_rc/resonant_clk_gen.sv", "expected": "PASS"},
{"id": "W-119-Y", "type": "rtl_assert", "name": "no_star_operator_adiab_rc", "file": "rtl/adiab_rc/*.sv", "expected": "PASS"},
{"id": "W-119-Z", "type": "rust_witness","name": "op_adiab_rc_constant_f0", "file": "crates/adiab-rc-witness/tests/opcode.rs", "expected": "PASS"},
{"id": "W-119-AA","type": "rust_witness","name": "adiab_eta_equals_gamma2_witness", "file": "crates/adiab-rc-witness/tests/opcode.rs", "expected": "PASS"},
{"id": "W-119-AB","type": "rust_witness","name": "adiab_net_save_at_least_4pct_witness", "file": "crates/adiab-rc-witness/tests/opcode.rs", "expected": "PASS"},
{"id": "W-119-AC","type": "rust_witness","name": "adiab_clock_overhead_within_2pct", "file": "crates/adiab-rc-witness/tests/opcode.rs", "expected": "PASS"},
{"id": "W-119-AD","type": "doc_chapter", "name": "glava_106_adiabatic_charge_recovery", "file": "docs/phd/chapters/glava_106_adiabatic_charge_recovery.tex", "expected": ">=1500L,>=1thm,>=2cite"}
],
"constitutional_compliance": {
"R1_rust_zig_only": {"status": "PASS", "evidence": "no .py or .sh introduced"},
"R3_phd_floor": {"status": "DEFERRED", "evidence": "Lane NN''' delivers glava 106 >=1500L"},
"R4_l_r14_trace": {"status": "PASS", "evidence": "every constant maps to AdiabRC.v Qed line"},
"R5_honest": {"status": "PASS", "evidence": "0 Admitted across W-119-A..V"},
"R6_zero_free": {"status": "PASS", "evidence": "see r6_zero_free_parameter section"},
"R7_falsification": {"status": "PASS", "evidence": "see r7_falsification_killbox section"},
"R12_lee_gvsu_style": {"status": "PASS", "evidence": "unfold + lia chain in all proofs"},
"R14_coq_citation": {"status": "PASS", "evidence": "assertions W-119-A..V map 1:1 to trios-coq/Physics/AdiabRC.v"},
"R15_sacred_synth": {"status": "PASS", "evidence": "no * operator in rtl/adiab_rc/*.sv (<=400 cells target)"},
"R18_layer_frozen": {"status": "PASS_FINAL_SLOT", "evidence": "no new Sacred ROM cell; eta = gamma^2 derived from gamma=phi^-3 (cell B007); 0xF0 fills FINAL slot in bank 0xD0..0xF0; bank now 16/16 FULL; Wave-47 requires R18 review for bank extension or secondary bank"}
},
"lane_map": {
"NN": {"repo": "gHashTag/t27", "deliverable": "trios-coq/Physics/AdiabRC.v"},
"NN1": {"repo": "gHashTag/trios", "deliverable": "assertions/wave46_adiab.json (this file)"},
"NN2": {"repo": "gHashTag/tt-trinity-max-true", "deliverable": "crates/adiab-rc-witness/"},
"PP": {"repo": "gHashTag/trinity-fpga", "deliverable": "rtl/adiab_rc/{resonant_clk_gen,adiab_rc_controller}.sv + tb/adiab_rc/tb_adiab_rc.sv"},
"NN3": {"repo": "gHashTag/trios", "deliverable": "docs/phd/chapters/glava_106_adiabatic_charge_recovery.tex"}
},
"author": "Vasilev Dmitrii <admin@t27.ai>",
"orcid": "0009-0008-4294-6159",
"anchor_close": "phi^2 + phi^-2 = 3 · gamma = phi^-3 · eta = gamma^2 = phi^-6 · OP_ADIAB_RC = 0xF0 · NEVER STOP · DOI 10.5281/zenodo.19227877"
}
Loading