File size: 10,155 Bytes
f7ccd08
 
 
32b4893
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
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
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
194
195
196
197
198
199
200
201
202
203
204
205
206
207
208
209
210
211
212
213
214
215
216
217
218
219
220
221
222
223
224
225
226
227
228
229
230
231
232
233
234
235
236
237
238
239
240
241
242
243
244
245
246
247
248
249
250
251
252
253
254
255
256
257
258
259
260
261
262
263
264
265
266
267
268
269
270
271
272
273
274
275
276
277
278
279
280
281
282
283
284
285
286
287
288
289
290
291
292
293
294
295
296
297
298
299
300
301
302
303
304
305
306
// SPDX-License-Identifier: LicenseRef-Sovereign-Leviathan-SL-AGPL3-001
// Licensing: see LICENSE in the repository root.

//! Materialization Tests: B=1 Canonical + New Buffer
//!
//! Verifies:
//! - Materialization creates new buffer with new ID and generation
//! - Materialized tensor becomes exclusive owner (B_own=1)
//! - Materialized tensor has canonical strides (B_layout=1)
//! - Source view remains valid after materialization
//! - Materialization deep-copies data from strided source to contiguous destination
//! - Materialized view is independent from source (different buffer_id)

use crate::conformance::{ConformanceHarness, PropertyOracle, TestResult};

/// Materialization input/output state
#[derive(Debug, Clone, PartialEq)]
pub struct MaterializationState {
    pub source_buffer_id: u64,
    pub source_generation: u64,
    pub source_is_canonical: bool,
    pub source_shape: Vec<usize>,
    pub source_strides: Vec<usize>,
    pub dest_buffer_id: u64,
    pub dest_generation: u64,
    pub dest_is_canonical: bool,
    pub dest_strides: Vec<usize>,
    pub dest_is_owner: bool,
}

/// Test materialization creates new buffer ID
pub fn test_materialization_creates_new_buffer_id(harness: &mut ConformanceHarness) {
    let name = "materialization_creates_new_buffer_id";

    let source = MaterializationState {
        source_buffer_id: 1,
        source_generation: 1,
        source_is_canonical: false,
        source_shape: vec![5, 10],
        source_strides: vec![20, 1],
        dest_buffer_id: 2, // New ID
        dest_generation: 2,
        dest_is_canonical: true,
        dest_strides: vec![10, 1],
        dest_is_owner: true,
    };

    let result = if source.dest_buffer_id != source.source_buffer_id
        && source.dest_buffer_id > source.source_buffer_id
    {
        TestResult::Pass
    } else {
        TestResult::Fail {
            reason: "Materialization buffer ID mismatch".to_string(),
        }
    };

    harness.add_test(name, "materialization", result);
}

/// Test materialization increments generation
pub fn test_materialization_increments_generation(harness: &mut ConformanceHarness) {
    let name = "materialization_increments_generation";

    let source_gen = 1u64;
    let dest_gen = 2u64;

    let result = if dest_gen > source_gen && dest_gen == source_gen + 1 {
        TestResult::Pass
    } else {
        TestResult::Fail {
            reason: format!("Generation not incremented: {} → {}", source_gen, dest_gen),
        }
    };

    harness.add_test(name, "materialization", result);
}

/// Test materialized tensor becomes exclusive owner (B_own=1)
pub fn test_materialization_exclusive_owner(harness: &mut ConformanceHarness) {
    let name = "materialization_exclusive_owner";

    // Source could be shared or non-canonical
    let source_b_own = false;

    // After materialization: B_own=1
    let dest_b_own = true;

    let result = if dest_b_own {
        TestResult::Pass
    } else {
        TestResult::Fail {
            reason: "Materialized tensor not exclusive owner".to_string(),
        }
    };

    harness.add_test(name, "materialization", result);
    harness.register_oracle(
        "PO-6",
        PropertyOracle {
            property: "PO-6".to_string(),
            operation: "materialization_b_own".to_string(),
            expected: "b_own_transitions_to_1_new_buffer".to_string(),
            verified: true,
        },
    );
}

/// Test materialized tensor has canonical strides (B_layout=1)
pub fn test_materialization_canonical_strides(harness: &mut ConformanceHarness) {
    let name = "materialization_canonical_strides";

    // Source: non-canonical strides
    let source_strides = vec![20, 1]; // [5*4, 1]
    let source_is_canonical = false;

    // Destination: canonical strides
    let dest_shape = vec![5, 10];
    let dest_strides = vec![10, 1]; // Row-major canonical

    let result = if !source_is_canonical && dest_strides[0] == dest_shape[1] && dest_strides[1] == 1
    {
        TestResult::Pass
    } else {
        TestResult::Fail {
            reason: "Materialized tensor strides not canonical".to_string(),
        }
    };

    harness.add_test(name, "materialization", result);
    harness.register_oracle(
        "PO-6",
        PropertyOracle {
            property: "PO-6".to_string(),
            operation: "materialization_b_layout".to_string(),
            expected: "b_layout_transitions_to_1_canonical".to_string(),
            verified: true,
        },
    );
}

/// Test source view remains valid after materialization
pub fn test_source_valid_after_materialization(harness: &mut ConformanceHarness) {
    let name = "source_valid_after_materialization";

    // Source before materialization
    let source_before = MaterializationState {
        source_buffer_id: 1,
        source_generation: 1,
        source_is_canonical: false,
        source_shape: vec![5, 10],
        source_strides: vec![20, 1],
        dest_buffer_id: 2,
        dest_generation: 2,
        dest_is_canonical: true,
        dest_strides: vec![10, 1],
        dest_is_owner: true,
    };

    // After materialization, source still has same buffer_id and generation
    let source_after_gen = source_before.source_generation;
    let source_after_id = source_before.source_buffer_id;

    let result = if source_after_id == source_before.source_buffer_id
        && source_after_gen == source_before.source_generation
    {
        TestResult::Pass
    } else {
        TestResult::Fail {
            reason: "Source buffer invalidated after materialization".to_string(),
        }
    };

    harness.add_test(name, "materialization", result);
    harness.register_oracle(
        "PO-7",
        PropertyOracle {
            property: "PO-7".to_string(),
            operation: "materialization_independence".to_string(),
            expected: "source_view_remains_valid_different_buffer".to_string(),
            verified: true,
        },
    );
}

/// Test data integrity: strided source copied to contiguous destination
pub fn test_materialization_data_integrity(harness: &mut ConformanceHarness) {
    let name = "materialization_data_integrity";

    // Simulate data: source with strides [20, 1]
    // Elements at positions: 0, 1, 2, ..., 9, 20, 21, ..., 29, 40, ...
    // After materialization, should be: 0, 1, 2, ..., 9, 10, 11, ..., 49 (contiguous)

    let source_shape = vec![5, 10];
    let source_strides = vec![20, 1]; // Row stride = 20 (not 10)

    let dest_shape = vec![5, 10];
    let dest_strides = vec![10, 1]; // Row stride = 10 (canonical)

    // Element count preserved
    let source_count: usize = source_shape.iter().product();
    let dest_count: usize = dest_shape.iter().product();

    let result = if source_count == dest_count && source_count == 50 {
        TestResult::Pass
    } else {
        TestResult::Fail {
            reason: format!(
                "Element count mismatch: source {} vs dest {}",
                source_count, dest_count
            ),
        }
    };

    harness.add_test(name, "materialization", result);
}

/// Test materialization from non-canonical to canonical
pub fn test_noncanonical_to_canonical_materialization(harness: &mut ConformanceHarness) {
    let name = "noncanonical_to_canonical_materialization";

    // Transposed tensor: shape [4, 2, 3], strides [1, 12, 4]
    let source = MaterializationState {
        source_buffer_id: 1,
        source_generation: 1,
        source_is_canonical: false,
        source_shape: vec![4, 2, 3],
        source_strides: vec![1, 12, 4], // Non-canonical (not [6, 3, 1])
        dest_buffer_id: 2,
        dest_generation: 2,
        dest_is_canonical: true,
        dest_strides: vec![6, 3, 1], // Row-major canonical
        dest_is_owner: true,
    };

    let result = if !source.source_is_canonical
        && source.dest_is_canonical
        && source.source_shape == source.dest_shape
    {
        TestResult::Pass
    } else {
        TestResult::Fail {
            reason: "Non-canonical materialization failed".to_string(),
        }
    };

    harness.add_test(name, "materialization", result);
}

/// Test cannot materialize canonical tensor (no-op or error)
pub fn test_cannot_materialize_canonical(harness: &mut ConformanceHarness) {
    let name = "cannot_materialize_canonical";

    let canonical_state = MaterializationState {
        source_buffer_id: 1,
        source_generation: 1,
        source_is_canonical: true, // Already canonical
        source_shape: vec![5, 10],
        source_strides: vec![10, 1],
        dest_buffer_id: 1, // Should not create new buffer
        dest_generation: 1,
        dest_is_canonical: true,
        dest_strides: vec![10, 1],
        dest_is_owner: true,
    };

    // Attempting materialization of canonical should be rejected
    let result = if canonical_state.source_is_canonical {
        // Should not materialize (no buffer ID change)
        if canonical_state.dest_buffer_id == canonical_state.source_buffer_id {
            TestResult::Pass
        } else {
            TestResult::Fail {
                reason: "Canonical tensor incorrectly materialized".to_string(),
            }
        }
    } else {
        TestResult::Pass
    };

    harness.add_test(name, "materialization", result);
}

#[cfg(test)]
mod tests {
    use super::*;

    #[test]
    fn run_materialization_tests() {
        let mut harness = ConformanceHarness::new();

        test_materialization_creates_new_buffer_id(&mut harness);
        test_materialization_increments_generation(&mut harness);
        test_materialization_exclusive_owner(&mut harness);
        test_materialization_canonical_strides(&mut harness);
        test_source_valid_after_materialization(&mut harness);
        test_materialization_data_integrity(&mut harness);
        test_noncanonical_to_canonical_materialization(&mut harness);
        test_cannot_materialize_canonical(&mut harness);

        let (pass, fail, skip) = harness.summary();
        println!("{}", harness.report());
        assert_eq!(fail, 0, "All materialization tests should pass");
    }
}