security/framework/REVIEW-GUIDE.tex

\documentclass[11pt]{article}
\usepackage[margin=1in]{geometry}
\usepackage{enumitem}
\usepackage{hyperref}
\title{Lux Post-Quantum Cryptography --- External Reviewer's Guide}
\author{Lux Industries --- Cryptography}
\date{}
\begin{document}
\maketitle

\noindent This is the entry point for an external cryptographer reviewing the
Lux PQ stack. It tells you \emph{what} to review, \emph{in what order}, the
exact \emph{claims} (with their assurance level), the \emph{open assumptions}
you are being asked to scrutinise, and how to \emph{reproduce} every check.
Read \texttt{framework/ASSURANCE.tex} (the standard + vocabulary) first.

\section{Honest status (read this before anything else)}
This stack is \textbf{review-ready, NOT externally audited / production-
certified}. No claim in any repository should read otherwise; if you find one
that does, that is itself a finding. The internal gate
(\texttt{framework/check.sh}) enforces that every claim carries a truthful
assurance level and that no security theorem is discharged by an axiom that
restates it. Your sign-off is the gate this stack has not yet passed.

\section{How to reproduce every internal check}
\begin{verbatim}
  # the canonical gate over all primitives (cheat-class detectors + budgets)
  bash ~/work/lux/luxfi/security/framework/check.sh
  # per-repo: build + test (the real assurance for the Go/Rust layers)
  (cd luxfi/pulsar    && go test ./ref/go/pkg/pulsar/ -count=1)
  (cd luxfi/corona    && go test ./... -count=1)
  (cd luxfi/magnetar  && CGO_ENABLED=1 go test ./... -count=1)
  (cd luxfi/consensus && GOWORK=off go test ./protocol/quasar/ -count=1)
  (cd luxfi/p3q       && cargo test --workspace)
\end{verbatim}
The assurance budget (\texttt{.assurance/budget.txt}) and acknowledged axioms
(\texttt{.assurance/reviewed-axioms.txt}) in each repo are the written-down
trust surface; the gate fails if either drifts.

\section{What to review, per primitive}
Each primitive ships a review package; the per-repo \texttt{PROOF-CLAIMS.md}
and \texttt{AXIOM-INVENTORY.md} are authoritative for the live counts (this
guide deliberately does not duplicate numbers). Apply the matching red-team
checklist in \texttt{framework/redteam/}.

\subsection{Pulsar --- threshold ML-DSA (FIPS 204, byte-equal)}
Checklist: \texttt{redteam/lattice.tex}. Package: \texttt{luxfi/pulsar/audit/
pulsar-v1/} (\texttt{SECURITY\_INVARIANTS}, \texttt{THREAT\_MODEL},
\texttt{TEST\_MATRIX}, \texttt{REPRO}, \texttt{REVIEW\_QUESTIONS},
\texttt{KNOWN\_BAD\_V03}). The headline claim --- a BCC/CEF threshold signature
verifies byte-for-byte under unmodified FIPS 204 --- is \textbf{interop-tested}
(circl + pq-crystals), not EC-proven. The leaking v0.3 \texttt{AlgebraicAggregate}
path is \textbf{removed}. The novel ZK parts (boundary-clearance, small-norm
range) are \textbf{fail-closed pending your review}. Open EC axioms are
bucketed in \texttt{AXIOM-INVENTORY.md}; the security-relevant ones
(\texttt{combine\_body\_*\_spec}) are flagged OPEN.

\subsection{Corona --- threshold Module-LWE (Ringtail/Raccoon family)}
Checklist: \texttt{redteam/lattice.tex}. The Go signing path is no-leak (native
masked-aggregate; \texttt{AUDIT-2026-06.md}). Scrutinise: (i) the EC byte-
equality proof still models a \emph{reconstruct-then-sign} abstraction with the
core reduction (steps 2--6) OPEN --- see \texttt{AXIOM-INVENTORY.md} bucket C;
(ii) the 256-bit-hedged session nonce (\texttt{CONSTANT-TIME-REVIEW.md}); (iii)
the aggregator-host trust limitation.

\subsection{Magnetar --- threshold SLH-DSA (FIPS 205, hash-based)}
Checklist: \texttt{redteam/hash-based.tex}. KEY POINT: cheap oracle-respecting
thresholdization is IMPOSSIBLE in the no-dealer model (Kondi--Kumar--Vanegas),
so production is \textbf{threshold certification over independent signatures},
not threshold signing. The \texttt{standalone} leg is sound; \texttt{THBS-SE}
is \textbf{research-only} (transient seed reconstruction at the combiner ---
\texttt{BLOCKERS.md::MAGNETAR-STRICT-ATOM}, OPEN); the TEE leg is honest
trust-relocation, not MPC. \texttt{SPEC.md} \S1.0 states this normatively.

\subsection{Quorum certificate + P3Q --- the consensus threshold}
Checklists: \texttt{redteam/lattice.tex} \S4 + \texttt{redteam/stark.tex}. The
production consensus threshold is the verifiable weighted quorum certificate
(\texttt{luxfi/consensus/protocol/quasar/quorum\_cert.go}): a quorum-weight
subset each sign independently (unmodified FIPS verify), and the predicate
(weighted-validator-set Merkle inclusion, distinct signers, $\Sigma$weight
$\ge$ threshold bound into the signed message, full consensus-field domain
separation) is checked directly or compressed by a P3Q STARK/FRI proof. P3Q
(\texttt{luxfi/p3q}) is a post-quantum Plonky3 fork (Goldilocks/SHA-3/FRI, no
pairings); its DEEP-STARK \texttt{verify\_air} soundness is adversarially
tested. The N-FIPS-verification circuit (Keccak-AIR in-circuit) is the
\textbf{staged} next step; until it exists, finality runs in full-node-
verifiable mode (raw signatures + direct predicate check).

\section{The questions we most want you to answer}
\begin{enumerate}[leftmargin=*]
  \item Pulsar BCC/CEF: is the boundary-clearance argument sound, and is the
    ML-DSA-65/87-only scope ($\|c t_0\|_\infty < \gamma_2$) correctly enforced?
  \item Corona: is the masked-aggregate no-leak argument sound, and can the EC
    proof be rebuilt around the real flow (not reconstruct-then-sign)?
  \item Quorum cert: is the predicate's envelope binding (threshold + position
    fields in the signed message) complete against finality forgery?
  \item P3Q: is the DEEP-ALI + FRI soundness argument complete for the
    eventual N-verification circuit?
  \item Are the OPEN security assumptions (bucket C in each
    \texttt{AXIOM-INVENTORY}) the right and minimal set?
\end{enumerate}
\end{document}