Broken promises

fn percent(part: int, whole: int) -> int {
    assert(whole > 0)
    return part * 100 / whole
}

fn share(done: int, total: int) -> int {
    return percent(done, total)     // hands the duty on to its caller
}

fn at_least_zero(n: int) -> int {
    return 0 if n < 0
    assert(n >= 0)                  // a claim about the result
    return n
}

fn per_row(rows: int) -> int {
    let r = at_least_zero(rows) + 1
    return percent(50, r)           // r >= 1: proved, no check
}

fn main() {
    println(f"{per_row(4)}% {share(3, 4)}%")
    // and this call breaks it:
    println(f"{share(1, 0)}%")
}

$ nikaia build
error[NK1207]: This call breaks `share`'s precondition `total > 0` every time it is reached.
   --> …/pre/src/main.nika:24:5
    |
 24 |     println(f"{share(1, 0)}%")
    |     ^^^^^^^^^^^^^^^^^^^^^^^^^^
    |
    = note: Here `total` is 0.
    = note: The precondition is `assert(whole > 0)` in `percent`, carried back to `share`'s entry.
    = help: Pass `share` arguments for which `total > 0` holds, or check them with a guard before the call.
1 claim shown false

fn fib(n: int) -> int {
    let mut a = 0
    let mut b = 1
    for _ in 0..<n {
        let next = a + b
        a = b
        b = next
    }
    return a
}

fn main() {
    assert(fib(10) == 54)
    println(f"{fib(10)}")
}

$ nikaia build
error[NK1207]: `fib(10) == 54` is false every time it is reached.
   --> …/fib/src/main.nika:13:5
    |
 13 |     assert(fib(10) == 54)
    |     ^^^^^^^^^^^^^^^^^^^^^
    |
    = note: What is known before it rules the claim out: no value of its own; the claim is false as written.
    = note: `fib(10)` is 55, run while the program was built.
    = help: If the claim is right, the code before it is wrong; if the code is right, the claim is.
1 claim shown false

use std::process

fn main() throws {
    let out = process::run("git", ["rev-parse", "HEAD"])
    let n: int = out.stdout.len()
    assert(n == 41)
    println(f"commit {out.stdout.trim()}")
}

$ nikaia build
error[NK1202]: `n == 41` is a claim about data from outside the program.
  --> …/outa/src/main.nika:6:5
   |
 6 |     assert(n == 41)
   |     ^^^^^^^^^^^^^^^
   |
   = note: `n` comes from outside the program, so nothing the compiler can see says what it holds.
   = note: That it is wrong is a case the program has to handle, not a defect an `assert` catches.
   = help: Check it where it arrives, with a guard the program handles: `throw BadInput(n) if !(n == 41)`, or `return … if !(n == 41)`. After that line, this `assert` is proved.
1 type error

use std::process

fn main() throws {
    let out = process::run("git", ["rev-parse", "HEAD"])
    let n: int = out.stdout.len()
    if n != 41 {
        println("not a commit id")
        return
    }
    assert(n == 41)
    println(f"commit {out.stdout.trim()}")
}

$ nikaia build --asserts
asserts in …/outb/src/main.nika: 1 - not proved 0 (refused 0, checked at run time 0, checked by a test 0); checked where the words arrive 0; proved 1 (proved 1, preconditions proved at every call 0)
  …/outb/src/main.nika:10  assert(n == 41)  proved
$ target/nikaia/bin/outb
commit 7e84ae5c523c8b9937bb4faacc6d029bf49d4f75

/// Divides 100 by a, a few times.
fn main(a: int; times: int = 4) {
    assert(a > 0)
    for i in 0..<times {
        println(f"{i}: {100 / a}")
    }
}

$ nikaia build --asserts
asserts in …/mainp/src/main.nika: 1 - not proved 0 (refused 0, checked at run time 0, checked by a test 0); checked where the words arrive 1; proved 0 (proved 0, preconditions proved at every call 0)
  …/mainp/src/main.nika:3  assert(a > 0)  precondition of `main`, checked where the words arrive
$ ./mainp 5 --times 2
0: 20
1: 20
$ ./mainp 0
error: `a` is 0, which breaks `main`'s precondition `a > 0`.
usage: mainp [--times <int>] <a>
For more, try `mainp --help`.
$ echo $?
2
$ ./mainp five
error: `a` is an `int`, and `five` is not one.
usage: mainp [--times <int>] <a>
For more, try `mainp --help`.
$ ./mainp --help
mainp
Divides 100 by a, a few times.

usage: mainp [--times <int>] <a>

arguments:
  <a>                  int; requires `a > 0`

options:
  --times <int>        int, default 4
  -h, --help           prints this help