Testing and Trust#

I distinguish tests, static checks, and proofs. They answer different questions.

Shadows#

A shadow is an executable test attached to a function:

fn double(value: int) -> int {
    return (* value 2)
}

shadow double {
    assert (== (double 0) 0)
    assert (== (double 3) 6)
}

During ordinary compilation I run dependency shadows before root shadows. My C seed uses a supervised interpreter child, selecting the shared VM bridge for imported callback shadows. My bytecode CLI executes a separate verified test module; my self-hosted native driver uses a separate test executable. --root-shadows-only narrows the selection. Source-only C emission does not run shadows. Deadlines supervise execution; they are not a security sandbox. A shadow tests the cases it executes; it does not prove the function for every input.

Compiler enforcement and project policy differ:

• The compiler normally warns about a missing shadow.
• It exempts extern functions, main, generated lambdas, GPU functions, and functions that call externs.
• Repository policy requires a useful shadow for every added or changed non-extern named function when it can be tested.

Property Tests and Coverage#

Property tests sample generated values and can shrink failures. Sampling is not exhaustive verification. Coverage reports which code executed; it does not establish correctness.

Contracts#

requires checks preconditions and ensures checks postconditions at their implemented boundary. A successful runtime check says that condition held for that execution.

Formal Verification#

My Coq development proves stated metatheory for a defined core model. It does not automatically prove every backend, foreign call, allocator, module, or user function.

Use the trust report to inspect the boundary:

./bin/nanoc program.nano --trust-report

Say proved only for a checked theorem in its stated model, tested only for behavior exercised by a named test, and assumed for unchecked platform or foreign behavior.

NSI, the POSIX fabric, effects-to-policy, and the trap journal are tested libraries. They are not in the Coq NanoCore subset. The journal API is not hooked into every NanoVM trap in 4.5. See Secure Runtime.

Useful Checks#

make test
make userguide-check
make check-stdlib-docs
python3 scripts/check_markdown_links.py