@@ -17,39 +17,6 @@ use std::fs::{self, OpenOptions};
1717use std:: path:: PathBuf ;
1818use std:: process:: Command ;
1919
20- /// Test sandbox that cleans up after itself
21- ///
22- /// Note: New tests should use fixtures::test_sandbox() instead.
23- /// This struct is kept for backward compatibility with existing tests.
24- struct TestSandbox {
25- root : PathBuf ,
26- }
27-
28- impl TestSandbox {
29- fn new ( name : & str ) -> Self {
30- let root = PathBuf :: from ( format ! (
31- "/tmp/vsh_rust_test_{}_{}" ,
32- name,
33- std:: time:: SystemTime :: now( )
34- . duration_since( std:: time:: UNIX_EPOCH )
35- . unwrap( )
36- . as_nanos( )
37- ) ) ;
38- fs:: create_dir_all ( & root) . unwrap ( ) ;
39- Self { root }
40- }
41-
42- fn path ( & self , rel : & str ) -> PathBuf {
43- self . root . join ( rel)
44- }
45- }
46-
47- impl Drop for TestSandbox {
48- fn drop ( & mut self ) {
49- let _ = fs:: remove_dir_all ( & self . root ) ;
50- }
51- }
52-
5320// ============================================================
5421// Reversibility Tests
5522// ============================================================
@@ -58,9 +25,9 @@ impl Drop for TestSandbox {
5825/// Lean theorem: mkdir_rmdir_reversible (FilesystemModel.lean:158)
5926#[ test]
6027fn test_mkdir_rmdir_reversible ( ) {
61- let sandbox = TestSandbox :: new ( "mkdir_rmdir" ) ;
28+ let temp = fixtures :: test_sandbox ( "mkdir_rmdir" ) ;
6229
63- let target = sandbox . path ( "testdir" ) ;
30+ let target = temp . path ( ) . join ( "testdir" ) ;
6431
6532 // Initial state: directory does not exist
6633 assert ! ( !target. exists( ) , "Precondition: path should not exist" ) ;
@@ -81,9 +48,9 @@ fn test_mkdir_rmdir_reversible() {
8148/// Lean theorem: createFile_deleteFile_reversible (FileOperations.lean)
8249#[ test]
8350fn test_create_delete_file_reversible ( ) {
84- let sandbox = TestSandbox :: new ( "create_delete" ) ;
51+ let temp = fixtures :: test_sandbox ( "create_delete" ) ;
8552
86- let target = sandbox . path ( "testfile.txt" ) ;
53+ let target = temp . path ( ) . join ( "testfile.txt" ) ;
8754
8855 // Initial state
8956 assert ! ( !target. exists( ) ) ;
@@ -104,13 +71,13 @@ fn test_create_delete_file_reversible() {
10471/// Lean theorem: operationSequenceReversible (FilesystemComposition.lean:129)
10572#[ test]
10673fn test_operation_sequence_reversible ( ) {
107- let sandbox = TestSandbox :: new ( "sequence" ) ;
74+ let temp = fixtures :: test_sandbox ( "sequence" ) ;
10875
10976 // Create a nested structure
110- let dir1 = sandbox . path ( "level1" ) ;
111- let dir2 = sandbox . path ( "level1/level2" ) ;
112- let file1 = sandbox . path ( "level1/file.txt" ) ;
113- let file2 = sandbox . path ( "level1/level2/nested.txt" ) ;
77+ let dir1 = temp . path ( ) . join ( "level1" ) ;
78+ let dir2 = temp . path ( ) . join ( "level1/level2" ) ;
79+ let file1 = temp . path ( ) . join ( "level1/file.txt" ) ;
80+ let file2 = temp . path ( ) . join ( "level1/level2/nested.txt" ) ;
11481
11582 // Apply sequence: mkdir a → mkdir a/b → touch a/f → touch a/b/n
11683 fs:: create_dir ( & dir1) . unwrap ( ) ;
@@ -142,9 +109,9 @@ fn test_operation_sequence_reversible() {
142109/// Coq: MkdirPrecondition requires ~path_exists
143110#[ test]
144111fn test_mkdir_eexist ( ) {
145- let sandbox = TestSandbox :: new ( "eexist" ) ;
112+ let temp = fixtures :: test_sandbox ( "eexist" ) ;
146113
147- let target = sandbox . path ( "existing" ) ;
114+ let target = temp . path ( ) . join ( "existing" ) ;
148115 fs:: create_dir ( & target) . unwrap ( ) ;
149116
150117 // Attempt to create again should fail
@@ -163,9 +130,9 @@ fn test_mkdir_eexist() {
163130/// Coq: MkdirPrecondition requires parent_exists
164131#[ test]
165132fn test_mkdir_enoent ( ) {
166- let sandbox = TestSandbox :: new ( "enoent" ) ;
133+ let temp = fixtures :: test_sandbox ( "enoent" ) ;
167134
168- let target = sandbox . path ( "nonexistent/child" ) ;
135+ let target = temp . path ( ) . join ( "nonexistent/child" ) ;
169136
170137 let result = fs:: create_dir ( & target) ;
171138 assert ! ( result. is_err( ) , "mkdir should fail when parent doesn't exist" ) ;
@@ -182,9 +149,9 @@ fn test_mkdir_enoent() {
182149/// Coq: RmdirPrecondition requires is_empty
183150#[ test]
184151fn test_rmdir_enotempty ( ) {
185- let sandbox = TestSandbox :: new ( "enotempty" ) ;
152+ let temp = fixtures :: test_sandbox ( "enotempty" ) ;
186153
187- let target = sandbox . path ( "nonempty" ) ;
154+ let target = temp . path ( ) . join ( "nonempty" ) ;
188155 fs:: create_dir ( & target) . unwrap ( ) ;
189156 fs:: write ( target. join ( "file.txt" ) , "content" ) . unwrap ( ) ;
190157
@@ -208,9 +175,9 @@ fn test_rmdir_enotempty() {
208175/// Coq: RmdirPrecondition requires is_directory
209176#[ test]
210177fn test_rmdir_enotdir ( ) {
211- let sandbox = TestSandbox :: new ( "enotdir" ) ;
178+ let temp = fixtures :: test_sandbox ( "enotdir" ) ;
212179
213- let target = sandbox . path ( "afile.txt" ) ;
180+ let target = temp . path ( ) . join ( "afile.txt" ) ;
214181 fs:: write ( & target, "content" ) . unwrap ( ) ;
215182
216183 let result = fs:: remove_dir ( & target) ;
@@ -221,9 +188,9 @@ fn test_rmdir_enotdir() {
221188/// Coq: DeleteFilePrecondition requires ~is_directory
222189#[ test]
223190fn test_rm_eisdir ( ) {
224- let sandbox = TestSandbox :: new ( "eisdir" ) ;
191+ let temp = fixtures :: test_sandbox ( "eisdir" ) ;
225192
226- let target = sandbox . path ( "adir" ) ;
193+ let target = temp . path ( ) . join ( "adir" ) ;
227194 fs:: create_dir ( & target) . unwrap ( ) ;
228195
229196 let result = fs:: remove_file ( & target) ;
@@ -238,9 +205,9 @@ fn test_rm_eisdir() {
238205/// Lean theorem: writeFileReversible (FileContentOperations.lean)
239206#[ test]
240207fn test_write_file_reversible ( ) {
241- let sandbox = TestSandbox :: new ( "write" ) ;
208+ let temp = fixtures :: test_sandbox ( "write" ) ;
242209
243- let target = sandbox . path ( "data.txt" ) ;
210+ let target = temp . path ( ) . join ( "data.txt" ) ;
244211 let original_content = b"original content" ;
245212 let new_content = b"modified content" ;
246213
@@ -273,11 +240,11 @@ fn test_write_file_reversible() {
273240/// Lean theorem: mkdirPreservesOtherPaths (FilesystemModel.lean)
274241#[ test]
275242fn test_operation_independence ( ) {
276- let sandbox = TestSandbox :: new ( "independence" ) ;
243+ let temp = fixtures :: test_sandbox ( "independence" ) ;
277244
278245 // Create two independent directories
279- let dir_a = sandbox . path ( "alpha" ) ;
280- let dir_b = sandbox . path ( "beta" ) ;
246+ let dir_a = temp . path ( ) . join ( "alpha" ) ;
247+ let dir_b = temp . path ( ) . join ( "beta" ) ;
281248
282249 fs:: create_dir ( & dir_a) . unwrap ( ) ;
283250
@@ -301,15 +268,15 @@ fn test_operation_independence() {
301268/// Simulates transaction behavior at filesystem level
302269#[ test]
303270fn test_transaction_rollback_simulation ( ) {
304- let sandbox = TestSandbox :: new ( "transaction" ) ;
271+ let temp = fixtures :: test_sandbox ( "transaction" ) ;
305272
306273 // Record operations for potential rollback
307274 let mut operations: Vec < ( & str , PathBuf ) > = Vec :: new ( ) ;
308275
309276 // Begin "transaction"
310- let target1 = sandbox . path ( "txn_dir1" ) ;
311- let target2 = sandbox . path ( "txn_dir2" ) ;
312- let target3 = sandbox . path ( "txn_file.txt" ) ;
277+ let target1 = temp . path ( ) . join ( "txn_dir1" ) ;
278+ let target2 = temp . path ( ) . join ( "txn_dir2" ) ;
279+ let target3 = temp . path ( ) . join ( "txn_file.txt" ) ;
313280
314281 // Execute operations
315282 fs:: create_dir ( & target1) . unwrap ( ) ;
@@ -348,9 +315,9 @@ fn test_transaction_rollback_simulation() {
348315/// Test: Empty file creation and deletion
349316#[ test]
350317fn test_empty_file ( ) {
351- let sandbox = TestSandbox :: new ( "empty" ) ;
318+ let temp = fixtures :: test_sandbox ( "empty" ) ;
352319
353- let target = sandbox . path ( "empty.txt" ) ;
320+ let target = temp . path ( ) . join ( "empty.txt" ) ;
354321 fs:: write ( & target, "" ) . unwrap ( ) ;
355322
356323 assert ! ( target. exists( ) ) ;
@@ -364,10 +331,10 @@ fn test_empty_file() {
364331/// Test: Deeply nested path operations
365332#[ test]
366333fn test_deep_nesting ( ) {
367- let sandbox = TestSandbox :: new ( "deep" ) ;
334+ let temp = fixtures :: test_sandbox ( "deep" ) ;
368335
369336 // Create deep path
370- let deep = sandbox . path ( "a/b/c/d/e/f/g" ) ;
337+ let deep = temp . path ( ) . join ( "a/b/c/d/e/f/g" ) ;
371338 fs:: create_dir_all ( & deep) . unwrap ( ) ;
372339 assert ! ( deep. exists( ) ) ;
373340
@@ -380,20 +347,20 @@ fn test_deep_nesting() {
380347
381348 // Remove directories from deepest to shallowest
382349 let mut current = deep. clone ( ) ;
383- while current != sandbox . root {
350+ while current != temp . path ( ) {
384351 if current. exists ( ) && fs:: read_dir ( & current) . unwrap ( ) . next ( ) . is_none ( ) {
385352 fs:: remove_dir ( & current) . unwrap ( ) ;
386353 }
387354 current = current. parent ( ) . unwrap ( ) . to_path_buf ( ) ;
388355 }
389356
390- assert ! ( !sandbox . path( "a" ) . exists( ) , "Deep cleanup should remove all" ) ;
357+ assert ! ( !temp . path( ) . join ( "a" ) . exists( ) , "Deep cleanup should remove all" ) ;
391358}
392359
393360/// Test: Special characters in paths
394361#[ test]
395362fn test_special_characters ( ) {
396- let sandbox = TestSandbox :: new ( "special" ) ;
363+ let temp = fixtures :: test_sandbox ( "special" ) ;
397364
398365 let targets = vec ! [
399366 "spaces in name" ,
@@ -403,7 +370,7 @@ fn test_special_characters() {
403370 ] ;
404371
405372 for name in & targets {
406- let target = sandbox . path ( name) ;
373+ let target = temp . path ( ) . join ( name) ;
407374 fs:: create_dir ( & target) . unwrap ( ) ;
408375 assert ! ( target. exists( ) , "Should handle special chars: {}" , name) ;
409376 fs:: remove_dir ( & target) . unwrap ( ) ;
0 commit comments