## lustrec / optim / oversampling / out / typed / g_step_assert_5_Coq.v @ 6a93d814

History | View | Annotate | Download (4.11 KB)

1 |
(* ---------------------------------------------------------- *) |
---|---|

2 |
(* --- Assertion (file oversampling0_4.c, line 358) --- *) |

3 |
(* ---------------------------------------------------------- *) |

4 |
Require Import ZArith. |

5 |
Require Import Reals. |

6 |
Require Import BuiltIn. |

7 |
Require Import bool.Bool. |

8 |
Require Import int.Int. |

9 |
Require Import int.Abs. |

10 |
Require Import int.ComputerDivision. |

11 |
Require Import real.Real. |

12 |
Require Import real.RealInfix. |

13 |
Require Import real.FromInt. |

14 |
Require Import map.Map. |

15 |
Require Import Qedlib. |

16 |
Require Import Qed. |

17 | |

18 |
Require Import S_g_mem_pack. |

19 |
Require Import Memory. |

20 |
Require Import Cint. |

21 |
Require Import Compound. |

22 |
Require Import Axiomatic. |

23 |
Require Import Globals. |

24 |
Require Import S_f_mem_pack. |

25 | |

26 |
Goal |

27 |
let a := (shift_sint32 ((global (L_cpt_458)%Z)) 0%Z) in |

28 |
let a_1 := (shift_sint32 ((global (L_last_y_459)%Z)) 0%Z) in |

29 |
forall (i_5 i_4 i_3 i_2 i_1 i : Z), |

30 |
forall (t : array Z), |

31 |
forall (t_7 t_6 t_5 t_4 t_3 t_2 t_1 : farray addr Z), |

32 |
forall (t_8 : farray addr addr), |

33 |
forall (a_3 a_2 : addr), |

34 |
forall (g_1 g : S_g_mem_pack), |

35 |
let a_4 := t_8.[ (shiftfield_F_g_mem_ni_1 a_3) ] in |

36 |
let a_5 := t_8.[ (shiftfield_F_g_mem_ni_0 a_3) ] in |

37 |
let a_6 := t_8.[ (shiftfield_F_f_mem_ni_2 a_5) ] in |

38 |
let x := (t_6.[ a_1 ])%Z in |

39 |
let a_7 := (shiftfield_F__arrow_reg__first |

40 |
((shiftfield_F__arrow_mem__reg a_4))) in |

41 |
let x_1 := (t_7.[ a_7 ])%Z in |

42 |
let m := (((t_6.[ a <- (i)%Z ]).[ a_1 <- (i_1)%Z ]).[ (shiftfield_F_f_reg___f_2 |

43 |
((shiftfield_F_f_mem__reg |

44 |
a_5))) <- |

45 |
(i_3)%Z ]).[ (shiftfield_F__arrow_reg__first |

46 |
((shiftfield_F__arrow_mem__reg a_6))) <- (i_4)%Z ] in |

47 |
let x_2 := (m.[ a_1 ])%Z in |

48 |
((IsS_g_mem_pack g)) -> |

49 |
((IsS_g_mem_pack g_1)) -> |

50 |
((framed t_8)) -> |

51 |
((linked t)) -> |

52 |
((is_uint32 i_2%Z)) -> |

53 |
(a_2 <> a_4) -> |

54 |
((valid_rw t a_2 1%Z)) -> |

55 |
((P_valid_g t t_8 a_3)) -> |

56 |
((((region ((base a_2))%Z)) <= 0)%Z) -> |

57 |
((((region ((base a_3))%Z)) <= 0)%Z) -> |

58 |
((separated a_3 3%Z a_2 1%Z)) -> |

59 |
((P_g_pack3 t_8 t_7 g_1 a_3)) -> |

60 |
(a_2 <> a_6) -> |

61 |
(a_4 <> a_6) -> |

62 |
(a <> a_6) -> |

63 |
(a_1 <> a_6) -> |

64 |
((P_valid_f ((t.[ (L_cpt_458)%Z <- (1)%Z ]).[ (L_last_y_459)%Z <- (1)%Z ]) |

65 |
t_8 a_5)) -> |

66 |
((separated a_2 1%Z a_5 2%Z)) -> |

67 |
((separated a_3 3%Z a_5 2%Z)) -> |

68 |
((separated a_3 3%Z a_4 1%Z)) -> |

69 |
((separated a_5 2%Z a_4 1%Z)) -> |

70 |
((is_sint32 x)) -> |

71 |
((separated a_5 2%Z a 1%Z)) -> |

72 |
((separated a_5 2%Z a_1 1%Z)) -> |

73 |
((is_uint32 x_1)) -> |

74 |
((separated a_3 3%Z a_6 1%Z)) -> |

75 |
((separated a_5 2%Z a_6 1%Z)) -> |

76 |
(itep ((0 = x_1)%Z) (t_1 = t_7) (t_1 = (t_7.[ a_7 <- (0)%Z ]))) -> |

77 |
(itep ((0 = i_2)%Z) (t_4 = t_6) |

78 |
((t_4 = t_5) /\ (t_6 = (t_5.[ a_1 <- (i_5)%Z ])))) -> |

79 |
(itep ((0 = x_1)%Z) |

80 |
((t_1 = t_2) /\ |

81 |
(t_4 = |

82 |
(t_2.[ a_1 <- (t_2.[ (shiftfield_F_g_reg___g_2 |

83 |
((shiftfield_F_g_mem__reg a_3))) ])%Z ]))) |

84 |
((t_1 = t_3) /\ (t_4 = (t_3.[ a_1 <- (0)%Z ])))) -> |

85 |
((P_g_pack2 t_8 m g a_3)) -> |

86 |
(forall (g_2 : S_g_mem_pack), ((IsS_g_mem_pack g_2)) -> |

87 |
(forall (g_3 : S_g_mem_pack), (P_g_pack0) -> ((IsS_g_mem_pack g_3)) -> |

88 |
((P_g_pack3 t_8 t_7 g_2 a_3)) -> (P_trans_gA))) -> |

89 |
(forall (g_2 : S_g_mem_pack), ((IsS_g_mem_pack g_2)) -> |

90 |
(forall (g_3 : S_g_mem_pack), ((IsS_g_mem_pack g_3)) -> |

91 |
((P_g_pack1 t_8 t_4 g_3 a_3)) -> ((P_g_pack3 t_8 t_7 g_2 a_3)) -> |

92 |
((P_trans_gC g_2 g_3 (t_4.[ a_1 ])%Z)))) -> |

93 |
(forall (g_2 : S_g_mem_pack), ((IsS_g_mem_pack g_2)) -> |

94 |
(forall (g_3 : S_g_mem_pack), ((IsS_g_mem_pack g_3)) -> |

95 |
((P_g_pack1 t_8 t_1 g_3 a_3)) -> ((P_g_pack3 t_8 t_7 g_2 a_3)) -> |

96 |
((P_trans_gB g_2 g_3 x_1)))) -> |

97 |
(forall (g_2 : S_g_mem_pack), ((IsS_g_mem_pack g_2)) -> |

98 |
(forall (g_3 : S_g_mem_pack), ((IsS_g_mem_pack g_3)) -> |

99 |
((P_g_pack1 t_8 t_6 g_3 a_3)) -> ((P_g_pack3 t_8 t_7 g_2 a_3)) -> |

100 |
((P_trans_gD i_2%Z i_5%Z g_2 g_3 x)))) -> |

101 |
(forall (f : S_f_mem_pack), ((IsS_f_mem_pack f)) -> |

102 |
(forall (f_1 : S_f_mem_pack), ((IsS_f_mem_pack f_1)) -> |

103 |
((P_f_pack2 t_8 t_6 f a_5)) -> ((P_f_pack2 t_8 m f_1 a_5)) -> |

104 |
((P_trans_fF x f f_1 x_2 (m.[ a ])%Z)))) -> |

105 |
((P_trans_gE i_2%Z i_5%Z g_1 g x_2)). |

106 | |

107 |
Proof. |

108 |
auto with zarith. |

109 |
Qed. |

110 |