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

History | View | Annotate | Download (4.43 KB)

1 | 6a93d814 | xthirioux | (* ---------------------------------------------------------- *) |
---|---|---|---|

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

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_8 t_7 t_6 t_5 t_4 t_3 t_2 t_1 : farray addr Z), |
||

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

33 | forall (a_3 a_2 : addr), |
||

34 | forall (g_1 g : S_g_mem_pack), |
||

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

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

37 | let a_6 := t_9.[ (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_8.[ 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_9)) -> |
||

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_9 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_pack2 t_9 t_7 g a_3)) -> |
||

60 | ((P_g_pack3 t_9 t_8 g_1 a_3)) -> |
||

61 | (a_2 <> a_6) -> |
||

62 | (a_4 <> a_6) -> |
||

63 | (a <> a_6) -> |
||

64 | (a_1 <> a_6) -> |
||

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

66 | t_9 a_5)) -> |
||

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

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

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

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

71 | ((is_sint32 x)) -> |
||

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

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

74 | ((is_uint32 x_1)) -> |
||

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

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

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

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

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

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

81 | ((t_1 = t_2) /\ |
||

82 | (t_4 = |
||

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

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

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

86 | (itep ((0 = i_2)%Z) (t_7 = (m.[ a_2 <- x_2 ])) (t_7 = m)) -> |
||

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

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

89 | ((P_g_pack3 t_9 t_8 g_2 a_3)) -> (P_trans_gA))) -> |
||

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

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

92 | ((P_g_pack1 t_9 t_4 g_3 a_3)) -> ((P_g_pack3 t_9 t_8 g_2 a_3)) -> |
||

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

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

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

96 | ((P_g_pack1 t_9 t_1 g_3 a_3)) -> ((P_g_pack3 t_9 t_8 g_2 a_3)) -> |
||

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

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

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

100 | ((P_g_pack1 t_9 t_6 g_3 a_3)) -> ((P_g_pack3 t_9 t_8 g_2 a_3)) -> |
||

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

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

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

104 | ((P_f_pack2 t_9 t_6 f a_5)) -> ((P_f_pack2 t_9 m f_1 a_5)) -> |
||

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

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

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

108 | ((P_g_pack3 t_9 t_8 g_2 a_3)) -> ((P_g_pack2 t_9 m g_3 a_3)) -> |
||

109 | ((P_trans_gE i_2%Z i_5%Z g_2 g_3 x_2)))) -> |
||

110 | ((P_trans_gF i_2%Z i_5%Z g_1 g (t_7.[ a_2 ])%Z (t_7.[ a_1 ])%Z)). |
||

111 | |||

112 | Proof. |
||

113 | auto with zarith. |
||

114 | Qed. |