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

# InsertBits

## Signature

primitive.bitwise.insert_bits: binary `u32, u32 -> u32` where first operand packs `offset`, `count`, and `newbits`; second operand is `original`. Inputs and output are encoded as little-endian `u32` words in the conformance byte stream.

## CPU Reference

```rust
pub fn cpu_insert_bits(packed: u32, original: u32) -> u32 {
    let offset = packed & 31;
    let count = (packed >> 5) & 31;
    let newbits = packed >> 10;
    if count == 0 { return original; }
    let width = count.min(32 - offset);
    let mask = if width == 32 { u32::MAX } else { (1u32 << width) - 1 };
    let cleared = original & !(mask << offset);
    cleared | ((newbits & mask) << offset)
}
```

Short inputs supplied by adversarial byte generators decode to zero output in the harness-level byte reference; typed reference functions above define the operation once operands are available.

## Semantic Properties Not Currently Declared

- ZeroCountRightIdentity: when `count = 0`, output is `original` (custom).
- OutsideFieldPreserved: bits outside the insertion field equal `original` (custom).
- InsertedFieldMatches: inserted field equals `newbits & mask` (custom).

`spec.laws` is currently empty for this operation, so these properties are not
checked by the algebra self-test.

## Algebraic Laws Not Satisfied

- Commutative: false.
- Associative: false.
- Identity(e): no fixed packed operand is a two-sided identity.
- Idempotent: false for general packed/original pairs.

## Equivalence Classes

- `count = 0` preserves original.
- `offset = 0` writes low bits.
- `offset in 1..31` writes shifted field.
- `offset + count <= 32` full requested width.
- `offset + count > 32` clamped width.
- `newbits` wider than count gets masked.

## Boundary Values

- `(0, 0)`
- `(0, 0xFFFF_FFFF)`
- `(0xFFFF_FFFF, 0)`
- `(0xFFFF_FFFF, 0xFFFF_FFFF)`
- `(1 << 5, 0)`
- `(31 | (1 << 5), 0)`
- `(0x0000_FC20, 0xAAAA_AAAA)`

Any backend difference on these boundaries is a conformance failure with the operation id, input words, expected output, actual output, and `Fix: implement the CPU reference semantics exactly` in the diagnostic.