vyre-conform 0.1.0

Conformance suite for vyre backends — proves byte-identical output to CPU reference
Documentation 
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74

# Coverage Overview

Coverage in vyre-conform does not mean "how many tests ran." It means how much
of the input space is proven, partitioned, or explicitly represented by the
suite. Ten million random inputs from one easy class can still be poor
coverage. One representative from every class plus every boundary can expose
bugs that random volume misses.

## Equivalence Class Coverage

Equivalence classes partition an operation's input space into semantic regions.
Coverage requires at least one representative from each declared class. For
division, divisor zero and divisor nonzero are different classes. For masked
shift, amounts around `31`, `32`, and `33` are structurally important.

Class coverage is:

```text
covered_equivalence_classes / total_equivalence_classes
```

## Boundary Value Coverage

Boundary values are explicit edge inputs. Every declared boundary must be run.
Missing a boundary is a coverage failure even if many random tests passed.

Boundary coverage is:

```text
covered_boundary_values / total_boundary_values
```

## Law Coverage

Law coverage records which declared laws were verified and at which strength:
exhaustive, witnessed, or combined. A law is fully covered for L2 only when it
passes the required exhaustive small-domain check and witnessed full-domain
check.

Law coverage is:

```text
fully_verified_laws / total_declared_laws
```

## Regression Coverage

Every persisted regression must be replayed. A skipped regression is a coverage
hole because it is a known historical failure mode.

Regression coverage is:

```text
replayed_regressions / total_regressions
```

## Overall Metric

The overall coverage score is the minimum of the required dimensions, not the
average:

```text
overall =
  min(
    equivalence_class_coverage,
    boundary_value_coverage,
    law_coverage,
    regression_coverage
  )
```

The minimum prevents a large number of easy tests from hiding a missing class,
missing boundary, unverified law, or skipped regression. A certificate should
also publish the component scores so readers can see exactly what was covered.