Commit 42741d7b authored by Marc Schoolderman's avatar Marc Schoolderman
Browse files

removed pvs files

parent 1bcdae7f
This diff is collapsed.
(* This file is generated by Why3's Coq driver *)
(* Beware! Only edit allowed sections below *)
Require Import BuiltIn.
Require BuiltIn.
Require bv.Pow2int.
Require int.Int.
Require int.Abs.
Require int.EuclideanDivision.
Require bv.BV_Gen.
Require bool.Bool.
Require map.Map.
(* Why3 assumption *)
Inductive address_space :=
| mk_address_space : (map.Map.map Z Z) -> address_space.
Axiom address_space_WhyType : WhyType address_space.
Existing Instance address_space_WhyType.
(* Why3 assumption *)
Definition data (v:address_space): (map.Map.map Z Z) :=
match v with
| (mk_address_space x) => x
end.
Parameter sum: (address_space* Z)%type -> Z -> Z -> Z.
Parameter stack_limit: Z.
Axiom t : Type.
Parameter t_WhyType : WhyType t.
Existing Instance t_WhyType.
Parameter t'int: t -> Z.
Axiom t'axiom : forall (i:t), (0%Z <= (t'int i))%Z /\ ((t'int i) <= 255%Z)%Z.
Parameter nth: t -> Z -> bool.
Parameter zeros: t.
Parameter one: t.
Parameter ones: t.
Parameter bw_and: t -> t -> t.
Parameter bw_or: t -> t -> t.
Parameter bw_xor: t -> t -> t.
Parameter bw_not: t -> t.
Parameter lsr: t -> Z -> t.
Parameter asr: t -> Z -> t.
Parameter lsl: t -> Z -> t.
Parameter rotate_right: t -> Z -> t.
Parameter rotate_left: t -> Z -> t.
Parameter to_int: t -> Z.
Parameter of_int: Z -> t.
Parameter size_bv: t.
Parameter add: t -> t -> t.
Parameter sub: t -> t -> t.
Parameter neg: t -> t.
Parameter mul: t -> t -> t.
Parameter udiv: t -> t -> t.
Parameter urem: t -> t -> t.
Parameter lsr_bv: t -> t -> t.
Parameter asr_bv: t -> t -> t.
Parameter lsl_bv: t -> t -> t.
Parameter rotate_right_bv: t -> t -> t.
Parameter rotate_left_bv: t -> t -> t.
Parameter nth_bv: t -> t -> bool.
Parameter eq_sub_bv: t -> t -> t -> t -> Prop.
Axiom register_file_invariant_strengthen : forall (m:(map.Map.map Z Z)),
(forall (i:Z), (0%Z <= (map.Map.get m i))%Z /\ ((map.Map.get m
i) < 256%Z)%Z) -> forall (i:Z) (j:Z), (0%Z <= ((map.Map.get m
i) * (map.Map.get m j))%Z)%Z /\ (((map.Map.get m i) * (map.Map.get m
j))%Z <= (255%Z * 255%Z)%Z)%Z.
(* Why3 goal *)
Theorem WP_parameter_mul16 : forall (reg:(map.Map.map Z Z)), (forall (i:Z),
((0%Z < (map.Map.get reg i))%Z \/ (0%Z = (map.Map.get reg i))) /\
((map.Map.get reg i) < 256%Z)%Z) -> forall (reg1:(map.Map.map Z Z)),
((forall (i:Z), ((0%Z < (map.Map.get reg1 i))%Z \/ (0%Z = (map.Map.get reg1
i))) /\ ((map.Map.get reg1 i) < 256%Z)%Z) /\ ((map.Map.set reg 23%Z
0%Z) = reg1)) -> forall (reg2:(map.Map.map Z Z)) (cf:bool), ((forall (i:Z),
((0%Z < (map.Map.get reg2 i))%Z \/ (0%Z = (map.Map.get reg2 i))) /\
((map.Map.get reg2 i) < 256%Z)%Z) /\ (((map.Map.set (map.Map.set reg1 0%Z
(int.EuclideanDivision.mod1 ((map.Map.get reg1 8%Z) * (map.Map.get reg1
3%Z))%Z 256%Z)) 1%Z (int.EuclideanDivision.div ((map.Map.get reg1
8%Z) * (map.Map.get reg1 3%Z))%Z 256%Z)) = reg2) /\ (((cf = true) /\
(1%Z = (int.EuclideanDivision.div ((map.Map.get reg1
8%Z) * (map.Map.get reg1 3%Z))%Z (bv.Pow2int.pow2 15%Z)))) \/
((~ (cf = true)) /\ (0%Z = (int.EuclideanDivision.div ((map.Map.get reg1
8%Z) * (map.Map.get reg1 3%Z))%Z (bv.Pow2int.pow2 15%Z))))))) ->
forall (reg3:(map.Map.map Z Z)), ((forall (i:Z), ((0%Z < (map.Map.get reg3
i))%Z \/ (0%Z = (map.Map.get reg3 i))) /\ ((map.Map.get reg3
i) < 256%Z)%Z) /\ ((map.Map.set (map.Map.set reg2 14%Z (map.Map.get reg2
0%Z)) 15%Z (map.Map.get reg2 1%Z)) = reg3)) -> forall (reg4:(map.Map.map Z
Z)) (cf1:bool), ((forall (i:Z), ((0%Z < (map.Map.get reg4 i))%Z \/
(0%Z = (map.Map.get reg4 i))) /\ ((map.Map.get reg4 i) < 256%Z)%Z) /\
(((map.Map.set (map.Map.set reg3 0%Z
(int.EuclideanDivision.mod1 ((map.Map.get reg3 7%Z) * (map.Map.get reg3
2%Z))%Z 256%Z)) 1%Z (int.EuclideanDivision.div ((map.Map.get reg3
7%Z) * (map.Map.get reg3 2%Z))%Z 256%Z)) = reg4) /\ (((cf1 = true) /\
(1%Z = (int.EuclideanDivision.div ((map.Map.get reg3
7%Z) * (map.Map.get reg3 2%Z))%Z (bv.Pow2int.pow2 15%Z)))) \/
((~ (cf1 = true)) /\ (0%Z = (int.EuclideanDivision.div ((map.Map.get reg3
7%Z) * (map.Map.get reg3 2%Z))%Z (bv.Pow2int.pow2 15%Z))))))) ->
forall (reg5:(map.Map.map Z Z)), ((forall (i:Z), ((0%Z < (map.Map.get reg5
i))%Z \/ (0%Z = (map.Map.get reg5 i))) /\ ((map.Map.get reg5
i) < 256%Z)%Z) /\ ((map.Map.set (map.Map.set reg4 12%Z (map.Map.get reg4
0%Z)) 13%Z (map.Map.get reg4 1%Z)) = reg5)) -> forall (reg6:(map.Map.map Z
Z)) (cf2:bool), ((forall (i:Z), ((0%Z < (map.Map.get reg6 i))%Z \/
(0%Z = (map.Map.get reg6 i))) /\ ((map.Map.get reg6 i) < 256%Z)%Z) /\
(((map.Map.set (map.Map.set reg5 0%Z
(int.EuclideanDivision.mod1 ((map.Map.get reg5 8%Z) * (map.Map.get reg5
2%Z))%Z 256%Z)) 1%Z (int.EuclideanDivision.div ((map.Map.get reg5
8%Z) * (map.Map.get reg5 2%Z))%Z 256%Z)) = reg6) /\ (((cf2 = true) /\
(1%Z = (int.EuclideanDivision.div ((map.Map.get reg5
8%Z) * (map.Map.get reg5 2%Z))%Z (bv.Pow2int.pow2 15%Z)))) \/
((~ (cf2 = true)) /\ (0%Z = (int.EuclideanDivision.div ((map.Map.get reg5
8%Z) * (map.Map.get reg5 2%Z))%Z (bv.Pow2int.pow2 15%Z))))))) ->
forall (reg7:(map.Map.map Z Z)) (cf3:bool), ((forall (i:Z),
((0%Z < (map.Map.get reg7 i))%Z \/ (0%Z = (map.Map.get reg7 i))) /\
((map.Map.get reg7 i) < 256%Z)%Z) /\ (((map.Map.set reg6 13%Z
(int.EuclideanDivision.mod1 ((map.Map.get reg6 13%Z) + (map.Map.get reg6
0%Z))%Z 256%Z)) = reg7) /\ (((cf3 = true) /\
(1%Z = (int.EuclideanDivision.div ((map.Map.get reg6
13%Z) + (map.Map.get reg6 0%Z))%Z 256%Z))) \/ ((~ (cf3 = true)) /\
(0%Z = (int.EuclideanDivision.div ((map.Map.get reg6
13%Z) + (map.Map.get reg6 0%Z))%Z 256%Z)))))) -> forall (reg8:(map.Map.map
Z Z)) (cf4:bool), ((forall (i:Z), ((0%Z < (map.Map.get reg8 i))%Z \/
(0%Z = (map.Map.get reg8 i))) /\ ((map.Map.get reg8 i) < 256%Z)%Z) /\
((((cf3 = true) /\ ((map.Map.set reg7 14%Z
(int.EuclideanDivision.mod1 (((map.Map.get reg7 14%Z) + (map.Map.get reg7
1%Z))%Z + 1%Z)%Z 256%Z)) = reg8)) \/ ((~ (cf3 = true)) /\
((map.Map.set reg7 14%Z (int.EuclideanDivision.mod1 (((map.Map.get reg7
14%Z) + (map.Map.get reg7 1%Z))%Z + 0%Z)%Z 256%Z)) = reg8))) /\
(((cf4 = true) /\ (((cf3 = true) /\
(1%Z = (int.EuclideanDivision.div (((map.Map.get reg7
14%Z) + (map.Map.get reg7 1%Z))%Z + 1%Z)%Z 256%Z))) \/ ((~ (cf3 = true)) /\
(1%Z = (int.EuclideanDivision.div (((map.Map.get reg7
14%Z) + (map.Map.get reg7 1%Z))%Z + 0%Z)%Z 256%Z))))) \/
((~ (cf4 = true)) /\ (((cf3 = true) /\
(0%Z = (int.EuclideanDivision.div (((map.Map.get reg7
14%Z) + (map.Map.get reg7 1%Z))%Z + 1%Z)%Z 256%Z))) \/ ((~ (cf3 = true)) /\
(0%Z = (int.EuclideanDivision.div (((map.Map.get reg7
14%Z) + (map.Map.get reg7 1%Z))%Z + 0%Z)%Z 256%Z)))))))) ->
forall (reg9:(map.Map.map Z Z)) (cf5:bool), ((forall (i:Z),
((0%Z < (map.Map.get reg9 i))%Z \/ (0%Z = (map.Map.get reg9 i))) /\
((map.Map.get reg9 i) < 256%Z)%Z) /\ ((((cf4 = true) /\ ((map.Map.set reg8
15%Z (int.EuclideanDivision.mod1 (((map.Map.get reg8
15%Z) + (map.Map.get reg8 23%Z))%Z + 1%Z)%Z 256%Z)) = reg9)) \/
((~ (cf4 = true)) /\ ((map.Map.set reg8 15%Z
(int.EuclideanDivision.mod1 (((map.Map.get reg8 15%Z) + (map.Map.get reg8
23%Z))%Z + 0%Z)%Z 256%Z)) = reg9))) /\ (((cf5 = true) /\ (((cf4 = true) /\
(1%Z = (int.EuclideanDivision.div (((map.Map.get reg8
15%Z) + (map.Map.get reg8 23%Z))%Z + 1%Z)%Z 256%Z))) \/
((~ (cf4 = true)) /\ (1%Z = (int.EuclideanDivision.div (((map.Map.get reg8
15%Z) + (map.Map.get reg8 23%Z))%Z + 0%Z)%Z 256%Z))))) \/
((~ (cf5 = true)) /\ (((cf4 = true) /\
(0%Z = (int.EuclideanDivision.div (((map.Map.get reg8
15%Z) + (map.Map.get reg8 23%Z))%Z + 1%Z)%Z 256%Z))) \/
((~ (cf4 = true)) /\ (0%Z = (int.EuclideanDivision.div (((map.Map.get reg8
15%Z) + (map.Map.get reg8 23%Z))%Z + 0%Z)%Z 256%Z)))))))) ->
forall (reg10:(map.Map.map Z Z)) (cf6:bool), ((forall (i:Z),
((0%Z < (map.Map.get reg10 i))%Z \/ (0%Z = (map.Map.get reg10 i))) /\
((map.Map.get reg10 i) < 256%Z)%Z) /\ (((map.Map.set (map.Map.set reg9 0%Z
(int.EuclideanDivision.mod1 ((map.Map.get reg9 7%Z) * (map.Map.get reg9
3%Z))%Z 256%Z)) 1%Z (int.EuclideanDivision.div ((map.Map.get reg9
7%Z) * (map.Map.get reg9 3%Z))%Z 256%Z)) = reg10) /\ (((cf6 = true) /\
(1%Z = (int.EuclideanDivision.div ((map.Map.get reg9
7%Z) * (map.Map.get reg9 3%Z))%Z (bv.Pow2int.pow2 15%Z)))) \/
((~ (cf6 = true)) /\ (0%Z = (int.EuclideanDivision.div ((map.Map.get reg9
7%Z) * (map.Map.get reg9 3%Z))%Z (bv.Pow2int.pow2 15%Z))))))) ->
forall (reg11:(map.Map.map Z Z)) (cf7:bool), ((forall (i:Z),
((0%Z < (map.Map.get reg11 i))%Z \/ (0%Z = (map.Map.get reg11 i))) /\
((map.Map.get reg11 i) < 256%Z)%Z) /\ (((map.Map.set reg10 13%Z
(int.EuclideanDivision.mod1 ((map.Map.get reg10 13%Z) + (map.Map.get reg10
0%Z))%Z 256%Z)) = reg11) /\ (((cf7 = true) /\
(1%Z = (int.EuclideanDivision.div ((map.Map.get reg10
13%Z) + (map.Map.get reg10 0%Z))%Z 256%Z))) \/ ((~ (cf7 = true)) /\
(0%Z = (int.EuclideanDivision.div ((map.Map.get reg10
13%Z) + (map.Map.get reg10 0%Z))%Z 256%Z)))))) ->
forall (reg12:(map.Map.map Z Z)) (cf8:bool), ((forall (i:Z),
((0%Z < (map.Map.get reg12 i))%Z \/ (0%Z = (map.Map.get reg12 i))) /\
((map.Map.get reg12 i) < 256%Z)%Z) /\ ((((cf7 = true) /\
((map.Map.set reg11 14%Z (int.EuclideanDivision.mod1 (((map.Map.get reg11
14%Z) + (map.Map.get reg11 1%Z))%Z + 1%Z)%Z 256%Z)) = reg12)) \/
((~ (cf7 = true)) /\ ((map.Map.set reg11 14%Z
(int.EuclideanDivision.mod1 (((map.Map.get reg11 14%Z) + (map.Map.get reg11
1%Z))%Z + 0%Z)%Z 256%Z)) = reg12))) /\ (((cf8 = true) /\ (((cf7 = true) /\
(1%Z = (int.EuclideanDivision.div (((map.Map.get reg11
14%Z) + (map.Map.get reg11 1%Z))%Z + 1%Z)%Z 256%Z))) \/
((~ (cf7 = true)) /\ (1%Z = (int.EuclideanDivision.div (((map.Map.get reg11
14%Z) + (map.Map.get reg11 1%Z))%Z + 0%Z)%Z 256%Z))))) \/
((~ (cf8 = true)) /\ (((cf7 = true) /\
(0%Z = (int.EuclideanDivision.div (((map.Map.get reg11
14%Z) + (map.Map.get reg11 1%Z))%Z + 1%Z)%Z 256%Z))) \/
((~ (cf7 = true)) /\ (0%Z = (int.EuclideanDivision.div (((map.Map.get reg11
14%Z) + (map.Map.get reg11 1%Z))%Z + 0%Z)%Z 256%Z)))))))) ->
forall (reg13:(map.Map.map Z Z)) (cf9:bool), ((forall (i:Z),
((0%Z < (map.Map.get reg13 i))%Z \/ (0%Z = (map.Map.get reg13 i))) /\
((map.Map.get reg13 i) < 256%Z)%Z) /\ ((((cf8 = true) /\
((map.Map.set reg12 15%Z (int.EuclideanDivision.mod1 (((map.Map.get reg12
15%Z) + (map.Map.get reg12 23%Z))%Z + 1%Z)%Z 256%Z)) = reg13)) \/
((~ (cf8 = true)) /\ ((map.Map.set reg12 15%Z
(int.EuclideanDivision.mod1 (((map.Map.get reg12 15%Z) + (map.Map.get reg12
23%Z))%Z + 0%Z)%Z 256%Z)) = reg13))) /\ (((cf9 = true) /\ (((cf8 = true) /\
(1%Z = (int.EuclideanDivision.div (((map.Map.get reg12
15%Z) + (map.Map.get reg12 23%Z))%Z + 1%Z)%Z 256%Z))) \/
((~ (cf8 = true)) /\ (1%Z = (int.EuclideanDivision.div (((map.Map.get reg12
15%Z) + (map.Map.get reg12 23%Z))%Z + 0%Z)%Z 256%Z))))) \/
((~ (cf9 = true)) /\ (((cf8 = true) /\
(0%Z = (int.EuclideanDivision.div (((map.Map.get reg12
15%Z) + (map.Map.get reg12 23%Z))%Z + 1%Z)%Z 256%Z))) \/
((~ (cf8 = true)) /\ (0%Z = (int.EuclideanDivision.div (((map.Map.get reg12
15%Z) + (map.Map.get reg12 23%Z))%Z + 0%Z)%Z 256%Z)))))))) ->
(((((map.Map.get reg13 12%Z) + ((bv.Pow2int.pow2 8%Z) * (map.Map.get reg13
13%Z))%Z)%Z + ((bv.Pow2int.pow2 16%Z) * (map.Map.get reg13
14%Z))%Z)%Z + ((bv.Pow2int.pow2 24%Z) * (map.Map.get reg13
15%Z))%Z)%Z = (((map.Map.get reg
2%Z) + ((bv.Pow2int.pow2 8%Z) * (map.Map.get reg
3%Z))%Z)%Z * ((map.Map.get reg
7%Z) + ((bv.Pow2int.pow2 8%Z) * (map.Map.get reg 8%Z))%Z)%Z)%Z).
intros reg h1 reg1 (h2,h3) reg2 cf (h4,(h5,h6)) reg3 (h7,h8) reg4 cf1
(h9,(h10,h11)) reg5 (h12,h13) reg6 cf2 (h14,(h15,h16)) reg7 cf3
(h17,(h18,h19)) reg8 cf4 (h20,(h21,h22)) reg9 cf5 (h23,(h24,h25)) reg10 cf6
(h26,(h27,h28)) reg11 cf7 (h29,(h30,h31)) reg12 cf8 (h32,(h33,h34)) reg13 cf9
(h35,(h36,h37)).
Qed.
This diff is collapsed.
This diff is collapsed.
Supports Markdown
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