aver_cert/
wall.rs

1//! Checker-owned Lean soundness wall.
2//!
3//! These sources are artifact-independent and embedded in the verifier. A
4//! certificate names the exact set through [`current_id`]; it never chooses a
5//! path, URL, or ambient installation from which the verifier loads code.
6
7use sha2::{Digest, Sha256};
8use std::sync::OnceLock;
9
10pub use crate::format::{CURRENT_WALL_ID as CURRENT_ID, FORMAT_VERSION};
11
12pub const LEAN_TOOLCHAIN: &str = include_str!("../assets/wall/current/lean-toolchain");
13
14pub const CERT_PRELUDE: &str = include_str!("../assets/wall/current/CertPrelude.lean");
15pub const CERT_DECODE: &str = include_str!("../assets/wall/current/CertDecode.lean");
16pub const CERT_SCHEMA: &str = include_str!("../assets/wall/current/Schema.lean");
17pub const CERT_SCHEMA_CORE: &str = include_str!("../assets/wall/current/SchemaCore.lean");
18pub const CERT_PLAN_CHECK: &str = include_str!("../assets/wall/current/PlanCheck.lean");
19pub const CERT_PLAN_LOWER: &str = include_str!("../assets/wall/current/PlanLower.lean");
20pub const CERT_PLAN_BYTES: &str = include_str!("../assets/wall/current/PlanBytes.lean");
21pub const CERT_WASM_SLICE: &str = include_str!("../assets/wall/current/WasmSlice.lean");
22pub const CERT_EXPR_FRAGMENT_ACCEPTED: &str =
23    include_str!("../assets/wall/current/ExprFragmentAccepted.lean");
24pub const CERT_ACCEPTED_ARTIFACT: &str =
25    include_str!("../assets/wall/current/AcceptedArtifact.lean");
26pub const CERT_ACCEPTED_ARTIFACT_CORE: &str =
27    include_str!("../assets/wall/current/AcceptedArtifactCore.lean");
28pub const CERT_CLAIM_AXES: &str = include_str!("../assets/wall/current/ClaimAxes.lean");
29pub const CERT_EXPR_FRAGMENT_SEMANTICS: &str =
30    include_str!("../assets/wall/current/ExprFragmentSemantics.lean");
31pub const CERT_INTERPRETER_SEQUENCING: &str =
32    include_str!("../assets/wall/current/InterpreterSequencing.lean");
33pub const CERT_EXPR_FRAGMENT_SOUNDNESS: &str =
34    include_str!("../assets/wall/current/ExprFragmentSoundness.lean");
35pub const CERT_FIELD_PROJECTION_SOUNDNESS: &str =
36    include_str!("../assets/wall/current/FieldProjectionSoundness.lean");
37pub const CERT_CONSTRUCT_VERBATIM_SOUNDNESS: &str =
38    include_str!("../assets/wall/current/ConstructVerbatimSoundness.lean");
39pub const CERT_INT_DISPATCH_SOUNDNESS: &str =
40    include_str!("../assets/wall/current/IntDispatchSoundness.lean");
41pub const CERT_ENVELOPE_LOWERING: &str =
42    include_str!("../assets/wall/current/EnvelopeLowering.lean");
43pub const CERT_WIDENED_ENVELOPE: &str = include_str!("../assets/wall/current/WidenedEnvelope.lean");
44pub const CERT_DECLARED_INDEX_ENVELOPE: &str =
45    include_str!("../assets/wall/current/DeclaredIndexEnvelope.lean");
46pub const CERT_DECLARED_ENVELOPE_ACCEPT_TRANSPORT: &str =
47    include_str!("../assets/wall/current/DeclaredEnvelopeAcceptTransport.lean");
48pub const CERT_STRING_SOUNDNESS: &str = include_str!("../assets/wall/current/StringSoundness.lean");
49pub const CERT_STANDARD_FACE: &str = include_str!("../assets/wall/current/StandardFace.lean");
50pub const CERT_RECURSION_SOUNDNESS: &str =
51    include_str!("../assets/wall/current/RecursionSoundness.lean");
52pub const CERT_MUTUAL_RECURSION_SOUNDNESS: &str =
53    include_str!("../assets/wall/current/MutualRecursionSoundness.lean");
54pub const CERT_COMPOSITION_SOUNDNESS: &str =
55    include_str!("../assets/wall/current/CompositionSoundness.lean");
56pub const CERT_ACCEPTANCE_SOUNDNESS_CORE: &str =
57    include_str!("../assets/wall/current/AcceptanceSoundnessCore.lean");
58pub const CERT_DISCHARGE_EXPR_FRAGMENT: &str =
59    include_str!("../assets/wall/current/DischargeExprFragment.lean");
60pub const CERT_DISCHARGE_FIELD_PROJECTION: &str =
61    include_str!("../assets/wall/current/DischargeFieldProjection.lean");
62pub const CERT_DISCHARGE_CONSTRUCT: &str =
63    include_str!("../assets/wall/current/DischargeConstruct.lean");
64pub const CERT_DISCHARGE_VERBATIM: &str =
65    include_str!("../assets/wall/current/DischargeVerbatim.lean");
66pub const CERT_DISCHARGE_STRING: &str = include_str!("../assets/wall/current/DischargeString.lean");
67pub const CERT_DISCHARGE_INT_DISPATCH: &str =
68    include_str!("../assets/wall/current/DischargeIntDispatch.lean");
69pub const CERT_DISCHARGE_RECURSION: &str =
70    include_str!("../assets/wall/current/DischargeRecursion.lean");
71pub const CERT_DISCHARGE_COMPOSITION: &str =
72    include_str!("../assets/wall/current/DischargeComposition.lean");
73pub const CERT_ACCEPTANCE_SOUNDNESS: &str =
74    include_str!("../assets/wall/current/AcceptanceSoundness.lean");
75pub const CERT_ARITH_TEMPLATE_DERISK: &str =
76    include_str!("../assets/wall/current/ArithTemplateDerisk.lean");
77
78#[derive(Clone, Copy, Debug, Eq, PartialEq)]
79pub struct Source {
80    pub name: &'static str,
81    pub contents: &'static str,
82}
83
84/// Exact checker-owned source set. Ordering is not part of the identity:
85/// [`compute_id`] sorts by filename before hashing.
86pub const SOURCES: [Source; 38] = [
87    Source {
88        name: "AcceptedArtifact.lean",
89        contents: CERT_ACCEPTED_ARTIFACT,
90    },
91    Source {
92        name: "ArithTemplateDerisk.lean",
93        contents: CERT_ARITH_TEMPLATE_DERISK,
94    },
95    Source {
96        name: "AcceptedArtifactCore.lean",
97        contents: CERT_ACCEPTED_ARTIFACT_CORE,
98    },
99    Source {
100        name: "AcceptanceSoundness.lean",
101        contents: CERT_ACCEPTANCE_SOUNDNESS,
102    },
103    Source {
104        name: "AcceptanceSoundnessCore.lean",
105        contents: CERT_ACCEPTANCE_SOUNDNESS_CORE,
106    },
107    Source {
108        name: "CertDecode.lean",
109        contents: CERT_DECODE,
110    },
111    Source {
112        name: "CertPrelude.lean",
113        contents: CERT_PRELUDE,
114    },
115    Source {
116        name: "ClaimAxes.lean",
117        contents: CERT_CLAIM_AXES,
118    },
119    Source {
120        name: "CompositionSoundness.lean",
121        contents: CERT_COMPOSITION_SOUNDNESS,
122    },
123    Source {
124        name: "ConstructVerbatimSoundness.lean",
125        contents: CERT_CONSTRUCT_VERBATIM_SOUNDNESS,
126    },
127    Source {
128        name: "DeclaredEnvelopeAcceptTransport.lean",
129        contents: CERT_DECLARED_ENVELOPE_ACCEPT_TRANSPORT,
130    },
131    Source {
132        name: "DeclaredIndexEnvelope.lean",
133        contents: CERT_DECLARED_INDEX_ENVELOPE,
134    },
135    Source {
136        name: "DischargeComposition.lean",
137        contents: CERT_DISCHARGE_COMPOSITION,
138    },
139    Source {
140        name: "DischargeConstruct.lean",
141        contents: CERT_DISCHARGE_CONSTRUCT,
142    },
143    Source {
144        name: "DischargeExprFragment.lean",
145        contents: CERT_DISCHARGE_EXPR_FRAGMENT,
146    },
147    Source {
148        name: "DischargeFieldProjection.lean",
149        contents: CERT_DISCHARGE_FIELD_PROJECTION,
150    },
151    Source {
152        name: "DischargeIntDispatch.lean",
153        contents: CERT_DISCHARGE_INT_DISPATCH,
154    },
155    Source {
156        name: "DischargeRecursion.lean",
157        contents: CERT_DISCHARGE_RECURSION,
158    },
159    Source {
160        name: "DischargeString.lean",
161        contents: CERT_DISCHARGE_STRING,
162    },
163    Source {
164        name: "DischargeVerbatim.lean",
165        contents: CERT_DISCHARGE_VERBATIM,
166    },
167    Source {
168        name: "EnvelopeLowering.lean",
169        contents: CERT_ENVELOPE_LOWERING,
170    },
171    Source {
172        name: "ExprFragmentAccepted.lean",
173        contents: CERT_EXPR_FRAGMENT_ACCEPTED,
174    },
175    Source {
176        name: "ExprFragmentSemantics.lean",
177        contents: CERT_EXPR_FRAGMENT_SEMANTICS,
178    },
179    Source {
180        name: "ExprFragmentSoundness.lean",
181        contents: CERT_EXPR_FRAGMENT_SOUNDNESS,
182    },
183    Source {
184        name: "FieldProjectionSoundness.lean",
185        contents: CERT_FIELD_PROJECTION_SOUNDNESS,
186    },
187    Source {
188        name: "IntDispatchSoundness.lean",
189        contents: CERT_INT_DISPATCH_SOUNDNESS,
190    },
191    Source {
192        name: "InterpreterSequencing.lean",
193        contents: CERT_INTERPRETER_SEQUENCING,
194    },
195    Source {
196        name: "MutualRecursionSoundness.lean",
197        contents: CERT_MUTUAL_RECURSION_SOUNDNESS,
198    },
199    Source {
200        name: "PlanBytes.lean",
201        contents: CERT_PLAN_BYTES,
202    },
203    Source {
204        name: "PlanCheck.lean",
205        contents: CERT_PLAN_CHECK,
206    },
207    Source {
208        name: "PlanLower.lean",
209        contents: CERT_PLAN_LOWER,
210    },
211    Source {
212        name: "RecursionSoundness.lean",
213        contents: CERT_RECURSION_SOUNDNESS,
214    },
215    Source {
216        name: "Schema.lean",
217        contents: CERT_SCHEMA,
218    },
219    Source {
220        name: "SchemaCore.lean",
221        contents: CERT_SCHEMA_CORE,
222    },
223    Source {
224        name: "StandardFace.lean",
225        contents: CERT_STANDARD_FACE,
226    },
227    Source {
228        name: "StringSoundness.lean",
229        contents: CERT_STRING_SOUNDNESS,
230    },
231    Source {
232        name: "WasmSlice.lean",
233        contents: CERT_WASM_SLICE,
234    },
235    Source {
236        name: "WidenedEnvelope.lean",
237        contents: CERT_WIDENED_ENVELOPE,
238    },
239];
240
241/// Roots whose complete import graph is artifact-independent and can therefore
242/// be cached before a certificate is seen.
243pub const PRISTINE_ROOTS: [&str; 36] = [
244    "CertPrelude",
245    "CertDecode",
246    "ArithTemplateDerisk",
247    "WasmSlice",
248    "SchemaCore",
249    "PlanCheck",
250    "PlanLower",
251    "PlanBytes",
252    "ExprFragmentAccepted",
253    "AcceptedArtifactCore",
254    "ClaimAxes",
255    "ExprFragmentSemantics",
256    "InterpreterSequencing",
257    "ExprFragmentSoundness",
258    "FieldProjectionSoundness",
259    "ConstructVerbatimSoundness",
260    "IntDispatchSoundness",
261    "StringSoundness",
262    "EnvelopeLowering",
263    "WidenedEnvelope",
264    "DeclaredIndexEnvelope",
265    "DeclaredEnvelopeAcceptTransport",
266    "StandardFace",
267    "RecursionSoundness",
268    "MutualRecursionSoundness",
269    "CompositionSoundness",
270    "AcceptanceSoundnessCore",
271    "DischargeExprFragment",
272    "DischargeFieldProjection",
273    "DischargeConstruct",
274    "DischargeVerbatim",
275    "DischargeString",
276    "DischargeIntDispatch",
277    "DischargeRecursion",
278    "DischargeComposition",
279    "AcceptanceSoundness",
280];
281
282#[derive(Debug)]
283pub struct Wall {
284    pub sources: &'static [Source],
285    pub pristine_roots: &'static [&'static str],
286    pub toolchain: &'static str,
287}
288
289pub static CURRENT: Wall = Wall {
290    sources: &SOURCES,
291    pristine_roots: &PRISTINE_ROOTS,
292    toolchain: LEAN_TOOLCHAIN,
293};
294
295/// Domain-separated digest of sorted, length-framed filenames and exact bytes.
296/// The exact Lean toolchain is part of the wall identity as a synthetic file.
297fn compute_id() -> String {
298    let mut files = SOURCES
299        .iter()
300        .map(|source| (source.name, source.contents.as_bytes()))
301        .chain(std::iter::once((
302            "lean-toolchain",
303            LEAN_TOOLCHAIN.as_bytes(),
304        )))
305        .collect::<Vec<_>>();
306    files.sort_unstable_by_key(|(name, _)| *name);
307
308    let mut hash = Sha256::new();
309    hash.update(b"aver-certificate-wall\0v1\0");
310    hash.update((files.len() as u64).to_be_bytes());
311    for (name, contents) in files {
312        hash.update((name.len() as u64).to_be_bytes());
313        hash.update(name.as_bytes());
314        hash.update((contents.len() as u64).to_be_bytes());
315        hash.update(contents);
316    }
317    format!("sha256:{:x}", hash.finalize())
318}
319
320/// Identity of the one wall embedded in this pre-public verifier.
321pub fn current_id() -> &'static str {
322    static VERIFIED: OnceLock<()> = OnceLock::new();
323    VERIFIED.get_or_init(|| {
324        assert_eq!(
325            compute_id(),
326            CURRENT_ID,
327            "embedded certificate wall changed without updating CURRENT_ID"
328        );
329    });
330    CURRENT_ID
331}
332
333/// Resolve only checker-embedded, byte-exact walls. There is intentionally no
334/// filesystem, environment, or network fallback.
335pub fn resolve(id: &str) -> Option<&'static Wall> {
336    (id == current_id()).then_some(&CURRENT)
337}
338
339/// Checker-authored Lean module containing the exact artifact bytes. A
340/// certificate package never supplies this module; production verification
341/// and direct-Lake test harnesses materialize it from the `.wasm` under test.
342pub fn render_artifact_bytes(bytes: &[u8]) -> String {
343    let numeral = if bytes.is_empty() {
344        "0".to_string()
345    } else {
346        let mut numeral = String::with_capacity(2 + bytes.len() * 2);
347        numeral.push_str("0x");
348        for byte in bytes.iter().rev() {
349            numeral.push_str(&format!("{byte:02x}"));
350        }
351        numeral
352    };
353    format!(
354        "import WasmSlice\n\nset_option maxRecDepth 200000\n\nnamespace AverCert.ArtifactBytes\n\ndef modBytes : Nat := {numeral}\ndef modLen : Nat := {}\n\nend AverCert.ArtifactBytes\n",
355        bytes.len()
356    )
357}
358
359#[cfg(test)]
360mod tests {
361    use super::*;
362
363    #[test]
364    fn wall_sources_have_unique_plain_filenames() {
365        let mut names = SOURCES.iter().map(|source| source.name).collect::<Vec<_>>();
366        names.sort_unstable();
367        names.dedup();
368        assert_eq!(names.len(), SOURCES.len());
369        assert!(
370            names
371                .iter()
372                .all(|name| name.ends_with(".lean") && !name.contains('/'))
373        );
374    }
375
376    #[test]
377    fn current_wall_resolves_only_by_exact_id() {
378        assert_eq!(compute_id(), CURRENT_ID);
379        assert!(std::ptr::eq(resolve(current_id()).unwrap(), &CURRENT));
380        assert!(resolve("sha256:deadbeef").is_none());
381    }
382}
aver_cert/wall.rs

aver_cert/
wall.rs
