Skip to content

Commit 31879f6

Browse files
hyperpolymathclaude
hyperpolymath
and
claude
committed
docs: add Level Achievement Status + paper Appendix A
- LEVEL-STATUS.md: 12-level table with E2E/proven[sfap]/formalised[sfap] status, versioning scheme (v1.0=L1-10, v1.1=L11-12, v2.0=L13+), proof inventory (0 believe_me across all 11 files) - Paper Appendix A: same table in LaTeX, explanation of "proven erased" and "formalised" categories, [sfap] qualification - [sfap] = "so far as possible" — honest about WasmCert gap Co-Authored-By: Claude Opus 4.6 (1M context) <noreply@anthropic.com>
1 parent e4253f0 commit 31879f6

2 files changed

Lines changed: 127 additions & 0 deletions

File tree

‎LEVEL-STATUS.md‎

Lines changed: 65 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,65 @@
1+
# SPDX-License-Identifier: PMPL-1.0-or-later
2+
# typed-wasm Level Achievement Status
3+
4+
## Versioning Scheme
5+
6+
typed-wasm versions track the highest fully-achieved level tier:
7+
8+
| Version | Levels | Meaning |
9+
|---------|--------|---------|
10+
| v1.0 | L1-10 | Proven erasable stack (proofs + runtime L1-6, compile-time L7-10) |
11+
| v1.1 | L11-12 | Tropical + epistemic (formalised → integrated into toolchain) |
12+
| v2.0 | L13+ | Future levels (probabilistic, differential privacy, etc.) |
13+
14+
## Current: v1.0 (L1-10 complete, L11-12 formalised)
15+
16+
| Level | Name | Idris2 Proof | Zig FFI | Tests | Status |
17+
|-------|------|-------------|---------|-------|--------|
18+
| 1 | Instruction validity | Region.idr | Parser | ECHIDNA 10^5 | **E2E complete** |
19+
| 2 | Region-binding | Region.idr + TypedAccess.idr | Schema lookup | ECHIDNA 10^5 | **E2E complete** |
20+
| 3 | Type-compatible access | TypedAccess.idr | Typed load/store | ECHIDNA 10^5 | **E2E complete** |
21+
| 4 | Null safety | Pointer.idr | Pointer kinds | ECHIDNA 10^5 | **E2E complete** |
22+
| 5 | Bounds-proof | TypedAccess.idr + Levels.idr | Bounds check | ECHIDNA 10^5 | **E2E complete** |
23+
| 6 | Result-type | TypedAccess.idr | Type flow | ECHIDNA 10^5 | **E2E complete** |
24+
| 7 | Aliasing safety | Pointer.idr (Unique) | Erased (QTT) | ECHIDNA 10^4 | **Proven [sfap], erased** |
25+
| 8 | Effect-tracking | Effects.idr | Erased (QTT) | ECHIDNA 10^4 | **Proven [sfap], erased** |
26+
| 9 | Lifetime safety | Lifetime.idr | Erased (QTT) | ECHIDNA 10^4 | **Proven [sfap], erased** |
27+
| 10 | Linearity | Linear.idr (QTT q=1) | Erased (QTT) | ECHIDNA 10^4 | **Proven [sfap], erased** |
28+
| 11 | Tropical cost-tracking | Tropical.idr (0 believe_me) | Not yet | None | **Formalised [sfap]** |
29+
| 12 | Epistemic safety | Epistemic.idr (0 believe_me) | Not yet | None | **Formalised [sfap]** |
30+
31+
**[sfap]** = "so far as possible" — proofs are machine-checked in Idris2 with
32+
zero dangerous patterns. They are as complete as the Idris2 type checker can
33+
verify. Full mechanical verification against a formal Wasm operational
34+
semantics (e.g. WasmCert-Isabelle) remains future work.
35+
36+
## What "proven, erased" means
37+
38+
Levels 7-10 are verified by the Idris2 type checker at compile time, then
39+
erased before code generation via QTT (Quantitative Type Theory). The
40+
emitted Wasm is identical to hand-written code — zero runtime overhead.
41+
This is by design, not a gap. The proofs exist to catch bugs at compile
42+
time; they are not needed at runtime.
43+
44+
## What "formalised" means
45+
46+
Levels 11-12 have Idris2 type definitions and proof structures with zero
47+
believe_me, but no Zig FFI implementation and no integration tests. They
48+
are machine-checked mathematical definitions, not runnable code. Wiring
49+
them into the toolchain is the v1.1 milestone.
50+
51+
## Proof inventory (0 believe_me across all files)
52+
53+
| File | Lines | believe_me | postulate | assert_total |
54+
|------|-------|-----------|-----------|-------------|
55+
| Region.idr | - | 0 | 0 | 0 |
56+
| TypedAccess.idr | - | 0 | 0 | 0 |
57+
| Levels.idr | - | 0 | 0 | 0 |
58+
| Pointer.idr | - | 0 | 0 | 0 |
59+
| Effects.idr | - | 0 | 0 | 0 |
60+
| Lifetime.idr | - | 0 | 0 | 0 |
61+
| Linear.idr | - | 0 | 0 | 0 |
62+
| MultiModule.idr | - | 0 | 0 | 0 |
63+
| Proofs.idr | - | 0 | 0 | 0 |
64+
| Tropical.idr | - | 0 | 0 | 0 |
65+
| Epistemic.idr | - | 0 | 0 | 0 |

‎docs/arxiv/typed-wasm.tex‎

Lines changed: 62 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -956,6 +956,68 @@ \section{Conclusion}
956956
that database query type safety is a transferable framework for these
957957
domains.
958958

959+
% ==========================================================================
960+
\appendix
961+
\section{Level Achievement Status}
962+
\label{app:levels}
963+
% ==========================================================================
964+
965+
Table~\ref{tab:levelstatus} reports the implementation status of each
966+
level as of version~1.0. Levels marked \emph{[sfap]} (``so far as
967+
possible'') have machine-checked proofs in Idris~2 with zero
968+
\texttt{believe\_me}, \texttt{postulate}, or \texttt{assert\_total}.
969+
Full mechanical verification against a formal Wasm operational semantics
970+
(e.g.\ WasmCert-Isabelle~\cite{watt2018}) remains future work.
971+
972+
\begin{table}[ht]
973+
\centering
974+
\caption{Level achievement status (v1.0).}
975+
\label{tab:levelstatus}
976+
\begin{tabular}{@{}rlllll@{}}
977+
\toprule
978+
\textbf{Lv} & \textbf{Name} & \textbf{Proof} & \textbf{Runtime} & \textbf{Tests} & \textbf{Status} \\
979+
\midrule
980+
1 & Instruction & Region.idr & Parser & $10^5$ & E2E \\
981+
2 & Region-binding & TypedAccess.idr & Schema & $10^5$ & E2E \\
982+
3 & Type-compat. & TypedAccess.idr & Load/store & $10^5$ & E2E \\
983+
4 & Null safety & Pointer.idr & Ptr kinds & $10^5$ & E2E \\
984+
5 & Bounds-proof & Levels.idr & Bounds chk & $10^5$ & E2E \\
985+
6 & Result-type & TypedAccess.idr & Type flow & $10^5$ & E2E \\
986+
\midrule
987+
7 & Aliasing & Pointer.idr & Erased & $10^4$ & Proven [sfap] \\
988+
8 & Effects & Effects.idr & Erased & $10^4$ & Proven [sfap] \\
989+
9 & Lifetime & Lifetime.idr & Erased & $10^4$ & Proven [sfap] \\
990+
10 & Linearity & Linear.idr & Erased & $10^4$ & Proven [sfap] \\
991+
\midrule
992+
11 & Tropical cost & Tropical.idr & --- & --- & Formalised [sfap] \\
993+
12 & Epistemic & Epistemic.idr & --- & --- & Formalised [sfap] \\
994+
\bottomrule
995+
\end{tabular}
996+
\end{table}
997+
998+
\textbf{Versioning scheme.}
999+
typed-wasm versions track the highest fully-achieved level tier:
1000+
v1.0 = L1--10 (proven erasable stack);
1001+
v1.1 = L11--12 (tropical + epistemic integrated into toolchain);
1002+
v2.0 = L13+ (future levels).
1003+
1004+
\textbf{``Proven, erased'' (L7--10).}
1005+
These levels are verified by the Idris~2 type checker at compile time,
1006+
then erased before code generation via QTT. The emitted Wasm instructions
1007+
are identical to hand-written code --- zero runtime overhead. This is by
1008+
design: the proofs catch bugs at compile time and are not needed at runtime.
1009+
1010+
\textbf{``Formalised'' (L11--12).}
1011+
Levels~11 and 12 have Idris~2 type definitions and proof structures with
1012+
zero \texttt{believe\_me}, but no Zig FFI implementation. They are
1013+
machine-checked mathematical definitions awaiting toolchain integration.
1014+
1015+
\textbf{Proof inventory.}
1016+
All 11 Idris~2 ABI files (Region, TypedAccess, Levels, Pointer, Effects,
1017+
Lifetime, Linear, MultiModule, Proofs, Tropical, Epistemic) contain zero
1018+
instances of \texttt{believe\_me}, \texttt{postulate}, or
1019+
\texttt{assert\_total}.
1020+
9591021
% ==========================================================================
9601022
% Bibliography
9611023
% ==========================================================================

0 commit comments

Comments
 (0)