// SPDX-License-Identifier: CC-BY-SA-4.0
// Copyright (c) 2026 Jonathan D.A. Jewell (hyperpolymath) <j.d.a.jewell@open.ac.uk>
= Publication Pre-Flight Standard
Jonathan D.A. Jewell <j.d.a.jewell@open.ac.uk>
:toc: macro
:sectnums:

Every hyperpolymath paper MUST pass this checklist before submission to
Zenodo, HAL, arXiv, or any journal/conference. No exceptions.

For repository and system stable-release gating before `v1.0.0`, see
link:../release-pre-flight/V1-GATE.adoc[Stable Release Gate].

[quote]
____
**Present with purpose as precedent a performant, profiled, probed, proven, portable program for production and publication.**
____

The 10 P's:

[cols="1,3"]
|===
| **Present** | Publishable — paper exists, compiles, reads well
| **Purpose** | Clear motivation — why does this matter, who benefits
| **Precedent** | Novel contribution — not a restatement of the obvious
| **Performant** | Benchmarked — numbers in the paper match runnable code
| **Profiled** | No pathological hotspots — performance is understood, not assumed
| **Probed** | panic-attack clean — no critical/high findings in static analysis
| **Proven** | Machine-checked proofs — Idris2/Lean4/Agda, zero believe_me
| **Portable** | Builds on CI — not just your machine, reproducible by reviewers
| **Production** | Ready to use — not a toy, not a sketch, real code behind every claim
| **Publication** | Worthy of a reader's time — not just something we think looks cool
|===

The standard is deliberately high. If a paper cannot survive all 10 P's,
it is not ready. Parking it is not failure — publishing prematurely is.

Prefer precise, properly parameterised, plainly provable propositions over padded, performative, premature, or purely persuasive prose. Please place every paper through punctilious, provably precise preflight preparation so premature promises never propagate past proof.

Push every proposition through a punishing pipeline: precise proofs, peer review, profiling, performance data, portability checks, point-to-point tests, and the prohibition on partial or padded placeholders. Partial promises, placeholder proofs, and padded prose are banned; only polished, provably complete submissions proceed beyond this gate.

PPP Pipeline mania: we demand Proof, Profiling, Performance, Portability, and Publication plus Panic-attack/Probing; think of each P as an artefact checkpoint, and if any P is missing, the paper or release is parked in `PROOF-NEEDS` / `TEST-NEEDS` until the gate is fully closed.

toc::[]

Quick profiles:

* link:HOL-SUITABILITY-CHECKLIST.adoc[HOL Suitability Checklist] for theorem-heavy papers that need proof-audience discipline.
* link:ZENODO-DEPOSIT-CHECKLIST.adoc[Zenodo Deposit Checklist] for DOI-facing archival releases.

== 1. Test Suite (ALL must pass)

[cols="1,3"]
|===
| Check | Description

| Point-to-point (P2P)
| Individual function/module tests. Every public function has at least one test.

| End-to-end (E2E)
| Full pipeline tests. Input → output matches expected for representative cases.

| Aspect tests
| Cross-cutting concerns: security (injection, XSS, SSRF), performance (no O(n²) where O(n) claimed), concurrency (no data races), accessibility (where applicable).

| Build tests
| `cargo build`, `mix compile`, `zig build`, `idris2 --check` — zero errors, zero warnings treated as errors.

| Execution tests
| Binary runs, produces expected output, exits cleanly. CLI --help works.

| Self-tests
| If the tool has built-in diagnostics (`opsm check`, `panic-attack assail`), run them on the repo itself.

| Benchmark suite
| If the paper claims performance numbers, benchmarks MUST exist in repo and be runnable. Results must match claims within 20%.

| Benchmark authenticity
| Benchmarks must execute real program logic, not placeholders, constants, or empty harnesses. `benches/.gitkeep`, `black_box(42)`, copied template benches, or no-op timing loops do NOT count as evidence.

| Test authenticity
| Placeholder fuzz files, copied template integration tests, or unchanged scaffold tests do NOT count. Submission-blocking if the repo gives a false impression of coverage through template artifacts.

| Domain-specific tests
| Security papers need security tests; parser papers need malformed-input tests; protocol papers need interop/conformance tests; proof-carrying systems need tests that exercise the implementation around the proven core. Generic unit tests alone are not sufficient.
|===

== 2. Static Analysis

[cols="1,3"]
|===
| Check | Description

| panic-attack assail
| Zero critical findings, zero high findings. Medium findings documented.

| Hypatia scan
| `.hypatia/` directory present with recent scan cache.

| Dangerous patterns
| `grep -r "believe_me\|sorry\|Admitted\|assert_total\|postulate\|unsafeCoerce\|Obj.magic"` — ZERO in proof code. Crypto axioms (SHA256 collision resistance etc.) are permitted IFF documented in paper with justification.

| Template contamination
| `grep -r "{{PROJECT}}\|TODO\|placeholder"` across proof, benchmark, test, and paper paths must not reveal scaffold residue that could misrepresent maturity. Any remaining template artifact in a claimed research contribution is a blocker.
|===

== 3. Formal Proofs

[cols="1,3"]
|===
| Check | Description

| Idris2
| All `.idr` files compile with `%default total`. No `believe_me`, `assert_total`, or `postulate` except documented crypto axioms.

| Lean4
| If claims are core to the paper, cross-validate at least the key theorems in Lean4.

| Agda / Coq
| If the paper is in a domain where Agda or Coq is standard (e.g. PL metatheory), provide proofs there too. Zero `sorry` / `Admitted`.

| Proof coverage
| Every theorem stated in the paper must have a machine-checked proof in the repo. If a theorem is conjectured (not proven), it MUST be labelled "Conjecture" not "Theorem".

| Proof authenticity
| The mere presence of `.idr`, `.lean`, `.agda`, or `.v` files does not count. Proof files must be project-specific, compile cleanly, and contain no template placeholders, open holes, or copied scaffold bodies masquerading as real verification.
|===

== 4. Bibliography

[cols="1,3"]
|===
| Check | Description

| .bib file exists
| Co-located with the .tex file. Every `\cite{}` resolves.

| Authors are real
| Every cited author appears on DBLP, Google Scholar, or Semantic Scholar with a real publication history.

| Papers exist
| Every cited paper can be found via its DOI, URL, or title search. No fabricated references.

| Impact quality
| At least 50% of citations should be from venues with known impact (POPL, PLDI, ICFP, OOPSLA, LICS, TOPLAS, JFP, IEEE S&P, CCS, USENIX Security, or equivalent). Arxiv preprints are acceptable but should not dominate.

| Self-citation
| Self-citations are permitted but must be minority (<30%). Each self-citation must be genuinely relevant, not padding.

| Recency
| At least 30% of citations from the last 5 years. Classic foundational references exempt.
|===

== 5. Claims Verification

[cols="1,3"]
|===
| Check | Description

| Quantitative claims
| Every number in the abstract (N modules, X% improvement, Y tests) must be reproducible by running code in the repo. `wc -l`, `grep -c`, test output, benchmark logs.

| No overclaims
| "We prove X" means a machine-checked proof exists. "We show X" means experimental evidence exists. "We conjecture X" means neither. Never use "prove" for "argue" or "demonstrate".

| Title and abstract parity
| If the title or abstract says "provable", "verified", "sound", "safe", "secure", "reversible", or similar, the repo must contain evidence at that exact level. Title-grade claims are held to the strictest reading.

| Claim posture
| State the strongest claim the artifact actually supports: no stronger, no weaker. Do not inflate a proposition into a theorem, and do not reduce a substantive theorem to a trivial observation just because it is easier to defend.

| Statement precision
| Every central claim must state its parameters, preconditions, semantic setting, and scope. If a result only holds for a fragment, bounded resource model, trusted FFI boundary, or assumed primitive, say so in the theorem statement and in the prose around it.

| Assumption ledger
| Every non-derived premise must be listed explicitly in one place in the paper: crypto assumptions, parser totality assumptions, string/IO primitives, trust boundaries, oracle models, or external solver assumptions. Hidden assumptions are a submission blocker.

| Paper/proof parity
| The theorem stated in the paper must match the mechanized statement in quantification, hypotheses, and conclusion. No paper theorem may silently omit side conditions that appear in the proof artifact.

| Non-triviality
| Contribution claims must be materially interesting. Do not pad the abstract or introduction with bookkeeping lemmas, definitional equalities, or routine closure facts unless they are genuinely the core technical obstacle.

| Comparison claims
| "Better than X" or "unlike X" claims must cite X and explain the specific dimension of comparison. No strawmen.

| Novelty claims
| "First to X" or "no existing system does X" — verify via thorough literature search. These are the claims most likely to be wrong.
|===

== 6. Zenodo / HAL Metadata

[cols="1,3"]
|===
| Check | Description

| `.zenodo.json`
| Present in repo root with title, description, creators, keywords, subjects, license.

| HAL metadata
| `hal-metadata.yml` present with title, authors, abstract, domains, keywords.

| GitHub release
| Tag `vX.Y.Z-paper` created. Zenodo auto-creates DOI from release.

| DOI badge
| After first Zenodo sync, add DOI badge to README.

| Dual deposit
| Submit to BOTH Zenodo (DOI) and HAL (French national archive) for maximum discoverability.
|===

== 7. Final Review

[cols="1,3"]
|===
| Check | Description

| Co-author review
| If there are co-authors, all have reviewed and approved.

| Licence headers
| SPDX headers on all source files. Paper itself under CC-BY-4.0 for text, PMPL for code.

| Reproducibility
| A reviewer should be able to: clone the repo, run the tests, verify the claims, in under 30 minutes. If setup takes longer, add a `setup.sh`.

| Spellcheck
| Run `aspell` or equivalent on the .tex file.

| LaTeX compiles
| `pdflatex` + `bibtex` produces a clean PDF with no warnings.
|===

== Traffic Light Summary

**GREEN** = all checks pass → submit immediately

**YELLOW** = 1-3 fixable issues → fix in one session, then re-check

**RED** = structural problems (missing implementation, unverified claims, wrong venue) → do not submit
