paper: retitle to "Progressive Type Safety" and extend to 12 levels

- Title changed from "Applying Database Query Type Safety to WebAssembly
  Linear Memory" to "Progressive Type Safety for WebAssembly Linear Memory"
- Abstract, introduction, contributions, conclusion updated from 10→12 levels
- New subsection "Novel Levels (11–12)" with full Idris2 code listings for
  tropical cost-tracking (L11, min-plus semiring) and epistemic safety (L12,
  knowledge modality with version-parameterised freshness proofs)
- Soundness conjecture extended with properties (g) cost boundedness and
  (h) epistemic freshness
- New "Tropical and Epistemic Foundations" subsection in formal foundations
- Cross-level composition entries for L11∧L5 and L12∧multi-module
- Related work: tropical semirings (Simon 1988) and epistemic logic
  (Fagin et al. 1995) with new bibliography entries
- HAL metadata updated: new title, 12-level abstract, added keywords
  (progressive type safety, tropical semiring, epistemic logic, cost-tracking)
- Whitepapers/academic version title synced

Co-Authored-By: Claude Opus 4.6 (1M context) <noreply@anthropic.com>

Author: hyperpolymath

docs/arxiv/hal-metadata.yml

@@ -5,7 +5,7 @@
 # HAL accepts PDF upload + manual metadata entry.
 # This file documents the values to enter.
 
-title: "typed-wasm: Applying Database Query Type Safety to WebAssembly Linear Memory"
+title: "typed-wasm: Progressive Type Safety for WebAssembly Linear Memory"
 
 authors:
   - name: "Jonathan D.A. Jewell"
@@ -18,18 +18,23 @@ abstract: |
   module boundaries. When independently compiled modules — potentially from
   different source languages — read and write the same memory regions, no
   existing type system covers the cross-module interface. We present
-  typed-wasm, a type system that applies a 10-level type safety framework,
-  originally developed for database query languages, to Wasm linear memory.
-  The system treats contiguous memory segments as typed region schemas and
-  load/store operations as typed projections verified against those schemas
-  at compile time. We formalise the system in Idris 2 using Quantitative
-  Type Theory (QTT), providing proofs of bounds safety, aliasing freedom,
-  effect purity, lifetime validity, and linearity — all erased before code
-  generation, yielding zero runtime overhead. Our principal contribution is
+  typed-wasm, a type system that applies a 12-level progressive type safety
+  framework, originally developed for database query languages, to Wasm
+  linear memory. The system treats contiguous memory segments as typed
+  region schemas and load/store operations as typed projections verified
+  against those schemas at compile time. We formalise the system in Idris 2
+  using Quantitative Type Theory (QTT), providing proofs of bounds safety,
+  aliasing freedom, effect purity, lifetime validity, linearity, cost
+  boundedness, and epistemic freshness — all erased before code generation,
+  yielding zero runtime overhead. Our principal contribution is
   multi-module schema agreement: a static verification that independently
   compiled Wasm modules agree on the layout, types, alignment, and
   invariants of shared memory regions — a property that no source-level
-  type system, and no existing Wasm proposal, can express.
+  type system, and no existing Wasm proposal, can express. We further
+  extend the framework with tropical cost-tracking (Level 11, bounding
+  access pattern costs via a min-plus semiring) and epistemic safety
+  (Level 12, preventing reads of stale shared state across module
+  boundaries).
 
 # HAL document type
 document_type: preprint  # "preprint" or "conference paper" or "journal article"
@@ -42,14 +47,17 @@ domains:
 
 keywords:
   - WebAssembly
-  - type safety
+  - progressive type safety
   - dependent types
   - linear memory
   - multi-module verification
   - quantitative type theory
   - memory safety
   - formal verification
   - Idris2
+  - tropical semiring
+  - epistemic logic
+  - cost-tracking
 
 language: en
 

docs/arxiv/typed-wasm.bib

@@ -145,6 +145,26 @@ @misc{wasmspec2024
   note         = {Accessed: 2026},
 }
 
+@book{fagin1995,
+  author    = {Ronald Fagin and Joseph Y. Halpern and Yoram Moses and Moshe Y. Vardi},
+  title     = {Reasoning About Knowledge},
+  publisher = {MIT Press},
+  year      = {1995},
+  isbn      = {978-0-262-56200-3},
+}
+
+@incollection{simon1988,
+  author    = {Imre Simon},
+  title     = {Recognizable Sets with Multiplicities in the Tropical Semiring},
+  booktitle = {Mathematical Foundations of Computer Science 1988},
+  series    = {Lecture Notes in Computer Science},
+  volume    = {324},
+  pages     = {107--120},
+  year      = {1988},
+  publisher = {Springer},
+  doi       = {10.1007/BFb0017135},
+}
+
 @inproceedings{wurthinger2017,
   author    = {Thomas W{\"u}rthinger and Christian Wimmer and Christian Humer and Andreas W{\"o}{\ss} and Lukas Stadler and Chris Seaton and Gilles Duboscq and Doug Simon and Matthias Grimmer},
   title     = {Practical Partial Evaluation for High-Performance Dynamic Language Runtimes},