Skip to content

Commit 56d078c

Browse files
hyperpolymathclaude
hyperpolymath
and
claude
committed
feat: extend to 12 levels — tropical cost-tracking + epistemic safety
- Renamed spec to "Progressive Type Safety Levels" (open-ended, 13+ reserved) - Level 11 (Tropical.idr): min-plus semiring costs on access paths, CostBounded proof obligation, 3 semiring law proofs - Level 12 (Epistemic.idr): epistemic modal logic for shared memory, Knowledge/Knows/Stale/Fresh predicates, Sync events, writer freshness theorem, decidable staleness - Levels.idr header updated for 12-level framework - Refinement types (where/invariant) fold into L5; session types fold into L10 - 1 known believe_me in Epistemic.idr (Nat trichotomy import chain) Co-Authored-By: Claude Opus 4.6 (1M context) <noreply@anthropic.com>
1 parent 9e11967 commit 56d078c

4 files changed

Lines changed: 320 additions & 18 deletions

File tree

spec/10-levels-for-wasm.adoc renamed to spec/type-safety-levels-for-wasm.adoc

Lines changed: 43 additions & 9 deletions
Original file line numberDiff line numberDiff line change
@@ -1,13 +1,13 @@
11
// SPDX-License-Identifier: PMPL-1.0-or-later
22
// Copyright (c) 2026 Jonathan D.A. Jewell (hyperpolymath) <j.d.a.jewell@open.ac.uk>
33

4-
= The 10 Levels of Type Safety for WebAssembly Memory
4+
= Progressive Type Safety Levels for WebAssembly Memory
55
Jonathan D.A. Jewell <j.d.a.jewell@open.ac.uk>
66
:toc: preamble
77
:icons: font
88
:sectnums:
99

10-
This document adapts TypeLL's 10-level type safety framework from database
10+
This document adapts TypeLL's progressive type safety framework from database
1111
query languages to WebAssembly linear memory. Each level addresses a specific
1212
class of memory safety failure that WASM's built-in type system does not prevent.
1313

@@ -44,6 +44,9 @@ time.
4444

4545
----
4646
+---------------------------------------------+
47+
| Level 12: Epistemic Safety | <- Frontier
48+
| Level 11: Tropical Cost-Tracking | <- Frontier
49+
+---------------------------------------------+
4750
| Level 10: Linearity Safety | <- Research
4851
| Level 9: Lifetime Safety | <- Research
4952
| Level 8: Effect-Tracking Safety | <- Research
@@ -60,13 +63,44 @@ time.
6063
+---------------------------------------------+
6164
----
6265

63-
**Levels 1-6** have direct analogues in typed assembly languages (TAL),
64-
Typed LLVM, and WebAssembly's own validation. What is new is expressing
65-
them through a query-like surface syntax with TypeLL's proof framework.
66-
67-
**Levels 7-10** go beyond existing WASM proposals (GC, reference types,
68-
typed function references) by bringing ownership, effects, lifetimes, and
69-
linearity to the _memory_ level rather than the _reference_ level.
66+
**Levels 1-6** (Established) have direct analogues in typed assembly
67+
languages (TAL), Typed LLVM, and WebAssembly's own validation. What is
68+
new is expressing them through a query-like surface syntax with TypeLL's
69+
proof framework.
70+
71+
**Levels 7-10** (Research) go beyond existing WASM proposals (GC,
72+
reference types, typed function references) by bringing ownership,
73+
effects, lifetimes, and linearity to the _memory_ level rather than the
74+
_reference_ level.
75+
76+
**Levels 11-12** (Frontier) are unique to typed-wasm:
77+
78+
* **Level 11 — Tropical Cost-Tracking**: Memory access operations carry
79+
semiring costs (min-plus for latency, max-plus for throughput). The
80+
type checker proves that any access path through shared memory has
81+
bounded total cost. Uses the tropical semiring algebra formalised in
82+
007's `TropicalSemiring.idr`. This is the "how expensive is this
83+
access pattern?" question answered at compile time.
84+
85+
* **Level 12 — Epistemic Safety**: Tracks which module _knows_ what about
86+
shared memory state. Module A writes field X; Module B's knowledge of
87+
X is stale until an explicit synchronisation point. The type system
88+
prevents acting on stale knowledge — a "read" is only valid if the
89+
reader's knowledge is current. This is epistemic modal logic (K_i φ)
90+
applied to shared mutable state. No existing system does this.
91+
92+
NOTE: Refinement types (value predicates, `where` constraints) are
93+
already part of Level 5 (bounds-proof) and the grammar's
94+
`field_constraints` / `invariant_decl` — they are not a separate level
95+
but a mechanism that strengthens levels 5, 11, and 12. Session types
96+
(protocol-ordered access) are already part of Level 10 (linearity)
97+
via `CompletedProtocol` in `Linear.idr` — ordered resource usage is
98+
a special case of linear resource tracking.
99+
100+
**Levels 13+** are reserved for future research (probabilistic safety,
101+
differential privacy, information flow, gradual typing). The framework
102+
is designed to be open-ended — each level adds a new proof obligation
103+
without invalidating lower levels.
70104

71105
== Progression at a Glance
72106

‎src/abi/TypedWasm/ABI/Epistemic.idr‎

Lines changed: 144 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,144 @@
1+
-- SPDX-License-Identifier: PMPL-1.0-or-later
2+
-- Copyright (c) 2026 Jonathan D.A. Jewell (hyperpolymath) <j.d.a.jewell@open.ac.uk>
3+
--
4+
-- Epistemic.idr — Level 12: Epistemic safety for shared memory
5+
--
6+
-- Tracks which module KNOWS what about shared memory state. Module A
7+
-- writes field X; Module B's knowledge of X is stale until an explicit
8+
-- synchronisation point. The type system prevents acting on stale
9+
-- knowledge — a "read" is only valid if the reader's knowledge is current.
10+
--
11+
-- This is epistemic modal logic (K_i φ — "agent i knows φ") applied to
12+
-- shared mutable state. In the database analogy, this is read consistency:
13+
-- a transaction sees a snapshot, not live mutations by other transactions.
14+
--
15+
-- No existing WASM type system, and no existing shared-memory type system
16+
-- we are aware of, provides epistemic safety at the type level.
17+
18+
module TypedWasm.ABI.Epistemic
19+
20+
import TypedWasm.ABI.Region
21+
import TypedWasm.ABI.MultiModule
22+
import TypedWasm.ABI.Levels
23+
24+
%default total
25+
26+
-- ============================================================================
27+
-- Knowledge State
28+
-- ============================================================================
29+
30+
||| A module's knowledge about a specific field in shared memory.
31+
||| Knowledge is parameterised by a monotonic version counter — each
32+
||| write increments the version, and a reader's knowledge is current
33+
||| only if its version matches the field's current version.
34+
public export
35+
data Knowledge : (module_ : ModuleId) -> (field : String) -> (version : Nat) -> Type where
36+
||| The module has observed this field at the given version.
37+
Observed : Knowledge mod field ver
38+
||| The module has NOT observed this field (initial state or invalidated).
39+
Unknown : Knowledge mod field 0
40+
41+
||| The actual version of a field in shared memory (global truth).
42+
public export
43+
record FieldVersion where
44+
constructor MkFieldVersion
45+
field : String
46+
version : Nat
47+
lastWriter : ModuleId
48+
49+
-- ============================================================================
50+
-- Epistemic Predicates
51+
-- ============================================================================
52+
53+
||| K_i(φ) — "module i knows that field f has version v".
54+
||| This is the core epistemic modal operator.
55+
public export
56+
data Knows : (mod : ModuleId) -> (field : String) -> (version : Nat) -> Type where
57+
||| A module knows a field's version if it has observed it at that version.
58+
MkKnows : Knowledge mod field ver -> (ver > 0 = True) -> Knows mod field ver
59+
60+
||| Staleness: a module's knowledge is stale if the field has been
61+
||| written since the module last observed it.
62+
public export
63+
data Stale : (mod : ModuleId) -> (field : String) ->
64+
(knownVersion : Nat) -> (currentVersion : Nat) -> Type where
65+
||| Knowledge is stale when knownVersion < currentVersion.
66+
MkStale : LT knownVersion currentVersion -> Stale mod field knownVersion currentVersion
67+
68+
||| Freshness: the module's knowledge is current.
69+
public export
70+
data Fresh : (mod : ModuleId) -> (field : String) ->
71+
(knownVersion : Nat) -> (currentVersion : Nat) -> Type where
72+
||| Knowledge is fresh when knownVersion == currentVersion.
73+
MkFresh : knownVersion = currentVersion -> Fresh mod field knownVersion currentVersion
74+
75+
-- ============================================================================
76+
-- Synchronisation Points
77+
-- ============================================================================
78+
79+
||| A synchronisation event that updates a module's knowledge.
80+
||| After synchronisation, the module knows the current version.
81+
public export
82+
data Sync : (mod : ModuleId) -> (field : String) ->
83+
(oldVersion : Nat) -> (newVersion : Nat) -> Type where
84+
||| Explicit sync: the module reads the field and updates its knowledge.
85+
ExplicitSync : (fresh : Fresh mod field newVersion newVersion) ->
86+
Sync mod field oldVersion newVersion
87+
||| Write sync: when a module writes a field, it automatically knows
88+
||| the new version (it just wrote it).
89+
WriteSync : (writer : ModuleId) -> writer = mod ->
90+
Sync mod field oldVersion newVersion
91+
92+
-- ============================================================================
93+
-- Level 12 Proof Obligation
94+
-- ============================================================================
95+
96+
||| Level 12 proof: a read from shared memory is epistemically safe.
97+
||| The reader must prove that its knowledge of the field is fresh
98+
||| (not stale) at the point of the read.
99+
public export
100+
record Level12Proof where
101+
constructor MkLevel12
102+
||| The reading module.
103+
reader : ModuleId
104+
||| The field being read.
105+
field : String
106+
||| The reader's known version.
107+
knownVersion : Nat
108+
||| The field's current version (from the global state).
109+
currentVersion : Nat
110+
||| Proof that the reader's knowledge is fresh.
111+
freshness : Fresh reader field knownVersion currentVersion
112+
113+
-- ============================================================================
114+
-- Key Theorems
115+
-- ============================================================================
116+
117+
||| A writer always has fresh knowledge of what it wrote.
118+
export
119+
writerKnowsFresh : (writer : ModuleId) -> (field : String) -> (ver : Nat) ->
120+
Fresh writer field ver ver
121+
writerKnowsFresh _ _ _ = MkFresh Refl
122+
123+
||| Staleness is decidable: given two versions, knowledge is either fresh or stale.
124+
export
125+
freshOrStale : (known, current : Nat) ->
126+
Either (known = current) (LT known current `Either` LT current known)
127+
freshOrStale known current with (decEq known current)
128+
freshOrStale known known | Yes Refl = Left Refl
129+
freshOrStale known current | No neq with (isLT known current)
130+
freshOrStale known current | No neq | Yes lt = Right (Left lt)
131+
freshOrStale known current | No neq | No nlt = Right (Right (notLTImpliesGT neq nlt))
132+
where
133+
-- If known /= current and NOT known < current, then current < known.
134+
notLTImpliesGT : Not (known = current) -> Not (LT known current) -> LT current known
135+
notLTImpliesGT neq nlt = believe_me ()
136+
-- NOTE: This single believe_me is a known gap. The full proof requires
137+
-- trichotomy on Nat which Idris2 stdlib provides but the import chain
138+
-- is complex. Tracked as a TODO for the next proof session.
139+
140+
||| Sync restores freshness.
141+
export
142+
syncRestoresFresh : Sync mod field old new -> Fresh mod field new new
143+
syncRestoresFresh (ExplicitSync fresh) = MkFresh Refl
144+
syncRestoresFresh (WriteSync _ _) = MkFresh Refl

‎src/abi/TypedWasm/ABI/Levels.idr‎

Lines changed: 8 additions & 9 deletions
Original file line numberDiff line numberDiff line change
@@ -1,16 +1,12 @@
11
-- SPDX-License-Identifier: PMPL-1.0-or-later
22
-- Copyright (c) 2026 Jonathan D.A. Jewell (hyperpolymath) <j.d.a.jewell@open.ac.uk>
33
--
4-
-- Levels.idr — The 10 levels of type safety as Idris2 proof types
4+
-- Levels.idr — Progressive type safety levels as Idris2 proof types
55
--
6-
-- Each of the 10 levels from the typed-wasm specification is encoded as
7-
-- a type (a proposition) that can be inhabited (proven) or not. A program
8-
-- that type-checks at level N has a proof witness for that level.
9-
--
10-
-- The levels form a stack: higher levels build on lower ones. Level 10
11-
-- (linearity) implies all of levels 1-9. A "proof certificate" is a
12-
-- product of all 10 level proofs — it is the strongest guarantee that
13-
-- typed-wasm can provide.
6+
-- Each level is encoded as a type (proposition) that can be inhabited
7+
-- (proven) or not. A program that type-checks at level N has a proof
8+
-- witness for that level. The levels form a stack: higher levels build
9+
-- on lower ones. A "proof certificate" is a product of level proofs.
1410
--
1511
-- Level 1: Instruction validity (well-formed syntax)
1612
-- Level 2: Region-binding (field resolves to declared schema)
@@ -22,6 +18,9 @@
2218
-- Level 8: Effect-tracking (Read/Write/Alloc/Free declared)
2319
-- Level 9: Lifetime safety (no use-after-free)
2420
-- Level 10: Linearity (resources used exactly once)
21+
-- Level 11: Tropical cost-tracking (access path cost bounded)
22+
-- Level 12: Epistemic safety (reader knowledge is fresh)
23+
-- Level 13+: Reserved (open-ended framework)
2524

2625
module TypedWasm.ABI.Levels
2726

‎src/abi/TypedWasm/ABI/Tropical.idr‎

Lines changed: 125 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,125 @@
1+
-- SPDX-License-Identifier: PMPL-1.0-or-later
2+
-- Copyright (c) 2026 Jonathan D.A. Jewell (hyperpolymath) <j.d.a.jewell@open.ac.uk>
3+
--
4+
-- Tropical.idr — Level 11: Tropical cost-tracking for memory access
5+
--
6+
-- Every memory access operation carries a cost in a tropical semiring.
7+
-- The min-plus semiring tracks latency (cheapest path), the max-plus
8+
-- semiring tracks throughput (bottleneck path). The type checker proves
9+
-- that any access path through shared memory has bounded total cost.
10+
--
11+
-- This is the "how expensive is this access pattern?" question answered
12+
-- at compile time. It prevents pathological access patterns (e.g. a
13+
-- tight loop doing random access across cache lines) from compiling
14+
-- without an explicit cost annotation acknowledging the expense.
15+
--
16+
-- The tropical semiring algebra is adapted from 007's TropicalSemiring.idr.
17+
18+
module TypedWasm.ABI.Tropical
19+
20+
import TypedWasm.ABI.Region
21+
import TypedWasm.ABI.Levels
22+
23+
%default total
24+
25+
-- ============================================================================
26+
-- Tropical Semiring
27+
-- ============================================================================
28+
29+
||| A tropical semiring value. In the min-plus semiring, addition is min
30+
||| and multiplication is plus. Infinity is the zero element.
31+
public export
32+
data TropCost : Type where
33+
||| Finite cost value (non-negative).
34+
Finite : (cost : Nat) -> TropCost
35+
||| Infinite cost — unreachable or unbounded.
36+
Infinity : TropCost
37+
38+
||| Tropical addition: min of two costs.
39+
public export
40+
tropAdd : TropCost -> TropCost -> TropCost
41+
tropAdd Infinity b = b
42+
tropAdd a Infinity = a
43+
tropAdd (Finite a) (Finite b) = Finite (min a b)
44+
45+
||| Tropical multiplication: sum of two costs (path composition).
46+
public export
47+
tropMul : TropCost -> TropCost -> TropCost
48+
tropMul Infinity _ = Infinity
49+
tropMul _ Infinity = Infinity
50+
tropMul (Finite a) (Finite b) = Finite (a + b)
51+
52+
-- ============================================================================
53+
-- Cost-Annotated Access
54+
-- ============================================================================
55+
56+
||| A memory access operation annotated with its tropical cost.
57+
||| The cost tracks cache-line crossings, alignment penalties, and
58+
||| sequential vs random access patterns.
59+
public export
60+
record CostAnnotatedAccess where
61+
constructor MkCostAccess
62+
||| The accessed field name.
63+
fieldName : String
64+
||| Cost of this individual access (cache lines crossed, alignment penalty).
65+
accessCost : TropCost
66+
||| Whether this access is sequential (stride-1) relative to the previous.
67+
sequential : Bool
68+
69+
||| A path through memory — a sequence of accesses with accumulated cost.
70+
public export
71+
data AccessPath : (totalCost : TropCost) -> Type where
72+
||| Empty path — zero cost.
73+
EmptyPath : AccessPath (Finite 0)
74+
||| Extend a path with one more access — cost accumulates via tropMul.
75+
ExtendPath : (prev : AccessPath prevCost) ->
76+
(access : CostAnnotatedAccess) ->
77+
AccessPath (tropMul prevCost access.accessCost)
78+
79+
-- ============================================================================
80+
-- Cost Bounds
81+
-- ============================================================================
82+
83+
||| Proof that a cost is bounded: `c <= bound`.
84+
public export
85+
data CostBounded : (cost : TropCost) -> (bound : Nat) -> Type where
86+
||| Finite cost within bound.
87+
BoundedFinite : LTE n bound -> CostBounded (Finite n) bound
88+
||| Infinity is never bounded (this constructor is impossible to inhabit).
89+
90+
||| Level 11 proof obligation: the total cost of an access path is bounded.
91+
||| A function that accesses shared memory must prove its access pattern
92+
||| has bounded cost. Without this proof, the access is rejected.
93+
public export
94+
record Level11Proof where
95+
constructor MkLevel11
96+
||| The access path with accumulated cost.
97+
path : AccessPath totalCost
98+
||| The declared cost bound for this function.
99+
bound : Nat
100+
||| Proof that the total cost respects the bound.
101+
bounded : CostBounded totalCost bound
102+
103+
-- ============================================================================
104+
-- Tropical semiring laws (for proof composition)
105+
-- ============================================================================
106+
107+
||| tropAdd is commutative.
108+
export
109+
tropAddComm : (a, b : TropCost) -> tropAdd a b = tropAdd b a
110+
tropAddComm Infinity Infinity = Refl
111+
tropAddComm Infinity (Finite _) = Refl
112+
tropAddComm (Finite _) Infinity = Refl
113+
tropAddComm (Finite a) (Finite b) = cong Finite (minCommutative a b)
114+
115+
||| Infinity is the identity for tropAdd (zero element).
116+
export
117+
tropAddIdentity : (a : TropCost) -> tropAdd a Infinity = a
118+
tropAddIdentity Infinity = Refl
119+
tropAddIdentity (Finite _) = Refl
120+
121+
||| Finite 0 is the identity for tropMul (one element).
122+
export
123+
tropMulIdentity : (a : TropCost) -> tropMul (Finite 0) a = a
124+
tropMulIdentity Infinity = Refl
125+
tropMulIdentity (Finite _) = Refl

0 commit comments

Comments
 (0)