diff --git a/test/Rust2.fst b/test/Rust2.fst index 44c90d5a..df2490d9 100644 --- a/test/Rust2.fst +++ b/test/Rust2.fst @@ -6,7 +6,7 @@ module B = LowStar.Buffer open FStar.HyperStack.ST #set-options "--fuel 0 --ifuel 0" - +(* let basic1 (): ST.Stack unit (fun _ -> True) (fun _ _ _ -> True) = push_frame (); let x = B.alloca 0ul 6ul in @@ -17,6 +17,7 @@ let basic1 (): ST.Stack unit (fun _ -> True) (fun _ _ _ -> True) = B.upd x 0ul 1ul; pop_frame () +(* let basic2 (): ST.Stack unit (fun _ -> True) (fun _ _ _ -> True) = push_frame (); let x = B.alloca 0ul 6ul in @@ -30,8 +31,33 @@ let basic2 (): ST.Stack unit (fun _ -> True) (fun _ _ _ -> True) = B.upd x0 0ul 2ul; B.upd x1 0ul 2ul; pop_frame () +*) + +let basic_copy1 (): ST.Stack unit (fun _ -> True) (fun _ _ _ -> True) = + push_frame (); + let x = B.alloca 0ul 6ul in + let y = B.alloca 1ul 6ul in + B.blit y 0ul x 0ul 6ul; + pop_frame() +*) +let basic_copy2 (): ST.Stack unit (fun _ -> True) (fun _ _ _ -> True) = + push_frame (); + let x = B.alloca 0ul 6ul in + let y = B.alloca 1ul 6ul in + let x0 = B.sub x 0ul 2ul in + let x1 = B.sub x0 0ul 1ul in + // let x2 = B.sub x 1ul 4ul in + let y0 = B.sub y 0ul 2ul in + let y1 = B.sub y 0ul 1ul in + // B.upd x0 0ul 5ul; + // B.upd y0 0ul 5ul; + B.upd x1 0ul 5ul; + B.upd y1 0ul 5ul; + B.blit y0 0ul x0 0ul 2ul; + pop_frame() +(* let doesnt_work (): ST.Stack unit (fun _ -> True) (fun _ _ _ -> True) = push_frame (); let x = B.alloca 0ul 6ul in @@ -43,8 +69,11 @@ let doesnt_work (): ST.Stack unit (fun _ -> True) (fun _ _ _ -> True) = B.upd x0 0ul 2ul; B.upd x1 0ul 2ul; pop_frame () +*) let main (): ST.Stack unit (fun _ -> True) (fun _ _ _ -> True) = - basic1 (); - basic2 (); - doesnt_work () +// basic1 (); +// // basic2 (); +// basic_copy1(); + basic_copy2() +// doesnt_work ()