diff --git a/docs/phd/AUDIT_REPORT.md b/docs/phd/AUDIT_REPORT.md index 485632c0e2..c2273a8ad0 100644 --- a/docs/phd/AUDIT_REPORT.md +++ b/docs/phd/AUDIT_REPORT.md @@ -40,12 +40,13 @@ https://raw.githubusercontent.com/gHashTag/trios/feat/phd-v5-tectonic-fix/assets | Приложение | Файл | Нужная иллюстрация | |---|---|---| | C — Golden Benchmark | `C-golden-benchmark.tex` | `app-c-acknowledgments.png` (есть в репо, не подключена) | -| F — FPGA Bitstream | `F-fpga-bitstream.tex` | требуется новая (макет bitstream-архива) | +| F — Coq Citation Map | `F-coq-citation-map.tex` | требуется новая (сводная статистика Coq-корпуса: 10 .v / 48 ствр / 35 Qed; в PASS-8 R5-honest сломанная ссылка на `app-f-bitstream-archive.png` убрана — PNG существует только на ветке `feat/illustrations`, плюс тематически неверно: bitstream-архив в Coq-citation appendix) | +| M — FPGA Bitstream | `M-fpga-bitstream.tex` | требуется новая (макет bitstream-архива; бывший именованный файл `app-f-bitstream-archive.png` / после PASS-8 предложено `app-m-bitstream-archive.png` — PNG лежит только на `feat/illustrations`, в файле стоит R5-honest TODO(LD)) | | N — Zenodo DOI | `N-zenodo-doi.tex` | `app-h-zenodo-doi-registry.png` (лежит на ветке `feat/illustrations`, не в `main`; в PASS-7 R5-honest `\includegraphics` убран во избежание silent-drop в tectonic — см. `N-zenodo-doi.tex`) | | K — Agent Memory | `K-agent-memory.tex` | требуется новая (схема памяти 27-агентного улья) | | L — Pollen Channel | `L-pollen-channel.tex` | требуется новая (Pollen-канал ↔ Railway flow) | -**Действие:** 2 иллюстрации (C, H) уже лежат в `assets/illustrations/` — нужно только подключить через `\includegraphics`. 3 иллюстрации (F, K, L) нужно сгенерировать. +**Действие:** 1 иллюстрация (C) уже лежит в `assets/illustrations/` — нужно только подключить через `\includegraphics`. 4 иллюстрации (F Coq citation map summary, M FPGA bitstream, K agent memory, L pollen channel) нужно сгенерировать. **PASS-8 R5 note:** N-zenodo-doi (уже исправлен в PASS-7) + F-coq-citation-map + M-fpga-bitstream все имеют PASS-N TODO(LD) после удаления сломанных `\includegraphics` в рамках phd-pdf-images-gate. --- diff --git a/docs/phd/appendix-G-expansion-audit.md b/docs/phd/appendix-G-expansion-audit.md index e7606f75f4..42b2b42af4 100644 --- a/docs/phd/appendix-G-expansion-audit.md +++ b/docs/phd/appendix-G-expansion-audit.md @@ -89,7 +89,7 @@ Phase 1 cross-reference invariants are **preserved**. The new `\ref{app:F}`, | 2.4 | AP.D Trinity↔Flos Aureus symmetry proof table | **DONE pre-existing** (6,246 B; symmetry table present, proof in §D.2) | | 2.5 | AP.E Lexicon constants | **deferred to Neon SSOT** (lesson #2, #5) | | **2.6** | **AP.G INV-1..7 + Zenodo DOIs** | **THIS LANE** ✅ 18,560 B | -| 2.7 | App.F FPGA bitstream + SHA-256 | open (4,932 B → ≥8 KB target) | +| 2.7 | App.M FPGA bitstream + SHA-256 (PASS-8 R5: renamed App.F→App.M to resolve appendix collision after App.F became Coq Citation Map; appendix-F-fpga-expansion-audit.md renamed accordingly) | open (4,932 B → ≥8 KB target) | | 2.8 | App.N 8 Zenodo DOI registry (PASS-7 R5: renamed H→N + reduced 13→8 description bundles per PASS-6 community-SOT alignment) | open (4,607 B) | | 2.9 | App.I XDC pin map | open (4,435 B) | | 2.10 | App.J Troubleshooting | open (6,100 B) | diff --git a/docs/phd/appendix-F-fpga-expansion-audit.md b/docs/phd/appendix-M-fpga-expansion-audit.md similarity index 85% rename from docs/phd/appendix-F-fpga-expansion-audit.md rename to docs/phd/appendix-M-fpga-expansion-audit.md index a838e010df..9574df24ed 100644 --- a/docs/phd/appendix-F-fpga-expansion-audit.md +++ b/docs/phd/appendix-M-fpga-expansion-audit.md @@ -1,4 +1,13 @@ -# Appendix F (FPGA bitstream) Expansion Audit · Phase 2 STUB-KILL task 2.7 · trios#380 +# Appendix M (FPGA bitstream) Expansion Audit · Phase 2 STUB-KILL task 2.7 · trios#380 + + **Branch:** `feat/phd-phase2-stubkill-2-7` (stacked on `feat/phd-phase2-stubkill-2-9`, tip `fede810`) **Author:** Dmitrii Vasilev ``, ORCID 0009-0008-4294-6159 diff --git a/docs/phd/appendix/F-coq-citation-map.tex b/docs/phd/appendix/F-coq-citation-map.tex index d382e52c33..51a85102bf 100644 --- a/docs/phd/appendix/F-coq-citation-map.tex +++ b/docs/phd/appendix/F-coq-citation-map.tex @@ -10,10 +10,16 @@ \section{Summary statistics} -\begin{figure}[H] -\centering -\includegraphics[width=0.92\textwidth,keepaspectratio]{app-f-bitstream-archive.png} -\end{figure} +% PASS-8 R5-honest (2026-05-12): removed broken \includegraphics block. +% The figure `app-f-bitstream-archive.png` is (a) thematically wrong for the +% Coq Citation Map appendix (it depicts the FPGA bitstream archive, which +% belongs in App.M not App.F), and (b) the PNG file does not exist on `main` +% (it lives only on branch `feat/illustrations`, blob 778610a4...). Per the +% phd-pdf-images-gate skill, tectonic silently skips missing graphics and +% exits 0, leaving a broken figure invisible in the rendered PDF. +% TODO(LD): commission a proper App.F summary-statistics blueprint figure +% (Coq corpus: 10 .v files, 48 statements, 35 Qed, 0 Admitted) via the +% phd-architectural-blueprint-figures skill. \begin{quote}\itshape ``Beware of bugs in the above code; I have only proved it correct, not tried it.'' diff --git a/docs/phd/appendix/M-fpga-bitstream.tex b/docs/phd/appendix/M-fpga-bitstream.tex index e61bad7863..524bd6d2cd 100644 --- a/docs/phd/appendix/M-fpga-bitstream.tex +++ b/docs/phd/appendix/M-fpga-bitstream.tex @@ -4,13 +4,17 @@ \chapter*{Appendix M: FPGA Bitstream Archive} -\begin{figure}[H] -\centering -\includegraphics[width=0.92\textwidth,keepaspectratio]{app-f-bitstream-archive.png} -\caption*{Figure --- FPGA bitstream archive --- SHA-256 manifest.} -\end{figure} - -\addcontentsline{toc}{chapter}{Appendix F: FPGA Bitstream Archive} +% PASS-8 R5-honest (2026-05-12): removed broken \includegraphics block. +% The figure `app-m-bitstream-archive.png` (previously `app-f-bitstream-archive.png` +% before the App.F→App.M rename completed in this PR) does not exist on `main` — +% it lives only on branch `feat/illustrations`. Per the phd-pdf-images-gate skill, +% tectonic silently skips missing graphics and exits 0, leaving a broken figure +% invisible in the rendered PDF. +% TODO(LD): commission a proper App.M bitstream-archive figure (SHA-256 manifest, +% XC7A100T target, 92 MHz timing closure) via the phd-architectural-blueprint-figures +% skill. + +\addcontentsline{toc}{chapter}{Appendix M: FPGA Bitstream Archive} \label{app:fpga-bitstream} \begin{quote}\itshape @@ -19,8 +23,8 @@ \chapter*{Appendix M: FPGA Bitstream Archive} --- Robert E.~Tarjan, \emph{Data Structures and Network Algorithms}, 1983. \end{quote} -\section*{F.0 Reading guide --- what a Xilinx 7-series bitstream is} -\label{sec:appF-reading} +\section*{M.0 Reading guide --- what a Xilinx 7-series bitstream is} +\label{sec:appM-reading} Before diving into the manifest below, a brief orientation is useful. A Xilinx 7-series \texttt{.bit} file is not source code or a binary @@ -31,7 +35,7 @@ \section*{F.0 Reading guide --- what a Xilinx 7-series bitstream is} that the configuration logic verifies before releasing the device into operational state. If the global CRC is wrong, the configuration logic holds the device in reset and reports the failure via the STAT register -(see \S F.4). If the IDCODE in the bitstream does not match the IDCODE +(see \S M.4). If the IDCODE in the bitstream does not match the IDCODE read from the actual silicon, the configuration is aborted at the IDCODE-check stage, again signalled via STAT. @@ -40,14 +44,14 @@ \section*{F.0 Reading guide --- what a Xilinx 7-series bitstream is} (ii) XDC constraints (Appendix~\ref{app:xdc-pin-map}), (iii) Vivado synthesis $\to$ \texttt{.bit} file, (iv) SHA-256 fingerprint of that file (recorded here), (v) JTAG download via the ESP32 XVC bridge -(\S F.5), (vi) STAT-register verification (\S F.4). Every step has a +(\S M.5), (vi) STAT-register verification (\S M.4). Every step has a unique signature, and a mismatch at any step retracts the hardware-validated claim. \textbf{Anchor invariant:} \(\varphi^2 + \varphi^{-2} = 3\). \section*{Silicon that survived contact with reality} -\label{sec:appF-silicon} +\label{sec:appM-silicon} Bitstreams are the moment theory meets silicon. Everything in the preceding chapters---the \(\varphi\)-numeric coprocessor, the Period-Locked Monitor at @@ -60,8 +64,8 @@ \section*{Silicon that survived contact with reality} experiment, this appendix tells you exactly which bitstream was used and how to verify its integrity before flashing. -\section*{F.1 Overview} -\label{sec:appF-overview} +\section*{M.1 Overview} +\label{sec:appM-overview} This appendix documents the hardware artefacts produced during the Trinity S\textsuperscript{3}AI FPGA validation campaign (2026-05-05). The bitstream implements the\emph{Period-Locked Monitor} @@ -70,8 +74,8 @@ \section*{F.1 Overview} \textbf{Anchor invariant:} \(\varphi^2 + \varphi^{-2} = 3\). -\section*{F.2 Target Device} -\label{sec:appF-target} +\section*{M.2 Target Device} +\label{sec:appM-target} \begin{table}[h] \centering @@ -100,8 +104,8 @@ \section*{F.2 Target Device} \item Bits 28--31: \texttt{0x1} --- silicon revision 1 \end{itemize} -\section*{F.3 Bitstream Integrity} -\label{sec:appF-integrity} +\section*{M.3 Bitstream Integrity} +\label{sec:appM-integrity} \begin{table}[h] \centering @@ -127,16 +131,16 @@ \section*{F.3 Bitstream Integrity} four and last four hex characters of the digest, separated by an ellipsis. This is intentional: the full 64-character digest is stored in the artefact \filepath{trinity-fpga/bitstream/design.bit.sha256} of -the \texttt{trinity-fpga} repository, and verification (\S F.8) reads +the \texttt{trinity-fpga} repository, and verification (\S M.8) reads from that artefact rather than from the monograph text. We elide the middle 56 characters because (i) inline transcription of a 64-character hex string is error-prone and would itself become a source of audit mismatches, and (ii) the truth-bearing object is the \texttt{.sha256} -file, not the LaTeX source. The reproduction protocol in \S F.8 is the +file, not the LaTeX source. The reproduction protocol in \S M.8 is the canonical way to obtain the full digest. -\section*{F.4 Configuration Status Register (STAT)} -\label{sec:appF-stat} +\section*{M.4 Configuration Status Register (STAT)} +\label{sec:appM-stat} After successful programming via ESP32 XVC WiFi bridge (Section~\ref{sec:xvc-bridge}), the STAT register was read using @@ -161,7 +165,7 @@ \section*{F.4 Configuration Status Register (STAT)} confirming bitstream integrity and correct CRC check by the FPGA configuration logic. -\section*{F.5 Programming Method}\label{sec:xvc-bridge} +\section*{M.5 Programming Method}\label{sec:xvc-bridge} The bitstream was loaded via a custom ESP32-based Xilinx Virtual Cable (XVC) server operating over 802.11 WiFi (IP~\texttt{192.168.1.30}, port~2542). @@ -173,8 +177,8 @@ \section*{F.5 Programming Method}\label{sec:xvc-bridge} --bitstream design.bit \end{verbatim} -\section*{F.6 Reproducibility} -\label{sec:appF-repro} +\section*{M.6 Reproducibility} +\label{sec:appM-repro} The complete firmware, XDC constraints, and bitstream are archived in \filepath{gHashTag/trinity-fpga} (Apache~2.0). To reproduce: @@ -186,8 +190,8 @@ \section*{F.6 Reproducibility} \item Verify STAT\,=\,\texttt{0x401079FC} \end{enumerate} -\section*{F.7 Bitstream lifecycle} -\label{sec:appF-lifecycle} +\section*{M.7 Bitstream lifecycle} +\label{sec:appM-lifecycle} The bitstream documented above is the output of a multi-stage pipeline. Each stage produces an artefact whose integrity must be verifiable @@ -199,7 +203,7 @@ \section*{F.7 Bitstream lifecycle} \texttt{Flow\_PerfOptimized\_high}. Output: post-synthesis netlist \filepath{trinity-fpga/build/synth/design.dcp}. The synthesis log records the number of LUTs and FFs inferred (83 and 27 - respectively, per \S F.3). + respectively, per \S M.3). \item \textbf{Place-and-route} --- Vivado P\&R consumes the netlist and the XDC constraints (Appendix~\ref{app:xdc-pin-map}). Output: \filepath{trinity-fpga/build/impl/design.dcp}. Timing closure at @@ -207,9 +211,9 @@ \section*{F.7 Bitstream lifecycle} on \texttt{clk50} retracts the hardware claim. \item \textbf{Bitstream emission} --- the \texttt{write\_bitstream} Vivado command turns the routed checkpoint into the \texttt{.bit} - file documented in \S F.3. + file documented in \S M.3. \item \textbf{SHA-256 fingerprint} --- the \texttt{.bit} file is - hashed (\S F.8) and the digest is appended to + hashed (\S M.8) and the digest is appended to \filepath{trinity-fpga/bitstream/design.bit.sha256}. This artefact is the single source of truth for bitstream identity. \item \textbf{Archive} --- the \texttt{.bit} and \texttt{.sha256} @@ -217,9 +221,9 @@ \section*{F.7 Bitstream lifecycle} Long-term preservation policy follows Appendix~N (Zenodo + GitHub + Software Heritage tertiary mirror). % PASS-7 R5: renamed H→N (Zenodo DOI registry is App.N) \item \textbf{Flash} --- the JTAG download via the ESP32 XVC bridge - described in \S F.5. + described in \S M.5. \item \textbf{STAT verification} --- post-flash readback of the STAT - register confirms successful configuration (\S F.4). + register confirms successful configuration (\S M.4). \end{enumerate} Every stage emits a structured log; the entire pipeline is replayable @@ -227,7 +231,7 @@ \section*{F.7 Bitstream lifecycle} bitstream was emitted. The Vivado strategy is fixed (no synthesis-time randomness) and the seed is pinned, so re-running stages 1--3 against the same Git SHA must produce a bit-identical \texttt{.bit} (verified -by SHA-256 match against \S F.3). +by SHA-256 match against \S M.3). \textbf{Cross-references.} The XDC consumed by stage 2 is documented in @@ -237,11 +241,11 @@ \section*{F.7 Bitstream lifecycle} mirroring policy referenced in stage 5 is detailed in Appendix~\ref{app:zenodo-doi}. -\section*{F.8 SHA-256 verification protocol} -\label{sec:appF-verify} +\section*{M.8 SHA-256 verification protocol} +\label{sec:appM-verify} To verify that the \texttt{design.bit} file in your local checkout -matches the integrity claim of \S F.3, run the Rust subcommand +matches the integrity claim of \S M.3, run the Rust subcommand (R1 compliance: no \texttt{.sh} or \texttt{.py} drivers in the repository): @@ -263,11 +267,11 @@ \section*{F.8 SHA-256 verification protocol} The first four characters of the published digest are \texttt{8536e265} and the last four are \texttt{d77352b}; the middle 56 characters are deliberately not transcribed in this monograph (see the R5 honesty -note at the end of \S F.3). To cross-verify against a third party, +note at the end of \S M.3). To cross-verify against a third party, the canonical reference is the file hash itself, not the LaTeX text. -\section*{F.9 Configuration frame anatomy} -\label{sec:appF-frame} +\section*{M.9 Configuration frame anatomy} +\label{sec:appM-frame} The Xilinx 7-series configuration logic (UG470, \emph{7~Series FPGAs Configuration User Guide}) defines a frame as the smallest unit that @@ -278,14 +282,14 @@ \section*{F.9 Configuration frame anatomy} populates a small fraction of these because the resource utilisation is \textless\,0.1\,\%. -The STAT register read in \S F.4 reports the high-level outcome of +The STAT register read in \S M.4 reports the high-level outcome of configuration. The decoded fields (CRC Error, Part Secured, MMCM Lock, DCI Match, EOS, GWE, GHIGH\_B, Done, DEC Error, ID Error) follow the UG470 STAT bit definitions verbatim. The value \texttt{0x401079FC} encodes the operational state ``configuration complete, no errors, device in user mode''. Any deviation --- e.g.\ CRC Error = 1 --- would manifest as a different STAT value and trigger the falsification -hook in \S F.11. +hook in \S M.11. \textbf{Why STAT alone is not sufficient.} The STAT register reports the configuration logic's view of the bitstream, but does not verify @@ -293,25 +297,25 @@ \section*{F.9 Configuration frame anatomy} digest. A maliciously crafted bitstream that passes the FPGA's CRC check but differs from the published \texttt{.bit} would set STAT to \texttt{0x401079FC} and pass the runtime probe. The SHA-256 digest in -\S F.3 / \S F.8 is therefore the necessary complement to STAT for +\S M.3 / \S M.8 is therefore the necessary complement to STAT for end-to-end provenance: SHA-256 verifies authorship and content, STAT verifies that what was sent to the device was accepted. -\section*{F.10 Open issues / audit-pending} -\label{sec:appF-open} +\section*{M.10 Open issues / audit-pending} +\label{sec:appM-open} The following items are honestly open and \textbf{must not} be cited in the main text as fully verified: \begin{description} - \item[Full SHA-256 in monograph] Per the R5 honesty note in \S F.3, + \item[Full SHA-256 in monograph] Per the R5 honesty note in \S M.3, the middle 56 characters of the digest are not transcribed in this LaTeX source. The canonical digest lives in \filepath{trinity-fpga/bitstream/design.bit.sha256}. The presence of that file in the published \filepath{gHashTag/trinity-fpga} repository at the published Git SHA has not been re-verified in this revision of the monograph; status: \texttt{audit-pending}. - \item[Numerical WNS] The 92\,MHz timing closure claim of \S F.7 + \item[Numerical WNS] The 92\,MHz timing closure claim of \S M.7 relies on a positive worst-negative-slack number, but the exact WNS in nanoseconds is not transcribed in this appendix. The Vivado timing report is the authoritative source. Status: @@ -331,33 +335,33 @@ \section*{F.10 Open issues / audit-pending} cross-version bit-identity. \end{description} -\section*{F.11 Falsification hooks} -\label{sec:appF-falsify} +\section*{M.11 Falsification hooks} +\label{sec:appM-falsify} In the spirit of R7 (Popper falsifiability) we pre-register the -observations that would invalidate the resolution claims of \S F.3 / -\S F.4 / \S F.8: +observations that would invalidate the resolution claims of \S M.3 / +\S M.4 / \S M.8: \begin{itemize} - \item The bitstream identity claim of \S F.3 is falsified by any + \item The bitstream identity claim of \S M.3 is falsified by any SHA-256 of the published \texttt{design.bit} that does not begin with \texttt{8536e265} or does not end with \texttt{d77352b}. - The reproduction protocol in \S F.8 is the operational falsifier: + The reproduction protocol in \S M.8 is the operational falsifier: a non-zero exit code from \texttt{cargo run -p trinity-fpga -- verify-bitstream} retracts the claim. - \item The IDCODE claim of \S F.2 is falsified by any JTAG IDCODE + \item The IDCODE claim of \S M.2 is falsified by any JTAG IDCODE read from the QMTech board returning a value other than \texttt{0x13631093}. We have observed values different from \texttt{0x13631093} only when JTAG was mis-wired (BLK-002 of Appendix~\ref{app:troubleshooting}); a clean wiring + this bitstream must produce \texttt{0x13631093} reliably. - \item The STAT register claim of \S F.4 is falsified by any STAT + \item The STAT register claim of \S M.4 is falsified by any STAT read returning a value different from \texttt{0x401079FC} on a - bitstream whose SHA-256 matches \S F.3. A divergent STAT despite + bitstream whose SHA-256 matches \S M.3. A divergent STAT despite a matching SHA indicates either a configuration-logic anomaly (rare) or an under-tested silicon revision; either way, the operational claim is retracted. - \item The synthesis-determinism claim of \S F.7 is falsified by any + \item The synthesis-determinism claim of \S M.7 is falsified by any two consecutive Vivado runs from the same Git SHA producing \texttt{.bit} files with different SHA-256 digests under fixed Vivado version, fixed strategy, and fixed seed. This falsifier is