|
| 1 | +# VERIFY — fpRust |
| 2 | + |
| 3 | +How an agent launches, checks, drives, and cleans up verification of this |
| 4 | +library. Read this plus the relevant `features/*.md` file before touching the |
| 5 | +code. |
| 6 | + |
| 7 | +`source_commit: 18a96af` · `last_verified_at: 2026-09-23` · `verification_status: passed` |
| 8 | + |
| 9 | +## Launch |
| 10 | + |
| 11 | +```bash |
| 12 | +cd <repo root> |
| 13 | +cargo test |
| 14 | +``` |
| 15 | + |
| 16 | +Runs 120 unit tests (in-module `#[test]` blocks under `src/`) plus 24 doc |
| 17 | +tests — ~10s total. `test.sh` and `paralleltest.sh` are legacy wrappers; |
| 18 | +`cargo test` is the canonical surface. `clippy.sh` runs the linter. |
| 19 | + |
| 20 | +## Doctor |
| 21 | + |
| 22 | +```bash |
| 23 | +cargo test maybe::test_maybe -- --exact # smoke: ~1s (name a real test) |
| 24 | +cargo build |
| 25 | +``` |
| 26 | + |
| 27 | +A healthy tree: smoke test PASS, `cargo build` clean, full suite |
| 28 | +`120 passed; 0 failed` + `24 passed` doc tests. |
| 29 | + |
| 30 | +## Drive |
| 31 | + |
| 32 | +- Per feature: run `cargo test <module>::` (e.g. `cargo test fp::`) from the |
| 33 | + feature file's Drive section. |
| 34 | +- For behavior not covered by a test, write a scratch driver **outside** the |
| 35 | + repo: `cargo new /tmp/fprust-driver`, add to its `Cargo.toml`: |
| 36 | + |
| 37 | + ```toml |
| 38 | + [dependencies] |
| 39 | + fp_rust = { path = "<repo root>" } |
| 40 | + futures = "0.3" |
| 41 | + ``` |
| 42 | + |
| 43 | + then `cargo run` — never add driver files inside the repo. |
| 44 | + |
| 45 | +## Evidence |
| 46 | + |
| 47 | +- Save `cargo test <module> -- --nocapture` output to files under a scratch |
| 48 | + dir (e.g. `/tmp/fprust-evidence/`). |
| 49 | +- For scratch drivers, record the driver source plus its stdout. |
| 50 | + |
| 51 | +## When a check fails |
| 52 | + |
| 53 | +Classify before fixing — four different failures need four different repairs: |
| 54 | + |
| 55 | +| Class | Meaning | Repair | |
| 56 | +| --- | --- | --- | |
| 57 | +| Product regression | Library behavior changed for the worse | Report; do not edit the map or tests to match | |
| 58 | +| Doc drift | The map/VERIFY.md no longer matches the library | Update the doc; the product is fine | |
| 59 | +| Spec/oracle error | The acceptance spec or test expectation is wrong | Oracles are read-only; propose the change for review | |
| 60 | +| Harness failure | Toolchain, cargo, target/, or environment broke | Fix the harness; the product is fine | |
| 61 | + |
| 62 | +Never "fix" a failing check by editing the map or a test to describe the new |
| 63 | +behavior — that hides product regressions. If the new behavior is intentional, |
| 64 | +the map/test update is a separate reviewed change. |
| 65 | + |
| 66 | +## Cleanup |
| 67 | + |
| 68 | +- Remove scratch driver dirs and evidence dirs you created. |
| 69 | +- `git status` must show no modifications inside the repo. |
0 commit comments