Commit 4343a6a7 authored by Jean-Christophe Filliâtre's avatar Jean-Christophe Filliâtre
Browse files

koda-ruskey: no more global array bits

parent 370bb109
...@@ -408,10 +408,9 @@ module KodaRuskey ...@@ -408,10 +408,9 @@ module KodaRuskey
val map_of_array (a: array 'a) : M.map int 'a val map_of_array (a: array 'a) : M.map int 'a
ensures { result = a.elts } ensures { result = a.elts }
val bits : array color
val ghost visited: ref visited val ghost visited: ref visited
let rec enum (ghost f0: forest) (st: list forest) : unit let rec enum (bits: array color) (ghost f0: forest) (st: list forest) : unit
requires { size_forest f0 = length bits } requires { size_forest f0 = length bits }
requires { valid_nums_forest f0 (length bits) } requires { valid_nums_forest f0 (length bits) }
requires { sub st f0 bits.elts } requires { sub st f0 bits.elts }
...@@ -435,14 +434,14 @@ module KodaRuskey ...@@ -435,14 +434,14 @@ module KodaRuskey
ghost visited := S.snoc !visited (map_of_array bits); ghost visited := S.snoc !visited (map_of_array bits);
() ()
| _ -> | _ ->
enum f0 st' enum bits f0 st'
end end
| Cons (N i f1 f2 as f) st' -> | Cons (N i f1 f2 as f) st' ->
assert { disjoint_stack f1 st' }; assert { disjoint_stack f1 st' };
assert { not (mem_stack i st') }; assert { not (mem_stack i st') };
let ghost visited1 = !visited in let ghost visited1 = !visited in
if bits[i] = White then begin if bits[i] = White then begin
'A: enum f0 (Cons f2 st'); 'A: enum bits f0 (Cons f2 st');
assert { sub st f0 bits.elts }; assert { sub st f0 bits.elts };
let ghost bits1 = map_of_array bits in let ghost bits1 = map_of_array bits in
let ghost visited2 = !visited in let ghost visited2 = !visited in
...@@ -451,7 +450,7 @@ module KodaRuskey ...@@ -451,7 +450,7 @@ module KodaRuskey
assert { white_forest f1 bits.elts }; assert { white_forest f1 bits.elts };
assert { unchanged (Cons f2 st') (at bits 'B).elts bits.elts}; assert { unchanged (Cons f2 st') (at bits 'B).elts bits.elts};
assert { inverse (Cons f2 st') (at bits 'A).elts bits.elts }; assert { inverse (Cons f2 st') (at bits 'A).elts bits.elts };
'C: enum f0 (Cons f1 (Cons f2 st')); 'C: enum bits f0 (Cons f1 (Cons f2 st'));
assert { bits[i] = Black }; assert { bits[i] = Black };
assert { final_forest f1 bits.elts }; assert { final_forest f1 bits.elts };
assert { if not (even_forest f1) assert { if not (even_forest f1)
...@@ -464,7 +463,7 @@ module KodaRuskey ...@@ -464,7 +463,7 @@ module KodaRuskey
end else begin end else begin
assert { if not (even_forest f1) then white_forest f2 bits.elts assert { if not (even_forest f1) then white_forest f2 bits.elts
else final_forest f2 bits.elts }; else final_forest f2 bits.elts };
'A: enum f0 (Cons f1 (Cons f2 st')); 'A: enum bits f0 (Cons f1 (Cons f2 st'));
assert { sub st f0 bits.elts }; assert { sub st f0 bits.elts };
let ghost bits1 = map_of_array bits in let ghost bits1 = map_of_array bits in
let ghost visited2 = !visited in let ghost visited2 = !visited in
...@@ -477,7 +476,7 @@ module KodaRuskey ...@@ -477,7 +476,7 @@ module KodaRuskey
assert { if even_forest f1 || even_forest f2 assert { if even_forest f1 || even_forest f2
then unchanged st' (at bits 'A).elts bits.elts then unchanged st' (at bits 'A).elts bits.elts
else inverse st' (at bits 'A).elts bits.elts }; else inverse st' (at bits 'A).elts bits.elts };
'C: enum f0 (Cons f2 st'); 'C: enum bits f0 (Cons f2 st');
assert { bits[i] = White }; assert { bits[i] = White };
assert { white_forest f bits.elts }; assert { white_forest f bits.elts };
ghost stored_trans2 f0 bits1 (map_of_array bits) ghost stored_trans2 f0 bits1 (map_of_array bits)
...@@ -485,7 +484,7 @@ module KodaRuskey ...@@ -485,7 +484,7 @@ module KodaRuskey
end end
end end
let main (f0: forest) let main (bits: array color) (f0: forest)
requires { white_forest f0 bits.elts } requires { white_forest f0 bits.elts }
requires { size_forest f0 = length bits } requires { size_forest f0 = length bits }
requires { valid_nums_forest f0 (length bits) } requires { valid_nums_forest f0 (length bits) }
...@@ -497,7 +496,7 @@ module KodaRuskey ...@@ -497,7 +496,7 @@ module KodaRuskey
not (eq_coloring (length bits) not (eq_coloring (length bits)
(S.get !visited j) (S.get !visited k)) } (S.get !visited j) (S.get !visited k)) }
= visited := S.empty; = visited := S.empty;
enum f0 (Cons f0 Nil) enum bits f0 (Cons f0 Nil)
end end
......
This diff is collapsed.
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment