Testing

Warp: one property, every case

Warp is the test framework built into Jacquard. Property testing, exhaustive checking, fault simulation and test caching usually come from separate libraries. In Warp they come from two things the language already has: handlers, and identity by hash.

A property finds a bug

This function decides how many boxes hold n items, twelve to a box. The property says every item gets a box. A generator is just a probability distribution: UniformInt(0, 1000).

-- How many boxes hold n items, twelve to a box.
boxes-needed : (Int) ->{} Int
boxes-needed(n) = div(n, 12)

boxes-suite =
  Group("boxes", [
    Case("a dozen fits in one box", fn () ->
      check.eq(boxes-needed(12), 1, int.eq, int.show, "boxes for 12")),

    Prop("every item gets a box", fn () -> {
      let items = sample(UniformInt(0, 1000))
      check.true(
        lt(sub(items, 1), mul(boxes-needed(items), 12)),
        text.concat("enough boxes for ", text.from-int(items)))
    })
  ])

$ jac test boxes.jac --seed 7 --no-cache
PASS boxes-suite/boxes/a dozen fits in one box (1 check)
FAIL boxes-suite/boxes/every item gets a box (prop: falsified on case 1 of 100, seed 7; shrunk to 1 choice [493])
  - enough boxes for 493
1 passed, 1 failed, 0 skipped, 0 refused
[exit status 1]

Sampling is seeded, so the failure is reproducible. Rounding down loses the leftover items.

The same property, over every case

Because a generator is a distribution, Warp can enumerate it instead of sampling it. Add one flag and the same property, unchanged, runs on all 1,001 inputs. It reports the first failure in order, the simplest one there is:

$ jac test boxes.jac --exhaustive --no-cache
PASS boxes-suite/boxes/a dozen fits in one box (1 check)
FAIL boxes-suite/boxes/every item gets a box (prop: falsified exhaustively)
  - enough boxes for 1
1 passed, 1 failed, 0 skipped, 0 refused
[exit status 1]

Round up instead:

-boxes-needed(n) = div(n, 12)
+boxes-needed(n) = div(add(n, 11), 12)

$ jac test boxes-fixed.jac --seed 7 --no-cache
PASS boxes-suite/boxes/a dozen fits in one box (1 check)
PASS boxes-suite/boxes/every item gets a box (prop: 100 cases, seed 7)
2 passed, 0 failed, 0 skipped, 0 refused

$ jac test boxes-fixed.jac --exhaustive
PASS boxes-suite/boxes/a dozen fits in one box (1 check)
PASS boxes-suite/boxes/every item gets a box (verified exhaustively (1001 cases))
2 passed, 0 failed, 0 skipped, 0 refused
cache: 0 hit, 2 ran

“Verified exhaustively” means every value the generators can produce: here, every count from 0 to 1,000. It is a complete check of that range, not a proof about every integer.

Every combination of faults

Code that talks to the outside world asks flaky, an operation of the Fault effect, whether a step should fail. In production a handler answers no. In a test, fault.all answers both yes and no at every site, resuming the rest of the program once for each answer. So a test can check every combination of failures, not just the ones someone thought to script.

-- Read the config from the primary, fall back to the replica, then to defaults.
read-config : () ->{Fault} Text
read-config() =
  if flaky("primary") then
    if flaky("replica") then "defaults" else "from replica"
  else
    "from primary"

config-suite =
  Group("config", [
    Case("every fault combination still yields a config", fn () ->
      match throw.to-result(fn () -> fault.all(fn () -> read-config(), 8)) {
        | Ok(outcomes) ->
            check.eq(
              text.join-list(outcomes, ", "),
              "from primary, from replica, defaults",
              text.eq,
              text.show,
              "outcomes")
        | Err(_) -> check.true(False, "fault budget exceeded")
      })
  ])

$ jac test faults.jac --no-cache
PASS config-suite/config/every fault combination still yields a config (1 check)
1 passed, 0 failed, 0 skipped, 0 refused

The three outcomes are every path through the two fault sites: the primary works; the primary fails and the replica works; both fail. With n sites, fault.all explores up to 2ⁿ executions, within a budget you set.

Tests that know when they don't need to run

A test's result is stored under the hash of the test, and that hash covers everything the test calls. Run the suite again and nothing reruns:

$ jac test boxes-fixed.jac --exhaustive
PASS boxes-suite/boxes/a dozen fits in one box (1 check) [cached]
PASS boxes-suite/boxes/every item gets a box (verified exhaustively (1001 cases)) [cached proof]
2 passed, 0 failed, 0 skipped, 0 refused
cache: 2 hit, 0 ran

Now an agent reformats the file, rewrites the comment and renames the variables. Every hash is unchanged, so the proof still stands:

$ jac test boxes-fixed-reformatted.jac --exhaustive
PASS boxes-suite/boxes/a dozen fits in one box (1 check) [cached]
PASS boxes-suite/boxes/every item gets a box (verified exhaustively (1001 cases)) [cached proof]
2 passed, 0 failed, 0 skipped, 0 refused
cache: 2 hit, 0 ran

Change boxes-needed itself and exactly the tests that depend on it run again. No dependency tags or affected-target rules are needed; a changed hash is the whole signal.

What you would otherwise assemble

Also in Warp

• World tests run code against scripted or recorded handlers, with strict replay of a recorded run.
• Probabilistic checks compare a model's exact posterior with what you expect. The worlds tour runs one.
• Schedule testing: --schedules N --seed S reruns concurrent tests under reproducible interleavings.
• Relational checks: jac relate reruns a program under a varied schedule, secret or grant and compares what it observes.
• Coverage by definition hash: --coverage.

Limits

• Exhaustive results are exhaustive only within the declared generators and budget.
• A failing sample is shrunk by editing the recorded random choices, which keeps every candidate valid. In 0.3.0 the shrinking is basic, as the sampled run above shows; --exhaustive is the reliable way to find the smallest failure in a small range.
• The sampling driver ignores observe, so a property that conditions its generator only means what it says under --exhaustive.

Every output on this page is recorded from Jacquard 0.3.0 and re-checked by scripts/verify_examples.sh. The full reference is docs/warp-testing.md.