Example programs

intent "a counter that never goes negative"
    example Inc, Inc, Dec -> 1
    example Dec -> refused: Underflow

state Counter
    n: u64 = 0

event Inc
event Dec

error Underflow

step Counter on Inc -> n + 1
step Counter on Dec -> try n.checked_sub(1) else Underflow

module hello

fn main()
    emit "hello, world"

intent "the n-th Fibonacci number, computed in linear time"
    check fib(0) == 0
    check fib(10) == 55

fn fib(n: u32) -> u64
    var a: u64 = 0
    var b: u64 = 1
    for _ in 0..n
        let t = a + b
        a = b
        b = t
    return a

module bank

intent "a bank account that refuses overdrafts"
    example Deposit(amount: 50), Withdraw(amount: 20) -> 30
    example Withdraw(amount: 1) -> refused: Insufficient

state Account
    balance: i64 = 0

event Deposit(amount: i64)
event Withdraw(amount: i64)

error Insufficient(need: i64)

struct Withdrawn
    amount: i64

step Account on Deposit(amount: a) if a > 0 -> balance + a
step Account on Deposit(amount: _) -> balance
step Account on Withdraw(amount: a)
    if a > balance
        fail Insufficient(need: a - balance)
    balance -= a
    emit Withdrawn(amount: a)

kind Shape
    Circle(r: f64)
    Rect(w: f64, h: f64)
    Empty

fn area(s: &Shape) -> f64
    match s
        Circle(r: r) -> 3.141592653589793 * r * r
        Rect(w: w, h: h) -> w * h
        Empty -> 0.0

fn first_even(xs: &[i64]) -> i64?
    for x in xs
        if x % 2 == 0
            return some(x)
    return none

fn or_zero(v: i64?) -> i64
    match v
        some(x) -> x
        none -> 0

error ParseFailed(at: u32)
error Empty

fn parse_digit(c: text) -> u8 ! ParseFailed
    if c.isdigit()
        return c.toint() as u8
    fail ParseFailed(at: 0)

fn sum_digits(s: text) -> u32 ! (ParseFailed)
    var total: u32 = 0
    for c in s.chars()
        total += (try parse_digit(c)) as u32
    return total

fn report(e: ParseFailed) -> u32 = e.at

fn safe(s: text) -> u32 = sum_digits(s) catch 0

fn logged(s: text) -> u32 = sum_digits(s) catch |e| report(e)

trait Describe
    fn describe(&self) -> text

trait Container
    type Item
    fn get(&self, i: usize) -> Self.Item?
    fn len(&self) -> usize

struct Point
    x: i64
    y: i64

impl Describe for Point
    fn describe(&self) -> text = "(" + self.x.tostr() + ", " + self.y.tostr() + ")"

impl Point
    fn origin() -> Point = Point(x: 0, y: 0)
    fn moved(self, dx: i64) -> Point = Point(x: self.x + dx, y: self.y)

fn max_of[T: Ord](xs: &[T]) -> T?
    var best: T? = none
    for x in xs
        match best
            none -> best = some(copy(x))
            some(b) if x > b -> best = some(copy(x))
            _ -> pass
    return best

trait Describe
    fn describe(&self) -> text

impl forall[T: Describe] Describe for List[T]
    fn describe(&self) -> text = ", ".join([x.describe() for x in self])

const N: usize = 64
const TABLE: [u32; 256] = comptime crc_table()

comptime fn crc_table() -> [u32; 256]
    var t = [0; 256]
    for i in 0..256
        var c: u32 = i as u32
        for _ in 0..8
            c = if c & 1 == 1 then 0xEDB88320 ^ (c >> 1) else c >> 1
        t[i] = c
    return t

fn zeros[comptime n: usize]() -> [u8; n]
    return [0; n]

fn word_lengths(s: &text) -> List[u32]
    var out: List[u32] = []
    with arena scratch
        let ws: List[text] @scratch = s.words()
        for w in ws
            out.append(w.len() as u32)
    return out

fn push_all(dst: &mut List[i64], src: &[i64])
    for x in src
        dst.append(x)

fn demo() -> usize
    var a: List[i64] = [1, 2, 3]
    let b: List[i64] = [4, 5]
    push_all(&mut a, &b)
    return a.len()

fn producer(out: chan i64, n: i64)
    for i in 0..n
        out <- i
    out.close()

fn main()
    let c = chan[i64](8)
    spawn producer(c, 100)
    var total = 0
    loop
        match <- c
            some(v) -> total += v
            none -> break
    emit total

fn merge(a: chan text, b: chan text, out: chan text)
    loop bound 1000
        select
            recv some(x) from a -> out <- x
            recv some(y) from b -> out <- y
            recv none from a -> break
            after 10 -> emit "idle"

event Get(reply: chan i64)
event Add(k: i64)

actor Tally
    total: i64 = 0
    on Add(k: k) -> total + k
    on Get(reply: r)
        r <- total

state Cart
    items: List[text] = []

state Stats
    adds: u64 = 0
    removes: u64 = 0

event AddItem(name: text)
event RemoveItem(name: text)
event Reset

step Cart on AddItem(name: n) -> items.with(n)
step Stats on AddItem(name: _)
    adds += 1
step Cart on RemoveItem(name: n)
    items = [copy(i) for i in items if i != n]
step Stats on RemoveItem(name: _)
    removes += 1
step Cart on Reset -> []

intent "a traffic light that cycles on each tick"
    example Tick, Tick -> light == Yellow

kind Light
    Red
    Green
    Yellow

state Signal
    light: Light = Red

event Tick

step Signal on Tick
    match light
        Red -> light = Green
        Green -> light = Yellow
        Yellow -> light = Red

error Diverged

fn collatz_steps(n: u64) -> u64 ! Diverged
    var x = n
    var k: u64 = 0
    while x != 1 bound 10_000
        x = if x % 2 == 0 then x / 2 else 3 * x + 1
        k += 1
    return k

error Empty

fn mean(xs: &[f64]) -> f64 ! Empty
    if xs.len() == 0
        fail Empty
    var s = 0.0
    for x in xs
        s += x
    return s / xs.len() as f64

const AVOGADRO: f64 = 6.02214076e23
const EPS = 1e-9

fn shout(s: &text) -> text = s.strip().upper() + "!"

fn is_palindrome(s: &text) -> bool
    let t = [c for c in s.lower().chars() if c.isalpha()]
    return t == t.reverse()

fn escapes() -> text = "tab\t newline\n quote\" snow \u{2603}"

fn freq(words: &[text]) -> Map[text, u32]
    var m: Map[text, u32] = {}
    for w in words
        m[w] = (m.get(w) catch 0) + 1
    return m

fn table() -> Map[text, i64] = {"a": 1, "b": 2,}

error DivByZero

fn divmod(a: i64, b: i64) -> (i64, i64) ! DivByZero
    if b == 0
        fail DivByZero
    return (a / b, a % b)

fn use_it() -> i64
    let (q, r) = divmod(17, 5) catch (0, 0)
    let pair = (q, r)
    return pair.0 + pair.1

fn classify(n: i64) -> text
    match n
        0 -> "zero"
        1 | 2 | 3 -> "small"
        4..=9 -> "digit"
        -1 -> "minus one"
        _ if n < 0 -> "negative"
        _ -> "large"

fn squares(xs: &[i64]) -> List[i64] = xs.map(fn(x: i64) => x * x)

fn evens(xs: &[i64]) -> List[i64] = xs.filter(fn(x: i64) => x % 2 == 0)

fn total(xs: &[i64]) -> i64 = xs.fold(0, fn(acc: i64, x: i64) => acc + x)

fn move_piece(source src: u8, target dst: u8) -> u8 = dst - src

fn call_it() -> u8 = move_piece(source: 2, target: 9)

fn popcount(x: u64) -> u32
    var v = x
    var c: u32 = 0
    while v != 0 bound 64
        v &= v - 1
        c += 1
    return c

fn mix(a: u32, b: u32) -> u32 = (a << 5 | a >> 27) ^ ~b & 0xFF

fn middle(xs: &[i64]) -> &[i64] = xs[1:-1]

fn head(xs: &[i64]) -> List[i64] = copy(xs[:2])

fn grid_get(g: &[[i64; 3]; 3], r: usize, c: usize) -> i64 = g[r][c]

kind Expr
    Num(v: i64)
    Add(a: Box[Expr], b: Box[Expr])
    Neg(e: Box[Expr])

fn depth_shallow(e: &Box[Expr]) -> u32 = 1

fn depth(e: &Expr) -> u32
    match e
        Num(v: _) -> 1
        Neg(e: inner) -> 1 + depth_shallow(inner)
        Add(a: _, b: _) -> 2

intent "a door that locks only when closed"
    "the door starts closed and unlocked"
    example Open, Close, Lock -> locked
    example Open, Lock -> refused: DoorOpen

state Door
    open: bool = false
    locked: bool = false

event Open
event Close
event Lock
event Unlock

error DoorOpen
error Locked

step Door on Open if locked
    fail Locked
step Door on Open
    open = true
step Door on Close
    open = false
step Door on Lock if open
    fail DoorOpen
step Door on Lock
    locked = true
step Door on Unlock
    locked = false

state Inventory
    stock: Map[text, u32] = {}

event Receive(sku: text, qty: u32)
event Ship(sku: text, qty: u32)
error OutOfStock(sku: text)

struct Shipped
    sku: text
    qty: u32

step Inventory on Receive(sku: s, qty: q)
    stock[s] = (stock.get(s) catch 0) + q
step Inventory on Ship(sku: s, qty: q)
    let have = stock.get(s) catch 0
    if have < q
        fail OutOfStock(sku: s)
    stock[s] = have - q
    emit Shipped(sku: s, qty: q)

fn table_size() -> usize
    comptime
        check N > 0
        check N % 8 == 0
    return N * 2

const N: usize = 16

fn vowel(c: &text) -> bool = c in "aeiou"

fn not_member(x: i64, xs: &[i64]) -> bool = x not in xs

fn same_range(a: i64) -> bool = a in 0..10 and not (a == 5)

type Pipe = chan (u64, text)
type Handler = fn(u64) -> bool
type Result2 = i64 ! Overflow

fn worker(input: chan (u64, text), output: chan u64)
    loop bound 1_000_000
        match <- input
            some((id, _)) -> output <- id
            none -> return

fn grade(score: u32) -> text
    if score >= 90
        return "A"
    elif score >= 80
        return "B"
    elif score >= 70
        if score == 77
            return "lucky C"
        return "C"
    else
        return "F"

fn long_call() -> i64
    let xs = [
        1, 2, 3,
        4, 5, 6,
    ]
    let total = xs.fold(
        0,
        fn(a: i64, b: i64) => a + b,
    )
    return total  # comments are allowed here

event Ping(n: u64, reply: chan u64)

actor Echo
    seen: u64 = 0
    on Ping(n: n, reply: r)
        seen += 1
        r <- n

fn main()
    let e = Echo()
    let r = chan[u64](1)
    e <- Ping(n: 7, reply: r)
    emit <- r

const MASK: u32 = 0xFF_FF
const FLAGS: u8 = 0b1010_0101
const PERMS: u16 = o755
const BIG: f64 = 1.5e+300
const SMALL: f64 = 2.5e-7

# Structural recursion: each self-call takes a field of a constructor the
# function matched, so the depth is bounded by the size of the value.
kind Tree
    Leaf(v: i64)
    Node(l: Box[Tree], r: Box[Tree])

fn tree_sum(t: &Tree) -> i64
    match t
        Leaf(v: v) -> return v
        Node(l: l, r: r) -> return tree_sum(l) + tree_sum(r)

fn sample_sum() -> i64
    let t = Node(l: Box(Leaf(v: 2)), r: Box(Node(l: Box(Leaf(v: 3)), r: Box(Leaf(v: 4)))))
    return tree_sum(&t)

check sample_sum() == 9

# A foreign function: C ABI, scalar results, borrowed buffers only.
# Only main and task functions may call it; its results enter the log.
extern "C" fn crc32(data: &[u8], seed: u32) -> u32

fn main()
    let bytes: List[u8] = [1, 2, 3]
    emit crc32(&bytes, 0)

# An arena with a fixed capacity, and explicit wrapping arithmetic for hashing.
fn fnv1a(s: &text) -> u32
    var h: u32 = 2166136261
    with arena scratch bound 4096
        let cs: List[text] @scratch = s.chars()
        for c in cs
            h = (h ^ (c.len() as u32)).wrapping_mul(16777619)
    return h

check (250 as u8).wrapping_add(10) == 4
check (250 as u8).saturating_add(10) == 255

# f32 arithmetic: computed in f64 and rounded once, so every target agrees bit for bit.
fn axpy(a: f32, x: f32, y: f32) -> f32
    return a * x + y

check axpy(2.0 as f32, 0.1 as f32, 1.0 as f32) == 1.2 as f32
check (0.1 as f32) as f64 != 0.1
check (16777217 as f32) as i64 == 16777216

# Lane-wise arithmetic on fixed-length arrays.
fn blend(a: [f64; 4], b: [f64; 4], w: [f64; 4]) -> [f64; 4]
    return a * w + b * ([1.0, 1.0, 1.0, 1.0] - w)

fn mix(a: [i32; 3], b: [i32; 3]) -> [i32; 3]
    return (a + b) % [7, 7, 7]

check mix([1, 2, 3], [10, 20, 30]) == [4, 1, 5]
check blend([1.0, 2.0, 3.0, 4.0], [0.0, 0.0, 0.0, 0.0], [1.0, 0.5, 0.0, 1.0]) == [1.0, 1.0, 0.0, 4.0]

# A device region holds fixed-size values only and performs no effects.
fn dot4(a: [f32; 4], b: [f32; 4]) -> f32
    var acc: f32 = 0 as f32
    with device gpu bound 4096
        let p: [f32; 4] = a * b
        for x in p
            acc = acc + x
    return acc

check dot4([1.0 as f32, 2.0 as f32, 3.0 as f32, 4.0 as f32], [1.0 as f32, 1.0 as f32, 1.0 as f32, 1.0 as f32]) == 10.0 as f32

# Text is indexed and measured in UTF-8 bytes.
fn first_byte(s: &text) -> u8
    return s[0]

check "héllo".len() == 6
const A: text = "A"
check first_byte(&A) == 65
check "héllo"[1] == 195
check "héllo"[0:1] == "h"
check "héllo"[1:3] == "é"

# Full-range u64 arithmetic, checked against [0, 2^64).
const BIG: u64 = 18446744073709551615

fn half(x: u64) -> u64
    return x / 2

check half(BIG) == 9223372036854775807
check BIG - 1 == 18446744073709551614
check (BIG / 3) * 3 == BIG
check BIG.checked_add(1).isnone()

# `lalr` is an ordinary name (it was wrongly reserved before 0.5).
const lalr: u64 = 1
check BIG - lalr + lalr == BIG

# Two producers on one select: the rotation guarantees neither is starved.
fn fan_in(a: chan u64, b: chan u64, out: chan u64)
    loop bound 1000
        select
            recv some(x) from a -> out <- x
            recv some(y) from b -> out <- y
            recv none from a -> break

# A linear handle must be consumed exactly once on every path.
linear struct File
    fd: i32

extern "C" fn c_open(path: &text) -> File
extern "C" fn c_close(f: File) -> i32
extern "C" fn c_write(f: File, n: u32) -> File

fn main()
    let p = "log.txt"
    let f = c_open(&p)
    let g = c_write(f, 3)
    if g.fd < 0
        let _ = c_close(g)
    else
        let r = c_close(g)
        emit r

# A program can raise or lower the default loop limit.
const LOOP_LIMIT: u64 = 5000000

fn count(n: u64) -> u64
    var k: u64 = 0
    while k < n
        k += 1
    return k

check count(2000000) == 2000000

# Iterators: push-model generators, bounded by the loop limit.
fn evens(n: u64) -> iter u64
    var i: u64 = 0
    while i < n
        yield i * 2
        i += 1

fn naturals() -> iter u64
    var i: u64 = 0
    loop
        yield i
        i += 1

fn first_over(t: u64) -> u64
    for x in naturals()
        if x > t
            return x
    return 0

fn total(n: u64) -> u64
    var s: u64 = 0
    for x in evens(n)
        s += x
    return s

check total(4) == 12
check evens(3).collect() == [0, 2, 4]
check first_over(100) == 101

module refined

intent "input validation is a declared predicate: an event whose payload is outside its refined type is refused, state unchanged"
    example SetVolume(pct: 40) -> level == 40
    example Rename(name: "ok") -> name == "ok"
    example Code(pin: "0042"), Code(pin: "9999") -> accepted == 2
    example SetVolume(pct: 40), Rename(name: "ok") -> level == 40

type Pct = u8 where self <= 100
type Name = text where self.len() >= 1 and self.len() <= 2
type Pin = text where self.isdigit() and self.len() == 4

state Volume
    level: Pct = 0

state Codes
    accepted: u32 = 0

state Profile
    name: text = "-"

event SetVolume(pct: Pct)
event Rename(name: Name)
event Code(pin: Pin)

step Volume on SetVolume(pct: p) -> p
step Codes on Code(pin: _) -> accepted + 1
step Profile on Rename(name: n) -> n

# rce-version: 0.8
module page

intent "untrusted text reaches HTML and SQL only through the context's encoder (5.16): markup and query syntax come from program literals"
    example Comment(body: "<script>x</script>") -> html.raw() == "<p>&lt;script&gt;x&lt;/script&gt;</p>"
    example Comment(body: "O'Brien") -> query.raw() == "SELECT id FROM users WHERE name = 'O''Brien'"
    example Comment(body: "a b&c") -> link.raw() == "/search?q=a%20b%26c"

state Page
    html: Text[Html] = Html.lit("<p></p>")
    query: Text[Sql] = Sql.lit("")
    link: Text[Url] = Url.lit("/")

event Comment(body: text)

step Page on Comment(body: b)
    html = Html.lit("<p>") + Html.encode(b) + Html.lit("</p>")
    query = Sql.lit("SELECT id FROM users WHERE name = ") + Sql.encode(b)
    link = Url.lit("/search?q=") + Url.encode(b)
    emit html

# rce-version: 0.8
module admin

intent "authority is a value (5.16): a Guarded field is written only by a step whose event carries the capability"
    example SetLimit(admin: (), limit: 50) -> limit == 50
    example SetLimit(admin: (), limit: 50), Spend(amount: 20) -> spent == 20
    example Spend(amount: 5) -> limit == 100

struct Root

state Policy
    limit: Guarded[u32, Root] = 100

state Ledger
    spent: u32 = 0

event SetLimit(admin: Cap[Root], limit: u32)
event Spend(amount: u32)

step Policy on SetLimit(admin: _, limit: n) -> n
step Ledger on Spend(amount: a) -> spent + a

# rce-version: 0.8
module login

intent "secrets are opaque (5.16): no literal can make one, no output can carry one, equality is the one release"
    example Enroll(pw: "s3cret"), Login(pw: "s3cret") -> ok == 1
    example Enroll(pw: "s3cret"), Login(pw: "guess") -> failed == 1

state Vault
    stored: Secret[text]? = none
    ok: u32 = 0
    failed: u32 = 0

event Enroll(pw: Secret[text])
event Login(pw: Secret[text])

step Vault on Enroll(pw: p)
    stored = some(p)
step Vault on Login(pw: p)
    if stored == some(p)
        ok += 1
    else
        failed += 1

module rcedb

intent "a keyed store written in RCE over the host's durable append (Appendix E.8): puts are state writes, a bound Synced event moves the durable mark, scans are in canonical key order"
    example Put(key: "b", val: "2"), Put(key: "a", val: "1"), Synced(upto: 1) -> durable == 1
    example Put(key: "k", val: "v"), Delete(key: "k") -> rows.len() == 0
    example Delete(key: "x") -> refused: Missing

state Db
    rows: Map[text, text] = {}
    writes: u64 = 0
    durable: u64 = 0

event Put(key: text, val: text)
event Delete(key: text)
event Synced(upto: u64)
event Scan(start: text)

error Missing(key: text)

struct Row
    key: text
    val: text

step Db on Put(key: k, val: v)
    rows[k] = v
    writes += 1
step Db on Delete(key: k)
    if not rows.contains(k)
        fail Missing(key: k)
    rows.remove(k)
    writes += 1
step Db on Synced(upto: n)
    if n > durable
        durable = n
step Db on Scan(start: f)
    var ks = rows.keys()
    ks.sort()
    for k in ks
        if k >= f
            let v = rows.get(k) catch ""
            emit Row(key: k.tostr(), val: v)

fn f() -> i64 = (x = 1)

fn f() -> i64
        let x = 1
    return x

fn f(a: i64) -> bool = 0 < a < 10

class Foo
    x: i64

fn f(a: bool) -> i64 = if a then 1

kind K
fn f() -> i64 = 1

intent "x"
    example Inc 1

state S
event E

state S
    n: i64 = 0
event E
step S E -> n

fn f() -> i64
	return 1

fn f(a: bool) -> i64 = if a then try g() else 0

fn f() -> text = "abc

fn f(s: &text) -> List[text]
    var out: List[text] = []
    with arena a
        let ws: List[text] @a = s.words()
        out = ws
    return out

fn f() -> i64
    let x = 1
    x = 2
    return x

fn f() -> &List[i64]
    let xs: List[i64] = [1]
    return &xs

fn main()
    with device gpu
        emit 1

extern "C" fn c_tick() -> u32

fn main()
    with device gpu
        let t = c_tick()

fn f(n: u64) -> u64
    with device gpu
        let xs: List[u64] = [n, n]
        return xs.len() as u64

extern "stdcall" fn c_f(n: u32) -> u32

fn main()
    emit c_f(1)

extern "C" fn c_rand() -> u32

fn roll() -> u32 = c_rand()

extern "C" fn c_take(xs: List[u8]) -> u32

fn main()
    emit c_take([1, 2])

extern "C" fn c_work(n: u32) -> u32

fn main()
    spawn c_work(3)

extern "C" fn c_name(n: u32) -> text

fn main()
    emit c_name(1)

fn f(x: f32) -> f32
    return x * 2.0

fn f(x: f32, y: f64) -> f32
    return x + y

fn f() -> i64
    fail 3

fn f(a: u8, b: i64) -> i64 = a + b

fn ticks(c: chan u64) -> iter u64
    yield 1

fn evens() -> iter u64
    yield 0

fn f() -> u64
    let it = evens()
    return 0

fn names() -> iter text
    yield 3

linear struct H
    id: i32

extern "C" fn c_close(h: H) -> i32

fn main()
    let h = H(id: 3)
    let g = copy(h)
    let _ = c_close(h)
    let _ = c_close(g)

linear struct H
    id: i32

struct Pair
    a: H
    b: i32

linear struct H
    id: i32

fn f(hs: List[H]) -> u64
    return 0

linear struct H
    id: i32

extern "C" fn c_close(h: H) -> i32

fn main()
    let h = H(id: 3)
    for i in 0..3
        let _ = c_close(h)

linear struct H
    id: i32

extern "C" fn c_close(h: H) -> i32

fn main()
    let h = H(id: 3)
    if h.id > 0
        let _ = c_close(h)

linear struct H
    id: i32

extern "C" fn c_close(h: H) -> i32

fn main()
    let h = H(id: 3)
    emit h.id

const LOOP_LIMIT: i64 = 10

fn f(x: i64) -> i64
    if x > 0
        return 1

fn f()
    var xs: List[i64] = [1, 2]
    for x in xs
        xs.append(x)

fn both(a: &mut List[i64], b: &List[i64])
    pass

fn bad()
    var xs: List[i64] = [1]
    both(&mut xs, &xs)

kind Light
    Red
    Green

fn f(l: Light) -> u8
    match l
        Red -> return 1

impl Eq for List[i64]
    fn eq(&self) -> bool = true

fn f(x: i64) -> i64
    emit x
    return x

fn countdown(n: u64) -> u64
    if n == 0
        return 0
    return countdown(n - 1)

kind Tree2
    Leaf2(v: i64)
    Node2(l: Box[Tree2], r: Box[Tree2])

fn loop_forever(t: &Tree2) -> i64
    match t
        Leaf2(v: v) -> return v
        Node2(l: l, r: r) -> return loop_forever(t)

fn f(n: u64) -> u64 = g(n)

fn g(n: u64) -> u64 = f(n)

fn f(a: chan u64)
    select
        recv some(x) from a -> pass
        after "soon" -> pass

fn f(a: [i32; 3], b: [i32; 4]) -> [i32; 3]
    return a + b

fn f(a: [text; 2], b: [text; 2]) -> [text; 2]
    return a * b

fn worker(c: chan i64, xs: &List[i64])
    c <- 1

fn main()
    let c = chan[i64](1)
    let xs: List[i64] = [1]
    spawn worker(c, &xs)

state S
    n: u64

event E

step S on E -> n

fn f(s: &text) -> bool
    return s[0] == "a"

fn f(a: u64, b: i64) -> u64
    return a + b

error E

fn g() -> i64 ! E
    fail E

fn f() -> i64 = g()

state Counter
    n: u64 = 0

event Inc
event Dec

step Counter on Inc -> n + 1

fn f() -> i64 = y + 1

state S
    n: u64 = 0

event E

step S on E -> n + 1
step S on E -> n + 2

fn f() -> i64
    let unsafe = 1
    return unsafe

fn take(s: text) -> u64 = s.len() as u64

fn twice(s: text) -> u64
    let a = take(s)
    return a + take(s)

fn f() -> u64
    yield 1
    return 0

fn build(n: u64) -> u64
    var k: u64 = 0
    with arena a bound 16
        let xs: List[u64] @a = [n, n, n, n, n, n, n, n, n, n]
        k = xs.len() as u64
    return k

check build(12345) == 10

check "héllo"[0:2] == "h"

const N: usize = 12

fn f() -> usize
    comptime
        check N % 8 == 0
    return N

const BIG: u8 = 200 + 100

check (1e39 as f32) as f64 > 0.0

intent "fib"
    check fib(10) == 56

fn fib(n: u32) -> u64
    var a: u64 = 0
    var b: u64 = 1
    for _ in 0..n
        let t = a + b
        a = b
        b = t
    return a

intent "guard trap refuses (S1)"
    example Go(d: 0) -> 1

state S
    n: i64 = 1

event Go(d: i64)

step S on Go(d: d) if 10 / d > 1 -> n + 1
step S on Go(d: _) -> n

const LOOP_LIMIT: u64 = 100

fn naturals() -> iter u64
    var i: u64 = 0
    loop
        yield i
        i += 1

check naturals().collect().len() == 5

fn f() -> u8 = 300

intent "x"
    check spin() == 0

fn spin() -> u64
    var k: u64 = 0
    while true bound 10
        k += 1
    return 0

const LOOP_LIMIT: u64 = 10

fn count(n: u64) -> u64
    var k: u64 = 0
    while k < n
        k += 1
    return k

check count(20) == 20

state S
    n: u8 = 255 + 1

event E

step S on E -> n

fn sub(a: u64, b: u64) -> u64
    return a - b

check sub(0, 1) == 0

intent "counter"
    example Dec -> 0

state Counter
    n: u64 = 0

event Dec

step Counter on Dec -> n - 1

intent "counter"
    example Inc, Inc -> 3

state Counter
    n: u64 = 0

event Inc

step Counter on Inc -> n + 1

intent "counter"
    example Dec -> refused: Other

state Counter
    n: u64 = 0

event Dec

error Underflow
error Other

step Counter on Dec -> try n.checked_sub(1) else Underflow