Skip to content

Commit 6249995

Browse files
hyperpolymathclaude
hyperpolymath
and
claude
committed
feat(abi): T5a access-typing spec-of-record + verifier↔spec agreement (the bound, named)
Lift the Tier-2 access-typing obligation into the Idris spec-of-record, mirroring VerifierSpec.idr's TrustedFixture design but for per-site access typing and grounded in PackedLayout (T4): field widths come from packedScalarSize, so the spec's offset/extent arithmetic IS the packed layout the producer emits. The determine-vs-bound asymmetry is made explicit (per the owner's cut-calculus framing): - SiteWellTyped / AccessTypingClean — the DETERMINABLE side: op matches the field's type+width (opMatchesField, transliterating Rust mem_op_matches_field; loads sign-sensitive, stores sign-collapsed), offset = packed field offset, extent in-region. Fixed by the schema; holds by construction. - TypedAccessFixture — the BOUNDABLE side: constructing one assumes the Rust pass decoded the operator stream faithfully (decode-faithfulness = the SoundWarrant / ADR-0005 analogue). The spec can't see the bytes, so this is named as the trust-injection, not proven. Grep MkTypedAccessFixture. typedVerifierIsSound / typedVerifierIsComplete are total by case analysis — the trust budget lives entirely inside any TypedAccessFixture the input carried. This is the verifier↔spec link for the Tier-2 obligation with the bound named crisply, rather than pretended to be an equality. idris2 --build: exit 0, 24 modules; no believe_me/postulate/sorry/assert_total; %default total; no new warnings. Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com>
1 parent 4d017b6 commit 6249995

2 files changed

Lines changed: 244 additions & 0 deletions

File tree

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

Lines changed: 243 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,243 @@
1+
-- SPDX-License-Identifier: MPL-2.0
2+
-- Copyright (c) 2026 Jonathan D.A. Jewell <j.d.a.jewell@open.ac.uk>
3+
--
4+
-- src/abi/TypedWasm/ABI/AccessTypingSpec.idr
5+
--
6+
-- T5a (verifier↔spec link) for the Tier-2 access-TYPING obligation.
7+
--
8+
-- This is the spec-of-record for what the Rust
9+
-- `verify_access_typing_from_module` pass (typed-wasm-verify) establishes
10+
-- when it returns a clean `AccessTypingReport` (errors = []). It mirrors
11+
-- `VerifierSpec.idr`'s TrustedFixture design, but for per-site access
12+
-- typing rather than L7/L10 ownership, and it is grounded in
13+
-- `PackedLayout.idr` (T4): field widths come from `packedScalarSize`, so
14+
-- the spec's offset/extent arithmetic IS the layout the producer emits.
15+
--
16+
-- The determine-vs-bound asymmetry made explicit:
17+
--
18+
-- * `SiteWellTyped` (the spec predicate) is the DETERMINABLE side — it
19+
-- is fixed entirely by the schema and the emitted op (type, width,
20+
-- offset, in-region), exactly what `mem_op_matches_field` +
21+
-- `field_byte_offset` + the region-bounds check decide in Rust. The
22+
-- equality holds by construction.
23+
-- * `TypedAccessFixture` (the trust-injection) is the BOUNDABLE side —
24+
-- constructing one ASSUMES the Rust pass faithfully decoded the
25+
-- module's operator stream (the decode-faithfulness hypothesis; the
26+
-- `SoundWarrant` / ADR-0005 analogue). The Idris spec cannot see the
27+
-- wasm bytes, so this is named here as a trust-injection, not proven.
28+
-- Grep `MkTypedAccessFixture` to enumerate every such injection.
29+
--
30+
-- The agreement lemmas below are TOTAL by case analysis: the trust budget
31+
-- lives entirely inside any `TypedAccessFixture` the input carried, spent
32+
-- at the site that constructed it.
33+
--
34+
-- NO `believe_me`, NO `assert_total`, NO `postulate`, NO `sorry`,
35+
-- NO `assert_smaller`. `%default total`.
36+
37+
module TypedWasm.ABI.AccessTypingSpec
38+
39+
import TypedWasm.ABI.Region
40+
import TypedWasm.ABI.PackedLayout
41+
import Data.Nat
42+
import Data.List
43+
import Data.List.Quantifiers
44+
45+
%default total
46+
47+
-- ============================================================================
48+
-- Field classification (width + int/float + signedness)
49+
-- ============================================================================
50+
51+
||| The storage class of a scalar field: an integer of a given byte width
52+
||| and signedness, or a float of a given byte width. `WBool` classifies
53+
||| as a 1-byte unsigned integer (packed-region storage; see PackedLayout).
54+
public export
55+
data FieldClass : Type where
56+
IntF : (bytes : Nat) -> (signed : Bool) -> FieldClass
57+
FloatF : (bytes : Nat) -> FieldClass
58+
59+
public export
60+
fieldClass : WasmType -> FieldClass
61+
fieldClass U8 = IntF 1 False
62+
fieldClass U16 = IntF 2 False
63+
fieldClass U32 = IntF 4 False
64+
fieldClass U64 = IntF 8 False
65+
fieldClass I8 = IntF 1 True
66+
fieldClass I16 = IntF 2 True
67+
fieldClass I32 = IntF 4 True
68+
fieldClass I64 = IntF 8 True
69+
fieldClass F32 = FloatF 4
70+
fieldClass F64 = FloatF 8
71+
fieldClass WBool = IntF 1 False
72+
73+
-- ============================================================================
74+
-- Spec-level memory ops (mirrors typed-wasm-verify `MemOp`)
75+
-- ============================================================================
76+
77+
||| The classification of the memory op the verifier decodes at a pinned
78+
||| site. Loads carry signedness (wasm `load8_s` vs `load8_u`); stores
79+
||| collapse it (only `store8` / `store16` exist) — exactly the asymmetry
80+
||| in the Rust `mem_op_matches_field`.
81+
public export
82+
data OpClass : Type where
83+
IntLoad : (bytes : Nat) -> (signed : Bool) -> OpClass
84+
IntStore : (bytes : Nat) -> OpClass
85+
FloatLoad : (bytes : Nat) -> OpClass
86+
FloatStore : (bytes : Nat) -> OpClass
87+
88+
||| Does the decoded op legitimately load OR store a field of type `ty`?
89+
||| A load must match width AND signedness; a store must match width only
90+
||| (sign-agnostic). Floats match width. Transliteration of the Rust
91+
||| `mem_op_matches_field`.
92+
public export
93+
opMatchesField : OpClass -> WasmType -> Bool
94+
opMatchesField (IntLoad b s) ty =
95+
case fieldClass ty of
96+
IntF b' s' => b == b' && s == s'
97+
FloatF _ => False
98+
opMatchesField (IntStore b) ty =
99+
case fieldClass ty of
100+
IntF b' _ => b == b'
101+
FloatF _ => False
102+
opMatchesField (FloatLoad b) ty =
103+
case fieldClass ty of
104+
FloatF b' => b == b'
105+
IntF _ _ => False
106+
opMatchesField (FloatStore b) ty =
107+
case fieldClass ty of
108+
FloatF b' => b == b'
109+
IntF _ _ => False
110+
111+
-- ============================================================================
112+
-- Spec access site
113+
-- ============================================================================
114+
115+
||| A pinned access site, projected to the facts the typing check decides.
116+
||| `siteFieldOff` is the field's PACKED byte offset (computed by
117+
||| `PackedLayout.packedOffsetsFrom` on the Rust side, = `resolve_field`);
118+
||| `siteRegionSz` is the region's `packedSize`. Bundling these projected
119+
||| facts keeps the predicate independent of how the schema was walked.
120+
public export
121+
record SpecSite where
122+
constructor MkSpecSite
123+
siteOp : OpClass -- the op decoded at the pinned instruction index
124+
siteOffset : Nat -- the op's static memarg offset
125+
siteField : WasmType -- the declared type of the field it reaches
126+
siteFieldOff : Nat -- the field's packed byte offset (PackedLayout)
127+
siteRegionSz : Nat -- the region's packed byte size (PackedLayout)
128+
129+
-- ============================================================================
130+
-- The spec predicate: a site is well-typed
131+
-- ============================================================================
132+
133+
||| `SiteWellTyped s` holds when, exactly as the Rust pass decides:
134+
||| (1) the decoded op is a load/store of the field's type & width,
135+
||| (2) its static offset equals the field's packed byte offset, and
136+
||| (3) the field's extent `[off, off + width)` stays within the region.
137+
||| The width is `packedScalarSize (siteField s)` — the SAME size T4's
138+
||| PackedLayout assigns — so this predicate is grounded in the canonical
139+
||| packed layout, not a fresh notion.
140+
public export
141+
data SiteWellTyped : SpecSite -> Type where
142+
MkSiteWellTyped :
143+
(opMatchesField (siteOp s) (siteField s) = True)
144+
-> (siteOffset s = siteFieldOff s)
145+
-> LTE (siteFieldOff s + packedScalarSize (siteField s)) (siteRegionSz s)
146+
-> SiteWellTyped s
147+
148+
||| The spec-of-record acceptance criterion for the access-typing pass:
149+
||| EVERY pinned site is well-typed (the Rust `errors = []` condition).
150+
public export
151+
AccessTypingClean : List SpecSite -> Type
152+
AccessTypingClean = All SiteWellTyped
153+
154+
-- A pinned site that is well-typed really does carry the op/field match
155+
-- (a projection showing the predicate has content, not just shape).
156+
export
157+
wellTypedMatches : SiteWellTyped s -> opMatchesField (siteOp s) (siteField s) = True
158+
wellTypedMatches (MkSiteWellTyped m _ _) = m
159+
160+
-- ...and its offset really equals the packed field offset.
161+
export
162+
wellTypedOffsetExact : SiteWellTyped s -> siteOffset s = siteFieldOff s
163+
wellTypedOffsetExact (MkSiteWellTyped _ o _) = o
164+
165+
-- ============================================================================
166+
-- Trusted fixture — the access-typing trust-injection (the BOUND)
167+
-- ============================================================================
168+
169+
||| Packages a clean verdict from the Rust `verify_access_typing_from_module`
170+
||| pass: a name/id plus the structural witness that every site is
171+
||| well-typed. CONSTRUCTING this is the trust-injection moment — it
172+
||| assumes the Rust pass decoded the operator stream faithfully (the
173+
||| decode-faithfulness hypothesis; the determine-vs-bound BOUND). Grep
174+
||| `MkTypedAccessFixture` to enumerate access-typing trust injections.
175+
public export
176+
record TypedAccessFixture (sites : List SpecSite) where
177+
constructor MkTypedAccessFixture
178+
tafName : String
179+
tafId : Nat
180+
tafWitness : AccessTypingClean sites
181+
182+
-- ============================================================================
183+
-- Spec / verifier acceptance (mirrors VerifierSpec)
184+
-- ============================================================================
185+
186+
||| The spec's access-typing acceptance: exactly the structural witness.
187+
public export
188+
data TypedSpecAccepts : List SpecSite -> Type where
189+
MkTypedSpecAccepts : AccessTypingClean sites -> TypedSpecAccepts sites
190+
191+
||| Verifier acceptance for access typing.
192+
||| * `TVAStructural` — acceptance from the same structural predicate the
193+
||| spec uses; no external trust.
194+
||| * `TVADifferential` — acceptance attested by the Rust pass via a
195+
||| `TypedAccessFixture`; the trust-injection is its construction.
196+
public export
197+
data TypedVerifierAccepts : List SpecSite -> Type where
198+
TVAStructural : AccessTypingClean sites -> TypedVerifierAccepts sites
199+
TVADifferential : TypedAccessFixture sites -> TypedVerifierAccepts sites
200+
201+
||| Smart constructor: verifier acceptance from a clean Rust verdict.
202+
public export
203+
typedAccessAttested :
204+
(name : String) -> (fid : Nat)
205+
-> AccessTypingClean sites
206+
-> TypedVerifierAccepts sites
207+
typedAccessAttested name fid w = TVADifferential (MkTypedAccessFixture name fid w)
208+
209+
||| Project a fixture into the spec via its wrapped witness.
210+
public export
211+
typedTrustedToSpec : TypedAccessFixture sites -> TypedSpecAccepts sites
212+
typedTrustedToSpec (MkTypedAccessFixture _ _ w) = MkTypedSpecAccepts w
213+
214+
-- ============================================================================
215+
-- The agreement lemmas (total by case analysis)
216+
-- ============================================================================
217+
218+
||| Soundness: if the Rust access-typing pass accepts a site list, the
219+
||| Idris spec accepts it too. Total. The differential case surfaces the
220+
||| structural witness the Rust pass attested.
221+
export
222+
typedVerifierIsSound :
223+
(sites : List SpecSite)
224+
-> TypedVerifierAccepts sites
225+
-> TypedSpecAccepts sites
226+
typedVerifierIsSound _ (TVAStructural w) = MkTypedSpecAccepts w
227+
typedVerifierIsSound _ (TVADifferential (MkTypedAccessFixture _ _ w)) =
228+
MkTypedSpecAccepts w
229+
230+
||| Completeness: if the spec accepts, the verifier accepts (structurally,
231+
||| no trust required). Total.
232+
export
233+
typedVerifierIsComplete :
234+
(sites : List SpecSite)
235+
-> TypedSpecAccepts sites
236+
-> TypedVerifierAccepts sites
237+
typedVerifierIsComplete _ (MkTypedSpecAccepts w) = TVAStructural w
238+
239+
||| Spec acceptance really delivers the per-site witnesses (content, not
240+
||| just shape): the cleanness predicate is the full `All` witness.
241+
export
242+
specAcceptsWitness : TypedSpecAccepts sites -> AccessTypingClean sites
243+
specAcceptsWitness (MkTypedSpecAccepts w) = w

‎src/abi/typed-wasm.ipkg‎

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -25,6 +25,7 @@ modules = TypedWasm.ABI.Region
2525
, TypedWasm.ABI.Epistemic
2626
, TypedWasm.ABI.Layout
2727
, TypedWasm.ABI.PackedLayout
28+
, TypedWasm.ABI.AccessTypingSpec
2829
, TypedWasm.ABI.Proofs
2930
, TypedWasm.ABI.VerifierSpec
3031
-- Cross-language layout contracts (aggregate library role, ADR-004).

0 commit comments

Comments
 (0)