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
75
76
77
78
79
80
81
82
83
84
// CONTRACT: format-parity-v1.yaml
// HASH: sha256:d6e7f8901234567a
// Generated by: pv probar --binding
// DO NOT EDIT — regenerate with `pv probar --binding`
use proptest::prelude::*;
proptest! {
/// Obligation: Transpose involution (invariant)
/// Formal: swap(swap([a, b])) == [a, b]
/// Transpose is its own inverse — double-swap returns original shape.
#[test]
fn prop_transpose_involution(
a in 1usize..10000,
b in 1usize..10000
) {
let original = [a, b];
let swapped = [original[1], original[0]];
let double_swapped = [swapped[1], swapped[0]];
prop_assert_eq!(
original, double_swapped,
"swap(swap([{}, {}])) = [{}, {}], expected [{}, {}]",
a, b, double_swapped[0], double_swapped[1], a, b
);
}
/// Obligation: Element count preserved (invariant)
/// Formal: product(gguf_shape) == product(apr_shape) for all tensors
/// GGUF→APR transpose swaps dimensions but preserves total element count.
#[test]
fn prop_element_count_preserved(
a in 1usize..10000,
b in 1usize..10000
) {
let gguf_shape = [a, b];
let apr_shape = [b, a]; // GGUF→APR: swap for 2D
let gguf_count = gguf_shape[0] * gguf_shape[1];
let apr_count = apr_shape[0] * apr_shape[1];
prop_assert_eq!(
gguf_count, apr_count,
"element count changed: GGUF {}x{}={} vs APR {}x{}={}",
gguf_shape[0], gguf_shape[1], gguf_count,
apr_shape[0], apr_shape[1], apr_count
);
}
/// Obligation: 1D no transpose (invariant)
/// Formal: 1D tensors are identity-mapped (no swap needed)
#[test]
fn prop_1d_no_transpose(
n in 1usize..100000
) {
let gguf_shape = [n];
let apr_shape = gguf_shape; // 1D: identity mapping
prop_assert_eq!(
gguf_shape[0], apr_shape[0],
"1D tensor shape changed: GGUF [{}] vs APR [{}]",
gguf_shape[0], apr_shape[0]
);
}
/// Obligation: Roundtrip equivalence (equivalence)
/// Formal: |convert(convert(tensor, GGUF→APR), APR→GGUF) - tensor| < ε
#[test]
#[ignore = "Requires format converter — realizar domain"]
fn prop_roundtrip_equivalence(
_x in proptest::collection::vec(-10.0f32..10.0, 1..32usize)
) {
// Blocked: requires full GGUF→APR→GGUF roundtrip through format converter
}
/// Obligation: SIMD format equivalence (equivalence)
#[test]
#[ignore = "SIMD equivalence — trueno domain"]
fn prop_simd_equivalence(
_x in proptest::collection::vec(-10.0f32..10.0, 1..32usize)
) {
// Format parity is pure shape math — no SIMD variant
}
}