IFC/TestingCommon.v at master · QuickChick/IFC · GitHub

1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
RequireImport ZArith.
RequireImport Coq.Strings.String.
RequireImport NPeano.

From QuickChick RequireImport QuickChick.

RequireExport Utils.
RequireExport Labels.
RequireExport Instructions.
RequireExport Memory.
RequireExport Lab4.
RequireExport Indist.
RequireExport Machine.

Module Lab4M <: FINLAT.
Definition Label := Lab4.
Definition FLat := FiniteLattice_Lab4.
End Lab4M.

Module MachineLab4M := MachineM Lab4M.
Export MachineLab4M.

Module IndistLab4M := IndistM Lab4M.
Export IndistLab4M.


Definition pure {A : Type} (x : A) : G A := returnGen x.

(*
Fixpoint foldGen {A B : Type} (f : A -> B -> G A) (l : list B) (a : A)
: G A :=
 match l with
 | [] => returnGen a
 | (x :: xs) => bindGen (f a x) (foldGen f xs)
 end.
*)

(* Variation stuff - should be deleted -- CH: ha? it seems used *)
Inductive Variation {A : Type} :=
| Var : Lab4 -> A -> A -> Variation.

Class ShrinkV (A : Type) := { shrinkV : @Variation A -> list (@Variation A) }.
(* End of to be deleted *)

Definition validJump (st : State) (addr : Z) :=
let '(St imem _ _ _ _) := st in
 (Z.to_nat addr) <? (List.length imem).
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
RequireImport ZArith.
RequireImport Coq.Strings.String.
RequireImport NPeano.

From QuickChick RequireImport QuickChick.

RequireExport Utils.
RequireExport Labels.
RequireExport Instructions.
RequireExport Memory.
RequireExport Lab4.
RequireExport Indist.
RequireExport Machine.

Module Lab4M <: FINLAT.
Definition Label := Lab4.
Definition FLat := FiniteLattice_Lab4.
End Lab4M.

Module MachineLab4M := MachineM Lab4M.
Export MachineLab4M.

Module IndistLab4M := IndistM Lab4M.
Export IndistLab4M.


Definition pure {A : Type} (x : A) : G A := returnGen x.

(*
Fixpoint foldGen {A B : Type} (f : A -> B -> G A) (l : list B) (a : A)
: G A :=
 match l with
 | [] => returnGen a
 | (x :: xs) => bindGen (f a x) (foldGen f xs)
 end.
*)

(* Variation stuff - should be deleted -- CH: ha? it seems used *)
Inductive Variation {A : Type} :=
| Var : Lab4 -> A -> A -> Variation.

Class ShrinkV (A : Type) := { shrinkV : @Variation A -> list (@Variation A) }.
(* End of to be deleted *)

Definition validJump (st : State) (addr : Z) :=
let '(St imem _ _ _ _) := st in
 (Z.to_nat addr) <? (List.length imem).
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
RequireImport ZArith.
RequireImport Coq.Strings.String.
RequireImport NPeano.

From QuickChick RequireImport QuickChick.

RequireExport Utils.
RequireExport Labels.
RequireExport Instructions.
RequireExport Memory.
RequireExport Lab4.
RequireExport Indist.
RequireExport Machine.

Module Lab4M <: FINLAT.
Definition Label := Lab4.
Definition FLat := FiniteLattice_Lab4.
End Lab4M.

Module MachineLab4M := MachineM Lab4M.
Export MachineLab4M.

Module IndistLab4M := IndistM Lab4M.
Export IndistLab4M.


Definition pure {A : Type} (x : A) : G A := returnGen x.

(*
Fixpoint foldGen {A B : Type} (f : A -> B -> G A) (l : list B) (a : A)
: G A :=
 match l with
 | [] => returnGen a
 | (x :: xs) => bindGen (f a x) (foldGen f xs)
 end.
*)

(* Variation stuff - should be deleted -- CH: ha? it seems used *)
Inductive Variation {A : Type} :=
| Var : Lab4 -> A -> A -> Variation.

Class ShrinkV (A : Type) := { shrinkV : @Variation A -> list (@Variation A) }.
(* End of to be deleted *)

Definition validJump (st : State) (addr : Z) :=
let '(St imem _ _ _ _) := st in
 (Z.to_nat addr) <? (List.length imem).
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
RequireImport ZArith.
RequireImport Coq.Strings.String.
RequireImport NPeano.

From QuickChick RequireImport QuickChick.

RequireExport Utils.
RequireExport Labels.
RequireExport Instructions.
RequireExport Memory.
RequireExport Lab4.
RequireExport Indist.
RequireExport Machine.

Module Lab4M <: FINLAT.
Definition Label := Lab4.
Definition FLat := FiniteLattice_Lab4.
End Lab4M.

Module MachineLab4M := MachineM Lab4M.
Export MachineLab4M.

Module IndistLab4M := IndistM Lab4M.
Export IndistLab4M.


Definition pure {A : Type} (x : A) : G A := returnGen x.

(*
Fixpoint foldGen {A B : Type} (f : A -> B -> G A) (l : list B) (a : A)
: G A :=
 match l with
 | [] => returnGen a
 | (x :: xs) => bindGen (f a x) (foldGen f xs)
 end.
*)

(* Variation stuff - should be deleted -- CH: ha? it seems used *)
Inductive Variation {A : Type} :=
| Var : Lab4 -> A -> A -> Variation.

Class ShrinkV (A : Type) := { shrinkV : @Variation A -> list (@Variation A) }.
(* End of to be deleted *)

Definition validJump (st : State) (addr : Z) :=
let '(St imem _ _ _ _) := st in
 (Z.to_nat addr) <? (List.length imem).
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
RequireImport ZArith.
RequireImport Coq.Strings.String.
RequireImport NPeano.

From QuickChick RequireImport QuickChick.

RequireExport Utils.
RequireExport Labels.
RequireExport Instructions.
RequireExport Memory.
RequireExport Lab4.
RequireExport Indist.
RequireExport Machine.

Module Lab4M <: FINLAT.
Definition Label := Lab4.
Definition FLat := FiniteLattice_Lab4.
End Lab4M.

Module MachineLab4M := MachineM Lab4M.
Export MachineLab4M.

Module IndistLab4M := IndistM Lab4M.
Export IndistLab4M.


Definition pure {A : Type} (x : A) : G A := returnGen x.

(*
Fixpoint foldGen {A B : Type} (f : A -> B -> G A) (l : list B) (a : A)
: G A :=
 match l with
 | [] => returnGen a
 | (x :: xs) => bindGen (f a x) (foldGen f xs)
 end.
*)

(* Variation stuff - should be deleted -- CH: ha? it seems used *)
Inductive Variation {A : Type} :=
| Var : Lab4 -> A -> A -> Variation.

Class ShrinkV (A : Type) := { shrinkV : @Variation A -> list (@Variation A) }.
(* End of to be deleted *)

Definition validJump (st : State) (addr : Z) :=
let '(St imem _ _ _ _) := st in
 (Z.to_nat addr) <? (List.length imem).
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
RequireImport ZArith.
RequireImport Coq.Strings.String.
RequireImport NPeano.

From QuickChick RequireImport QuickChick.

RequireExport Utils.
RequireExport Labels.
RequireExport Instructions.
RequireExport Memory.
RequireExport Lab4.
RequireExport Indist.
RequireExport Machine.

Module Lab4M <: FINLAT.
Definition Label := Lab4.
Definition FLat := FiniteLattice_Lab4.
End Lab4M.

Module MachineLab4M := MachineM Lab4M.
Export MachineLab4M.

Module IndistLab4M := IndistM Lab4M.
Export IndistLab4M.


Definition pure {A : Type} (x : A) : G A := returnGen x.

(*
Fixpoint foldGen {A B : Type} (f : A -> B -> G A) (l : list B) (a : A)
: G A :=
 match l with
 | [] => returnGen a
 | (x :: xs) => bindGen (f a x) (foldGen f xs)
 end.
*)

(* Variation stuff - should be deleted -- CH: ha? it seems used *)
Inductive Variation {A : Type} :=
| Var : Lab4 -> A -> A -> Variation.

Class ShrinkV (A : Type) := { shrinkV : @Variation A -> list (@Variation A) }.
(* End of to be deleted *)

Definition validJump (st : State) (addr : Z) :=
let '(St imem _ _ _ _) := st in
 (Z.to_nat addr) <? (List.length imem).
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
RequireImport ZArith.
RequireImport Coq.Strings.String.
RequireImport NPeano.

From QuickChick RequireImport QuickChick.

RequireExport Utils.
RequireExport Labels.
RequireExport Instructions.
RequireExport Memory.
RequireExport Lab4.
RequireExport Indist.
RequireExport Machine.

Module Lab4M <: FINLAT.
Definition Label := Lab4.
Definition FLat := FiniteLattice_Lab4.
End Lab4M.

Module MachineLab4M := MachineM Lab4M.
Export MachineLab4M.

Module IndistLab4M := IndistM Lab4M.
Export IndistLab4M.


Definition pure {A : Type} (x : A) : G A := returnGen x.

(*
Fixpoint foldGen {A B : Type} (f : A -> B -> G A) (l : list B) (a : A)
: G A :=
 match l with
 | [] => returnGen a
 | (x :: xs) => bindGen (f a x) (foldGen f xs)
 end.
*)

(* Variation stuff - should be deleted -- CH: ha? it seems used *)
Inductive Variation {A : Type} :=
| Var : Lab4 -> A -> A -> Variation.

Class ShrinkV (A : Type) := { shrinkV : @Variation A -> list (@Variation A) }.
(* End of to be deleted *)

Definition validJump (st : State) (addr : Z) :=
let '(St imem _ _ _ _) := st in
 (Z.to_nat addr) <? (List.length imem).
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
RequireImport ZArith.
RequireImport Coq.Strings.String.
RequireImport NPeano.

From QuickChick RequireImport QuickChick.

RequireExport Utils.
RequireExport Labels.
RequireExport Instructions.
RequireExport Memory.
RequireExport Lab4.
RequireExport Indist.
RequireExport Machine.

Module Lab4M <: FINLAT.
Definition Label := Lab4.
Definition FLat := FiniteLattice_Lab4.
End Lab4M.

Module MachineLab4M := MachineM Lab4M.
Export MachineLab4M.

Module IndistLab4M := IndistM Lab4M.
Export IndistLab4M.


Definition pure {A : Type} (x : A) : G A := returnGen x.

(*
Fixpoint foldGen {A B : Type} (f : A -> B -> G A) (l : list B) (a : A)
: G A :=
 match l with
 | [] => returnGen a
 | (x :: xs) => bindGen (f a x) (foldGen f xs)
 end.
*)

(* Variation stuff - should be deleted -- CH: ha? it seems used *)
Inductive Variation {A : Type} :=
| Var : Lab4 -> A -> A -> Variation.

Class ShrinkV (A : Type) := { shrinkV : @Variation A -> list (@Variation A) }.
(* End of to be deleted *)

Definition validJump (st : State) (addr : Z) :=
let '(St imem _ _ _ _) := st in
 (Z.to_nat addr) <? (List.length imem).