aver_cert/
format.rs

1//! Stable, compiler-independent certificate format declarations.
2//!
3//! The producer imports this module from `aver-cert`; there is intentionally
4//! no separate format crate. The verifier is the authority for this surface,
5//! and the compiler depends on it in the non-trust-bearing direction.
6
7/// Public certificate-package layout understood by this verifier.
8pub const FORMAT_VERSION: u32 = 1;
9
10/// Manifest schema accepted by the standalone verifier. Version 2 made the
11/// subject's `hostRoleTable` optional: modules without the Int box helper
12/// declare `null`, pinned against a byte-derived proof of the helper's
13/// absence, while modules with the helper pin the exact decoded table. A
14/// module whose role scan the decoder cannot complete matches no manifest
15/// value. The declared arith helper indices (carrier, limb, and the
16/// decompose/normalize/strip/umagCmp sub-routines) are proof-term data in the
17/// generated Lean certificate, not public JSON, so the acceptance pin can
18/// confirm each declared add/sub/mul helper body byte-for-byte without moving
19/// the public schema.
20pub const CERT_SCHEMA_VERSION: u32 = 2;
21
22/// Named theorem audited by the checker-owned witness.
23pub const ARTIFACT_CERTIFICATE_ROOT: &str = "AverCert.Artifact.certificate";
24
25/// Identity of the exact checker-owned Lean wall shipped by this release.
26pub const CURRENT_WALL_ID: &str =
27    "sha256:d34b2bb4ac4f86ba722649651560758c85484c84524bfdaf4e7b222335b10722";
28
29/// Complete host-import surface admitted by the wasm-gc certificate format.
30///
31/// This list is verifier-owned. `aver-lang` tests its `EffectName` lowering
32/// against it, so adding a compiler import cannot silently broaden what the
33/// independent verifier accepts.
34pub const WASM_GC_CAPABILITIES: &[(&str, &str)] = &[
35    ("aver", "console_print"),
36    ("aver", "console_error"),
37    ("aver", "console_warn"),
38    ("aver", "time_unix_ms"),
39    ("aver", "request_method"),
40    ("aver", "request_url"),
41    ("aver", "request_query"),
42    ("aver", "request_body"),
43    ("aver", "request_headers_load"),
44    ("aver", "response_text"),
45    ("aver", "response_set_header"),
46    ("aver", "http_send"),
47    ("aver", "http_add_request_header"),
48    ("aver", "http_clear_request_headers"),
49    ("aver", "env_get"),
50    ("aver", "env_set"),
51    ("aver", "console_read_line"),
52    ("aver", "args_len"),
53    ("aver", "args_get"),
54    ("aver", "random_float"),
55    ("aver", "random_int"),
56    ("aver", "time_sleep"),
57    ("aver", "time_now"),
58    ("aver", "float_sin"),
59    ("aver", "float_cos"),
60    ("aver", "float_atan2"),
61    ("aver", "float_pow"),
62    ("aver", "terminal_enable_raw_mode"),
63    ("aver", "terminal_disable_raw_mode"),
64    ("aver", "terminal_clear"),
65    ("aver", "terminal_move_to"),
66    ("aver", "terminal_print"),
67    ("aver", "terminal_set_color"),
68    ("aver", "terminal_reset_color"),
69    ("aver", "terminal_read_key"),
70    ("aver", "terminal_size"),
71    ("aver", "terminal_hide_cursor"),
72    ("aver", "terminal_show_cursor"),
73    ("aver", "terminal_flush"),
74    ("aver", "disk_read_text"),
75    ("aver", "disk_write_text"),
76    ("aver", "disk_append_text"),
77    ("aver", "disk_exists"),
78    ("aver", "disk_delete"),
79    ("aver", "disk_delete_dir"),
80    ("aver", "disk_list_dir"),
81    ("aver", "disk_make_dir"),
82    ("aver", "tcp_connect"),
83    ("aver", "tcp_write_line"),
84    ("aver", "tcp_read_line"),
85    ("aver", "tcp_close"),
86    ("aver", "tcp_send"),
87    ("aver", "tcp_ping"),
88    ("aver", "http_get"),
89    ("aver", "http_head"),
90    ("aver", "http_delete"),
91    ("aver", "http_post"),
92    ("aver", "http_put"),
93    ("aver", "http_patch"),
94    ("aver", "record_enter_group"),
95    ("aver", "record_set_branch"),
96    ("aver", "record_exit_group"),
97];
98
99#[cfg(test)]
100mod tests {
101    use super::*;
102
103    #[test]
104    fn capability_pairs_are_unique() {
105        let unique = WASM_GC_CAPABILITIES
106            .iter()
107            .copied()
108            .collect::<std::collections::BTreeSet<_>>();
109        assert_eq!(unique.len(), WASM_GC_CAPABILITIES.len());
110    }
111}
aver_cert/format.rs

aver_cert/
format.rs
