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/// First public schema accepted by the standalone verifier.
11pub const CERT_SCHEMA_VERSION: u32 = 1;
12
13/// Named theorem audited by the checker-owned witness.
14pub const ARTIFACT_CERTIFICATE_ROOT: &str = "AverCert.Artifact.certificate";
15
16/// Identity of the exact checker-owned Lean wall shipped by this release.
17pub const CURRENT_WALL_ID: &str =
18    "sha256:a362a446db77142750423abaae80eafeffd040fa0b8f7b57fb53fac60b22eea6";
19
20/// Complete host-import surface admitted by the wasm-gc certificate format.
21///
22/// This list is verifier-owned. `aver-lang` tests its `EffectName` lowering
23/// against it, so adding a compiler import cannot silently broaden what the
24/// independent verifier accepts.
25pub const WASM_GC_CAPABILITIES: &[(&str, &str)] = &[
26    ("aver", "console_print"),
27    ("aver", "console_error"),
28    ("aver", "console_warn"),
29    ("aver", "time_unix_ms"),
30    ("aver", "request_method"),
31    ("aver", "request_url"),
32    ("aver", "request_query"),
33    ("aver", "request_body"),
34    ("aver", "request_headers_load"),
35    ("aver", "response_text"),
36    ("aver", "response_set_header"),
37    ("aver", "http_send"),
38    ("aver", "http_add_request_header"),
39    ("aver", "http_clear_request_headers"),
40    ("aver", "env_get"),
41    ("aver", "env_set"),
42    ("aver", "console_read_line"),
43    ("aver", "args_len"),
44    ("aver", "args_get"),
45    ("aver", "random_float"),
46    ("aver", "random_int"),
47    ("aver", "time_sleep"),
48    ("aver", "time_now"),
49    ("aver", "float_sin"),
50    ("aver", "float_cos"),
51    ("aver", "float_atan2"),
52    ("aver", "float_pow"),
53    ("aver", "terminal_enable_raw_mode"),
54    ("aver", "terminal_disable_raw_mode"),
55    ("aver", "terminal_clear"),
56    ("aver", "terminal_move_to"),
57    ("aver", "terminal_print"),
58    ("aver", "terminal_set_color"),
59    ("aver", "terminal_reset_color"),
60    ("aver", "terminal_read_key"),
61    ("aver", "terminal_size"),
62    ("aver", "terminal_hide_cursor"),
63    ("aver", "terminal_show_cursor"),
64    ("aver", "terminal_flush"),
65    ("aver", "disk_read_text"),
66    ("aver", "disk_write_text"),
67    ("aver", "disk_append_text"),
68    ("aver", "disk_exists"),
69    ("aver", "disk_delete"),
70    ("aver", "disk_delete_dir"),
71    ("aver", "disk_list_dir"),
72    ("aver", "disk_make_dir"),
73    ("aver", "tcp_connect"),
74    ("aver", "tcp_write_line"),
75    ("aver", "tcp_read_line"),
76    ("aver", "tcp_close"),
77    ("aver", "tcp_send"),
78    ("aver", "tcp_ping"),
79    ("aver", "http_get"),
80    ("aver", "http_head"),
81    ("aver", "http_delete"),
82    ("aver", "http_post"),
83    ("aver", "http_put"),
84    ("aver", "http_patch"),
85    ("aver", "record_enter_group"),
86    ("aver", "record_set_branch"),
87    ("aver", "record_exit_group"),
88];
89
90#[cfg(test)]
91mod tests {
92    use super::*;
93
94    #[test]
95    fn capability_pairs_are_unique() {
96        let unique = WASM_GC_CAPABILITIES
97            .iter()
98            .copied()
99            .collect::<std::collections::BTreeSet<_>>();
100        assert_eq!(unique.len(), WASM_GC_CAPABILITIES.len());
101    }
102}
aver_cert/format.rs

aver_cert/
format.rs
