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

aver_cert/
wall.rs
