security/framework/ASSURANCE.tex

\documentclass[11pt]{article}
\usepackage[margin=1in]{geometry}
\usepackage{enumitem}
\title{The Lux High-Assurance Cryptography Framework}
\author{Lux Industries --- Cryptography}
\date{}
\begin{document}
\maketitle

\noindent
This is the normative standard for assurance claims about Lux cryptographic
primitives (\texttt{luxfi/pulsar}, \texttt{corona}, \texttt{magnetar},
\texttt{p3q}, and the \texttt{consensus} quorum certificate). It exists
because a 2026-06 internal audit found the same failure modes across three
independent primitives: they are \emph{framework} gaps, not isolated bugs. The
companion gate \texttt{framework/check.sh} enforces this document mechanically.

\section{The cardinal rule}
A security claim's \emph{word} must match its \emph{artifact}. It is better to
state a weaker true claim than a stronger false one. ``Honest disclosure'' is
not a courtesy; it is the load-bearing property of a high-assurance system,
because every downstream decision is taken against the stated assurance level.

\section{The assurance vocabulary}
Every claim in a \texttt{PROOF-CLAIMS} entry MUST carry exactly one level:
\begin{description}[leftmargin=2.2cm,style=nextline]
  \item[machine-checked] A proof assistant (Lean, EasyCrypt) verifies the
    statement with \textbf{zero} \texttt{sorry}/\texttt{admit} and no axiom
    that restates the conclusion. The named file is clean.
  \item[sound-by-reduction] A written reduction to a stated hardness
    assumption, reviewed but not mechanized. The assumption is named.
  \item[interop-tested] Output byte-equality demonstrated against
    $\geq 2$ \emph{independent} implementations (e.g. \texttt{cloudflare/circl}
    and \texttt{pq-crystals}), not the signer's own library.
  \item[asserted-axiom] Taken as an axiom. It counts against the budget
    (\S\ref{sec:budget}) and must be justified (a serialization/layout fact,
    a cited hardness assumption) --- never a restatement of a theorem.
  \item[fail-closed-pending-review] Implemented but gated so the production
    path \textbf{refuses} until an external review clears it; the default
    verifier returns an error.
  \item[open-research] Not achievable with current technique; stated as open.
\end{description}

\section{Prohibited shapes (the gate fails on these)}
\begin{enumerate}[leftmargin=*]
  \item \textbf{Circular proof.} A load-bearing theorem discharged by
    \texttt{apply}/\texttt{exact} of a locally declared axiom whose statement
    is the theorem (``\,theorem $X$ := axiom-asserting-$X$\,''), or a Lean
    body that is \texttt{:= True}/\texttt{trivial}/\texttt{sorry}.
  \item \textbf{Proof-by-rename.} A property declared \texttt{CLOSED} whose
    enforcement is an identifier-name \texttt{grep}/AST check rather than a
    functional or timing test. Renaming a secret to \texttt{tmp} must not
    flip a security gate.
  \item \textbf{Fail-open verifier.} A \texttt{Verify}/\texttt{Validate}/
    \texttt{Check} function with no reject path; a default/unregistered
    verifier that returns \texttt{nil}; a fail-closed gate rewritten as a
    conditional \texttt{return nil}.
  \item \textbf{Budget drift.} New \texttt{sorry}/\texttt{admit}/\texttt{axiom}
    beyond the declared \texttt{.assurance/budget.txt} without updating the
    budget \emph{and} \texttt{PROOF-CLAIMS}.
  \item \textbf{Claim/artifact mismatch.} \texttt{PROOF-CLAIMS} prose that
    contradicts the named artifact (``proven'' on a \texttt{sorry};
    ``byte-equal'' with one verifier).
\end{enumerate}

\section{The unproven-assertion budget}\label{sec:budget}
Each \texttt{sorry}, \texttt{admit}, \texttt{axiom}, and vacuous body is an
unproven assertion: the real surface of trust. Every repo declares its budget
in \texttt{.assurance/budget.txt} (\texttt{SORRY}, \texttt{ADMIT},
\texttt{AXIOM}, \texttt{VACUOUS}; omitted $\Rightarrow$ $0$). The count may
only \emph{decrease} without an accompanying \texttt{PROOF-CLAIMS} +
\texttt{AXIOM-INVENTORY} update; the gate fails on any increase.

\section{The canonical fail-closed verifier pattern}
Novel cryptography (any construction not covered by a standard or a mechanized
proof) ships behind a registered-verifier seam whose \textbf{default fails
closed}: the production path is disabled until a sound, externally-reviewed
verifier is explicitly registered (cf. \texttt{pulsar/ref/go/pkg/pulsar/proof.go}).
There is exactly one such pattern; no construction is enabled by a default.

\section{Per-family red-team checklists}
Each primitive is reviewed under its family's threat model, not a generic one:
lattice (rejection/hint leakage, norm bounds, nonce reuse), hash-based
(one-time-key reuse, ADRS domain separation, seed reconstruction, leaf-index
uniqueness under replay/rollback), and STARK/FRI (constraint completeness,
soundness of the low-degree test, in-circuit hash fidelity). The checklists
live in \texttt{framework/redteam/}.

\end{document}