Skip to content

EXAMPLES.md

Latest commit

 

History

History
435 lines (367 loc) · 12 KB

EXAMPLES.md

File metadata and controls

435 lines (367 loc) · 12 KB
Raw

📄 Mumei Examples & Test Suite Reference

Introductory .mm Samples

These samples were previously shown in the README. They are useful after the no-.mm workflow has identified contracts worth migrating into Mumei source.

Refinement types

type Nat = i64 where v >= 0;

atom increment(n: Nat)
  requires: n >= 0;
  ensures: result >= 1;
  body: n + 1;

// Explicit return types for Str, f64, enums (Plan 18)
atom greet(name: Str) -> Str
  requires: true;
  ensures: true;
  body: "Hello, " + name;

Effects

Side effects are verified at compile time — undeclared effects will not compile.

effect FileWrite;
effect Log;

atom write_log(msg: Nat)
    effects: [FileWrite, Log];
    requires: msg >= 0;
    ensures: result == msg;
    body: {
        perform FileWrite.write(msg);
        perform Log.info(msg);
        msg
    };

Traits with algebraic laws

Z3 proves every implementation satisfies the trait laws.

trait Comparable {
    fn leq(a: Self, b: Self) -> bool;
    law reflexive: leq(x, x) == true;
    law transitive: leq(a, b) && leq(b, c) => leq(a, c);
}

impl Comparable for i64 {
    fn leq(a: i64, b: i64) -> bool { a <= b }
}

Additional .mm Examples

Loop invariant + termination proof

Z3 proves the loop terminates and the invariant holds inductively.

atom sum_up_to(n: i64)
    requires: n >= 0;
    ensures: result >= 0;
    body: {
        let s = 0;
        let i = 0;
        while i < n
        invariant: s >= 0 && i <= n
        decreases: n - i
        {
            s = s + i;
            i = i + 1;
        };
        s
    };

Higher-order function contracts

contract(f) lets Z3 verify generic callbacks without trusted.

atom apply_twice(x: i64, f: atom_ref(i64) -> i64)
    requires: x >= 0;
    ensures: result >= 0;
    contract(f): requires: x >= 0, ensures: result >= 0;
    body: {
        let first = call(f, x);
        call(f, first)
    };

Deadlock-free concurrency

Resource priorities are verified at compile time.

resource db   priority: 1 mode: exclusive;
resource cache priority: 2 mode: shared;

async atom transfer(amount: i64)
    resources: [db, cache];
    requires: amount >= 0;
    ensures: result >= 0;
    body: {
        acquire db { acquire cache { amount } }
    };

Verification Suite (sword_test.mm)

The test suite exercises 8 atoms, 2 structs, 1 generic struct, 1 generic enum, 1 trait + impl, covering every verification feature:

type Nat = i64 where v >= 0;
type Pos = f64 where v > 0.0;
struct Point { x: f64 where v >= 0.0, y: f64 where v >= 0.0 }
struct Pair<T, U> { first: T, second: U }
enum Option<T> { Some(T), None }
trait Comparable {
    fn leq(a: Self, b: Self) -> bool;
    law reflexive: leq(x, x) == true;
}
impl Comparable for i64 {
    fn leq(a: i64, b: i64) -> bool { a <= b }
}
atom sword_sum(n: Nat) ...   // Loop invariant + termination
atom scale(x: Pos) ...       // Float refinement
atom stack_push(...) ...      // Overflow prevention
atom stack_pop(...) ...       // Underflow prevention
atom circle_area(r: Pos) ... // Geometric invariant
atom robust_push(...) ...     // Bounded stack push
atom stack_clear(...) ...     // Termination proof
atom dist_squared(...) ...    // Non-negative guarantee

Verified Properties

Atom Verification
sword_sum Loop invariant + termination (decreases: n - i)
scale Float refinement (Pos > 0.0 ⟹ result > 0.0)
stack_push Overflow prevention (top < max ⟹ top+1 ≤ max)
stack_pop Underflow prevention (top > 0 ⟹ top-1 ≥ 0)
circle_area Geometric invariant (r > 0 ⟹ area > 0)
robust_push Bounded stack push (0 ≤ top' ≤ max)
stack_clear Loop termination (decreases: i) + invariant preservation
dist_squared Non-negative distance (dx² + dy² ≥ 0)
Pair<T,U> Generic struct (monomorphization)
Option<T> Generic enum (monomorphization)
Comparable Trait law reflexive verified by Z3 for impl i64

Pattern Matching Test (examples/match_atm.mm)

Demonstrates Enum + match + guards + Refinement Types:

type Balance = i64 where v >= 0;
enum AtmState { Idle, Authenticated, Dispensing, Error }
atom atm_transition(state, action, balance: Balance)
    requires: state >= 0 && state <= 3 && action >= 0 && action <= 3;
    ensures: result >= 0 && result <= 3;
    body: {
        match state {
            0 => match action { 0 => 1, _ => 3 },
            1 => match action { 1 => 2, 3 => 0, _ => 3 },
            2 => match action { 2 if balance > 0 => 0, 2 => 3, 3 => 0, _ => 3 },
            _ => 3
        }
    }

Inter-atom Call Test (examples/call_test.mm)

atom increment(n: Nat) requires: n >= 0; ensures: result >= 1; body: { n + 1 };
atom double_increment(n: Nat) requires: n >= 0; ensures: result >= 1;
body: { let x = increment(n); increment(x) };

Multi-file Import Test (examples/import_test/)

examples/import_test/
├── lib/math_utils.mm    # safe_add, safe_double
└── main.mm              # import "./lib/math_utils.mm" as math;

Higher-Order Functions Demo (examples/higher_order_demo.mm)

Demonstrates atom_ref + call + contract() for first-class function references with Z3-verified contracts:

atom increment(x: i64)
    requires: x >= 0;
    ensures: result == x + 1;
    body: x + 1;

// contract(f) lets Z3 verify without trusted (Phase B: call_with_contract)
atom apply(x: i64, f: atom_ref(i64) -> i64)
    requires: x >= 0;
    ensures: result >= 0;
    contract(f): ensures: result >= 0;
    body: call(f, x);

// At call site, increment's contract IS propagated via atom_ref
atom demo_apply()
    requires: true;
    ensures: result >= 0;
    body: apply(5, atom_ref(increment));

mumei verify examples/higher_order_demo.mm   # Z3 verification
mumei build examples/higher_order_demo.mm -o dist/higher_order_demo

Str Type Demo (examples/str_demo.mm)

Demonstrates Str type string operations with -> Str return type annotation (Plan 9 + Plan 18):

atom greet(name: Str) -> Str
    requires: true;
    ensures: true;
    body: "Hello, " + name

atom is_same(a: Str, b: Str)
    requires: true;
    ensures: result >= 0 && result <= 1;
    body: { if a == b { 1 } else { 0 } }

Enum Payload Demo (examples/enum_payload.mm)

Demonstrates tagged unions with payload data and match pattern matching (Plan 14):

enum Shape {
    Circle(i64),
    Rectangle(i64, i64)
}

atom area(s: Shape)
    requires: true;
    ensures: result >= 0;
    body: {
        match s {
            Circle(r) => r * r * 3,
            Rectangle(w, h) => w * h
        }
    }

JSON Demo (examples/json_demo.mm)

Demonstrates std.json operations — object construction, array manipulation, and stringify (Plan 10 + Plan 17):

import "std/json" as json;

atom build_user(name: Str, age: i64)
    requires: age >= 0;
    ensures: result >= 0;
    body: {
        let obj = json::object_new();
        let name_val = json::from_str(name);
        let age_val = json::from_int(age);
        let obj = json::object_set(obj, "name", name_val);
        let obj = json::object_set(obj, "age", age_val);
        obj
    }

HTTP Demo (examples/http_demo.mm)

Demonstrates std.http GET requests and response processing (Plan 11 + Plan 17):

import "std/http" as http;

atom fetch_status(url: Str)
    requires: true;
    ensures: result >= 0;
    body: {
        let response = http::get(url);
        http::status(response)
    }

Concurrent HTTP Demo (examples/concurrent_http.mm)

Demonstrates task_group for parallel HTTP requests (Plan 8 + Plan 11):

import "std/http" as http;

atom fetch_all(url1: Str, url2: Str)
    requires: true;
    ensures: result >= 0;
    body: {
        task_group(all) {
            task { fetch_one(url1) },
            task { fetch_one(url2) }
        }
    }

Path Safety Demo (examples/path_safety.mm)

Demonstrates compile-time directory traversal prevention using parameterized effects with compound && constraints:

// Security policy: only /tmp/ paths, no ".." allowed
effect SafeFileRead(path: Str) where starts_with(path, "/tmp/") && not_contains(path, "..");

// SAFE: user_id is constrained — passes verification
atom safe_read(user_id: Str)
    effects: [SafeFileRead(path)]
    requires: not_contains(user_id, "..") && not_contains(user_id, "\0");
    ensures: result >= 0;
    body: {
        let path = "/tmp/" + user_id + "/log.txt";
        perform SafeFileRead.read(path);
        1
    }

// UNSAFE: user_id unconstrained — compile error
atom unsafe_read(user_id: Str)
    effects: [SafeFileRead(path)]
    requires: true;
    ensures: result >= 0;
    body: {
        let path = "/tmp/" + user_id + "/log.txt";
        perform SafeFileRead.read(path);
        1
    }

Verified Properties

Atom Verification
safe_read Path starts with /tmp/, no .. traversal (Z3 String constraints)
unsafe_read Rejected — Z3 finds counterexample: user_id = ".."

Verified HTTP Server Demo (examples/verified_server.mm)

Combines path safety with temporal effect verification for a mathematically verified HTTP server:

effect SafeFileRead(path: Str) where starts_with(path, "/tmp/") && not_contains(path, "..");

effect HttpServer
    states: [Init, Bound, Listening, Responding];
    initial: Init;
    transition bind: Init -> Bound;
    transition listen: Bound -> Listening;
    transition accept: Listening -> Responding;
    transition respond: Responding -> Listening;
    transition close: Listening -> Init;

// SAFE: constrained path + correct temporal ordering
atom serve_safe_file(req_path: Str)
    effects: [SafeFileRead(path), HttpServer]
    requires: not_contains(req_path, "..") && not_contains(req_path, "\0");
    ensures: result >= 0;
    body: {
        let path = "/tmp/public/" + req_path;
        perform SafeFileRead.read(path);
        1
    }

// Double response — compile error (temporal violation)
atom double_respond(req: i64)
    effects: [HttpServer]
    requires: req > 0;
    ensures: result >= 0;
    body: {
        perform HttpServer.respond(req);
        perform HttpServer.respond(req);
        1
    }

Verified Properties

Atom Verification
serve_safe_file Path safety (Z3 String) + temporal ordering
serve_unsafe_file Rejected — path traversal possible
double_respond Rejected — temporal violation (respond from Listening state)

E2E Verification Tests

File Tests
tests/test_str_type.mm Str concat, equality, inequality, empty string
tests/test_enum_payload.mm Match variants, wildcards, nested match
tests/test_json_operations.mm Object roundtrip, array ops, type checks
tests/test_path_safety.mm Safe read, literal path, concat prefix
tests/test_verified_server.mm Safe file serving, server bind, combined effects 
for f in tests/test_*.mm; do
    mumei check "$f" && echo "PASS ✓" || echo "FAIL ✗"
done

Negative Test Suite

File Expected Error Category
postcondition_fail.mm Postcondition not satisfied Basic
division_by_zero.mm Potential division by zero Safety
array_oob.mm Potential Out-of-Bounds Safety
match_non_exhaustive.mm Match is not exhaustive Completeness
consume_ref_conflict.mm Cannot consume ref parameter Ownership
invariant_fail.mm Invariant fails initially Loop
requires_not_met.mm Precondition not satisfied at call site Inter-atom
termination_fail.mm Decreases does not strictly decrease Termination
forall_ensures_fail.mm forall in ensures not satisfied Quantifier 
for f in tests/negative/*.mm; do
    mumei verify "$f" && echo "UNEXPECTED PASS" || echo "EXPECTED FAIL ✓"
done

Outputs

Output Path Contents
LLVM IR dist/katana_<AtomName>.ll Pattern Matrix match, StructType