counter.deed

// A Deed program that actually runs. `deed test examples/counter.deed` executes
// the tests at the bottom.
//
// examples/transfer.deed could not run when this was written. It named types and
// handlers that lived in modules the compiler had no way to load, and `Result`
// was on that list too, which is why `Result` is part of the language rather
// than a library. Cross module loading arrived later and transfer.deed runs its
// own tests now.

module examples/counter

// A refinement. `bump(0)` and `bump(-1)` are not writable.
type Positive = Int where value > 0

choice CounterError {
    OverLimit { limit: Int },
}

// An effect declares operations and nothing else.
effect Counter {
    fn value() -> Int
    fn bump(by: Positive) -> ()
}

// A handler implements them. `state` is the only mutable thing in the
// language, and only a handler can have it.
handler InMemory implements Counter {
    state count: Int

    fn value() -> Int {
        count
    }

    fn bump(by) -> () {
        count = count + by
    }
}

// A handler that accepts writes and ignores them, which is enough to make a
// function break its own postcondition. There is a test for that in the Rust
// suite, since a file of tests that are supposed to fail cannot live here.
handler Frozen implements Counter {
    state count: Int

    fn value() -> Int {
        count
    }

    fn bump(by) -> () {}
}

// The contract is the review surface. `old(...)` is the value on entry, and
// the compiler checks the effect row against what the body actually performs.
fn bump_twice(by: Positive) -> Int
  where
    by > 0,
  uses
    Counter.bump,
    Counter.value,
  ensures
    ok  => Counter.value() == old(Counter.value()) + by + by,
{
    Counter.bump(by)
    Counter.bump(by)
    Counter.value()
}

// A pure function with a postcondition. `result` is what the function
// returned, and it is the only name besides `value` that the language
// introduces on its own.
//
// Without it a pure function could not have a postcondition at all, since its
// return value is the only thing it produces.
fn clamp(n: Int, limit: Positive) -> Int
  ensures
    ok  => result <= limit,
    ok  => result == n || result == limit,
{
    if n > limit {
        return limit
    }
    n
}

// Reading changes nothing, and `unchanged` says so. It compares the state of
// the handler installed for `Counter` before and after the call.
fn peek() -> Int
  uses
    Counter.value,
  ensures
    ok  => unchanged(Counter),
{
    Counter.value()
}

// Failure is a value. `Result`, `ok` and `err` are part of the language, so a
// function can fail without importing anything.
//
// The `err` obligation is the interesting one: on the failing path the counter
// must not have moved, and that is checked when the function actually fails.
fn bump_within(by: Positive, limit: Int) -> Result<Int, CounterError>
  uses
    Counter.bump,
    Counter.value,
  ensures
    err => unchanged(Counter),
{
    if Counter.value() + by > limit {
        return err(OverLimit { limit })
    }
    Counter.bump(by)
    ok(Counter.value())
}

// `?` returns the error case and unwraps the success case, so the bump below
// it never happens when the first call fails.
fn bump_within_then_force(by: Positive, limit: Int) -> Result<Int, CounterError>
  uses
    Counter.bump,
    Counter.value,
{
    bump_within(by, limit)?
    Counter.bump(by)
    ok(Counter.value())
}

// Or handle the failure here. Both cases need an arm, and a wildcard is
// rejected, so the failure case cannot be swallowed by accident.
//
// The field is bound as `reached` rather than `limit` because `limit` is
// already a parameter and Deed does not allow shadowing. The first version of
// this function was rejected for exactly that.
fn bump_or_limit(by: Positive, limit: Int) -> Int
  uses
    Counter.bump,
    Counter.value,
{
    match bump_within(by, limit) {
        ok(count) => count,
        err(OverLimit { limit: reached }) => reached,
    }
}

test "bumping twice adds twice" {
    with InMemory { count: 0 } {
        assert bump_twice(5) == 10
        assert Counter.value() == 10
    }
}

test "bumping starts from whatever the handler was given" {
    with InMemory { count: 100 } {
        assert bump_twice(1) == 102
    }
}

test "reading leaves the counter alone" {
    with InMemory { count: 7 } {
        assert peek() == 7
        assert peek() == 7
        assert Counter.value() == 7
    }
}

test "a frozen counter never moves" {
    with Frozen { count: 3 } {
        assert Counter.value() == 3
        assert peek() == 3
    }
}

test "a bump within the limit succeeds" {
    with InMemory { count: 0 } {
        assert bump_within(5, 100) == ok(5)
        assert Counter.value() == 5
    }
}

test "a bump over the limit fails and leaves the counter alone" {
    with InMemory { count: 99 } {
        assert bump_within(5, 100) == err(OverLimit { limit: 100 })
        assert Counter.value() == 99
    }
}

test "the question mark stops the rest of the body" {
    with InMemory { count: 100 } {
        assert bump_within_then_force(1, 100) == err(OverLimit { limit: 100 })
        // The unconditional bump after the `?` never ran.
        assert Counter.value() == 100
    }
}

test "a match can handle the failure instead of propagating it" {
    with InMemory { count: 0 } {
        assert bump_or_limit(5, 100) == 5
    }
}

test "and the failing arm gets the error it was given" {
    with InMemory { count: 100 } {
        assert bump_or_limit(5, 100) == 100
        assert Counter.value() == 100
    }
}

test "clamping keeps its promise both ways" {
    assert clamp(3, 10) == 3
    assert clamp(30, 10) == 10
}