#veri

#Use as a dependency

moon add mizchi/veri

import {
  "mizchi/veri/bounds",
}

options("proof-enabled": true)

pub fn digit(value : Int) -> Int  {
  proof_ensure: result => 0 <= result && result <= 9,
} {
  @bounds.clamp(value, 0, 9)
}

test "clamp includes its upper bound" {
  assert_eq(digit(10), 9)
}

moon test --target js
moon prove

#Verify the repository

just setup-solvers # Install the additional prover locally (network needed once)
just doctor        # Check versions and bundled Why3 data
just verify        # Run proofs, negative controls, reference checks, and backend tests

just prove         # Prove both workspace modules: MoonBit → Why3 → SMT
just prove-machine # Prove bounds, runtime bridges, and their example with machine integers
just prove-collections-machine # Prove collection implementations and clients with machine integers
just prove-foundations-machine # Prove order, arithmetic, real and IEEE error contracts with machine integers
just core-capabilities # Probe direct calls to core from contracted functions
just conversion-capabilities # Probe native numeric casts and UInt16 support
just array-capabilities # Report old-state/snapshot support and mutable-alias rejection
just smt           # UNSAT proofs and SAT witnesses for FP, bitvectors, arrays, and strings
just negative      # Check that deliberately false claims in each model are not proved
just negative bitvector runtime/uint32 runtime/uint64 # Select affected negative controls
just test js       # Run runtime checks
just quickcheck js # Run only the QuickCheck properties
just bench native # Compare collections with core; save timings and ratios
just bench-backends # Run the comparisons sequentially on all four backends
just bench-check native 1.0 # Fail unless both measurement orders meet the ratio limit
just test-backends # JS / wasm / wasm-gc / native
just test-release  # Run the same checks in optimized builds
just fp-capabilities # Report native Float/Double proof-lowering support
just vectors       # Regenerate expected results from Z3
just vectors-check # Compare checked-in reference values with the current Z3 results
just fmt           # Format sources and generate public interfaces
just package-check # Execute and prove both README quickstarts from the package ZIP

#Structure and guarantees

veri/
├── moon.mod                 # mizchi/veri
├── moon.work                # members: ".", "examples"
├── bounds/
├── bitvector/
├── encoding/
├── algebra/
├── graph/
├── arrays/
├── strings/
├── fset/
├── seq/
├── list/                    # laws, indexed, conversions
├── bag/
├── fmap/
├── bintree/
├── ieee754/
├── integer/
├── runtime/                 # numeric/text bridges and collection implementations
├── testing/commands/
└── examples/
    ├── moon.mod             # mizchi/veri-examples; imports mizchi/veri@0.1.0
    ├── models/
    ├── bridges/
    ├── floating/
    ├── collections/
    └── toolkit/

// Import mizchi/veri/ieee754 and enable proof-enabled in moon.pkg.
// Place the following in a .mbtp file.
lemma adding_nan_is_nan(x : @ieee754.Float64, y : @ieee754.Float64)  {
  proof_require: @ieee754.is_nan(x),
  proof_ensure: @ieee754.is_nan(
    @ieee754.add(@ieee754.nearest_even(), x, y),
  ),
} {}

#Bitvector API

using @bitvector {type Bv8, type Bv16, type Bv32, type Bv64}

#Checked arithmetic, codecs, algebra and graphs

#Orders, number theory, reals, and error bounds

• binary32: 2^-24 * |z| + 2^-150
• binary64: 2^-53 * |z| + 2^-1075

#Runtime collection API

// Import "mizchi/veri/runtime/queue".
test "persistent queue and Iter" {
  let original : @queue.Queue[Int] = @queue.Queue::new()
  let queue = original.push(1).push(2)
  assert_true(original.is_empty())
  assert_eq(queue.iter().map(x => x * 2).to_array(), [2, 4])
}

#FixedArray updates and ranges

// Import "mizchi/veri/runtime/array".
test "range updates" {
  let xs : FixedArray[Int] = [0, 1, 2, 3]
  assert_true(@array.fill(xs, 9, { start: 1, count: 2 }))
  assert_true(@array.copy_within(xs, { start: 0, count: 3 }, 1))
  assert_eq(xs, [0, 0, 9, 9])
}

#QuickCheck properties

test "quickcheck: wrapping roundtrip" {
  @quickcheck.check(
    (input : (UInt, UInt)) => {
      let (value, delta) = input
      @uint32.sub(@uint32.add(value, delta), delta) == value
    },
    count=1000,
    seed=20260914,
  )
}

#Collection benchmarks

#Collection models and implementations

#Binding architecture

MoonBit contracts / .mbtp → Why3 theories → SMT-LIB 2 → Z3 / CVC5
checks/**/*.smt2 ─────────────────────────→ SMT-LIB 2 → Z3

#Correspondence with MoonBit runtime types

model(add(x, y)) = bv.add(model(x), model(y))
model(sub(x, y)) = bv.sub(model(x), model(y))
less(x, y)       = bv.ult(model(x), model(y))

// Import mizchi/veri/runtime/uint32 and mizchi/veri/runtime/text.
test {
  assert_eq(@uint32.add(0xffffffffU, 1U), 0U)
  let text = @text.from_string("A😀é").unwrap()
  assert_eq(text.length(), 3)
  assert_eq(text.substring(1, 2).to_string(), "😀é")
}

#Proof encodings and package boundaries

#Scope of IEEE 754 verification

// Import mizchi/veri/runtime/float32 and mizchi/veri/runtime/float64.
test {
  let one = @float32.from_bits(0x3f800000U)
  let half_ulp = @float32.from_bits(0x33800000U)
  assert_true(@float32.matches(@float32.add(one, half_ulp), Bits(0x3f800000U)))
  let wide = @float32.to_double(one)
  assert_true(@float64.matches(wide, Bits(0x3ff0000000000000UL)))
}

a = 2^53, b = -2^53, c = 0.5, rounding mode RNE

(a + b) + c = 0.5
a + (b + c) = 0.0

#Trusted boundary and limitations

• The type mappings, argument order, and Why3 symbol mappings in #proof_external / #proof_import, along with Why3, the solver, and MoonBit's translation, are trusted. No custom proof_axiomatized declarations are used.
• Default integer proofs use mathematical integers. Bounds, unsigned wrapping adapters, FixedArray reads and updates, collections, strings, and their examples are also proved separately with the bundled machine-integer model. min <= max for clamp and lower < upper for clamp_half_open are caller preconditions, not runtime input checks.
• The runtime check profile is binary32 and binary64 with RNE. The logical API exposes five rounding modes, but runtime configuration and testing of all modes are not implemented.
• NaN payloads, signaling versus quiet NaNs, exception flags, traps, decimal formats, runtime FMA, and floating-point string conversions are not checked. SMT-LIB's FP theory itself does not distinguish signaling from quiet NaNs.
• Transcendental functions such as sin / exp, and proofs of error bounds relative to real-valued algorithms, require separate work.
• unknown and timeouts mean unproved; they do not establish truth or falsity. Positive SMT checks fail unless the expected unsat result is returned. The negative control only checks that a false theorem remains unproved; it does not claim that the solver produced a counterexample.
• Use just prove to verify both workspace modules, rather than relying only on targeted proofs that assume dependency packages.
• The project currently uses the local toolchain. Pinning toolchain distributions and solver versions for shared CI remains future work.

#References

• MoonBit Formal Verification: Contracts, external theories, and the trust model.
• FSet in moonbit-community/verified: A reference for importing finite-set models. This repository provides its own small binding API and usage examples.
• A practical example of MoonBit formal verification (Japanese): Integer contracts, differences from runtime behavior, and floating-point differential tests.
• Why3 ieee_float: Logical IEEE types and operations.
• Why3 standard library: Sources for the sequence, list, bag, finite-map, tree, stack, queue, and priority-queue specifications. The bundled files determine the available theories.
• SMT-LIB FloatingPoint: IEEE FP operations, rounding modes, and the scope of NaN representation.
• Berkeley TestFloat / SoftFloat: Arithmetic conformance testing and a software reference implementation.

• Z3 Guide: Bitvectors: Fixed widths, signed/unsigned operations, and modular arithmetic.
• Z3 Guide: Arrays: Select/store and extensional arrays.
• Z3 Guide: Strings: String operations and Unicode semantics.

#License