## lustrec / optim / oversampling / out / typed / f_step_assert_6.coq @ 6a93d814

History | View | Annotate | Download (3.09 KB)

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

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

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_f_mem_pack. |
||

19 | Require Import Memory. |
||

20 | Require Import Cint. |
||

21 | Require Import Compound. |
||

22 | Require Import Axiomatic. |
||

23 | |||

24 | Goal |
||

25 | forall (i_1 i : Z), |
||

26 | forall (t : array Z), |
||

27 | forall (t_2 t_1 : farray addr Z), |
||

28 | forall (t_3 : farray addr addr), |
||

29 | forall (a_2 a_1 a : addr), |
||

30 | forall (f_1 f : S_f_mem_pack), |
||

31 | let a_3 := t_3.[ (shiftfield_F_f_mem_ni_2 a_2) ] in |
||

32 | let x := (1%Z + i_1%Z)%Z in |
||

33 | let m := t_2.[ a_1 <- x ] in |
||

34 | let a_4 := (shiftfield_F__arrow_reg__first |
||

35 | ((shiftfield_F__arrow_mem__reg a_3))) in |
||

36 | let x_1 := (m.[ a_4 ])%Z in |
||

37 | let x_2 := (1%Z + i%Z)%Z in |
||

38 | let m_1 := t_1.[ a <- x_2 ] in |
||

39 | let a_5 := (shiftfield_F_f_reg___f_2 ((shiftfield_F_f_mem__reg a_2))) in |
||

40 | let m_2 := m_1.[ a_5 <- x_2 ] in |
||

41 | let x_3 := (t_1.[ a_1 ])%Z in |
||

42 | (a <> a_1) -> |
||

43 | ((IsS_f_mem_pack f)) -> |
||

44 | ((IsS_f_mem_pack f_1)) -> |
||

45 | ((framed t_3)) -> |
||

46 | ((linked t)) -> |
||

47 | ((is_sint32 i%Z)) -> |
||

48 | ((is_sint32 i_1%Z)) -> |
||

49 | (a <> a_3) -> |
||

50 | (a_1 <> a_3) -> |
||

51 | ((valid_rw t a 1%Z)) -> |
||

52 | ((valid_rw t a_1 1%Z)) -> |
||

53 | ((P_valid_f t t_3 a_2)) -> |
||

54 | ((((region ((base a))%Z)) <= 0)%Z) -> |
||

55 | ((((region ((base a_1))%Z)) <= 0)%Z) -> |
||

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

57 | ((separated a_2 2%Z a 1%Z)) -> |
||

58 | ((separated a_2 2%Z a_1 1%Z)) -> |
||

59 | ((P_f_pack2 t_3 t_2 f_1 a_2)) -> |
||

60 | ((separated a_2 2%Z a_3 1%Z)) -> |
||

61 | ((is_uint32 x_1)) -> |
||

62 | ((P_f_pack2 t_3 m_2 f a_2)) -> |
||

63 | (itep ((0 = x_1)%Z) (t_1 = m) (t_1 = (m.[ a_4 <- (0)%Z ]))) -> |
||

64 | (itep ((0 = x_1)%Z) ((i = (t_1.[ a_5 ]))%Z) ((0 = i)%Z)) -> |
||

65 | (forall (f_2 : S_f_mem_pack), ((IsS_f_mem_pack f_2)) -> |
||

66 | (forall (f_3 : S_f_mem_pack), (P_f_pack0) -> ((IsS_f_mem_pack f_3)) -> |
||

67 | ((P_f_pack2 t_3 t_2 f_2 a_2)) -> (P_trans_fA))) -> |
||

68 | (forall (f_2 : S_f_mem_pack), ((IsS_f_mem_pack f_2)) -> |
||

69 | (forall (f_3 : S_f_mem_pack), (P_f_pack0) -> ((IsS_f_mem_pack f_3)) -> |
||

70 | ((P_f_pack2 t_3 t_2 f_2 a_2)) -> ((P_trans_fB i_1%Z x)))) -> |
||

71 | (forall (f_2 : S_f_mem_pack), ((IsS_f_mem_pack f_2)) -> |
||

72 | (forall (f_3 : S_f_mem_pack), ((IsS_f_mem_pack f_3)) -> |
||

73 | ((P_f_pack1 t_3 t_1 f_3 a_2)) -> ((P_f_pack2 t_3 t_2 f_2 a_2)) -> |
||

74 | ((P_trans_fD i_1%Z f_2 f_3 x_3 i%Z)))) -> |
||

75 | (forall (f_2 : S_f_mem_pack), ((IsS_f_mem_pack f_2)) -> |
||

76 | (forall (f_3 : S_f_mem_pack), ((IsS_f_mem_pack f_3)) -> |
||

77 | ((P_f_pack2 t_3 t_2 f_2 a_2)) -> ((P_f_pack1 t_3 m_1 f_3 a_2)) -> |
||

78 | ((P_trans_fE i_1%Z f_2 f_3 (m_1.[ a_1 ])%Z x_2)))) -> |
||

79 | (forall (f_2 : S_f_mem_pack), ((IsS_f_mem_pack f_2)) -> |
||

80 | (forall (f_3 : S_f_mem_pack), ((IsS_f_mem_pack f_3)) -> |
||

81 | ((P_f_pack1 t_3 t_1 f_3 a_2)) -> ((P_f_pack2 t_3 t_2 f_2 a_2)) -> |
||

82 | ((P_trans_fC i_1%Z f_2 f_3 x_3 x_1)))) -> |
||

83 | ((P_trans_fF i_1%Z f_1 f (m_2.[ a_1 ])%Z (m_2.[ a ])%Z)). |