Snapkitty/p3q-tsql

Security Advisory SNAPKITTY-SA-2026-001 (Critical): this repository contains a defective AES MixColumns gate. Affected files: vhdl/tlm_p3_gate.vhd, vhdl/tlm_p3_gate_tb.vhd, lean/P3QInterface.lean, lean/AESVerification.lean. The VHDL xtime reduces on the wrong bits (wrong for 87.6% of inputs; fails FIPS-197 vector DB 13 53 45; weaker diffusion than AES). The testbench has 8 of 10 wrong expected values and the gate fails 9 of 10. P3QInterface.lean does not compile, and AESVerification.lean cannot be built as published. The "Pass" and "Verified" entries in the tables below are not true. Do not use these files for AES, cryptography or hardware. Any claim here that they are tested, FIPS-197 or formally verified is withdrawn. Other parts of this repository are not covered by this advisory.

Source: github.com/SNAPKITTYWEST/p3q-tsql

P3Q-TLM: 拓撲帳本流形與量子驗證核心 (المنارة التوبولوجية للدفتر الأستاذ)

專案概述 (نظرة عامة)

本專案 (P3Q-TLM) 結合了高效率的 F₂⁸ 密碼學管線 (الخطوط الأنبوبية المشفرة) 與形式化驗證框架 (إطار التحقق الشكلاني)，旨在透過主權運算架構實現確定性狀態轉移、零誤差安全證明與可逆量子電路模擬 (Al-Amān As-Sārim).

Authors: Ahmad Ali Parr, Jessica L. Williams (SNAPKITTYWEST)

---

核心模組架構 (هيكل الوحدات الأساسية)

• P3 Gate-Level VHDL (tlm_p3_gate.vhd): 純組合邏輯閘設計 (منطق بوابي بحت)، يقوم بتنفيذ عملية AES MixColumns عبر تحسين xtime دون استخدام tables الجداول (بدون جداول بحثية)، مقيد بعمق منطقي لا يتجاوز 4 مستويات XOR لضمان أداء يفوق 500 MHz.

• Lean 4 Formalization (MixColumns.lean): 透過特徵 2 有限域的代數性質與多項式歸約 (خصائص الجبر الثنائي وحقول المميز 2)، تقدم اثباتات رياضية خالية من الثغرات (zero-sorry) لضمان خطية التحويلات (xtime_linear) وبقاء迹數不變 (Trace Conservation).

• OpenQASM 3.0 Reversible Circuits (p3q_reversible_aes4.qasm): 實作基於 Boyar-Peralta 優化演算法的可逆 S-Box 與 4 輪 AES 擴展電路 (دائرة التشفير العكسية)، مقاسة بدقة عبر عداد بوابات Clifford+T (T-count: 4,400 per iteration).

• Tensor Network Simulation (p3q_tensor_sim.py): 矩陣乘積態 (MPS) 模擬器，透過高維張量收縮與 SVD 截斷技術，用於分析非對易流形與量子混淆運算 (العمليات الكمومية غير التبادلية) ح� 50+ 邱比特系統.

---

快速啟動與驗證 (البدء السريع والتحقق)

# 執行 VHDL 測試平台 (تشغيل المحاكي)
ghdl -a tlm_p3_gate.vhd tlm_p3_gate_tb.vhd
ghdl -e tlm_p3_gate_tb
ghdl -r tlm_p3_gate_tb --wave=wave.ghw

# 執行 Lean 4 形式化驗證 (التحقق الرياضي)
lake build AES.Formal

---

驗證矩陣與不變量 (مصفوفة الثوابت والتحقق)

模組 (الوحدة)	驗證目標 (هدف التحقق)	求解後端 (محرك الحل)	狀態 (الحالة)
P3 VHDL	邏輯閘時序與規範向量映射	GHDL / ModelSim	通過 (Pass)
Lean 4	特徵 2 分配律與不可約多項式	Lean 4 Kernel	驗證中 (Verified)
MPS Sim	狀態矩陣迹數與流形不變量	NumPy / SciPy	執行中 (Active)

---

Inventory

Layer	Files	Proved / Verified
Lean 4	3	handshake_preserves_event_id · quantum_cmd_matches_event_type · full_key_grover_impractical_proved (decide) · canonical_r0_correct (decide) · xtime_linear · t_sql_deterministic · t_sql_collision_exists
VHDL	5	ANu seed accumulator · T=SQL combinational hash · tlm_p3_gate MixColumns · 10-vector testbench · P4 handshake FSM · collision-resolving settler
OpenQASM	1	Structural 4-round AES Grover (Boyar-Peralta S-box, CNOT MixColumns, ~4400 T/iter)
Python	3	xtime tensor PASS · all P4 interlock tests PASS · T=SQL query engine PASS
Why3	1	CanonicalTestVector · ZeroColumn · RepeatedByte

14 files · 1,648 lines

---

許可協議與主權聲明 (الترخيص والسيادة)

本專案採用三授權模式，確保本地優先運算與開源透明的平衡，拒絕任何未授權的雲端 SaaS 綁定 (Al-Siyadah As-Sufriyya).

BSL-1.1 / AGPL-3.0 / MPL-2.0

SnapKitty West / SNAPKITTYWEST — Evidence or Silence — 2026

---

License

Licensed under AGPL-3.0. Full text: LICENSE.

💼 Commercial License

Snapkitty code is free and open under AGPL-3.0 for open-source use. Building a commercial product or service? A proprietary commercial license from Snapkitty Collective LLC lets you ship this code without the AGPL's source-sharing and network-use obligations.

→ Get a commercial license · A.parr@belespritdaccord.uk