Skip to content

STDLIB.md

Latest commit

 

History

History
698 lines (538 loc) · 31.5 KB

STDLIB.md

File metadata and controls

698 lines (538 loc) · 31.5 KB
Raw

📦 Mumei Standard Library Reference

Overview

Module Auto-import Description
std/prelude.mm ✅ Yes Traits, ADTs, collection interfaces
std/alloc.mm ❌ import "std/alloc" Dynamic memory, Vector, HashMap
std/option.mm ❌ import "std/option" Option<T> operations
std/stack.mm ❌ import "std/stack" Bounded stack operations
std/result.mm ❌ import "std/result" Result<T, E> operations
std/list.mm ❌ import "std/list" Recursive list ADT + Sort algorithms
std/container/bounded_array.mm ❌ import "std/container/bounded_array" Bounded array with sorted operations
std/libc.mm ❌ import "std/libc" Verified C standard library wrappers
std/container/verified_vector.mm ❌ import "std/container/verified_vector" Verified vector with quantifier-based contracts
std/contracts.mm ❌ import "std/contracts" Verified contract catalog (types + validators)
std/math/fixed_point.mm ❌ import "std/math/fixed_point" Fixed-point arithmetic (4 decimal places)
std/container/safe_queue.mm ❌ import "std/container/safe_queue" Verified FIFO queue
std/http_secure.mm ❌ import "std/http_secure" HTTPS-only HTTP client
std/concurrency/aviation.mm ❌ import "std/concurrency/aviation" Ordered runway allocation state machine
std/container/sorted_map.mm ❌ import "std/container/sorted_map" Verified sorted key-value map helpers
std/math/factorial.mm ❌ import "std/math/factorial" Factorial safety and step helpers
std/math/fibonacci.mm ❌ import "std/math/fibonacci" Fibonacci accumulator and termination helpers
std/string/validator.mm ❌ import "std/string/validator" ASCII validator predicates

Cross-project sync points

std/crypto/primitives.mm is a forge-generated, Z3-decidable crypto predicate module that does not require Lean escalation. The mumei-lean bridge currently keeps fourteen live generated theorem paths synchronized with this standard-library surface:

  • abs_saturating
  • bounded_mul_with_overflow_check
  • constant_time_eq_flag
  • ff_zero_eq_zero
  • verified_insertion_sort_ascending
  • poly_bound_monotone
  • exists_pivot_partition
  • sum_nonneg_inductive
  • rtgs_transfer_conservation
  • ff_mul_commutative
  • ff_mul_associative
  • ff_mul_add_distributive
  • predicate_guard_collapse
  • ff_pow_square_expands

The ascending-sort path lowers forall(i, 0, n-1, arr[i] <= arr[i+1]) to mathlib's List.Sorted through the MumeiLean.Sort bridge. See the cross-project roadmap and the mumei-lean harness contract for bridge ownership and E2E evidence.

std/prelude.mm (Auto-imported)

The prelude is automatically loaded by the compiler. No import statement needed.

Traits

Trait Methods Laws Description
Eq eq(a, b) -> bool reflexive, symmetric Equality
Ord leq(a, b) -> bool reflexive, transitive Total ordering
Numeric add, sub, mul, div(b where v!=0) commutative_add Arithmetic with zero-division prevention
Sequential seq_len(s) -> i64, seq_get(s, i) -> i64 non_negative_length, bounds_safe Abstract collection interface
Hashable hash(a) -> i64 deterministic Hash key constraint
Owned is_alive(a) -> bool, consume(a) -> Self alive_before_consume Ownership tracking

ADTs

enum Option<T> { None, Some(T) }
enum Result<T, E> { Ok(T), Err(E) }
enum List<T> { Nil, Cons(T, Self) }
struct Pair<T, U> { first: T, second: U }

Prelude Atoms

Atom Requires Ensures Description
prelude_is_some(opt) opt >= 0 && opt <= 1 result >= 0 && result <= 1 Check if Option is Some
prelude_is_none(opt) opt >= 0 && opt <= 1 result >= 0 && result <= 1 Check if Option is None
prelude_is_ok(res) res >= 0 && res <= 1 result >= 0 && result <= 1 Check if Result is Ok

std/alloc.mm — Dynamic Memory Management

import "std/alloc" as alloc;

Pointer Types

Type Definition Description
RawPtr i64 where v >= 0 Valid heap pointer
NullablePtr i64 where v >= -1 Nullable pointer (-1 = null)

Vector<T>

struct Vector<T> {
    ptr: i64 where v >= 0,   // heap pointer
    len: i64 where v >= 0,   // current element count
    cap: i64 where v > 0     // allocated capacity
}
Atom Requires Ensures Description
alloc_raw(size) size > 0 result >= -1 Allocate heap memory
dealloc_raw(ptr) ptr >= 0 result >= 0 Free heap memory
vec_new(cap) cap > 0 result >= 0 Create empty vector
vec_push(len, cap) len >= 0 && cap > 0 && len < cap result >= 0 && result <= cap && result == len + 1 Push element (precise length)
vec_get(len, index) len > 0 && index >= 0 && index < len result >= 0 Get element (bounds-checked)
vec_len(len) len >= 0 result == len Get length
vec_is_empty(len) len >= 0 0 or 1 Check if empty
vec_grow(old, new) old > 0 && new > old result > old Grow capacity
vec_drop(len, ptr) len >= 0 && ptr >= 0 result >= 0 Free vector
vec_push_safe(len, cap) len >= 0 && cap > 0 0=Ok, 1=Err Safe push with capacity check
vec_set(len, index, value) len > 0 && index >= 0 && index < len && value >= 0 result >= 0 Set element (bounds-checked)
vec_swap(len, i, j) len > 0 && i >= 0 && i < len && j >= 0 && j < len result >= 0 Swap two elements (bounds-checked)
vec_slice(len, start, end) len >= 0 && start >= 0 && end >= start && end <= len result >= 0 && result == end - start Slice (range-checked)
vec_insert(len, cap, index) len >= 0 && cap > 0 && len < cap && index >= 0 && index <= len result >= 0 && result == len + 1 Insert at index (bounds + capacity)
vec_remove(len, index) len > 0 && index >= 0 && index < len result >= 0 && result == len - 1 Remove at index (bounds-checked)

HashMap<K, V>

Key constraint: K must satisfy Hashable + Eq (defined in prelude).

struct HashMap<K, V> {
    buckets: i64 where v >= 0,    // bucket array pointer
    size: i64 where v >= 0,       // current element count
    capacity: i64 where v > 0     // bucket count
}
Atom Requires Ensures Description
map_new(capacity) capacity > 0 result >= 0 Create empty map
map_insert(size, cap) size >= 0 && cap > 0 && size < cap result <= size + 1 Insert key-value
map_get(size, hash) size >= 0 && hash >= 0 0=Ok, 1=Err Lookup by key hash
map_contains_key(size, hash) size >= 0 && hash >= 0 0 or 1 Check key existence
map_remove(size, hash) size >= 0 && hash >= 0 result <= size Remove by key
map_size(size) size >= 0 result == size Get size
map_is_empty(size) size >= 0 0 or 1 Check if empty
map_rehash(old, new) old > 0 && new > old result > old Grow and rehash
map_drop(size, buckets) size >= 0 && buckets >= 0 result >= 0 Free map
map_insert_safe(size, cap) size >= 0 && cap > 0 0=Ok, 1=Err Safe insert
map_should_rehash(size, cap) size >= 0 && cap > 0 0 or 1 Load factor check (75%)

std/option.mm

import "std/option" as option;
Atom Description
is_some(opt) Returns 1 if Some, 0 if None
is_none(opt) Returns 1 if None, 0 if Some
unwrap_or(opt, default) Returns value or default
map(opt, f) Phase A: Higher-order map via atom_ref — applies f to Some, returns 0 for None (trusted)
map_apply(opt, default, mapped) Map (workaround): applies transformation (Some→mapped, None→default) — @deprecated, use map
and_then_apply(opt, inner_opt) AndThen/FlatMap: chains Option-returning operations
or_else(opt, alternative) OrElse: provides fallback Option
filter(opt, condition) Filter: Some→None if condition is false

std/stack.mm

import "std/stack" as stack;

struct Stack<T> { top: i64 where v >= 0, max: i64 where v > 0 }
Atom Description
stack_push(top, max) Push (requires top < max)
stack_pop(top) Pop (requires top > 0)
stack_is_empty(top) Check if empty
stack_is_full(top, max) Check if full
stack_clear(top) Clear with termination proof

std/result.mm

import "std/result" as result;
Atom Description
is_ok(res) Returns 1 if Ok, 0 if Err
is_err(res) Returns 1 if Err, 0 if Ok
unwrap_or_default(res, default) Returns value or default
safe_divide(a, b) Division returning Result (Err on zero)
result_map(res, f) Phase A: Higher-order map via atom_ref — applies f to Ok, returns 1 for Err (trusted)
result_map_apply(res, default, mapped) Map (workaround): Ok→mapped, Err→default — @deprecated, use result_map
result_and_then(res, inner_res) AndThen/FlatMap: chains Result operations
result_or_else(res, alternative) OrElse: provides fallback on Err
result_map_err(res, mapped_err) MapErr: transforms Err value
result_wrap_err(res, err_code, offset) WrapErr: remap error code for package boundaries
result_unwrap_or_else(res, ok_val, err_default) UnwrapOrElse: final error handling
result_flatten(outer, inner) Flatten: Result<Result<T,E>,E> → Result<T,E>

std/list.mm

import "std/list" as list;

enum List { Nil, Cons(i64, Self) }
Atom Description
is_empty(list) Check if Nil
head_or(list, default) Get head or default
is_sorted_pair(a, b) Check if a <= b
insert_sorted(val, sorted_tag) Insert into sorted position

Immutable List Operations

Atom Requires Ensures Description
list_head(list) list ∈ {0,1} result ∈ {0,1} Head as Option (Nil→None, Cons→Some)
list_tail(list) list ∈ {0,1} result ∈ {0,1} Tail (new list, original unchanged)
list_append(list, value) list ∈ {0,1} result == 1 Append returns non-empty list
list_prepend(list, value) list ∈ {0,1} result == 1 Prepend (O(1), Cons construction)
list_length(list) list ∈ {0,1} result >= 0 Length (tag-based abstraction)
list_reverse(list) list ∈ {0,1} result == list Reverse (tag preserved)

Higher-Order Fold / Map (Phase A)

Atom Requires Ensures Description
fold_left(n, init, f) n >= 0 result >= 0 Phase A: Generic left fold via atom_ref — f: atom_ref(i64, i64) -> i64 (trusted, body uses arr[i] stub)
list_map(n, f) n >= 0 result == n Phase A: Map via atom_ref — f: atom_ref(i64) -> i64 (trusted, element count preserved)

Warning: fold_left body references arr[i] without an array parameter — do NOT run mumei build std/list.mm in isolation. Phase B will add proper array parameter support.

Reduce / Fold Operations

Atom Requires Ensures Description
fold_sum(n) n >= 0 && forall(i, 0, n, arr[i] >= 0) result >= 0 Sum all elements
fold_count_gte(n, threshold) n >= 0 && len(arr) >= n 0 <= result <= n Count elements ≥ threshold
fold_min_index(n) n >= 0 -1 <= result < n Index of minimum element
fold_max_index(n) n >= 0 -1 <= result < n Index of maximum element
fold_all_gte(n, threshold) n >= 0 && len(arr) >= n result ∈ {0,1} All elements ≥ threshold? (runtime forall)
fold_any_gte(n, threshold) n >= 0 && len(arr) >= n result ∈ {0,1} Any element ≥ threshold? (runtime exists)

Sort Algorithms (Verified)

Atom Requires Ensures Description
insertion_sort(n) n >= 0 result == n Insertion sort with termination proof
merge_sort(n) n >= 0 result == n Merge sort with inductive invariant
verified_insertion_sort(n) n >= 0 result == n Real nested-while insertion sort body using arr[i] = val + Z3 Array::store. trusted due to MIR move-analysis false-positive on inner-loop i = i + 1; only element-count preservation is asserted (no sorted-output guarantee — use verified_insertion_sort_identity for that).
verified_insertion_sort_identity(n) n >= 0 && forall(i, 0, n-1, arr[i] <= arr[i+1]) result == n && forall(i, 0, result-1, arr[i] <= arr[i+1]) Identity body (body: n); provable sorted-in → sorted-out contract without trusted. Use when the caller needs a verified sortedness postcondition.
verified_merge_sort(n) n >= 0 result == n Divide-and-conquer skeleton (control flow only — no aux buffer). trusted for recursive async-atom analysis; only element-count preservation is asserted.
verified_merge_sort_identity(n) n >= 0 && forall(i, 0, n-1, arr[i] <= arr[i+1]) result == n && forall(i, 0, result-1, arr[i] <= arr[i+1]) Identity body (body: n); provable sorted-in → sorted-out contract without trusted.
binary_search(n, target) n >= 0 result >= -1 && result < n Binary search with termination proof
binary_search_sorted(n, target) n >= 0 && forall(...) result >= -1 && result < n Binary search with sorted precondition

Lean escalation fixture: tests/fixtures/sort_ascending.mm defines verified_insertion_sort_ascending(n) with ensures: result == n && forall(i, 0, result - 1, arr[i] <= arr[i + 1]). Z3 returns unknown on the Array+forall quantifier (spurious counterexample), so this atom is a Lean escalation candidate via --escalate-lean. The mumei-lean bridge connects it to MumeiLean.Sort.insertion_sort_ascending_bridge backed by mathlib's List.Sorted. This fixture is kept outside std/ to avoid verify-std regression.

std/container/verified_vector.mm

import "std/container/verified_vector" as vvec;

struct VerifiedVector { len: i64 where v >= 0, cap: i64 where v > 0 }
Atom Requires Ensures Description
vvec_sum(n) n >= 0 && forall(arr[i] >= 0) result >= 0 Sum all non-negative elements
vvec_all_bounded(n, upper) n >= 0 && upper >= 0 && forall(0 <= arr[i] <= upper) result == 1 Check all elements within bound
vvec_push_n(len, cap, count) len >= 0 && cap > 0 && count >= 0 && len + count <= cap result >= 0 && result == len + count Batch push with length guarantee
vvec_range_check(len, start, end) len > 0 && start >= 0 && end > start && end <= len result == 1 Validate index range
vvec_binary_search(n, target) n >= 0 && forall(sorted) result >= -1 && result < n Binary search (sorted precondition)

std/container/bounded_array.mm

import "std/container/bounded_array" as bounded;

struct BoundedArray { len: i64 where v >= 0, cap: i64 where v > 0 }
Atom Requires Ensures Description
bounded_push(len, cap) len >= 0 && cap > 0 && len < cap result == len + 1 Push with overflow prevention
bounded_pop(len) len > 0 result == len - 1 Pop with underflow prevention
bounded_is_empty(len) len >= 0 0 or 1 Check if empty
bounded_is_full(len, cap) len >= 0 && cap > 0 0 or 1 Check if full
sorted_identity(n) n >= 0 && forall(sorted) result == n && forall(sorted) Sorted invariant preservation
sorted_insert_len(n, cap) n >= 0 && cap > 0 && n < cap result == n + 1 Sorted insert (length tracking)

std/libc.mm — Verified C Library Wrappers

import "std/libc" as libc;

Verified wrappers for C standard library functions via extern "C" FFI. Each extern function declares strict requires/ensures contracts verified by Z3 at call sites. Parameters use mumei's abstract size representation (i64) rather than raw pointers.

Memory Operations

Atom Requires Ensures Description
libc::safe_memcpy(dst_size, src_size, n) n >= 0 && dst_size >= n && src_size >= n result >= 0 Copy n bytes (no overlap)
libc::safe_memmove(dst_size, src_size, n) n >= 0 && dst_size >= n && src_size >= n result >= 0 Move n bytes (overlap safe)
libc::safe_memset(buf_size, value, n) n >= 0 && buf_size >= n && value >= 0 && value <= 255 result >= 0 Fill n bytes with value

String Operations

Atom Requires Ensures Description
libc::safe_strlen(buf_size) buf_size > 0 result >= 0 && result < buf_size Get string length (bounded)
libc::safe_snprintf(buf_size, n) buf_size > 0 && n > 0 && n <= buf_size result >= 0 Formatted print to buffer

Memory Allocation

Atom Requires Ensures Description
libc::safe_malloc(size) size > 0 result >= -1 Allocate memory (-1 = failure)
libc::safe_calloc(count, size) count > 0 && size > 0 result >= -1 Allocate zeroed memory (-1 = failure)
libc::safe_realloc(ptr, old_size, new_size) ptr >= 0 && old_size >= 0 && new_size > 0 result >= -1 Reallocate memory (-1 = failure)
libc::safe_free(ptr) ptr >= 0 result >= 0 Free allocated memory

C Header Generation

mumei build std/libc.mm --emit c-header generates a .h file with Doxygen @pre/@post annotations:

/**
 * @brief safe_memcpy
 * @pre n >= 0 && dst_size >= n && src_size >= n
 * @post result >= 0
 */
extern int64_t safe_memcpy(int64_t dst_size, int64_t src_size, int64_t n);

std/json.mm — JSON Operations

import "std/json" as json;

FFI-backed standard library for JSON parsing and generation. Wraps Rust serde_json behind a handle-based API.

Parse / Stringify

Atom Requires Ensures Description
json::parse(input) true result >= 0 Parse JSON string and return a handle
json::stringify(handle) handle >= 0 true Convert JSON handle to string

Value Access

Atom Requires Ensures Description
json::get(handle, key) handle >= 0 result >= 0 Get value from object by key
json::get_int(handle, key) handle >= 0 true Get integer value
json::get_str(handle, key) handle >= 0 true Get string value
json::get_bool(handle, key) handle >= 0 result in {0,1} Get boolean value

Array Operations

Atom Requires Ensures Description
json::array_len(handle) handle >= 0 result >= 0 Get array length
json::array_get(handle, index) handle >= 0 && index >= 0 result >= 0 Get array element
json::array_new() true result >= 0 Create empty array
json::array_push(handle, value) handle >= 0 result >= 0 Append value to array

Type Checks

Atom Requires Ensures Description
json::is_null(handle) handle >= 0 result in {0,1} Check if null
json::is_object(handle) handle >= 0 result in {0,1} Check if object
json::is_array(handle) handle >= 0 result in {0,1} Check if array

Value Construction

Atom Requires Ensures Description
json::object_new() true result >= 0 Create empty object
json::object_set(handle, key, value) handle >= 0 result >= 0 Set key-value pair on object
json::from_int(value) true result >= 0 Create JSON value from integer
json::from_str(value) true result >= 0 Create JSON value from string
json::from_bool(value) value in {0,1} result >= 0 Create JSON value from boolean

Memory Management (Plan 16)

Atom Requires Ensures Description
json::free(handle) handle >= 0 result in {0,1} Release JSON handle (1=success, 0=invalid)
json::str_free(handle) handle >= 0 result in {0,1} Release string handle (1=success, 0=invalid)

std/http.mm — HTTP Client

import "std/http" as http;

HTTP client wrapping Rust reqwest via FFI. Provides a handle-based API. Can be combined with task_group for parallel requests.

Requests

Atom Requires Ensures Description
http::get(url) true result >= 0 HTTP GET request
http::post(url, body) true result >= 0 HTTP POST request
http::put(url, body) true result >= 0 HTTP PUT request
http::delete(url) true result >= 0 HTTP DELETE request

Response

Atom Requires Ensures Description
http::status(handle) handle >= 0 result >= 0 Get status code (200, 404, etc.)
http::body(handle) handle >= 0 result >= 0 Get response body (string handle)
http::body_json(handle) handle >= 0 result >= 0 Parse response body as JSON
http::is_ok(handle) handle >= 0 result in {0,1} Check success (2xx)
http::is_error(handle) handle >= 0 result in {0,1} Check error

Headers

Atom Requires Ensures Description
http::header_get(handle, name) handle >= 0 result >= 0 Get header value
http::header_set(handle, name, value) handle >= 0 result >= 0 Set header value

Memory Management (Plan 16)

Atom Requires Ensures Description
http::free(handle) handle >= 0 result in {0,1} Release HTTP response handle (1=success, 0=invalid)

std/contracts.mm — Verified Contract Catalog

import "std/contracts" as contracts;

Refinement Types

Type Definition Description
Port i64 where v >= 1 && v <= 65535 Valid TCP/UDP port number
Percentage i64 where v >= 0 && v <= 100 Percentage value (0-100)
PositiveAmount i64 where v > 0 Strictly positive integer
NonNegative i64 where v >= 0 Non-negative integer
Byte i64 where v >= 0 && v <= 255 Byte value (0-255)
HttpStatus i64 where v >= 100 && v < 600 HTTP status code
ExitCode i64 where v >= 0 && v <= 255 Process exit code

Atoms

Atom Requires Ensures Description
is_within_range(val, min_val, max_val) min_val <= max_val 0 or 1 Range check
clamp(val, min_val, max_val) min_val <= max_val result >= min_val && result <= max_val Clamp value to range
abs_val(x) true result >= 0 Absolute value
max_of(a, b) true result >= a && result >= b Max of two values
min_of(a, b) true result <= a && result <= b Min of two values
is_valid_port(port) true 0 or 1 Port validation (1-65535)
is_valid_http_status(status) true 0 or 1 HTTP status validation (100-599)
safe_divide(a, b) b != 0 true Division (zero-division safe)
safe_modulo(a, b) b > 0 result >= 0 Modulo (positive divisor)

std/math/fixed_point.mm — Fixed-Point Arithmetic

import "std/math/fixed_point" as fp;

Scale factor: 10000 (4 decimal places). Example: 1.5 = 15000.

struct FixedPoint { value: i64 where v >= -999999999999 && v <= 999999999999 }
Atom Requires Ensures Description
fp_add(a, b) overflow-safe range result == a + b Addition
fp_sub(a, b) overflow-safe range result == a - b Subtraction
fp_mul(a, b) range true Multiplication (a * b / 10000)
fp_div(a, b) range + b != 0 true Division (a * 10000 / b)
fp_from_int(n) n >= -99999999 && n <= 99999999 result == n * 10000 Integer to fixed-point
fp_to_int(fp_val) range true Fixed-point to integer
fp_is_positive(fp_val) range 0 or 1 Positive check
fp_abs(fp_val) range result >= 0 Absolute value

std/container/safe_queue.mm — Verified FIFO Queue

import "std/container/safe_queue" as queue;

struct SafeQueue { len: i64 where v >= 0, cap: i64 where v > 0, head: i64 where v >= 0, tail: i64 where v >= 0 }
Atom Requires Ensures Description
enqueue(q_len, q_cap) q_len >= 0 && q_cap > 0 && q_len < q_cap result == q_len + 1 Enqueue with overflow prevention
dequeue(q_len) q_len > 0 result == q_len - 1 Dequeue with underflow prevention
queue_is_empty(q_len) q_len >= 0 0 or 1 Check if empty
queue_is_full(q_len, q_cap) q_len >= 0 && q_cap > 0 0 or 1 Check if full
queue_remaining(q_len, q_cap) q_len >= 0 && q_cap > 0 && q_len <= q_cap result == q_cap - q_len Remaining capacity
enqueue_safe(q_len, q_cap) q_len >= 0 && q_cap > 0 0=Ok, 1=Err Safe enqueue with capacity check
dequeue_safe(q_len) q_len >= 0 0=Ok, 1=Err Safe dequeue with empty check
batch_enqueue(q_len, q_cap, count) q_len >= 0 && q_cap > 0 && count >= 0 && q_len + count <= q_cap result == q_len + count Batch enqueue

std/http_secure.mm — HTTPS-only HTTP Client

import "std/http_secure" as https;

HTTPS-only wrapper around std/http.mm FFI backend. Enforces starts_with(url, "https://") at compile time via parameterized effects.

Effects

Effect Constraint Description
SecureHttpGet(url) starts_with(url, "https://") HTTPS GET
SecureHttpPost(url) starts_with(url, "https://") HTTPS POST
SecureHttpPut(url) starts_with(url, "https://") HTTPS PUT
SecureHttpDelete(url) starts_with(url, "https://") HTTPS DELETE

Requests

Atom Requires Ensures Description
secure_get(url) starts_with(url, "https://") result >= 0 HTTPS GET
secure_post(url, body) starts_with(url, "https://") result >= 0 HTTPS POST
secure_put(url, body) starts_with(url, "https://") result >= 0 HTTPS PUT
secure_delete(url) starts_with(url, "https://") result >= 0 HTTPS DELETE

Response

Atom Requires Ensures Description
status(handle) handle >= 0 result >= 0 Get status code
body(handle) handle >= 0 true Get response body
is_ok(handle) handle >= 0 result in {0,1} Check success (2xx)
free(handle) handle >= 0 result in {0,1} Release handle

vStd Forge Expansion Modules

These modules were added or refreshed by the P9-D vStd autonomous expansion workflow.

std/concurrency/aviation.mm — Ordered Runway Allocation

import "std/concurrency/aviation" as aviation;

Defines the RunwayAllocation temporal effect (Idle -> Ordered -> Allocated) and ordered exclusive runway resources.

Atom Requires Ensures Description
allocate_runway(flight, runway1, runway2, lock_state) flight >= 0 && runway1 >= 0 && runway2 >= 0 && runway1 != runway2 && runway1 < runway2 result != 0 && result == runway1 + runway2 Acquire runway resources in priority order

std/container/sorted_map.mm — Verified Sorted Key-Value Map

import "std/container/sorted_map" as smap;
Atom Requires Ensures Description
sorted_map_insert_position(pos, len) len >= 0 && pos >= 0 && pos <= len result == pos && result <= len Insertion-position witness
sorted_map_insert_len(len, cap) cap > 0 && len >= 0 && len < cap result == len + 1 && result <= cap Length after insertion
sorted_map_key_ordered(left_key, right_key) true 0 or 1 Adjacent key order witness
sorted_map_new(initial_cap) initial_cap > 0 result == 0 Empty sorted map length
sorted_map_insert(map_len, map_cap, key, value) map_len < map_cap result == map_len + 1 Trusted array-store insertion
sorted_map_get(map_len, key) map_len >= 0 -1 or valid index Binary-search style index witness
sorted_map_remaining_capacity(map_len, map_cap) map_len <= map_cap result == map_cap - map_len Capacity bookkeeping
sorted_map_is_sorted(n) sorted-key witness result == 1 Sortedness witness

std/math/factorial.mm — Verified Factorial Helpers

import "std/math/factorial" as factorial;
Atom Requires Ensures Description
factorial_step(acc, n) acc >= 1 && n >= 1 && n <= 20 && acc <= 1000000 result == acc * n && result >= 1 One bounded factorial step
factorial_in_range(n) true 0 or 1 Range predicate for 0 <= n <= 20

std/math/fibonacci.mm — Verified Fibonacci Helpers

import "std/math/fibonacci" as fib;
Atom Requires Ensures Description
fib_step_next(a, b) a >= 0 && b >= 0 && a + b <= i64::MAX result == a + b && result >= b Next accumulator value
fib_remaining_decreases(remaining) remaining > 0 result == remaining - 1 && result < remaining Loop termination witness

std/string/validator.mm — Verified String Validators

import "std/string/validator" as validator;
Atom Requires Ensures Description
is_numeric_ascii_code(code) code >= 0 && code <= 127 0 or 1 ASCII digit predicate
is_alphanumeric_ascii_code(code) code >= 0 && code <= 127 0 or 1 ASCII digit/letter predicate

Path Resolution

The resolver searches for std/ imports in order:

  1. Project root — base_dir/std/option.mm
  2. Compiler binary directory — alongside mumei executable
  3. Current working directory
  4. CARGO_MANIFEST_DIR — for development builds
  5. MUMEI_STD_PATH — custom installation path