mirror of
https://github.com/saymrwulf/proof-aware-crypto-tooling-agent.git
synced 2026-09-03 19:53:43 +00:00
paper form round: every defect from the socratic inspection fixed + check-paper.sh gate
Triggered by the operator's hint (references flow into App A but a full break sits between B and C). Full-document inspection found and fixed: - ghost page 23 (~85% blank): the fossil \clearpage before Appendix C, placed under an older pagination, removed; appendix policy now DECLARED: the block starts on a fresh page, then flows with no internal breaks - claim matrix (the paper's honesty centerpiece): solid-set rows merged visually and narrow justified columns gaped (badness-10000 in every build log, never read) -- now ragged-right columns, 3pt row air, EUF-CMA/SHA-256 unbreakable - Figure 3 still drew the July 13-leaf snapshot in a v0.11 paper that narrates 19 leaves -- extended: leaves 13-18, August-2026 brace, dual-signed size-19 head box, pq-styled leaf 18 - ConsRec hyphenated as Con-sRec and set in serif vs sans elsewhere -> math-face identifiers in the mechanization table - 'tuple' stranded its last syllable as a whole line in Definition 1; 'timestamp' broke as times-tamp -> mbox + \hyphenation - thesis box hyphenated its showcase slogan -> ragged-right no-hyphen (first attempt justified+nohyphen was caught by the new gate itself) - Appendix E header caps + layer-cell caps + continuation row cleanup; related-work 3.4pt overfull removed - NEW check-paper.sh: fails on overfull>10pt, any badness-10000, ghost pages (<300 chars/page), missing version on title page, ?? refs; 4-check selftest; renders all pages for the mandatory eye pass All 25 pages re-rendered and flipped by eye. Gate green. Tests green.
This commit is contained in:
parent
46a3094216
commit
810d6f47f1
4 changed files with 132 additions and 31 deletions
1
paper/.gitignore
vendored
1
paper/.gitignore
vendored
|
|
@ -2,3 +2,4 @@
|
|||
*.log
|
||||
*.out
|
||||
*.toc
|
||||
rendered-pages/
|
||||
|
|
|
|||
76
paper/check-paper.sh
Executable file
76
paper/check-paper.sh
Executable file
|
|
@ -0,0 +1,76 @@
|
|||
#!/usr/bin/env bash
|
||||
# check-paper.sh — the paper's form gate.
|
||||
#
|
||||
# Ports the book's check-book.sh lesson to the paper: the 2026-08-16
|
||||
# socratic round found a ghost page (a fossil \clearpage) and a solid-set
|
||||
# claim matrix whose badness-10000 warnings had printed in EVERY build,
|
||||
# unread. This gate makes both classes of defect fail the build instead
|
||||
# of shipping silently. It cannot replace the render-and-look eye pass —
|
||||
# it renders the pages so the eye pass has no excuse.
|
||||
#
|
||||
# Usage: ./check-paper.sh build + all gates + render pages
|
||||
# ./check-paper.sh --selftest exercise the gate parsers on
|
||||
# known-bad and known-good log lines
|
||||
set -euo pipefail
|
||||
cd "$(dirname "$0")"
|
||||
|
||||
OVERFULL_LIMIT_PT=10
|
||||
MIN_PAGE_CHARS=300 # calibrated 2026-08-16: real minimum was 922 (claim-matrix page)
|
||||
PAGES_DIR=rendered-pages
|
||||
|
||||
fail() { echo "FAIL: $*" >&2; exit 1; }
|
||||
|
||||
# --- gate parsers (pure text -> verdict; selftestable) -------------------
|
||||
overfull_violations() { # stdin: build log -> lines exceeding the limit
|
||||
grep -i 'Overfull \\hbox' | grep -oP '\(\K[0-9.]+(?=pt too wide)' \
|
||||
| awk -v lim="$OVERFULL_LIMIT_PT" '$1 > lim' || true
|
||||
}
|
||||
badness_violations() { # stdin: build log -> badness-10000 underfull lines
|
||||
grep -i 'Underfull \\hbox (badness 10000)' || true
|
||||
}
|
||||
|
||||
if [[ "${1:-}" == "--selftest" ]]; then
|
||||
n=0
|
||||
t() { n=$((n+1)); [[ "$2" == "$3" ]] && echo "selftest $n ok: $1" || fail "selftest $n: $1 (got '$3', want '$2')"; }
|
||||
t "80pt overfull trips" "80.05" \
|
||||
"$(echo 'warning: x.tex:1: Overfull \hbox (80.05pt too wide) in paragraph' | overfull_violations)"
|
||||
t "3.4pt overfull passes" "" \
|
||||
"$(echo 'warning: x.tex:1: Overfull \hbox (3.374pt too wide) in paragraph' | overfull_violations)"
|
||||
t "badness 10000 trips" "1" \
|
||||
"$(echo 'warning: x.tex:1: Underfull \hbox (badness 10000) in paragraph' | badness_violations | wc -l)"
|
||||
t "badness 2913 passes" "0" \
|
||||
"$(echo 'warning: x.tex:1: Underfull \hbox (badness 2913) in paragraph' | badness_violations | wc -l)"
|
||||
echo "selftest: $n/$n ok"; exit 0
|
||||
fi
|
||||
|
||||
# --- 1. build ------------------------------------------------------------
|
||||
LOG=$(mktemp); trap 'rm -f "$LOG"' EXIT
|
||||
tectonic ltl.tex 2>&1 | tee "$LOG" >/dev/null
|
||||
grep -qi '^error' "$LOG" && fail "TeX errors in build log"
|
||||
|
||||
# --- 2. overfull gate ----------------------------------------------------
|
||||
OV=$(overfull_violations <"$LOG")
|
||||
[[ -z "$OV" ]] || fail "overfull hbox beyond ${OVERFULL_LIMIT_PT}pt: $OV"
|
||||
|
||||
# --- 3. loose-typesetting gate (the ignored-warnings class) --------------
|
||||
BAD=$(badness_violations <"$LOG" | wc -l)
|
||||
[[ "$BAD" -eq 0 ]] || fail "$BAD underfull badness-10000 lines (gappy table/paragraph)"
|
||||
|
||||
# --- 4. ghost-page gate (the fossil-clearpage class) ---------------------
|
||||
NPAGES=$(pdfinfo ltl.pdf | awk '/^Pages:/{print $2}')
|
||||
for p in $(seq 1 $((NPAGES-1))); do
|
||||
chars=$(pdftotext -f "$p" -l "$p" ltl.pdf - 2>/dev/null | tr -d '[:space:]' | wc -c)
|
||||
[[ "$chars" -ge "$MIN_PAGE_CHARS" ]] || fail "page $p is mostly blank ($chars chars) — ghost page"
|
||||
done
|
||||
|
||||
# --- 5. content probes ---------------------------------------------------
|
||||
VERSION=$(grep -oP '\\date\{[^}]*---\s*\Kv[0-9.]+' ltl.tex || true)
|
||||
[[ -n "$VERSION" ]] || fail "cannot extract version from \\date{...} in ltl.tex"
|
||||
pdftotext -f 1 -l 1 ltl.pdf - | grep -q "$VERSION" || fail "title page does not carry $VERSION"
|
||||
! pdftotext ltl.pdf - | grep -q '??' || fail "unresolved ?? reference in PDF"
|
||||
|
||||
# --- 6. render for the mandatory eye pass --------------------------------
|
||||
rm -rf "$PAGES_DIR"; mkdir -p "$PAGES_DIR"
|
||||
pdftoppm -png -r 110 ltl.pdf "$PAGES_DIR/p"
|
||||
echo "OK: $VERSION, $NPAGES pages, no overfull>${OVERFULL_LIMIT_PT}pt, no badness-10000, no ghost pages, no ?? refs."
|
||||
echo "NOW LOOK: the render-and-look law is not automated. Flip every page in $PAGES_DIR/."
|
||||
BIN
paper/ltl.pdf
BIN
paper/ltl.pdf
Binary file not shown.
|
|
@ -26,6 +26,7 @@
|
|||
\newcommand{\Hh}{\mathsf{H}}
|
||||
\newcommand{\hleaf}{\mathsf{h}_{\rm leaf}}
|
||||
\newcommand{\hnode}{\mathsf{h}_{\rm node}}
|
||||
\hyphenation{time-stamp time-stamps}
|
||||
\newcommand{\MTH}{\mathsf{MTH}}
|
||||
\newcommand{\Root}{\mathsf{Root}}
|
||||
\newcommand{\Path}{\mathsf{Path}}
|
||||
|
|
@ -135,7 +136,7 @@ The contribution is not a new Merkle tree and not a new theorem prover. It is a
|
|||
trust decomposition for distributing machine-checked correctness evidence:
|
||||
|
||||
\begin{center}
|
||||
\fbox{\parbox{0.91\linewidth}{
|
||||
\fbox{\parbox{0.91\linewidth}{\raggedright\hyphenpenalty=10000\exhyphenpenalty=10000
|
||||
\textbf{Expensive deterministic verification produces an observation.
|
||||
Transparency makes that observation accountable. Consumer-local policy decides
|
||||
whether the observation is acceptable.}}}
|
||||
|
|
@ -295,7 +296,7 @@ observed axiom-name set. The deployed schema additionally carries diagnostics,
|
|||
resource controls, scope, and exclusions.
|
||||
|
||||
\begin{definition}[Attestation-transparency scheme]
|
||||
An attestation-transparency scheme is a tuple
|
||||
An attestation-transparency scheme is a~\mbox{tuple}
|
||||
\[
|
||||
\Pi=(\mathsf{KeyGen},\mathsf{Append},\mathsf{ProveIncl},
|
||||
\mathsf{VerifyIncl},\mathsf{ProveCons},\mathsf{VerifyCons},\mathsf{Verdict})
|
||||
|
|
@ -1207,32 +1208,42 @@ boundary axiom, \code{LTLAcc.sha256}.
|
|||
\centering
|
||||
\begin{tikzpicture}[
|
||||
>=Latex,
|
||||
box/.style={draw,rounded corners=2pt,minimum width=1.03cm,minimum height=.52cm,font=\scriptsize,align=center},
|
||||
box/.style={draw,rounded corners=2pt,minimum width=.78cm,minimum height=.5cm,font=\tiny,align=center,inner sep=1.5pt},
|
||||
fail/.style={box,fill=black!6,draw=black!45,text=black!60},
|
||||
pq/.style={box,fill=violet!8,draw=violet!60!black,text=violet!55!black},
|
||||
ok/.style={box,fill=green!7!white,draw=deepgreen,text=deepgreen!80!black},
|
||||
acc/.style={box,fill=blue!7!white,draw=deepblue,text=deepblue},
|
||||
arrow/.style={->,draw=black!55}
|
||||
]
|
||||
\foreach \i in {0,...,3} {\node[fail] (l\i) at (1.08*\i,0) {\i\\failed};}
|
||||
\foreach \i in {4,...,7} {\node[ok] (l\i) at (1.08*\i,0) {\i\\clean};}
|
||||
\foreach \i in {8,...,11} {\node[ok] (l\i) at (1.08*\i,0) {\i\\clean};}
|
||||
\node[acc] (l12) at (1.08*12,0) {12\\accum.};
|
||||
\foreach \i in {0,...,3} {\node[fail] (l\i) at (0.82*\i,0) {\i\\failed};}
|
||||
\foreach \i in {4,...,7} {\node[ok] (l\i) at (0.82*\i,0) {\i\\clean};}
|
||||
\foreach \i in {8,...,11} {\node[ok] (l\i) at (0.82*\i,0) {\i\\clean};}
|
||||
\node[acc] (l12) at (0.82*12,0) {12\\accum.};
|
||||
\foreach \i in {13,...,16} {\node[ok] (l\i) at (0.82*\i,0) {\i\\re-att.};}
|
||||
\node[acc] (l17) at (0.82*17,0) {17\\accum.};
|
||||
\node[pq] (l18) at (0.82*18,0) {18\\slh-dsa};
|
||||
\draw[decorate,decoration={brace,mirror,raise=5pt},black!45]
|
||||
($(l0.south west)+(-.05,0)$)--($(l3.south east)+(.05,0)$)
|
||||
($(l0.south west)+(.05,0)$)--($(l3.south east)+(-.05,0)$)
|
||||
node[midway,below=11pt,font=\scriptsize]{run 1};
|
||||
\draw[decorate,decoration={brace,mirror,raise=5pt},deepgreen]
|
||||
($(l4.south west)+(-.05,0)$)--($(l7.south east)+(.05,0)$)
|
||||
($(l4.south west)+(.05,0)$)--($(l7.south east)+(-.05,0)$)
|
||||
node[midway,below=11pt,font=\scriptsize]{run 2};
|
||||
\draw[decorate,decoration={brace,mirror,raise=5pt},deepgreen]
|
||||
($(l8.south west)+(-.05,0)$)--($(l11.south east)+(.05,0)$)
|
||||
($(l8.south west)+(.05,0)$)--($(l11.south east)+(-.05,0)$)
|
||||
node[midway,below=11pt,font=\scriptsize]{run 3};
|
||||
\node[draw,rounded corners,fill=softgray,minimum width=4.3cm,minimum height=.7cm,font=\small] (sth) at (6.7,1.65)
|
||||
{signed head: size 13, root \code{3488a2d0...}};
|
||||
\draw[arrow] (l12.north) -- (sth.south east);
|
||||
\draw[decorate,decoration={brace,mirror,raise=5pt},deepblue]
|
||||
($(l13.south west)+(.05,0)$)--($(l18.south east)+(-.05,0)$)
|
||||
node[midway,below=11pt,font=\scriptsize]{August 2026};
|
||||
\node[draw,rounded corners,fill=softgray,minimum width=5.9cm,minimum height=.85cm,align=center,font=\small] (sth) at (7.4,1.75)
|
||||
{signed head: size 19, root \code{7ee23940...}\\dual-signed: Ed25519 $+$ SLH-DSA};
|
||||
\draw[arrow] (l6.north) -- (sth.south west);
|
||||
\draw[arrow] (l18.north) -- (sth.south east);
|
||||
\end{tikzpicture}
|
||||
\caption{The public 13-leaf deployment. Failure leaves are retained; entry 13
|
||||
attests the accumulator corpus itself, scoped to the recursive model.}
|
||||
\caption{The public nineteen-leaf deployment. Failure leaves are retained; leaf
|
||||
12 (the thirteenth entry) attests the accumulator corpus itself, scoped to the
|
||||
recursive model; leaves 13--16 re-attest the four forks at 44 certificates
|
||||
each; leaf 17 the hardened accumulator corpus; leaf 18 the SLH-DSA verify
|
||||
path. Heads are dual-signed from size 14 on.}
|
||||
\label{fig:deployment}
|
||||
\end{figure}
|
||||
|
||||
|
|
@ -1249,11 +1260,11 @@ refinement from the deployed iterative consistency verifier remain outside the
|
|||
corpus.
|
||||
|
||||
\begin{center}\small
|
||||
\begin{tabularx}{\textwidth}{@{}lXX@{}}
|
||||
\begin{tabularx}{\textwidth}{@{}l>{\raggedright\arraybackslash}X>{\raggedright\arraybackslash}X@{}}
|
||||
\toprule
|
||||
Layer & Mechanized evidence & Explicit boundary \\
|
||||
\midrule
|
||||
Merkle definitions & MTH, Root, Path, recursive ConsRec & single SHA-256 boundary axiom \\
|
||||
Merkle definitions & $\MTH$, $\Root$, $\Path$, recursive $\ConsRec$ & single SHA-256 boundary axiom \\
|
||||
Inclusion & completeness and named collision extractor & collision resistance interpreted externally \\
|
||||
Consistency & recursive-model soundness and extractor & no general consistency-completeness theorem \\
|
||||
Pinning & per-step monotonicity and prefix correctness & signature layer and multi-step closure external \\
|
||||
|
|
@ -1332,7 +1343,7 @@ structure actually differs.
|
|||
|
||||
\paragraph{Transparency.}
|
||||
Certificate Transparency introduced publicly auditable append-only logs for
|
||||
certificate issuance~\cite{ct1,ct2}; Crosby and Wallach developed efficient
|
||||
certificate issuance~\cite{ct1,ct2}; Crosby and Wallach built efficient
|
||||
tamper-evident history trees~\cite{crosby}; Dowling et al. formalized security
|
||||
notions for secure logging and CT~\cite{dghs} --- the games of
|
||||
\S\ref{sec:games} adapt that two-transcript style to replay attestation, with
|
||||
|
|
@ -1557,24 +1568,38 @@ Verification Pipeline with AI Provers: An Experience Report. arXiv:2605.30106,
|
|||
|
||||
\end{thebibliography}
|
||||
|
||||
% Appendix policy (declared 2026-08-16): the appendix block starts on a
|
||||
% fresh page and then flows continuously -- no page breaks between
|
||||
% individual appendices. The claim matrix is one unbreakable tabularx.
|
||||
\clearpage
|
||||
\appendix
|
||||
|
||||
\section{End-to-end claim matrix}\label{app:matrix}
|
||||
\begin{center}\small
|
||||
\begin{tabularx}{\textwidth}{@{}XXX@{}}
|
||||
\begin{tabularx}{\textwidth}{@{}>{\raggedright\arraybackslash}X>{\raggedright\arraybackslash}X>{\raggedright\arraybackslash}X@{}}
|
||||
\toprule
|
||||
Consumer conclusion & Established by & Remaining assumption \\
|
||||
\midrule
|
||||
Leaf has an authentic opening with a position-bound leaf value at index $m$ under head $h$ & inclusion proof and signed head & SHA-256 collision resistance; correct public key; EUF-CMA of the head signature \\
|
||||
Leaf has an authentic opening with a position-bound leaf value at index $m$ under head $h$ & inclusion proof and signed head & \mbox{SHA-256} collision resistance; correct public key; \mbox{EUF-CMA} of the head signature \\
|
||||
\addlinespace[3pt]
|
||||
Head root commits the published numbered leaf list & full-mirror recomputation (\code{verify.py --all}) & mirror availability and retention \\
|
||||
Head was authorized by the log identity & Ed25519 verification & correct key acquisition; EUF-CMA \\
|
||||
New pinned head extends old pinned head & consistency proof & SHA-256 collision resistance; recursive-model soundness; authentic size/root pairing for deployment \\
|
||||
Equal-size unequal roots in one log context conflict & two valid signatures & correct public key; EUF-CMA; operationally, a retaining observer must compare the heads \\
|
||||
\addlinespace[3pt]
|
||||
Head was authorized by the log identity & Ed25519 verification & correct key acquisition; \mbox{EUF-CMA} \\
|
||||
\addlinespace[3pt]
|
||||
New pinned head extends old pinned head & consistency proof & \mbox{SHA-256} collision resistance; recursive-model soundness; authentic size/root pairing for deployment \\
|
||||
\addlinespace[3pt]
|
||||
Equal-size unequal roots in one log context conflict & two valid signatures & correct public key; \mbox{EUF-CMA}; operationally, a retaining observer must compare the heads \\
|
||||
\addlinespace[3pt]
|
||||
Observed cone matches local boundary policy & exact set equality & semantic identity of named declarations \\
|
||||
Operator claims the kernel produced the observation & attestation signature and leaf inclusion & correct provider key; EUF-CMA \\
|
||||
\addlinespace[3pt]
|
||||
Operator claims the kernel produced the observation & attestation signature and leaf inclusion & correct provider key; \mbox{EUF-CMA} \\
|
||||
\addlinespace[3pt]
|
||||
Kernel actually produced the recorded observation & not cryptographically established; independently checkable by replay & operator and replay-pipeline honesty, or faithful independent replay \\
|
||||
\addlinespace[3pt]
|
||||
Recorded cone was produced by an audit that performed its checks & not established --- the audit driver is itself part of the replay pipeline & audit-gate integrity; adversarial gate self-tests reduce this exposure, they do not eliminate it \\
|
||||
\addlinespace[3pt]
|
||||
Source corresponds to deployed binary & not established & reproducible build and compiler assurance \\
|
||||
\addlinespace[3pt]
|
||||
Claimed signer implementation produced STH & not established & execution provenance \\
|
||||
\bottomrule
|
||||
\end{tabularx}
|
||||
|
|
@ -1595,7 +1620,6 @@ additionally relies on an unmechanized authentic-size/root invariant
|
|||
Its exclusions name SHA-256 collision resistance, deployed-verifier extensional
|
||||
equality, the signature/STH layer, and asymptotic cost claims.
|
||||
|
||||
\clearpage
|
||||
\section{Compact receipt-verification core}\label{app:verifier}
|
||||
The following code is only the Merkle inclusion core. A complete receipt
|
||||
verifier must additionally validate the signed tree head, log identifier,
|
||||
|
|
@ -1671,17 +1695,17 @@ five oracles.
|
|||
\begin{center}\small
|
||||
\begin{tabular}{@{}lll@{}}
|
||||
\toprule
|
||||
Layer & Lean declaration(s) & oracles in the cone \\
|
||||
Layer & Lean declaration(s) & Oracles in the cone \\
|
||||
\midrule
|
||||
digit/byte plumbing & \code{to_int_loop_eq}, \code{to_byte_loop_eq} & --- \\
|
||||
& \code{wots_csum_loop_eq}, \code{base2b_outer_loop_eq} & --- \\
|
||||
chain walk & \code{chain_free_loop_eq} & \code{f} \\
|
||||
Digit/byte plumbing & \code{to_int_loop_eq}, \code{to_byte_loop_eq} & --- \\
|
||||
& \code{wots_csum_loop_eq}, \code{base2b_outer_loop_eq} & \\
|
||||
Chain walk & \code{chain_free_loop_eq} & \code{f} \\
|
||||
WOTS pk recomputation & \code{wots_loop1_eq} & \code{f} \\
|
||||
XMSS Merkle ascent & \code{xmss_loop_eq} & \code{h} \\
|
||||
FORS inner ascent & \code{fors_inner_loop_eq} & \code{h} \\
|
||||
FORS outer loop & \code{fors_outer_loop_eq} & \code{f}, \code{h} \\
|
||||
hypertree walk & \code{ht_loop_eq} & \code{f}, \code{h}, \code{t_l} \\
|
||||
acceptance characterization & \code{slh_verify_128s_accepts_iff} & all five \\
|
||||
Hypertree walk & \code{ht_loop_eq} & \code{f}, \code{h}, \code{t_l} \\
|
||||
Acceptance characterization & \code{slh_verify_128s_accepts_iff} & all five \\
|
||||
\bottomrule
|
||||
\end{tabular}
|
||||
\end{center}
|
||||
|
|
|
|||
Loading…
Reference in a new issue