module CiseAnalysis

 use export why3.BuiltIn.BuiltIn
 use export why3.Bool.Bool
 use export why3.Unit.Unit
 use export tree.Tree
 use export why3.Tuple2.Tuple2
 use export int.Int
 use import map.Map as M
 use import set.Fset as F
 use seq.Seq, seq.Mem, seq.Distinct

predicate same_ext (m1 m2: 'a -> 'b) = forall x: 'a. m1 x = m2 x

val equal_elt (e1 e2 : elt) : bool
 ensures {result <-> e1 = e2}

let ghost predicate state_equality (s1 s2 : state)
 =
   same_ext s1.parent s2.parent &&
   equal_elt s1.root s2.root &&
   F.(==) s1.nodes s2.nodes

let ghost move_move_analysis (ghost _:()) : (state, state)
   ensures  { match result with
		| x1, x2 -> state_equality x1 x2
		end }  =
   let ghost c1 = any elt in
   let ghost np1 = any elt in
   let ghost state1 = any state in
   let ghost c2 = any elt in
   let ghost np2 = any elt in
   let ghost state2 = any state in
   assume { (F.mem np1 state1.nodes) /\
	    (F.mem np2 state2.nodes) /\
	    (F.mem c1 state1.nodes) /\
	    (F.mem c2 state2.nodes) /\
	    (not (reachability state1.parent np1 c1)) /\
	    (not (reachability state2.parent np2 c2)) /\
	    (c1 <> state1.root) /\
	    (c2 <> state2.root) /\
	    (c1 <> np1) /\
	    (c2 <> np2) /\
	    state_equality state1 state2 };
  move c1 np1 state1;
  move c2 np2 state1;
  move c2 np2 state2;
  move c1 np1 state2;
  (state1, state2)

let ghost remove_remove_analysis (ghost _:()) : (state, state)
   ensures  { match result with
		| x1, x2 -> state_equality x1 x2
		end } =
   let ghost n1 = any elt in
   let ghost state1 = any state in
   let ghost n2 = any elt in
   let ghost state2 = any state in
   assume { (F.mem n1 state1.nodes) /\
	    (F.mem n2 state2.nodes) /\
	    (forall x. state1.parent x <> n1 ) /\
	    (forall x. state2.parent x <> n2 ) /\
	    (n1 <> state1.root) /\
	    (n2 <> state2.root) /\
	   state_equality state1 state2 };
   remove n2 state1;
   remove n1 state1;
   remove n1 state2;
   remove n2 state2;
   (state1, state2)

let ghost add_add_analysis (ghost _:()) : (state, state)
   ensures  { match result with
		| x1, x2 -> state_equality x1 x2
		end } =
   let ghost n1 = any elt in
   let ghost p1 = any elt in
   let ghost state1 = any state in
   let ghost n2 = any elt in
   let ghost p2 = any elt in
   let ghost state2 = any state in
   assume { ((not F.mem n1 (nodes state1) /\ F.mem p1 (nodes state1)) /\
	    not F.mem n2 (nodes state2) /\ F.mem p2 (nodes state2)) /\
	    state_equality state1 state2 };
   add n1 p1 state1;
   add n2 p2 state1;
   add n2 p2 state2;
   add n1 p1 state2;
   (state1, state2)

let ghost remove_move_analysis (ghost _:()) : (state, state)
   ensures  { match result with
		| x1, x2 -> state_equality x1 x2
		end } =
   let ghost n1 = any elt in
   let ghost state1 = any state in
   let ghost c2 = any elt in
   let ghost np2 = any elt in
   let ghost state2 = any state in
   assume { (forall x. state1.parent x <> n1 ) /\
	    (n1 <> state1.root) /\
	    (F.mem np2 state2.nodes) /\
	    (F.mem c2 state2.nodes) /\
	    (not (reachability state2.parent np2 c2)) /\
	    (c2 <> state2.root) /\
	    (c2 <> np2) /\
	    state_equality state1 state2 };
   move c2 np2 state1;
   remove n1 state1;
   remove n1 state2;
   move c2 np2 state2;
   (state1, state2)

let ghost add_move_analysis (ghost _:()) : (state, state)
   ensures  { match result with
		| x1, x2 -> state_equality x1 x2
		end } =
   let ghost n1 = any elt in
   let ghost p1 = any elt in
   let ghost state1 = any state in
   let ghost c2 = any elt in
   let ghost np2 = any elt in
   let ghost state2 = any state in
   assume { (not F.mem n1 (nodes state1) /\ F.mem p1 (nodes state1)) /\
	    (F.mem np2 state2.nodes) /\
	    (F.mem c2 state2.nodes) /\
	    (not (reachability state2.parent np2 c2)) /\
	    (not (reachability state1.parent np2 c2)) /\
	    (c2 <> state2.root) /\
	     (c2 <> np2) /\
	    state_equality state1 state2 };
   add n1 p1 state1;
   move c2 np2 state1;
   move c2 np2 state2;
   add n1 p1 state2;
   (state1, state2)

let ghost add_remove_analysis (ghost _:()) : (state, state)
   ensures  { match result with
		| x1, x2 -> state_equality x1 x2
		end } =
   let ghost n1 = any elt in
   let ghost p1 = any elt in
   let ghost state1 = any state in
   let ghost n2 = any elt in
   let ghost state2 = any state in
   assume { (not F.mem n1 (nodes state1) /\ F.mem p1 (nodes state1)) /\
	    (forall x. state2.parent x <> n2 ) /\
	    (n2 <> state2.root) /\
	    state_equality state1 state2 };
   remove n2 state1;
   add n1 p1 state1;
   add n1 p1 state2;
   remove n2 state2;
   (state1, state2)

end