Verification
The repository separates fast development checks from finite, reproducible conformance claims. Passing a corpus proves only the declared formats, operations, rounding modes, targets, and fixture revisions.
Verification Layers
| Layer | Command | Purpose |
|---|---|---|
| Documentation | just docs | Locale/file/heading/link checks plus executable documentation examples |
| Formatting | just fmt | MoonBit formatter |
| Pull request | just pr [jobs] | Generated interfaces, all-target checks, native tests, Python tests, smoke corpora |
| IEEE decimal | just gate decimal [jobs] | Checked-in decimal32/64/128 DPD/BID vectors across supported targets |
| GDA decimal | just gate decimal_gda [jobs] | Pinned official and official0 .decTest legal scalar rows |
| Binary | just gate binary [jobs] | Pinned TestFloat level-1 matrix and MPFR data |
| Interval | just gate interval [jobs] | Pinned ITF1788 strict supported phases |
| Complete | just ci [jobs] | All generated-interface, target, unit, and conformance gates |
Run the narrowest relevant check first, then broaden before release.
Shared Conformance Runner
All suites use one dispatcher:
just conformance <build|run|smoke|plan|fetch> \
<decimal|decimal_gda|binary|interval> [options]decimal means the independent IEEE decimal corpus; decimal_gda means GDA .decTest. binary combines TestFloat and MPFR sources. interval uses ITL.
smoke runs committed fixtures without downloading external corpora. plan shows deterministic tasks. fetch verifies pinned provenance before installing ignored data below .tmp/. run executes the chosen suite. Backend-specific filters, phases, targets, strict mode, sharding, and JSON output are documented under testdata/*/README.md.
Published Claims
- GDA: all 64,986 legal executable scalar rows in the 144-file
officialcorpus pass; all 16,124 legal rows inofficial0pass. The 141#placeholder/non-scalar invalid rows are diagnostic exclusions, not unsupported legal behavior. - Binary: 7,461,360 TestFloat vectors cover binary16/32/64/128 add, subtract, multiply, divide, and square root, five rounding directions, and both tininess modes. The pinned MPFR square-root dataset adds 1,055 rows.
- IEEE decimal: committed decimal32/64/128 DPD and BID fixtures cover encoding, special values, flags, core arithmetic, and all 1,024 DPD declets on native, Wasm, Wasm-GC, and JavaScript. LLVM is excluded from this gate.
- Interval: the strict ITF1788 phases cover declared set, relation, observation, arithmetic, cancellation, elementary, power, trigonometric, FMA, integer-power, and extrema operations. Reverse operations remain unsupported.
These are finite claims. They do not imply every IEEE 754 or IEEE 1788 operation, arbitrary resource sizes, every NaN payload policy, or unpinned future corpus revisions.
Reproducibility
External artifacts are revision- and SHA-256-pinned in corpus manifests. Builds use backend-named outputs and isolated target directories so parallel jobs do not overwrite one another. Shards select deterministic case indices, and merged summaries retain exact totals and failed IDs.
The MoonBit frontend parses and executes numeric rows. Python orchestrates downloads, task planning, subprocesses, target selection, and aggregation. An optional oracle is never silently replaced by a weaker implementation; missing requirements must be reported explicitly.
Performance evidence is separate from semantic conformance. Benchmark manifests pin baseline source, dependencies, toolchain, target, schedule, sample count, and dispersion limits. A performance threshold never changes correctness.
Failure Triage
- Re-run the failing backend with the smallest case, ID filter, phase, or shard that reproduces it.
- Distinguish parse diagnostics, unsupported cases, legacy classifications, executable mismatches, and infrastructure failures.
- Record expected value, actual value, flags, context, target, corpus revision, and command.
- Run the matching white-box package test to decide whether the defect is in parsing, arithmetic, interchange, or aggregation.
- After a fix, run the focused case, committed smoke fixture, backend gate, and finally
just prorjust cias appropriate.
Do not weaken strict support, discard flags, or change the denominator to make a failing gate pass.
Release Gate
Before publishing:
- align
moon.mod, root README, localized indexes, standards, and changelog; - run
just docsand inspect generated interface differences; - run
just prduring iteration; - run
just cifor the release candidate; - publish through the repository GitHub Actions workflow.
Local moon publish is not the Luna-Flow release path because organization credentials are supplied by the workflow.