Library mathlib
Require Export include.
Require Export memory.
Require Export memdata.
Require Export assertion.
Require Export absop.
Require Export simulation.
Require Export language.
Require Export opsem.
Require Export os_program.
Require Export os_spec.
Require Export inferules.
Require Export os_code_notations.
Require Export os_code_defs.
Require Export os_ucos_h.
Require Export os_time.
Require Export baseTac.
Require Export auxdef.
Require Export seplog_lemmas.
Require Export seplog_tactics.
Require Export derivedrules.
Require Export hoare_conseq.
Require Export symbolic_execution.
Require Export hoare_assign.
Require Export hoare_lemmas.
Require Export BaseAsrtDef.
Require Export inv_prop.
Require Export InternalFunSpec.
Require Export IntLib.
Require Export List.
Require Export can_change_aop_proof.
Require Export cancel_absdata.
Require Export hoare_tactics.
Require Export type_val_match.
Require Export init_spec.
Require Export sep_pure.
Require Export mathsolver.
Require Export absop_rules.
Require Import Coq.Logic.FunctionalExtensionality.
Require Export common.
Require Export mathlib_join.
Set Implicit Arguments.
Close Scope nat_scope.
Open Scope Z_scope.
Open Scope code_scope.
Module ht.
Lemma a_div_b_multi_b_plus_b_ge_a: forall a b, 0<=a -> 0<b -> a/b*b +b >= a.
Ltac revs := match goal with
| |- ?a < ?b => cut (b > a); [intro; omega| idtac]
| |- ?a > ?b => cut (b < a); [intro; omega| idtac]
| |- ?a >= ?b => cut (b <= a); [intro; omega| idtac]
| |- ?a <= ?b => cut (b >= a); [intro; omega| idtac]
end.
Ltac revs´ H := match type of H with
| ?a < ?b => assert (b > a) by omega
| ?a > ?b => assert (b < a) by omega
| ?a >= ?b => assert (b <= a) by omega
| ?a <= ?b => assert (b >= a) by omega
end.
Lemma div_lt_lt: forall a b c, c > 0 -> a/c < b/c -> a<b.
Ltac bfunc_invert´ H :=
match type of H with
| (if ?e then true else false) = false => destruct (e); [inversion H|idtac]
end.
Ltac get_int_max := unfold Int.max_unsigned, Int.modulus; simpl.
Ltac rewrite_un_repr := rewrite Int.unsigned_repr;[ idtac| ht.get_int_max; omega].
Ltac rewrite_un_repr_in l := rewrite Int.unsigned_repr in l;[ idtac| ht.get_int_max; omega].
Ltac intrange x tac :=let xval := fresh in let xrange := fresh in destruct x as [xval xrange]; unfold Int.modulus, two_power_nat, shift_nat in xrange; simpl in xrange; simpl; tac.
Ltac handle_z2n_compare_nat rel z2nat_rule :=
let H0 := fresh in
match goal with
| |- rel ( Z.to_nat _ ) ?x => assert (Z.to_nat (Z.of_nat x) = x)%nat as H0 by (apply Nat2Z.id);rewrite <- H0; rewrite <- z2nat_rule;simpl; int auto
end.
Ltac handle_z2n_lt_nat := handle_z2n_compare_nat lt Z2Nat.inj_lt.
Ltac get_unsigned_sup_pow x p := let H := fresh in assert (Int.unsigned x < (two_p p)) by (unfold two_p; unfold two_power_pos; unfold shift_pos; simpl; omega).
Ltac get_unsigned_sz_sup´ x p := let H:= fresh in let H0 := fresh in let H1 := fresh in assert (0<=p) as H1 by omega; assert (0<=Int.unsigned x < two_p p ) as H by (split; [int auto| auto]); set (Int.size_interval_2 x _ H1 H) as H0.
Ltac get_unsigned_sz_sup x p:= get_unsigned_sup_pow x p; get_unsigned_sz_sup´ x p.
Ltac get_unsigned_sz_inf x := let H := fresh in assert (0<= Int.size x) by (set (Int.size_range x) as H; inversion H;auto).
Lemma int_not_0_sz_not_0 : forall n, Int.unsigned n = 0 <-> Int.size n = 0.
Lemma and_xy_x: forall x y, (forall n, 0<=n -> Z.testbit x n = true -> Z.testbit y n = true) -> Z.land x y = x.
Lemma lt_imply_le : forall n m: Z, n<m -> n<=m.
Lemma lt_is_gt : forall n m: Z, n<m <-> m>n.
Lemma le_is_ge : forall n m:Z, n<=m <-> m>=n.
Ltac bfunction_invert :=
let H := fresh in
match goal with
| Htmp: (if ?e then true else false) = true|-_ => assert (e = true) by (apply Classical_Prop.NNPP; intros H; apply not_true_is_false in H; rewrite H in Htmp; inversion Htmp)
end.
Lemma if_eq_true_cond_is_true: forall x:bool, (if x then true else false) = true <-> x =true.
Ltac tidspec_dec_true := try (rewrite TcbMod.set_a_get_a in *; [idtac | apply tidspec.eq_beq_true; auto]).
Ltac tidspec_dec_false := try (rewrite TcbMod.set_a_get_a´ in *; [idtac | apply tidspec.neq_beq_false; auto]).
Ltac tidspec_dec x y :=let t := fresh
with t1 := fresh
with t2 := fresh
in remember (Classical_Prop.classic (x=y)) as t; destruct t as [t1| t2]; [rewrite t1 in * ; tidspec_dec_true | tidspec_dec_false].
Ltac ecbspec_dec_true x := let H := fresh in let H0 := fresh in remember (EcbMod.beq_refl x) as H eqn: H0; clear H0; try rewrite (EcbMod.get_a_sig_a _ H); try rewrite H; try rewrite EcbMod.set_a_get_a; auto.
Ltac ecbspec_dec_false v Hneq := let H := fresh in let H0 := fresh in remember (tidspec.neq_beq_false Hneq) as H eqn:H0; clear H0; try rewrite (EcbMod.get_a_sig_a´ _ H); rewrite (EcbMod.set_a_get_a´ v _ H).
Ltac ecbspec_dec v x a := let H0 := fresh in let H0´ := fresh in remember (Classical_Prop.classic (x=a)) as H0 eqn: H0´; clear H0´; destruct H0;[ rewrite -> H0 in *; ecbspec_dec_true a | ecbspec_dec_false v H0].
Lemma nthval´_has_value : forall l len n, array_type_vallist_match Tint8 l -> length l = len -> (n < len)%nat ->exists x, nth_val´ n l = Vint32 x /\ true = rule_type_val_match Tint8 (Vint32 x).
Lemma disj_star_elim´´
: forall p q x y r: asrt, (( p\\//q\\//x\\//y) ** r) ==> (p**r) \\// (q**r) \\// (x**r) \\// (y**r).
Lemma mod_0_div_eq_eq: forall a b c, c>0 -> a mod c = b mod c -> a / c = b / c -> a =b.
Ltac solve_int_range i:= repeat ht.rewrite_un_repr; split; [try omega| ht.get_int_max;try ht.intrange i omega; try omega]; try ht.intrange i omega.
Ltac simpl_int_repr H := match type of (H) with
| $ (?x) = $ (?y) => let H´ := fresh in assert ( Int.unsigned ($ x) =Int.unsigned ($ y)) as H´ by (rewrite H; trivial);try rewrite Int.unsigned_repr in H´; repeat ht.rewrite_un_repr_in H´
end.
Ltac solve_mod_range tac := match goal with
| |- _ <= ?a mod ?x <= _ => let H:= fresh in assert (0<x) as H by omega;set (Z.mod_pos_bound a x H); tac; clear H
end.
Ltac copy H := let copy_of_H := fresh in let e:= fresh in remember H as copy_of_H eqn: e; clear e.
Ltac simpl_mod_in H := try rewrite Zminus_mod in H; try rewrite Z_mod_same_full in H; try rewrite <- Zminus_0_l_reverse in H; try rewrite <- Zmod_div_mod in H;[idtac| try omega ..| try (apply Zdivide_intro with 1; auto)].
Ltac clear_useless_int32 :=
match goal with
| a : int32 |- _ => clear dependent a
end.
Ltac clear_all_useless_int32 := repeat clear_useless_int32.
Lemma a_mult_b_ge_b : forall a b, 0<a -> 0<=b -> a*b >= b.
Lemma div_in_intrange: forall x a mx, 0<=x <=mx -> a>0 -> 0<=x/a<=mx.
Ltac solve_int_range´ :=
match goal with
| i : int32 |- _ => let xval := fresh in let xrange := fresh in destruct i as [xval xrange]; unfold Int.modulus, two_power_nat, shift_nat in xrange; simpl in xrange; simpl in *; solve_int_range´
| _ => subst; try rewrite max_unsigned_val; solve [ omega | apply div_in_intrange; omega ]
end.
Ltac rangesolver :=clear_all_useless_int32; try solve_int_range´; repeat (rewrite Int.unsigned_repr; try solve_int_range´).
Ltac ur_rewriter := rewrite Int.unsigned_repr; [idtac| try solve[rangesolver] ].
Ltac ur_rewriter_in H := rewrite Int.unsigned_repr in H; [idtac|clear H; try solve[rangesolver] ].
End ht.
Module kz.
Ltac trivial_ur_rewriterH H := repeat (rewrite Int.unsigned_repr in H; [idtac |solve [split;[omega| rewrite max_unsigned_val; omega]]]).
Ltac bfunc_invertH H := let HH := fresh in
match type of H with
| (if ?e then true else false) = false => rename H into HH; destruct e as [H|H]; [inversion HH|idtac]; clear HH
| (if ?e then true else false) = true => rename H into HH; destruct e as [H|H]; [idtac| inversion HH]; clear HH
end.
Ltac Iltu_simplerH H := unfold Int.ltu in H; bfunc_invertH H; try trivial_ur_rewriterH H.
Ltac Irepr_simplerH H := match type of (H) with
| $ (?x) = $ (?y) => let H´ := fresh in rename H into H´; assert ( Int.unsigned ($ x) =Int.unsigned ($ y)) as H by (rewrite H´; trivial);try rewrite Int.unsigned_repr in H; repeat ht.rewrite_un_repr_in H;clear H´
end.
Ltac trivial_mod_range := match goal with
| |- _ <= ?a mod ?x <= _ => let H:= fresh in assert (0<x) as H by omega;set (Z.mod_pos_bound a x H); omega; clear H
end.
Ltac Imod_simplerH H :=let H´ := fresh in unfold Int.modu in H; repeat trivial_ur_rewriterH H; try (Irepr_simplerH H;[idtac| rewrite max_unsigned_val; trivial_mod_range]).
Ltac Zmod_simplerH H k newval := match type of H with
| ?a mod ?n = ?b =>
let H´ := fresh in
rewrite <- (Z_mod_plus _ k) in H;[idtac|omega]; assert ( a + k * n = newval) as H´ by omega ; rewrite H´ in H; clear H´
end.
Lemma unsigned_ge0 : forall x, Int.unsigned x >=0.
Lemma Zplus_minus : forall z x, z+x-x=z.
Ltac ge0_solver := solve [omega| apply unsigned_ge0| apply Z_div_ge0; [omega| ge0_solver] ].
Ltac le0_solver := ht.revs; ge0_solver.
Ltac revsH H := let H´ := fresh in
match type of H with
| ?a < ?b => assert (a < b -> b > a) as H´ by omega; apply H´ in H; clear H´
| ?a > ?b => assert (a > b -> b < a) as H´ by omega; apply H´ in H; clear H´
| ?a >= ?b => assert (a>=b -> b <= a) as H´ by omega; apply H´ in H; clear H´
| ?a <= ?b => assert (a<=b -> b >= a) as H´ by omega; apply H´ in H; clear H´
end.
Ltac Zdivsup_simplerH H := match type of H with
| ?a / ?b < ?c =>
let H´´ := fresh in let H´ := fresh in let e := fresh in rewrite (Z.mul_lt_mono_pos_r b) in H; [idtac | omega]; rewrite (Z.add_lt_mono_r _ _ b ) in H; assert ( a / b * b + b >= a ) as H´´ by (apply (@ht.a_div_b_multi_b_plus_b_ge_a a b); omega); revsH H´´; remember (Z.le_lt_trans _ _ _ H´´ H) as H´ eqn: e; simpl in H´; clear e; clear H´´
end.
Ltac revs := match goal with
| |- ?a < ?b => cut (b > a); [intro; omega| idtac]
| |- ?a > ?b => cut (b < a); [intro; omega| idtac]
| |- ?a >= ?b => cut (b <= a); [intro; omega| idtac]
| |- ?a <= ?b => cut (b >= a); [intro; omega| idtac]
| |- (?a < ?b)%nat => cut (b > a)%nat; [intro; omega| idtac]
| |- (?a > ?b)%nat => cut (b < a)%nat; [intro; omega| idtac]
| |- (?a >= ?b)%nat => cut (b <= a)%nat; [intro; omega| idtac]
| |- (?a <= ?b)%nat => cut (b >= a)%nat; [intro; omega| idtac]
end.
End kz.
Lemma int_not_leq : forall i j, i>=0 -> j >=0 -> ~i + j < i.
Lemma Z_prop : forall x y a, 0<a -> (x + a * y - x) / a = y.
Lemma prio_destruct1 :
forall x, 0 <= x < 17 <->
x = 0 \/ x = 1 \/ x = 2 \/ x = 3 \/ x = 4 \/ x = 5 \/ x = 6 \/ x = 7 \/
x = 8 \/ x = 9 \/ x = 10 \/ x = 11 \/ x = 12 \/ x = 13 \/ x = 14 \/ x = 15 \/
x = 16.
Lemma int_aux :Int.unsigned ($ (0 + (4 + 0) - (0 + (4 + 0)))) / Int.unsigned ($ 4) =0.
Lemma prio_destruct2 :
forall x, 17 <= x < 32 <->
x = 17 \/ x = 18 \/ x = 19\/ x = 20 \/ x = 21 \/ x = 22 \/ x = 23 \/
x = 24 \/ x = 25 \/ x = 26 \/ x = 27 \/ x = 28 \/ x = 29 \/ x = 30 \/ x = 31.
Lemma prio_destruct3 :
forall x, 32 <= x < 48 <->
x = 32 \/ x = 33 \/ x = 34 \/ x = 35 \/ x = 36 \/ x = 37 \/ x = 38 \/ x = 39 \/
x = 40 \/ x = 41 \/ x = 42 \/ x = 43 \/ x = 44 \/ x = 45 \/ x = 46 \/ x = 47.
Lemma prio_destruct4 :
forall x, 48 <= x < 64 <->
x = 48 \/ x = 49 \/ x = 50 \/ x = 51 \/ x = 52 \/ x = 53 \/ x = 54 \/ x = 55 \/
x = 56 \/ x = 57 \/ x = 58 \/ x = 59 \/ x = 60 \/ x = 61 \/ x = 62 \/ x = 63.
Lemma prio_range_com :
forall x, 0 <= x < 17 \/ 17 <= x < 32 \/ 32 <= x < 48 \/ 48 <= x < 64 <->
0 <= x < 64.
Lemma prio_destruct :
forall x, 0 <= x < 64 <->
x = 0 \/ x = 1 \/ x = 2 \/ x = 3 \/ x = 4 \/ x = 5 \/ x = 6 \/ x = 7 \/
x = 8 \/ x = 9 \/ x = 10 \/ x = 11 \/ x = 12 \/ x = 13 \/ x = 14 \/ x = 15 \/
x = 16 \/ x = 17 \/ x = 18 \/ x = 19 \/ x = 20 \/ x = 21 \/ x = 22 \/ x = 23 \/
x = 24 \/ x = 25 \/ x = 26 \/ x = 27 \/ x = 28 \/ x = 29 \/ x = 30 \/ x = 31 \/
x = 32 \/ x = 33 \/ x = 34 \/ x = 35 \/ x = 36 \/ x = 37 \/ x = 38 \/ x = 39 \/
x = 40 \/ x = 41 \/ x = 42 \/ x = 43 \/ x = 44 \/ x = 45 \/ x = 46 \/ x = 47 \/
x = 48 \/ x = 49 \/ x = 50 \/ x = 51 \/ x = 52 \/ x = 53 \/ x = 54 \/ x = 55 \/
x = 56 \/ x = 57 \/ x = 58 \/ x = 59 \/ x = 60 \/ x = 61 \/ x = 62 \/ x = 63.
Lemma prio_prop :
forall prio,
0 <= prio ->
prio < 64 ->
Int.unsigned (Int.shru ($ prio) ($ 3)) < 8.
Lemma Z_le_nat :
forall x, (0<= x < 8)%Z-> ( ∘x < 8) %nat.
Lemma val_inj_1 :
val_inj
(if Int.ltu Int.zero (Int.notbool Int.one) &&Int.ltu Int.zero (Int.notbool Int.one)
then Some (Vint32 Int.one)
else Some (Vint32 Int.zero)) = Vint32 Int.zero.
Lemma isptr_vundef2:
forall x,
isptr x -> val_inj
(bool_and (val_inj (notint (val_inj (val_eq x Vnull))))
(Vint32 (Int.notbool Int.one))) <> Vundef.
Lemma val_inj_12 :
forall x , val_inj
(bool_and
(val_inj
(notint (val_inj (val_eq (Vptr (x, Int.zero)) Vnull))))
(Vint32 (Int.notbool Int.one))) = Vint32 Int.zero.
Lemma val_inj_12´ :
forall x , isptr x -> val_inj
(bool_and
(val_inj
(notint (val_inj (val_eq x Vnull))))
(Vint32 (Int.notbool Int.one))) = Vint32 Int.zero.
Lemma isptr_vundef_not :
forall x, isptr x -> val_inj
match val_inj (notint (val_inj (val_eq x Vnull))) with
| Vundef => None
| Vnull => None
| Vint32 n2 =>
if Int.ltu Int.zero (Int.notbool Int.one) && Int.ltu Int.zero n2
then Some (Vint32 Int.one)
else Some (Vint32 Int.zero)
| Vptr _ => None
end <> Vundef.
Lemma val_inj_122 :
forall x , isptr x ->val_inj
match val_inj (notint (val_inj (val_eq x Vnull))) with
| Vundef => None
| Vnull => None
| Vint32 n2 =>
if Int.ltu Int.zero (Int.notbool Int.one) &&
Int.ltu Int.zero n2
then Some (Vint32 Int.one)
else Some (Vint32 Int.zero)
| Vptr _ => None
end = Vint32 Int.zero.
Lemma val_eq_vundef:
forall i0,
val_inj
(if Int.eq i0 ($ OS_EVENT_TYPE_Q)
then Some (Vint32 Int.one)
else Some (Vint32 Int.zero)) <> Vundef.
Lemma val_eq_vundef´:
forall i0,
val_inj
(notint
(val_inj
(if Int.eq i0 ($ OS_EVENT_TYPE_Q)
then Some (Vint32 Int.one)
else Some (Vint32 Int.zero)))) <> Vundef.
Lemma val_inj_eq_q:
forall i0,
val_inj
(notint
(val_inj
(if Int.eq i0 ($ OS_EVENT_TYPE_Q)
then Some (Vint32 Int.one)
else Some (Vint32 Int.zero)))) = Vint32 Int.zero \/
val_inj
(notint
(val_inj
(if Int.eq i0 ($ OS_EVENT_TYPE_Q)
then Some (Vint32 Int.one)
else Some (Vint32 Int.zero)))) = Vnull ->
i0 = ($ OS_EVENT_TYPE_Q).
Lemma int_land_zero:
forall x, Int.zero&(Int.one<<(x &$ 7)) <> Int.one<<(x &$ 7).
Lemma nat8_des:
forall x2 Heq ,
(Heq < 8) %nat ->
match Heq with
| 0%nat => Some (Vint32 Int.zero)
| 1%nat => Some (Vint32 Int.zero)
| 2%nat => Some (Vint32 Int.zero)
| 3%nat => Some (Vint32 Int.zero)
| 4%nat => Some (Vint32 Int.zero)
| 5%nat => Some (Vint32 Int.zero)
| 6%nat => Some (Vint32 Int.zero)
| 7%nat => Some (Vint32 Int.zero)
| S (S (S (S (S (S (S (S _))))))) => None
end = Some (Vint32 x2) -> x2 = Int.zero.
Lemma ecbmod_get_sig_set:
forall v x y,
EcbMod.get v x = None ->
EcbMod.joinsig x y v (EcbMod.set v x y).
Lemma ecbmod_join_get :
forall x x0 x1 v´37 eid,
x <> eid -> EcbMod.joinsig x x0 x1 v´37 ->
EcbMod.get x1 eid = None -> EcbMod.get v´37 eid = None.
Lemma leftmoven:
forall n,
(0 <= n < 8)%nat ->
$ 1<<$ Z.of_nat n <> $ 0.
Lemma abs_disj_get_merge:
forall O´ O x y,
OSAbstMod.disj O´ O ->
OSAbstMod.get O x = Some y ->
OSAbstMod.get (OSAbstMod.merge O´ O) x = Some y.
Lemma disj_star_elim: forall p q r, ( p \\// q )** r ==> (p ** r) \\// (q ** r).
Lemma math_prop_l1: val_inj
(notint
(val_inj
(if Int.eq ($ OS_EVENT_TYPE_Q) ($ OS_EVENT_TYPE_Q)
then Some (Vint32 Int.one)
else Some (Vint32 Int.zero)))) = Vint32 Int.zero.
Lemma math_prop_l2 : val_inj
(if Int.eq ($ 1) ($ 0)
then Some (Vint32 Int.one)
else Some (Vint32 Int.zero)) = Vint32 Int.zero.
Lemma math_prop_l3 : val_inj
(notint
(val_inj
(if Int.eq ($1) ($ 0)
then Some (Vint32 Int.one)
else Some (Vint32 Int.zero)))) <> Vint32 Int.zero.
Ltac solve_disj:=
match goal with
| H : _ \/ _ |- _ =>
let Hx := fresh in
let Hy := fresh in
(destruct H as [Hx | Hy]; [subst; eexists; simpl; splits; eauto| idtac])
| _ => try (subst; eexists; simpl; splits; eauto)
end.
Lemma int8_neq0_ex:
forall i ,
Int.unsigned i <= 255 ->
Int.eq i ($ 0) = false ->
exists n, (0 <= n < 8)%nat /\ i &($ 1<<$ Z.of_nat n) = $ 1<<$ Z.of_nat n.
Lemma length8_ex:
forall v´40 :vallist,
length v´40 = ∘OS_EVENT_TBL_SIZE ->
exists v1 v2 v3 v4 v5 v6 v7 v8,
v´40 = v1::v2::v3::v4::v5::v6::v7::v8::nil.
Lemma int_true_le255:
forall x,
(if Int.unsigned x <=? Byte.max_unsigned then true else false) = true ->
Int.unsigned x <= 255.
Lemma n07_arr_len_ex:
forall n v´40,
(0 <= n < 8)%nat ->
array_type_vallist_match Int8u v´40 ->
length v´40 = ∘OS_EVENT_TBL_SIZE ->
exists v, nth_val n v´40 = Some (Vint32 v) /\ Int.unsigned v <= 255.
Lemma nat8_ex_shift3:
forall n,
(0 <= n < 8) %nat ->
exists y, $ Z.of_nat n = Int.shru ($ y) ( $ 3) /\ 0 <= y < 64.
Lemma math_des88:
forall n xx,
(0 <= n < 8)%nat ->
(xx = $ 0 \/
xx = $ 1 \/
xx = $ 2 \/ xx = $ 3 \/ xx = $ 4 \/ xx = $ 5 \/ xx = $ 6 \/ xx = $ 7) ->
exists y, 0 <= y < 64 /\ xx = $ y & $ 7 /\ ($ Z.of_nat n = Int.shru ($ y) ( $ 3)).
Lemma ltu_ex_and :
forall vv,
Int.ltu ($ 0) vv = true->
Int.unsigned vv <= 255 ->
exists x,
vv&(Int.one<< x) = Int.one<< x /\
(x = $0 \/ x = $1 \/ x = $2 \/ x = $3 \/
x = $4 \/ x = $5 \/ x = $6 \/ x = $7).
Lemma eight_destruct: forall x, 0<=x<8 <-> x=0 \/ x=1 \/ x=2\/x=3\/x=4\/x=5\/x=6\/x=7.
Qed.
Lemma prio_inq:
forall vv n v´40,
(0 <= n < 8)%nat ->
Int.ltu ($ 0) vv = true ->
Int.unsigned vv <= 255 ->
nth_val n v´40 = Some (Vint32 vv) ->
exists prio,
PrioWaitInQ prio v´40.
Lemma inlist_ex :
forall x4 (x:tidspec.A),
In x x4 -> exists y z, x4 = y :: z.
Lemma l4 : forall i, val_inj
(notint
(val_inj
(if Int.eq i ($ 0)
then Some (Vint32 Int.one)
else Some (Vint32 Int.zero)))) <>
Vint32 Int.zero -> Int.eq i ($ 0) = false.
Lemma list_prop1 : forall (t: Type) (a:t) (l1 l2: list t), l1 ++ ((a::nil) ++ l2) = l1 ++ (a::l2).
Lemma l5 : forall i , val_inj
(notint
(val_inj
(if Int.eq i ($ 0)
then Some (Vint32 Int.one)
else Some (Vint32 Int.zero)))) = Vint32 Int.zero \/
val_inj
(notint
(val_inj
(if Int.eq i ($ 0)
then Some (Vint32 Int.one)
else Some (Vint32 Int.zero)))) = Vnull -> i = $ 0.
Lemma ecblistp_length_eq_1 : forall x y l1 l2 t1 t2,
ECBList_P x y l1 l2 t1 t2 -> length l1 = length l2.
Lemma ecblistp_length_eq : forall x l1 z l2 l1´ z´ l2´ t1 t2,
ECBList_P x Vnull (l1 ++ (z::nil) ++ l2) (l1´ ++ (z´::nil) ++ l2´) t1 t2-> length l1 = length l1´ -> length l2 = length l2´.
Lemma ECBList_last_val :
forall x y v1 v2 v3 v4,
v1 <> nil ->
ECBList_P x y v1 v2 v3 v4 ->
exists a b, last v1 (nil,nil) = (a,b)
/\ nth_val 5 a = Some y.
Lemma get_eidls_inlist: forall x ls,
In x (get_eidls x ls).
Inductive listsub (T : Type) : list T -> list T -> Prop :=
| listsub1:forall x, listsub nil x
| listsubrec: forall x y lsx lsy, x = y ->
listsub lsx lsy ->
listsub (x :: lsx) (y :: lsy).
Lemma list_sub_prop1 :
forall v1 (z:EventCtr) v1´, listsub (v1++(z::nil)) (v1 ++(z::v1´)).
Lemma list_sub_prop2 :
forall x y, listsub x y -> listsub (get_eid_ecbls x) (get_eid_ecbls y).
Lemma removelast_prop:
forall (t: Type) (a : t) x , x <> nil -> removelast (a::x) = a :: removelast x.
Lemma list_sub_prop3 :
forall (x : val) y z , listsub y z -> In x y -> In x z.
Lemma list_sub_prop4 :
forall (x :vallist) y, listsub x y -> listsub (removelast x) (removelast y).
Lemma nil_get_eid_nil:
forall x, x <> nil -> get_eid_ecbls x <> nil.
Lemma in_get_eidls :
forall v1 y x z vl´,
In y (get_eidls x (v1 ++ (z :: nil)))
->In y (get_eidls x (v1 ++ (z :: vl´))).
Lemma get_remove_exchange:
forall x, removelast (get_eid_ecbls x) = get_eid_ecbls (removelast x).
Ltac usimpl H := unfolds in H; simpl in H; inverts H.
Lemma ecbmod_joinsig_get :
forall x y mqls mqls´,
EcbMod.joinsig x y mqls mqls´ ->
EcbMod.get mqls´ x = Some y.
Lemma qwaitset_notnil_ex:
forall qwaitset : waitset ,
qwaitset <> nil ->
exists tid, In tid qwaitset.
Lemma prioinq_exists:
forall prio v´58,
PrioWaitInQ prio v´58 ->
exists n,
(0 <= n < 8)%nat /\ nth_val n v´58 <> Some (V$0).
Lemma int_usign_eq :
forall m,
0 <= m -> m <= Int.max_unsigned ->
(Int.unsigned ($ m)) = m.
Lemma ecbmod_joinsig_sig:
forall x y mqls mqls´,
EcbMod.joinsig x y mqls mqls´ ->
EcbMod.join mqls (EcbMod.sig x y) mqls´.
Lemma ecbmod_get_join_get:
forall eid y m x z t,
eid <> y ->
EcbMod.get m eid = Some t ->
EcbMod.join x (EcbMod.sig y z) m ->
EcbMod.get x eid = Some t.
Lemma ecbjoin_sig_join : forall x x1 v´35 x0 v´61 v3 i5,
EcbMod.join x x1 v´35 ->
EcbMod.join x0
(EcbMod.sig (v´61, Int.zero) (absmsgq v3 i5, nil))
x1 -> exists y, EcbMod.join x0 x y /\ EcbMod.join y
(EcbMod.sig (v´61, Int.zero) (absmsgq v3 i5, nil)) v´35.
Lemma length_zero_nil : forall (t : Type) (x : list t), length x = 0%nat -> x = nil.
Lemma nil_simp : forall (t : Type) (x : list t), nil ++ x = x.
Lemma ge_0_minus_1_in_range:
forall i2,
Int.unsigned i2 <= 65535 ->
Int.ltu ($ 0) i2 = true ->
Int.unsigned (i2 -ᵢ $ 1) <=? Int16.max_unsigned = true.
Lemma qacc_dl_vl_match:
forall vl, true = dl_vl_match ((dcons pevent (Tptr OS_EVENT) ) dnil) (rev vl) -> (exists v,vl = (Vptr v)::nil\/ vl =Vnull::nil) .
Lemma notint_neq_zero_eq:
forall x y,
val_inj
(notint
(val_inj
(if Int.eq x y
then Some (Vint32 Int.one)
else Some (Vint32 Int.zero)))) <>
Vint32 Int.zero -> Int.eq x y = false.
Lemma ecb_get_set_join_join:
forall ml a b ml1 ml2 ml1´ b´,
EcbMod.get ml a = Some b ->
EcbMod.joinsig a
b ml1´ ml1 ->
EcbMod.join ml2 ml1 ml ->
exists ml1n, EcbMod.joinsig a b´ ml1´ ml1n /\ EcbMod.join ml2 ml1n (EcbMod.set ml a b´).
Fixpoint all_elem_p {X:Type} p (l: @list X) :=
match l with
| nil => True
| h :: t => p h = true /\ all_elem_p p t
end.
Lemma array_type_vallist_match_is_all_elem_p: forall t l, array_type_vallist_match t l <-> all_elem_p (rule_type_val_match t) l.
Lemma all_elem_hold_for_upd: forall n x l p, all_elem_p p l -> p x = true -> all_elem_p p (update_nth_val n l x).
Lemma not_and_p: forall v´41 v´12, Int.unsigned v´12 <= 255 ->Int.unsigned v´41 <= 128 -> Int.unsigned (v´12&Int.not v´41) <= 255.
Lemma not_and_p´: forall v´41 v´12, Int.unsigned v´12 <= 255 ->Int.unsigned v´41 <= 255 -> Int.unsigned (v´12&Int.not v´41) <= 255.
Lemma array_type_vallist_match_int8u_update_hold:
forall v´38 v´69 v´40 v´13,
length v´13 = ∘OS_EVENT_TBL_SIZE ->
Int.unsigned v´38 <= 7 ->
Int.unsigned v´69 <= 255 ->
Int.unsigned v´40 <= 128 ->
array_type_vallist_match Int8u v´13 ->
array_type_vallist_match Int8u
(update_nth_val (Z.to_nat (Int.unsigned v´38)) v´13
(Vint32 (v´69&Int.not v´40))).
Lemma array_type_vallist_match_int8u_update_hold_255:
forall v´38 v´69 v´40 v´13,
length v´13 = ∘OS_EVENT_TBL_SIZE ->
Int.unsigned v´38 <= 7 ->
Int.unsigned v´69 <= 255 ->
Int.unsigned v´40 <= 255 ->
array_type_vallist_match Int8u v´13 ->
array_type_vallist_match Int8u
(update_nth_val (Z.to_nat (Int.unsigned v´38)) v´13
(Vint32 (v´69&Int.not v´40))).
Lemma int_unsigned_or_prop:
forall v´57 v´41,
Int.unsigned v´57 <= 255 ->
Int.unsigned v´41 <= 128 ->
Int.unsigned (Int.or v´57 v´41) <= 255.
Lemma array_type_vallist_match_int8u_update_hold´:
forall v´37 ( v´38 v´40 : int32) (v´13 : list val),
length v´37 = nat_of_Z OS_RDY_TBL_SIZE ->
array_type_vallist_match Tint8 v´37 ->
length v´13 = nat_of_Z OS_EVENT_TBL_SIZE ->
Int.unsigned v´38 <= 7 ->
Int.unsigned v´40 <= 128 ->
array_type_vallist_match Tint8 v´13 ->
array_type_vallist_match Tint8
(update_nth_val (Z.to_nat (Int.unsigned v´38)) v´13
(val_inj
(or (nth_val´ (Z.to_nat (Int.unsigned v´38)) v´37) (Vint32 v´40)))).
Lemma length_n_change:
forall v´38 v´37 v´40,
length v´37 = nat_of_Z OS_RDY_TBL_SIZE ->
Int.unsigned v´38 <= 7 ->
length
(update_nth_val (Z.to_nat (Int.unsigned v´38)) v´37
(val_inj
(or (nth_val´ (Z.to_nat (Int.unsigned v´38)) v´37) (Vint32 v´40)))) =
nat_of_Z OS_RDY_TBL_SIZE.
Lemma disj_star_elim´
: forall p q x y r z: asrt, ((p \\// q \\// x \\// y)** z) ** r ==> (p ** z ** r) \\// (q ** z ** r) \\// (x** z** r) \\// (y** z ** r).
Lemma ltu_eq_false: forall i1 i2, Int.ltu i2 i1 = true -> Int.eq i1 i2 = false.
Lemma val_inj_i1_i2_lt:
forall i1 i2,
val_inj
(bool_or
(val_inj
(if Int.ltu i2 i1
then Some (Vint32 Int.one)
else Some (Vint32 Int.zero)))
(val_inj
(if Int.eq i1 i2
then Some (Vint32 Int.one)
else Some (Vint32 Int.zero)))) = Vint32 Int.zero \/
val_inj
(bool_or
(val_inj
(if Int.ltu i2 i1
then Some (Vint32 Int.one)
else Some (Vint32 Int.zero)))
(val_inj
(if Int.eq i1 i2
then Some (Vint32 Int.one)
else Some (Vint32 Int.zero)))) = Vnull -> Int.ltu i1 i2 = true.
Lemma val_inj_eq_p:
forall x6 v´49 x,
isptr x6 ->
val_inj
match x6 with
| Vundef => None
| Vnull => Some (Vint32 Int.zero)
| Vint32 _ => None
| Vptr (b2, ofs2) =>
if peq v´49 b2
then
if Int.eq (x+ᵢInt.mul ($ 1) ($ 4)) ofs2
then Some (Vint32 Int.one)
else Some (Vint32 Int.zero)
else Some (Vint32 Int.zero)
end <> Vint32 Int.zero -> x6 = Vptr (v´49, (x+ᵢInt.mul ($ 1) ($ 4)) ).
Lemma val_inj_eq_elim:
forall x6 v´49 x,
val_inj
match x6 with
| Vundef => None
| Vnull => Some (Vint32 Int.zero)
| Vint32 _ => None
| Vptr (b2, ofs2) =>
if peq v´49 b2
then
if Int.eq (x+ᵢInt.mul ($ 1) ($ 4)) ofs2
then Some (Vint32 Int.one)
else Some (Vint32 Int.zero)
else Some (Vint32 Int.zero)
end = Vint32 Int.zero \/
val_inj
match x6 with
| Vundef => None
| Vnull => Some (Vint32 Int.zero)
| Vint32 _ => None
| Vptr (b2, ofs2) =>
if peq v´49 b2
then
if Int.eq (x+ᵢInt.mul ($ 1) ($ 4)) ofs2
then Some (Vint32 Int.one)
else Some (Vint32 Int.zero)
else Some (Vint32 Int.zero)
end = Vnull -> x6 <> Vptr (v´49, (x+ᵢInt.mul ($ 1) ($ 4))).
Lemma isptr_val_inj_false: forall x0, isptr x0 -> val_inj (val_eq x0 Vnull) = Vnull -> False.
Definition myAnd := Logic.and.
Lemma array_int8u_nth_lt_len :
forall vl m,
array_type_vallist_match Int8u vl ->
(m < length vl)%nat ->
exists i, nth_val´ m vl = Vint32 i /\ Int.unsigned i <= 255.
Lemma int_lemma1:
forall i1 i2,
Int.unsigned i1 <= 255 ->
Int.unsigned i2 <= 255 ->
Int.unsigned (i1 & Int.not i2) <= 255.
Lemma array_type_vallist_match_hold :
forall vl n t v,
array_type_vallist_match t vl ->
(n < length vl)%nat ->
rule_type_val_match t v = true ->
array_type_vallist_match t (update_nth_val n vl v).
Lemma tcbmod_neq_set_get:
forall x y b tcbls,
x <> y ->
TcbMod.get (TcbMod.set tcbls y b) x = TcbMod.get tcbls x.
Lemma ltu_zero_eq_zero:
forall i, Int.unsigned i <= 65535 -> false = Int.ltu ($ 0) i -> i = Int.zero.
Lemma bool_and_true_1 : forall {v1 v2 x},
istrue x = Some true -> bool_and v1 v2 = Some x ->
exists n1, v1 = Vint32 n1 /\ Int.ltu Int.zero n1 = true.
Lemma ltu_zero_notbool_true : forall {i2},
Int.ltu Int.zero (Int.notbool i2) = true -> Int.eq i2 Int.zero = true.
Lemma val_eq_zero_neq : forall {v1 v2 i},
val_eq v1 v2 = Some (Vint32 i) -> Int.eq i Int.zero = true -> v1 <> v2.
Lemma bool_and_true_gt: forall {v1 v2 x},
bool_and v1 v2 = Some x -> istrue x = Some true ->
exists n1 n2, v1 = Vint32 n1 /\ v2 = Vint32 n2 /\ Int.ltu Int.zero n1 = true /\ Int.ltu Int.zero n2 = true.
Lemma list_cons_assoc : forall {A} l1 l2 (n:A),
l1 ++ n :: l2 = (l1 ++ n::nil) ++ l2.
Lemma upd_vallist_eq_length: forall vl n v´,
length vl = length (update_nth_val n vl v´).
Lemma vallist_destru:
forall vl:vallist , length vl = ∘OS_EVENT_TBL_SIZE ->
exists v1 v2 v3 v4,
exists v5 v6 v7 v8,
vl = v1 ::v2 ::v3 ::v4 ::v5 ::v6::v7::v8 :: nil.
Lemma eq_1 :Int.zero+ᵢ($ 4+ᵢ($ 2+ᵢ($ 1+ᵢ$ 1))) = $ 8.
Lemma eq_2 : $ 8+ᵢ ($ 1) = $ 9.
Lemma eq_3 : $ 9+ᵢ ($ 1) = $10.
Lemma eq_4 : $ 10+ᵢ($ 1) = $11.
Lemma eq_5 : $11+ᵢ ($ 1) = $ 12.
Lemma eq_6 : $ 12+ᵢ ($ 1) = $ 13.
Lemma eq_7 : $ 13+ᵢ($ 1) = $ 14.
Lemma eq_8 : $ 14+ᵢ ($ 1) = $ 15.
Lemma eq_9 : $0+ᵢ$ 1 = $1.
Lemma eq_10 :$1+ᵢ$ 1 = $2.
Lemma eq_11 :$2+ᵢ$2 = $4.
Lemma eq_12 :$4+ᵢ$4 = $8.
Lemma eq_13 :$8+ᵢ$8 = $16.
Lemma xx:forall P Q R, (P \\// Q) ** R ==> (P ** R) \\// (Q ** R).
Lemma is_length_neq_zero_elim:
forall v´1, val_inj (val_eq (is_length (0%nat :: v´1)) (V$1)) <> Vint32 Int.zero -> v´1=nil.
Lemma true_if_else_true: forall x, x =true -> (if x then true else false) = true.
Ltac rtmatch_solve:=
apply true_if_else_true;
apply Zle_is_le_bool;
try rewrite byte_max_unsigned_val; try rewrite max_unsigned_val;
try omega.
Lemma z_le_7_imp_n: forall x, Int.unsigned x <= 7 -> (Z.to_nat (Int.unsigned x) < 8)%nat.
Lemma z_le_255_imp_n: forall x, Int.unsigned x <= 255 -> (Z.to_nat (Int.unsigned x) < 256)%nat.
Lemma OSUnMapVallist_type_vallist_match: array_type_vallist_match Tint8 OSUnMapVallist.
Lemma pos_to_nat_range_0_255:
forall z, 0<=z -> z<=255 -> (0<=Z.to_nat z<=255)%nat.
Lemma sn_le_n_le_minus1:
forall (n x:nat), (S n <= x -> n <= x-1)%nat.
Lemma osunmapvallist_prop:
forall i, (Int.unsigned i <= 255) -> exists x, nth_val´ (Z.to_nat (Int.unsigned i)) OSUnMapVallist = Vint32 x /\ Int.unsigned x <=?7 = true.
Lemma int_iwordsize_gt_3:
Int.ltu ($ 3) Int.iwordsize = true.
Lemma shl3_add_range:
forall x x0,
(Int.unsigned x <=? 7) = true ->
(Int.unsigned x0 <=? 7) = true ->
Int.unsigned ((x<<$ 3) +ᵢ x0) <=? 63 =true.
Ltac auto_shiftl := unfold Z.shiftl; unfold Pos.iter; int auto.
Lemma int_unsigned_le_z2nat_lt:
forall x z,Int.unsigned x <= z ->
(Z.to_nat (Int.unsigned x) < Z.to_nat (z+1))%nat.
Require Export memory.
Require Export memdata.
Require Export assertion.
Require Export absop.
Require Export simulation.
Require Export language.
Require Export opsem.
Require Export os_program.
Require Export os_spec.
Require Export inferules.
Require Export os_code_notations.
Require Export os_code_defs.
Require Export os_ucos_h.
Require Export os_time.
Require Export baseTac.
Require Export auxdef.
Require Export seplog_lemmas.
Require Export seplog_tactics.
Require Export derivedrules.
Require Export hoare_conseq.
Require Export symbolic_execution.
Require Export hoare_assign.
Require Export hoare_lemmas.
Require Export BaseAsrtDef.
Require Export inv_prop.
Require Export InternalFunSpec.
Require Export IntLib.
Require Export List.
Require Export can_change_aop_proof.
Require Export cancel_absdata.
Require Export hoare_tactics.
Require Export type_val_match.
Require Export init_spec.
Require Export sep_pure.
Require Export mathsolver.
Require Export absop_rules.
Require Import Coq.Logic.FunctionalExtensionality.
Require Export common.
Require Export mathlib_join.
Set Implicit Arguments.
Close Scope nat_scope.
Open Scope Z_scope.
Open Scope code_scope.
Module ht.
Lemma a_div_b_multi_b_plus_b_ge_a: forall a b, 0<=a -> 0<b -> a/b*b +b >= a.
Ltac revs := match goal with
| |- ?a < ?b => cut (b > a); [intro; omega| idtac]
| |- ?a > ?b => cut (b < a); [intro; omega| idtac]
| |- ?a >= ?b => cut (b <= a); [intro; omega| idtac]
| |- ?a <= ?b => cut (b >= a); [intro; omega| idtac]
end.
Ltac revs´ H := match type of H with
| ?a < ?b => assert (b > a) by omega
| ?a > ?b => assert (b < a) by omega
| ?a >= ?b => assert (b <= a) by omega
| ?a <= ?b => assert (b >= a) by omega
end.
Lemma div_lt_lt: forall a b c, c > 0 -> a/c < b/c -> a<b.
Ltac bfunc_invert´ H :=
match type of H with
| (if ?e then true else false) = false => destruct (e); [inversion H|idtac]
end.
Ltac get_int_max := unfold Int.max_unsigned, Int.modulus; simpl.
Ltac rewrite_un_repr := rewrite Int.unsigned_repr;[ idtac| ht.get_int_max; omega].
Ltac rewrite_un_repr_in l := rewrite Int.unsigned_repr in l;[ idtac| ht.get_int_max; omega].
Ltac intrange x tac :=let xval := fresh in let xrange := fresh in destruct x as [xval xrange]; unfold Int.modulus, two_power_nat, shift_nat in xrange; simpl in xrange; simpl; tac.
Ltac handle_z2n_compare_nat rel z2nat_rule :=
let H0 := fresh in
match goal with
| |- rel ( Z.to_nat _ ) ?x => assert (Z.to_nat (Z.of_nat x) = x)%nat as H0 by (apply Nat2Z.id);rewrite <- H0; rewrite <- z2nat_rule;simpl; int auto
end.
Ltac handle_z2n_lt_nat := handle_z2n_compare_nat lt Z2Nat.inj_lt.
Ltac get_unsigned_sup_pow x p := let H := fresh in assert (Int.unsigned x < (two_p p)) by (unfold two_p; unfold two_power_pos; unfold shift_pos; simpl; omega).
Ltac get_unsigned_sz_sup´ x p := let H:= fresh in let H0 := fresh in let H1 := fresh in assert (0<=p) as H1 by omega; assert (0<=Int.unsigned x < two_p p ) as H by (split; [int auto| auto]); set (Int.size_interval_2 x _ H1 H) as H0.
Ltac get_unsigned_sz_sup x p:= get_unsigned_sup_pow x p; get_unsigned_sz_sup´ x p.
Ltac get_unsigned_sz_inf x := let H := fresh in assert (0<= Int.size x) by (set (Int.size_range x) as H; inversion H;auto).
Lemma int_not_0_sz_not_0 : forall n, Int.unsigned n = 0 <-> Int.size n = 0.
Lemma and_xy_x: forall x y, (forall n, 0<=n -> Z.testbit x n = true -> Z.testbit y n = true) -> Z.land x y = x.
Lemma lt_imply_le : forall n m: Z, n<m -> n<=m.
Lemma lt_is_gt : forall n m: Z, n<m <-> m>n.
Lemma le_is_ge : forall n m:Z, n<=m <-> m>=n.
Ltac bfunction_invert :=
let H := fresh in
match goal with
| Htmp: (if ?e then true else false) = true|-_ => assert (e = true) by (apply Classical_Prop.NNPP; intros H; apply not_true_is_false in H; rewrite H in Htmp; inversion Htmp)
end.
Lemma if_eq_true_cond_is_true: forall x:bool, (if x then true else false) = true <-> x =true.
Ltac tidspec_dec_true := try (rewrite TcbMod.set_a_get_a in *; [idtac | apply tidspec.eq_beq_true; auto]).
Ltac tidspec_dec_false := try (rewrite TcbMod.set_a_get_a´ in *; [idtac | apply tidspec.neq_beq_false; auto]).
Ltac tidspec_dec x y :=let t := fresh
with t1 := fresh
with t2 := fresh
in remember (Classical_Prop.classic (x=y)) as t; destruct t as [t1| t2]; [rewrite t1 in * ; tidspec_dec_true | tidspec_dec_false].
Ltac ecbspec_dec_true x := let H := fresh in let H0 := fresh in remember (EcbMod.beq_refl x) as H eqn: H0; clear H0; try rewrite (EcbMod.get_a_sig_a _ H); try rewrite H; try rewrite EcbMod.set_a_get_a; auto.
Ltac ecbspec_dec_false v Hneq := let H := fresh in let H0 := fresh in remember (tidspec.neq_beq_false Hneq) as H eqn:H0; clear H0; try rewrite (EcbMod.get_a_sig_a´ _ H); rewrite (EcbMod.set_a_get_a´ v _ H).
Ltac ecbspec_dec v x a := let H0 := fresh in let H0´ := fresh in remember (Classical_Prop.classic (x=a)) as H0 eqn: H0´; clear H0´; destruct H0;[ rewrite -> H0 in *; ecbspec_dec_true a | ecbspec_dec_false v H0].
Lemma nthval´_has_value : forall l len n, array_type_vallist_match Tint8 l -> length l = len -> (n < len)%nat ->exists x, nth_val´ n l = Vint32 x /\ true = rule_type_val_match Tint8 (Vint32 x).
Lemma disj_star_elim´´
: forall p q x y r: asrt, (( p\\//q\\//x\\//y) ** r) ==> (p**r) \\// (q**r) \\// (x**r) \\// (y**r).
Lemma mod_0_div_eq_eq: forall a b c, c>0 -> a mod c = b mod c -> a / c = b / c -> a =b.
Ltac solve_int_range i:= repeat ht.rewrite_un_repr; split; [try omega| ht.get_int_max;try ht.intrange i omega; try omega]; try ht.intrange i omega.
Ltac simpl_int_repr H := match type of (H) with
| $ (?x) = $ (?y) => let H´ := fresh in assert ( Int.unsigned ($ x) =Int.unsigned ($ y)) as H´ by (rewrite H; trivial);try rewrite Int.unsigned_repr in H´; repeat ht.rewrite_un_repr_in H´
end.
Ltac solve_mod_range tac := match goal with
| |- _ <= ?a mod ?x <= _ => let H:= fresh in assert (0<x) as H by omega;set (Z.mod_pos_bound a x H); tac; clear H
end.
Ltac copy H := let copy_of_H := fresh in let e:= fresh in remember H as copy_of_H eqn: e; clear e.
Ltac simpl_mod_in H := try rewrite Zminus_mod in H; try rewrite Z_mod_same_full in H; try rewrite <- Zminus_0_l_reverse in H; try rewrite <- Zmod_div_mod in H;[idtac| try omega ..| try (apply Zdivide_intro with 1; auto)].
Ltac clear_useless_int32 :=
match goal with
| a : int32 |- _ => clear dependent a
end.
Ltac clear_all_useless_int32 := repeat clear_useless_int32.
Lemma a_mult_b_ge_b : forall a b, 0<a -> 0<=b -> a*b >= b.
Lemma div_in_intrange: forall x a mx, 0<=x <=mx -> a>0 -> 0<=x/a<=mx.
Ltac solve_int_range´ :=
match goal with
| i : int32 |- _ => let xval := fresh in let xrange := fresh in destruct i as [xval xrange]; unfold Int.modulus, two_power_nat, shift_nat in xrange; simpl in xrange; simpl in *; solve_int_range´
| _ => subst; try rewrite max_unsigned_val; solve [ omega | apply div_in_intrange; omega ]
end.
Ltac rangesolver :=clear_all_useless_int32; try solve_int_range´; repeat (rewrite Int.unsigned_repr; try solve_int_range´).
Ltac ur_rewriter := rewrite Int.unsigned_repr; [idtac| try solve[rangesolver] ].
Ltac ur_rewriter_in H := rewrite Int.unsigned_repr in H; [idtac|clear H; try solve[rangesolver] ].
End ht.
Module kz.
Ltac trivial_ur_rewriterH H := repeat (rewrite Int.unsigned_repr in H; [idtac |solve [split;[omega| rewrite max_unsigned_val; omega]]]).
Ltac bfunc_invertH H := let HH := fresh in
match type of H with
| (if ?e then true else false) = false => rename H into HH; destruct e as [H|H]; [inversion HH|idtac]; clear HH
| (if ?e then true else false) = true => rename H into HH; destruct e as [H|H]; [idtac| inversion HH]; clear HH
end.
Ltac Iltu_simplerH H := unfold Int.ltu in H; bfunc_invertH H; try trivial_ur_rewriterH H.
Ltac Irepr_simplerH H := match type of (H) with
| $ (?x) = $ (?y) => let H´ := fresh in rename H into H´; assert ( Int.unsigned ($ x) =Int.unsigned ($ y)) as H by (rewrite H´; trivial);try rewrite Int.unsigned_repr in H; repeat ht.rewrite_un_repr_in H;clear H´
end.
Ltac trivial_mod_range := match goal with
| |- _ <= ?a mod ?x <= _ => let H:= fresh in assert (0<x) as H by omega;set (Z.mod_pos_bound a x H); omega; clear H
end.
Ltac Imod_simplerH H :=let H´ := fresh in unfold Int.modu in H; repeat trivial_ur_rewriterH H; try (Irepr_simplerH H;[idtac| rewrite max_unsigned_val; trivial_mod_range]).
Ltac Zmod_simplerH H k newval := match type of H with
| ?a mod ?n = ?b =>
let H´ := fresh in
rewrite <- (Z_mod_plus _ k) in H;[idtac|omega]; assert ( a + k * n = newval) as H´ by omega ; rewrite H´ in H; clear H´
end.
Lemma unsigned_ge0 : forall x, Int.unsigned x >=0.
Lemma Zplus_minus : forall z x, z+x-x=z.
Ltac ge0_solver := solve [omega| apply unsigned_ge0| apply Z_div_ge0; [omega| ge0_solver] ].
Ltac le0_solver := ht.revs; ge0_solver.
Ltac revsH H := let H´ := fresh in
match type of H with
| ?a < ?b => assert (a < b -> b > a) as H´ by omega; apply H´ in H; clear H´
| ?a > ?b => assert (a > b -> b < a) as H´ by omega; apply H´ in H; clear H´
| ?a >= ?b => assert (a>=b -> b <= a) as H´ by omega; apply H´ in H; clear H´
| ?a <= ?b => assert (a<=b -> b >= a) as H´ by omega; apply H´ in H; clear H´
end.
Ltac Zdivsup_simplerH H := match type of H with
| ?a / ?b < ?c =>
let H´´ := fresh in let H´ := fresh in let e := fresh in rewrite (Z.mul_lt_mono_pos_r b) in H; [idtac | omega]; rewrite (Z.add_lt_mono_r _ _ b ) in H; assert ( a / b * b + b >= a ) as H´´ by (apply (@ht.a_div_b_multi_b_plus_b_ge_a a b); omega); revsH H´´; remember (Z.le_lt_trans _ _ _ H´´ H) as H´ eqn: e; simpl in H´; clear e; clear H´´
end.
Ltac revs := match goal with
| |- ?a < ?b => cut (b > a); [intro; omega| idtac]
| |- ?a > ?b => cut (b < a); [intro; omega| idtac]
| |- ?a >= ?b => cut (b <= a); [intro; omega| idtac]
| |- ?a <= ?b => cut (b >= a); [intro; omega| idtac]
| |- (?a < ?b)%nat => cut (b > a)%nat; [intro; omega| idtac]
| |- (?a > ?b)%nat => cut (b < a)%nat; [intro; omega| idtac]
| |- (?a >= ?b)%nat => cut (b <= a)%nat; [intro; omega| idtac]
| |- (?a <= ?b)%nat => cut (b >= a)%nat; [intro; omega| idtac]
end.
End kz.
Lemma int_not_leq : forall i j, i>=0 -> j >=0 -> ~i + j < i.
Lemma Z_prop : forall x y a, 0<a -> (x + a * y - x) / a = y.
Lemma prio_destruct1 :
forall x, 0 <= x < 17 <->
x = 0 \/ x = 1 \/ x = 2 \/ x = 3 \/ x = 4 \/ x = 5 \/ x = 6 \/ x = 7 \/
x = 8 \/ x = 9 \/ x = 10 \/ x = 11 \/ x = 12 \/ x = 13 \/ x = 14 \/ x = 15 \/
x = 16.
Lemma int_aux :Int.unsigned ($ (0 + (4 + 0) - (0 + (4 + 0)))) / Int.unsigned ($ 4) =0.
Lemma prio_destruct2 :
forall x, 17 <= x < 32 <->
x = 17 \/ x = 18 \/ x = 19\/ x = 20 \/ x = 21 \/ x = 22 \/ x = 23 \/
x = 24 \/ x = 25 \/ x = 26 \/ x = 27 \/ x = 28 \/ x = 29 \/ x = 30 \/ x = 31.
Lemma prio_destruct3 :
forall x, 32 <= x < 48 <->
x = 32 \/ x = 33 \/ x = 34 \/ x = 35 \/ x = 36 \/ x = 37 \/ x = 38 \/ x = 39 \/
x = 40 \/ x = 41 \/ x = 42 \/ x = 43 \/ x = 44 \/ x = 45 \/ x = 46 \/ x = 47.
Lemma prio_destruct4 :
forall x, 48 <= x < 64 <->
x = 48 \/ x = 49 \/ x = 50 \/ x = 51 \/ x = 52 \/ x = 53 \/ x = 54 \/ x = 55 \/
x = 56 \/ x = 57 \/ x = 58 \/ x = 59 \/ x = 60 \/ x = 61 \/ x = 62 \/ x = 63.
Lemma prio_range_com :
forall x, 0 <= x < 17 \/ 17 <= x < 32 \/ 32 <= x < 48 \/ 48 <= x < 64 <->
0 <= x < 64.
Lemma prio_destruct :
forall x, 0 <= x < 64 <->
x = 0 \/ x = 1 \/ x = 2 \/ x = 3 \/ x = 4 \/ x = 5 \/ x = 6 \/ x = 7 \/
x = 8 \/ x = 9 \/ x = 10 \/ x = 11 \/ x = 12 \/ x = 13 \/ x = 14 \/ x = 15 \/
x = 16 \/ x = 17 \/ x = 18 \/ x = 19 \/ x = 20 \/ x = 21 \/ x = 22 \/ x = 23 \/
x = 24 \/ x = 25 \/ x = 26 \/ x = 27 \/ x = 28 \/ x = 29 \/ x = 30 \/ x = 31 \/
x = 32 \/ x = 33 \/ x = 34 \/ x = 35 \/ x = 36 \/ x = 37 \/ x = 38 \/ x = 39 \/
x = 40 \/ x = 41 \/ x = 42 \/ x = 43 \/ x = 44 \/ x = 45 \/ x = 46 \/ x = 47 \/
x = 48 \/ x = 49 \/ x = 50 \/ x = 51 \/ x = 52 \/ x = 53 \/ x = 54 \/ x = 55 \/
x = 56 \/ x = 57 \/ x = 58 \/ x = 59 \/ x = 60 \/ x = 61 \/ x = 62 \/ x = 63.
Lemma prio_prop :
forall prio,
0 <= prio ->
prio < 64 ->
Int.unsigned (Int.shru ($ prio) ($ 3)) < 8.
Lemma Z_le_nat :
forall x, (0<= x < 8)%Z-> ( ∘x < 8) %nat.
Lemma val_inj_1 :
val_inj
(if Int.ltu Int.zero (Int.notbool Int.one) &&Int.ltu Int.zero (Int.notbool Int.one)
then Some (Vint32 Int.one)
else Some (Vint32 Int.zero)) = Vint32 Int.zero.
Lemma isptr_vundef2:
forall x,
isptr x -> val_inj
(bool_and (val_inj (notint (val_inj (val_eq x Vnull))))
(Vint32 (Int.notbool Int.one))) <> Vundef.
Lemma val_inj_12 :
forall x , val_inj
(bool_and
(val_inj
(notint (val_inj (val_eq (Vptr (x, Int.zero)) Vnull))))
(Vint32 (Int.notbool Int.one))) = Vint32 Int.zero.
Lemma val_inj_12´ :
forall x , isptr x -> val_inj
(bool_and
(val_inj
(notint (val_inj (val_eq x Vnull))))
(Vint32 (Int.notbool Int.one))) = Vint32 Int.zero.
Lemma isptr_vundef_not :
forall x, isptr x -> val_inj
match val_inj (notint (val_inj (val_eq x Vnull))) with
| Vundef => None
| Vnull => None
| Vint32 n2 =>
if Int.ltu Int.zero (Int.notbool Int.one) && Int.ltu Int.zero n2
then Some (Vint32 Int.one)
else Some (Vint32 Int.zero)
| Vptr _ => None
end <> Vundef.
Lemma val_inj_122 :
forall x , isptr x ->val_inj
match val_inj (notint (val_inj (val_eq x Vnull))) with
| Vundef => None
| Vnull => None
| Vint32 n2 =>
if Int.ltu Int.zero (Int.notbool Int.one) &&
Int.ltu Int.zero n2
then Some (Vint32 Int.one)
else Some (Vint32 Int.zero)
| Vptr _ => None
end = Vint32 Int.zero.
Lemma val_eq_vundef:
forall i0,
val_inj
(if Int.eq i0 ($ OS_EVENT_TYPE_Q)
then Some (Vint32 Int.one)
else Some (Vint32 Int.zero)) <> Vundef.
Lemma val_eq_vundef´:
forall i0,
val_inj
(notint
(val_inj
(if Int.eq i0 ($ OS_EVENT_TYPE_Q)
then Some (Vint32 Int.one)
else Some (Vint32 Int.zero)))) <> Vundef.
Lemma val_inj_eq_q:
forall i0,
val_inj
(notint
(val_inj
(if Int.eq i0 ($ OS_EVENT_TYPE_Q)
then Some (Vint32 Int.one)
else Some (Vint32 Int.zero)))) = Vint32 Int.zero \/
val_inj
(notint
(val_inj
(if Int.eq i0 ($ OS_EVENT_TYPE_Q)
then Some (Vint32 Int.one)
else Some (Vint32 Int.zero)))) = Vnull ->
i0 = ($ OS_EVENT_TYPE_Q).
Lemma int_land_zero:
forall x, Int.zero&(Int.one<<(x &$ 7)) <> Int.one<<(x &$ 7).
Lemma nat8_des:
forall x2 Heq ,
(Heq < 8) %nat ->
match Heq with
| 0%nat => Some (Vint32 Int.zero)
| 1%nat => Some (Vint32 Int.zero)
| 2%nat => Some (Vint32 Int.zero)
| 3%nat => Some (Vint32 Int.zero)
| 4%nat => Some (Vint32 Int.zero)
| 5%nat => Some (Vint32 Int.zero)
| 6%nat => Some (Vint32 Int.zero)
| 7%nat => Some (Vint32 Int.zero)
| S (S (S (S (S (S (S (S _))))))) => None
end = Some (Vint32 x2) -> x2 = Int.zero.
Lemma ecbmod_get_sig_set:
forall v x y,
EcbMod.get v x = None ->
EcbMod.joinsig x y v (EcbMod.set v x y).
Lemma ecbmod_join_get :
forall x x0 x1 v´37 eid,
x <> eid -> EcbMod.joinsig x x0 x1 v´37 ->
EcbMod.get x1 eid = None -> EcbMod.get v´37 eid = None.
Lemma leftmoven:
forall n,
(0 <= n < 8)%nat ->
$ 1<<$ Z.of_nat n <> $ 0.
Lemma abs_disj_get_merge:
forall O´ O x y,
OSAbstMod.disj O´ O ->
OSAbstMod.get O x = Some y ->
OSAbstMod.get (OSAbstMod.merge O´ O) x = Some y.
Lemma disj_star_elim: forall p q r, ( p \\// q )** r ==> (p ** r) \\// (q ** r).
Lemma math_prop_l1: val_inj
(notint
(val_inj
(if Int.eq ($ OS_EVENT_TYPE_Q) ($ OS_EVENT_TYPE_Q)
then Some (Vint32 Int.one)
else Some (Vint32 Int.zero)))) = Vint32 Int.zero.
Lemma math_prop_l2 : val_inj
(if Int.eq ($ 1) ($ 0)
then Some (Vint32 Int.one)
else Some (Vint32 Int.zero)) = Vint32 Int.zero.
Lemma math_prop_l3 : val_inj
(notint
(val_inj
(if Int.eq ($1) ($ 0)
then Some (Vint32 Int.one)
else Some (Vint32 Int.zero)))) <> Vint32 Int.zero.
Ltac solve_disj:=
match goal with
| H : _ \/ _ |- _ =>
let Hx := fresh in
let Hy := fresh in
(destruct H as [Hx | Hy]; [subst; eexists; simpl; splits; eauto| idtac])
| _ => try (subst; eexists; simpl; splits; eauto)
end.
Lemma int8_neq0_ex:
forall i ,
Int.unsigned i <= 255 ->
Int.eq i ($ 0) = false ->
exists n, (0 <= n < 8)%nat /\ i &($ 1<<$ Z.of_nat n) = $ 1<<$ Z.of_nat n.
Lemma length8_ex:
forall v´40 :vallist,
length v´40 = ∘OS_EVENT_TBL_SIZE ->
exists v1 v2 v3 v4 v5 v6 v7 v8,
v´40 = v1::v2::v3::v4::v5::v6::v7::v8::nil.
Lemma int_true_le255:
forall x,
(if Int.unsigned x <=? Byte.max_unsigned then true else false) = true ->
Int.unsigned x <= 255.
Lemma n07_arr_len_ex:
forall n v´40,
(0 <= n < 8)%nat ->
array_type_vallist_match Int8u v´40 ->
length v´40 = ∘OS_EVENT_TBL_SIZE ->
exists v, nth_val n v´40 = Some (Vint32 v) /\ Int.unsigned v <= 255.
Lemma nat8_ex_shift3:
forall n,
(0 <= n < 8) %nat ->
exists y, $ Z.of_nat n = Int.shru ($ y) ( $ 3) /\ 0 <= y < 64.
Lemma math_des88:
forall n xx,
(0 <= n < 8)%nat ->
(xx = $ 0 \/
xx = $ 1 \/
xx = $ 2 \/ xx = $ 3 \/ xx = $ 4 \/ xx = $ 5 \/ xx = $ 6 \/ xx = $ 7) ->
exists y, 0 <= y < 64 /\ xx = $ y & $ 7 /\ ($ Z.of_nat n = Int.shru ($ y) ( $ 3)).
Lemma ltu_ex_and :
forall vv,
Int.ltu ($ 0) vv = true->
Int.unsigned vv <= 255 ->
exists x,
vv&(Int.one<< x) = Int.one<< x /\
(x = $0 \/ x = $1 \/ x = $2 \/ x = $3 \/
x = $4 \/ x = $5 \/ x = $6 \/ x = $7).
Lemma eight_destruct: forall x, 0<=x<8 <-> x=0 \/ x=1 \/ x=2\/x=3\/x=4\/x=5\/x=6\/x=7.
Qed.
Lemma prio_inq:
forall vv n v´40,
(0 <= n < 8)%nat ->
Int.ltu ($ 0) vv = true ->
Int.unsigned vv <= 255 ->
nth_val n v´40 = Some (Vint32 vv) ->
exists prio,
PrioWaitInQ prio v´40.
Lemma inlist_ex :
forall x4 (x:tidspec.A),
In x x4 -> exists y z, x4 = y :: z.
Lemma l4 : forall i, val_inj
(notint
(val_inj
(if Int.eq i ($ 0)
then Some (Vint32 Int.one)
else Some (Vint32 Int.zero)))) <>
Vint32 Int.zero -> Int.eq i ($ 0) = false.
Lemma list_prop1 : forall (t: Type) (a:t) (l1 l2: list t), l1 ++ ((a::nil) ++ l2) = l1 ++ (a::l2).
Lemma l5 : forall i , val_inj
(notint
(val_inj
(if Int.eq i ($ 0)
then Some (Vint32 Int.one)
else Some (Vint32 Int.zero)))) = Vint32 Int.zero \/
val_inj
(notint
(val_inj
(if Int.eq i ($ 0)
then Some (Vint32 Int.one)
else Some (Vint32 Int.zero)))) = Vnull -> i = $ 0.
Lemma ecblistp_length_eq_1 : forall x y l1 l2 t1 t2,
ECBList_P x y l1 l2 t1 t2 -> length l1 = length l2.
Lemma ecblistp_length_eq : forall x l1 z l2 l1´ z´ l2´ t1 t2,
ECBList_P x Vnull (l1 ++ (z::nil) ++ l2) (l1´ ++ (z´::nil) ++ l2´) t1 t2-> length l1 = length l1´ -> length l2 = length l2´.
Lemma ECBList_last_val :
forall x y v1 v2 v3 v4,
v1 <> nil ->
ECBList_P x y v1 v2 v3 v4 ->
exists a b, last v1 (nil,nil) = (a,b)
/\ nth_val 5 a = Some y.
Lemma get_eidls_inlist: forall x ls,
In x (get_eidls x ls).
Inductive listsub (T : Type) : list T -> list T -> Prop :=
| listsub1:forall x, listsub nil x
| listsubrec: forall x y lsx lsy, x = y ->
listsub lsx lsy ->
listsub (x :: lsx) (y :: lsy).
Lemma list_sub_prop1 :
forall v1 (z:EventCtr) v1´, listsub (v1++(z::nil)) (v1 ++(z::v1´)).
Lemma list_sub_prop2 :
forall x y, listsub x y -> listsub (get_eid_ecbls x) (get_eid_ecbls y).
Lemma removelast_prop:
forall (t: Type) (a : t) x , x <> nil -> removelast (a::x) = a :: removelast x.
Lemma list_sub_prop3 :
forall (x : val) y z , listsub y z -> In x y -> In x z.
Lemma list_sub_prop4 :
forall (x :vallist) y, listsub x y -> listsub (removelast x) (removelast y).
Lemma nil_get_eid_nil:
forall x, x <> nil -> get_eid_ecbls x <> nil.
Lemma in_get_eidls :
forall v1 y x z vl´,
In y (get_eidls x (v1 ++ (z :: nil)))
->In y (get_eidls x (v1 ++ (z :: vl´))).
Lemma get_remove_exchange:
forall x, removelast (get_eid_ecbls x) = get_eid_ecbls (removelast x).
Ltac usimpl H := unfolds in H; simpl in H; inverts H.
Lemma ecbmod_joinsig_get :
forall x y mqls mqls´,
EcbMod.joinsig x y mqls mqls´ ->
EcbMod.get mqls´ x = Some y.
Lemma qwaitset_notnil_ex:
forall qwaitset : waitset ,
qwaitset <> nil ->
exists tid, In tid qwaitset.
Lemma prioinq_exists:
forall prio v´58,
PrioWaitInQ prio v´58 ->
exists n,
(0 <= n < 8)%nat /\ nth_val n v´58 <> Some (V$0).
Lemma int_usign_eq :
forall m,
0 <= m -> m <= Int.max_unsigned ->
(Int.unsigned ($ m)) = m.
Lemma ecbmod_joinsig_sig:
forall x y mqls mqls´,
EcbMod.joinsig x y mqls mqls´ ->
EcbMod.join mqls (EcbMod.sig x y) mqls´.
Lemma ecbmod_get_join_get:
forall eid y m x z t,
eid <> y ->
EcbMod.get m eid = Some t ->
EcbMod.join x (EcbMod.sig y z) m ->
EcbMod.get x eid = Some t.
Lemma ecbjoin_sig_join : forall x x1 v´35 x0 v´61 v3 i5,
EcbMod.join x x1 v´35 ->
EcbMod.join x0
(EcbMod.sig (v´61, Int.zero) (absmsgq v3 i5, nil))
x1 -> exists y, EcbMod.join x0 x y /\ EcbMod.join y
(EcbMod.sig (v´61, Int.zero) (absmsgq v3 i5, nil)) v´35.
Lemma length_zero_nil : forall (t : Type) (x : list t), length x = 0%nat -> x = nil.
Lemma nil_simp : forall (t : Type) (x : list t), nil ++ x = x.
Lemma ge_0_minus_1_in_range:
forall i2,
Int.unsigned i2 <= 65535 ->
Int.ltu ($ 0) i2 = true ->
Int.unsigned (i2 -ᵢ $ 1) <=? Int16.max_unsigned = true.
Lemma qacc_dl_vl_match:
forall vl, true = dl_vl_match ((dcons pevent (Tptr OS_EVENT) ) dnil) (rev vl) -> (exists v,vl = (Vptr v)::nil\/ vl =Vnull::nil) .
Lemma notint_neq_zero_eq:
forall x y,
val_inj
(notint
(val_inj
(if Int.eq x y
then Some (Vint32 Int.one)
else Some (Vint32 Int.zero)))) <>
Vint32 Int.zero -> Int.eq x y = false.
Lemma ecb_get_set_join_join:
forall ml a b ml1 ml2 ml1´ b´,
EcbMod.get ml a = Some b ->
EcbMod.joinsig a
b ml1´ ml1 ->
EcbMod.join ml2 ml1 ml ->
exists ml1n, EcbMod.joinsig a b´ ml1´ ml1n /\ EcbMod.join ml2 ml1n (EcbMod.set ml a b´).
Fixpoint all_elem_p {X:Type} p (l: @list X) :=
match l with
| nil => True
| h :: t => p h = true /\ all_elem_p p t
end.
Lemma array_type_vallist_match_is_all_elem_p: forall t l, array_type_vallist_match t l <-> all_elem_p (rule_type_val_match t) l.
Lemma all_elem_hold_for_upd: forall n x l p, all_elem_p p l -> p x = true -> all_elem_p p (update_nth_val n l x).
Lemma not_and_p: forall v´41 v´12, Int.unsigned v´12 <= 255 ->Int.unsigned v´41 <= 128 -> Int.unsigned (v´12&Int.not v´41) <= 255.
Lemma not_and_p´: forall v´41 v´12, Int.unsigned v´12 <= 255 ->Int.unsigned v´41 <= 255 -> Int.unsigned (v´12&Int.not v´41) <= 255.
Lemma array_type_vallist_match_int8u_update_hold:
forall v´38 v´69 v´40 v´13,
length v´13 = ∘OS_EVENT_TBL_SIZE ->
Int.unsigned v´38 <= 7 ->
Int.unsigned v´69 <= 255 ->
Int.unsigned v´40 <= 128 ->
array_type_vallist_match Int8u v´13 ->
array_type_vallist_match Int8u
(update_nth_val (Z.to_nat (Int.unsigned v´38)) v´13
(Vint32 (v´69&Int.not v´40))).
Lemma array_type_vallist_match_int8u_update_hold_255:
forall v´38 v´69 v´40 v´13,
length v´13 = ∘OS_EVENT_TBL_SIZE ->
Int.unsigned v´38 <= 7 ->
Int.unsigned v´69 <= 255 ->
Int.unsigned v´40 <= 255 ->
array_type_vallist_match Int8u v´13 ->
array_type_vallist_match Int8u
(update_nth_val (Z.to_nat (Int.unsigned v´38)) v´13
(Vint32 (v´69&Int.not v´40))).
Lemma int_unsigned_or_prop:
forall v´57 v´41,
Int.unsigned v´57 <= 255 ->
Int.unsigned v´41 <= 128 ->
Int.unsigned (Int.or v´57 v´41) <= 255.
Lemma array_type_vallist_match_int8u_update_hold´:
forall v´37 ( v´38 v´40 : int32) (v´13 : list val),
length v´37 = nat_of_Z OS_RDY_TBL_SIZE ->
array_type_vallist_match Tint8 v´37 ->
length v´13 = nat_of_Z OS_EVENT_TBL_SIZE ->
Int.unsigned v´38 <= 7 ->
Int.unsigned v´40 <= 128 ->
array_type_vallist_match Tint8 v´13 ->
array_type_vallist_match Tint8
(update_nth_val (Z.to_nat (Int.unsigned v´38)) v´13
(val_inj
(or (nth_val´ (Z.to_nat (Int.unsigned v´38)) v´37) (Vint32 v´40)))).
Lemma length_n_change:
forall v´38 v´37 v´40,
length v´37 = nat_of_Z OS_RDY_TBL_SIZE ->
Int.unsigned v´38 <= 7 ->
length
(update_nth_val (Z.to_nat (Int.unsigned v´38)) v´37
(val_inj
(or (nth_val´ (Z.to_nat (Int.unsigned v´38)) v´37) (Vint32 v´40)))) =
nat_of_Z OS_RDY_TBL_SIZE.
Lemma disj_star_elim´
: forall p q x y r z: asrt, ((p \\// q \\// x \\// y)** z) ** r ==> (p ** z ** r) \\// (q ** z ** r) \\// (x** z** r) \\// (y** z ** r).
Lemma ltu_eq_false: forall i1 i2, Int.ltu i2 i1 = true -> Int.eq i1 i2 = false.
Lemma val_inj_i1_i2_lt:
forall i1 i2,
val_inj
(bool_or
(val_inj
(if Int.ltu i2 i1
then Some (Vint32 Int.one)
else Some (Vint32 Int.zero)))
(val_inj
(if Int.eq i1 i2
then Some (Vint32 Int.one)
else Some (Vint32 Int.zero)))) = Vint32 Int.zero \/
val_inj
(bool_or
(val_inj
(if Int.ltu i2 i1
then Some (Vint32 Int.one)
else Some (Vint32 Int.zero)))
(val_inj
(if Int.eq i1 i2
then Some (Vint32 Int.one)
else Some (Vint32 Int.zero)))) = Vnull -> Int.ltu i1 i2 = true.
Lemma val_inj_eq_p:
forall x6 v´49 x,
isptr x6 ->
val_inj
match x6 with
| Vundef => None
| Vnull => Some (Vint32 Int.zero)
| Vint32 _ => None
| Vptr (b2, ofs2) =>
if peq v´49 b2
then
if Int.eq (x+ᵢInt.mul ($ 1) ($ 4)) ofs2
then Some (Vint32 Int.one)
else Some (Vint32 Int.zero)
else Some (Vint32 Int.zero)
end <> Vint32 Int.zero -> x6 = Vptr (v´49, (x+ᵢInt.mul ($ 1) ($ 4)) ).
Lemma val_inj_eq_elim:
forall x6 v´49 x,
val_inj
match x6 with
| Vundef => None
| Vnull => Some (Vint32 Int.zero)
| Vint32 _ => None
| Vptr (b2, ofs2) =>
if peq v´49 b2
then
if Int.eq (x+ᵢInt.mul ($ 1) ($ 4)) ofs2
then Some (Vint32 Int.one)
else Some (Vint32 Int.zero)
else Some (Vint32 Int.zero)
end = Vint32 Int.zero \/
val_inj
match x6 with
| Vundef => None
| Vnull => Some (Vint32 Int.zero)
| Vint32 _ => None
| Vptr (b2, ofs2) =>
if peq v´49 b2
then
if Int.eq (x+ᵢInt.mul ($ 1) ($ 4)) ofs2
then Some (Vint32 Int.one)
else Some (Vint32 Int.zero)
else Some (Vint32 Int.zero)
end = Vnull -> x6 <> Vptr (v´49, (x+ᵢInt.mul ($ 1) ($ 4))).
Lemma isptr_val_inj_false: forall x0, isptr x0 -> val_inj (val_eq x0 Vnull) = Vnull -> False.
Definition myAnd := Logic.and.
Lemma array_int8u_nth_lt_len :
forall vl m,
array_type_vallist_match Int8u vl ->
(m < length vl)%nat ->
exists i, nth_val´ m vl = Vint32 i /\ Int.unsigned i <= 255.
Lemma int_lemma1:
forall i1 i2,
Int.unsigned i1 <= 255 ->
Int.unsigned i2 <= 255 ->
Int.unsigned (i1 & Int.not i2) <= 255.
Lemma array_type_vallist_match_hold :
forall vl n t v,
array_type_vallist_match t vl ->
(n < length vl)%nat ->
rule_type_val_match t v = true ->
array_type_vallist_match t (update_nth_val n vl v).
Lemma tcbmod_neq_set_get:
forall x y b tcbls,
x <> y ->
TcbMod.get (TcbMod.set tcbls y b) x = TcbMod.get tcbls x.
Lemma ltu_zero_eq_zero:
forall i, Int.unsigned i <= 65535 -> false = Int.ltu ($ 0) i -> i = Int.zero.
Lemma bool_and_true_1 : forall {v1 v2 x},
istrue x = Some true -> bool_and v1 v2 = Some x ->
exists n1, v1 = Vint32 n1 /\ Int.ltu Int.zero n1 = true.
Lemma ltu_zero_notbool_true : forall {i2},
Int.ltu Int.zero (Int.notbool i2) = true -> Int.eq i2 Int.zero = true.
Lemma val_eq_zero_neq : forall {v1 v2 i},
val_eq v1 v2 = Some (Vint32 i) -> Int.eq i Int.zero = true -> v1 <> v2.
Lemma bool_and_true_gt: forall {v1 v2 x},
bool_and v1 v2 = Some x -> istrue x = Some true ->
exists n1 n2, v1 = Vint32 n1 /\ v2 = Vint32 n2 /\ Int.ltu Int.zero n1 = true /\ Int.ltu Int.zero n2 = true.
Lemma list_cons_assoc : forall {A} l1 l2 (n:A),
l1 ++ n :: l2 = (l1 ++ n::nil) ++ l2.
Lemma upd_vallist_eq_length: forall vl n v´,
length vl = length (update_nth_val n vl v´).
Lemma vallist_destru:
forall vl:vallist , length vl = ∘OS_EVENT_TBL_SIZE ->
exists v1 v2 v3 v4,
exists v5 v6 v7 v8,
vl = v1 ::v2 ::v3 ::v4 ::v5 ::v6::v7::v8 :: nil.
Lemma eq_1 :Int.zero+ᵢ($ 4+ᵢ($ 2+ᵢ($ 1+ᵢ$ 1))) = $ 8.
Lemma eq_2 : $ 8+ᵢ ($ 1) = $ 9.
Lemma eq_3 : $ 9+ᵢ ($ 1) = $10.
Lemma eq_4 : $ 10+ᵢ($ 1) = $11.
Lemma eq_5 : $11+ᵢ ($ 1) = $ 12.
Lemma eq_6 : $ 12+ᵢ ($ 1) = $ 13.
Lemma eq_7 : $ 13+ᵢ($ 1) = $ 14.
Lemma eq_8 : $ 14+ᵢ ($ 1) = $ 15.
Lemma eq_9 : $0+ᵢ$ 1 = $1.
Lemma eq_10 :$1+ᵢ$ 1 = $2.
Lemma eq_11 :$2+ᵢ$2 = $4.
Lemma eq_12 :$4+ᵢ$4 = $8.
Lemma eq_13 :$8+ᵢ$8 = $16.
Lemma xx:forall P Q R, (P \\// Q) ** R ==> (P ** R) \\// (Q ** R).
Lemma is_length_neq_zero_elim:
forall v´1, val_inj (val_eq (is_length (0%nat :: v´1)) (V$1)) <> Vint32 Int.zero -> v´1=nil.
Lemma true_if_else_true: forall x, x =true -> (if x then true else false) = true.
Ltac rtmatch_solve:=
apply true_if_else_true;
apply Zle_is_le_bool;
try rewrite byte_max_unsigned_val; try rewrite max_unsigned_val;
try omega.
Lemma z_le_7_imp_n: forall x, Int.unsigned x <= 7 -> (Z.to_nat (Int.unsigned x) < 8)%nat.
Lemma z_le_255_imp_n: forall x, Int.unsigned x <= 255 -> (Z.to_nat (Int.unsigned x) < 256)%nat.
Lemma OSUnMapVallist_type_vallist_match: array_type_vallist_match Tint8 OSUnMapVallist.
Lemma pos_to_nat_range_0_255:
forall z, 0<=z -> z<=255 -> (0<=Z.to_nat z<=255)%nat.
Lemma sn_le_n_le_minus1:
forall (n x:nat), (S n <= x -> n <= x-1)%nat.
Lemma osunmapvallist_prop:
forall i, (Int.unsigned i <= 255) -> exists x, nth_val´ (Z.to_nat (Int.unsigned i)) OSUnMapVallist = Vint32 x /\ Int.unsigned x <=?7 = true.
Lemma int_iwordsize_gt_3:
Int.ltu ($ 3) Int.iwordsize = true.
Lemma shl3_add_range:
forall x x0,
(Int.unsigned x <=? 7) = true ->
(Int.unsigned x0 <=? 7) = true ->
Int.unsigned ((x<<$ 3) +ᵢ x0) <=? 63 =true.
Ltac auto_shiftl := unfold Z.shiftl; unfold Pos.iter; int auto.
Lemma int_unsigned_le_z2nat_lt:
forall x z,Int.unsigned x <= z ->
(Z.to_nat (Int.unsigned x) < Z.to_nat (z+1))%nat.
nth_val'的定义非常的奇怪，而且显的冗余。
其实nth_val' = get_option_value nth_val.
但nth_val'的fixpoint是递归在n上的，为了和nth_val统一，
我又定义了my_nth_val', 然后证明了my_nth_val' = nth_val',
接着证my_nth_val' = get_option_value nth_val.
最后有, nth_val' = get_option_value nth_val.
Fixpoint my_nth_val´ (n:nat)(vl:list val){struct vl} : val :=
match vl with
| nil => Vundef
| v :: vl´ => match n with
| 0%nat => v
| S n´ => my_nth_val´ n´ vl´
end
end.
Lemma my_nth_val´_eql_yours:
forall n vl,
nth_val´ n vl = my_nth_val´ n vl.
Definition get_option_value (v : option val) : val :=
match v with
| None => Vundef
| Some v´ => v´
end.
Lemma my_nth_val´_and_nth_val:
forall n vl,
my_nth_val´ n vl = get_option_value (nth_val n vl).
Lemma nth_val´_and_nth_val:
forall n vl,
nth_val´ n vl = get_option_value (nth_val n vl).
Lemma prio_in_rtbl_has_tid:
forall rtbl ptbl p vhold,
0 <= Int.unsigned p < 64 ->
RL_RTbl_PrioTbl_P rtbl ptbl vhold->
prio_in_tbl p rtbl ->
exists x, nth_val´ (Z.to_nat (Int.unsigned p)) ptbl = Vptr x.
Lemma update_nth_val_length_eq:
forall n vl v, length vl = length (update_nth_val n vl v).
Lemma int_unsigned_or_prop´
: forall v´57 v´41 : int32,
Int.unsigned v´57 <= 255 ->
Int.unsigned v´41 <= 255 -> Int.unsigned (Int.or v´57 v´41) <= 255.
Lemma nth_val´_imp_nth_val_int:
forall z vl v,
nth_val´ (Z.to_nat z) vl = Vint32 v -> nth_val ∘z vl = Some (Vint32 v).
Lemma unsigned_to_z_eq: forall i, nat_of_Z (Int.unsigned i) =Z.to_nat (Int.unsigned i) .
Ltac clean_ptr H H´ v:=
let x:= fresh in
destruct H;
[assert (exists x,v=Vptr x) by pauto;mytac;clear H H´|
false;eapply isptr_val_inj_false;eauto].
Lemma Int_eq_false_Vptr_neq :
forall i1 i2 b,
Int.eq i1 i2 = false ->
Vptr (b, i1) <> Vptr (b, i2).
Lemma qentries_eq_zero :
forall (i:int32),
(val_inj
(if Int.ltu ($ 0) i
then Some (Vint32 Int.one)
else Some (Vint32 Int.zero)) = Vint32 Int.zero \/
val_inj
(if Int.ltu ($ 0) i
then Some (Vint32 Int.one)
else Some (Vint32 Int.zero)) = Vnull) ->
i = Int.zero.
Lemma update_nth_aux:
forall vl x a n,
update_nth_ectrls (x :: vl) (S n) a =
x :: (update_nth_ectrls vl n a).
Lemma upd_last_prop´:
forall v´40 v´51 v v0 x8,
v´40 <> nil ->
v´51 = upd_last_ectrls ((v, v0) :: v´40) x8 ->
exists vl, v´51 = ((v,v0) :: vl) /\
vl = upd_last_ectrls v´40 x8.
Lemma math_prop_and:
forall x0 n,
0 <= Int.unsigned x0 < 64 ->
(0 <= n < 8)%nat ->
n <> Z.to_nat (Int.unsigned (Int.shru x0 ($ 3))) ->
(Int.not ($ 1<<(Int.shru x0 ($ 3)))&($ 1<<$ Z.of_nat n)) = ($ 1<<$ Z.of_nat n).
Lemma math_prop_eq0:
forall x0,
0 <= Int.unsigned x0 < 64 ->
Int.not ($ 1<<(Int.shru x0 ($ 3)))&
($ 1<<$ Z.of_nat (Z.to_nat (Int.unsigned (Int.shru x0 ($ 3)
)))) = $ 0.
Lemma math_and_zero:
forall n x ,
0 <= Int.unsigned x < 64 ->
(0 <= n < 8)%nat ->
n <> Z.to_nat (Int.unsigned (Int.shru x ($ 3))) ->
($ 1<<$ Z.of_nat n)&($ 1<<(Int.shru x ($ 3))) = $ 0.
Lemma math_prop_neq_zero:
forall x,
0 <= Int.unsigned x < 64 ->
($ 1<<$ Z.of_nat (Z.to_nat (Int.unsigned (Int.shru x ($ 3)))))&($ 1<<(Int.shru x ($ 3))) <>
$ 0.
Lemma int_usigned_tcb_range:
forall x,
0 <= Int.unsigned x < 64 ->
0 <=Int.unsigned (x&$ 7) < 8 /\
0 <= Int.unsigned (Int.shru x ($ 3)) < 8.
Lemma prio_int_disj:
forall x y,
0 <= Int.unsigned x < 256 ->
0 <= Int.unsigned y < 8 ->
(x &($ 1<<y) = $ 1<<y) \/ (x&($ 1<<y) = $ 0).
Lemma nat_int64_range_eq:
forall x,
(0 <= Int.unsigned x < 64) ->
(0<=∘ (Int.unsigned x) < 64)% nat.
Lemma prio_neq_grpeq_prop :
forall prio0 prio,
0 <= Int.unsigned prio0 < 64 ->
0 <= Int.unsigned prio < 64 ->
prio0 <> prio ->
∘(Int.unsigned (Int.shru prio0 ($ 3))) = ∘(Int.unsigned (Int.shru prio ($ 3)))->
(Int.not ($ 1<<(prio&$ 7))&($ 1<<(prio0&$ 7))) =
$ 1<<(prio0&$ 7).
Lemma math_lshift_neq_zero:
forall x0,
0 <= Int.unsigned x0 < 64 ->
Int.zero <> $ 1<<$ Z.of_nat (Z.to_nat (Int.unsigned (Int.shru x0 ($ 3)))).
Ltac simpl_hyp :=
repeat progress
match goal with
| H : ?f _ = Some _ |- _ => unfold f in H; simpl in H; inverts H
end.
Ltac funfold H:=
match type of H with
| ?f _ =>
unfold f in H ;mytac; simpl_hyp
| ?f _ _ =>
unfold f in H ;mytac; simpl_hyp
| ?f _ _ _ =>
unfold f in H ;mytac; simpl_hyp
| ?f _ _ _ _ =>
unfold f in H ;mytac; simpl_hyp
| ?f _ _ _ _ _ =>
unfold f in H ;mytac; simpl_hyp
| _ => idtac
end.
Lemma nth_upd_neq :
forall vl n m x y,
n <> m ->
nth_val n (update_nth_val m vl x) = Some y ->
nth_val n vl = Some y.
Lemma nth_upd_eq :
forall vl n x y,
nth_val n (update_nth_val n vl x) = Some y ->
x = y.
Lemma int_unsigned_inj:
forall x,
0 <= x <= Int.max_unsigned -> $ x = $ 0 -> x = 0.
Lemma int_or_zero_split:
forall x y,
Int.or x y = $ 0 -> x = $0 /\ y = $ 0.
Lemma R_Prio_NoChange_Prio_hold:
forall tcb tid st msg prio st´ msg´,
R_Prio_No_Dup tcb ->
TcbMod.get tcb tid = Some (prio, st, msg) ->
R_Prio_No_Dup (TcbMod.set tcb tid (prio, st´, msg´)).
Lemma math_prop_neq_zero2:
forall x,
0 <= Int.unsigned x < 64 ->
$ 1<<(x&$ 7) <>
$ 0.
Lemma int_eq_false_ltu : forall x,
Int.eq x ($ 0) = false ->
Int.ltu ($ 0) x = true.
Lemma int_ltu_true:
forall x x0,
0 <= Int.unsigned x < 64 ->
Int.ltu ($ 0) (Int.or x0 ($ 1<<(x&$ 7))) = true.
Lemma math_prop_eq:
forall x ,
0 <= Int.unsigned x < 64 ->
($ 1<<$ Z.of_nat (Z.to_nat (Int.unsigned (Int.shru x ($ 3))))) =
$ 1<<(Int.shru x ($ 3)).
Lemma int8_range_nat:
forall z,
0 <= Int.unsigned z < 8 ->
(0<=Z.to_nat (Int.unsigned z) <8)%nat.
Lemma prio_rtbl_dec:
forall x rtbl,
0 <= Int.unsigned x < 64 ->
array_type_vallist_match Int8u rtbl ->
length rtbl = ∘OS_RDY_TBL_SIZE ->
prio_in_tbl x rtbl \/ prio_not_in_tbl x rtbl.
Lemma nat_of_Z_eq:
forall x y,
nat_of_Z (Int.unsigned x) = nat_of_Z (Int.unsigned y) ->
x = y.
Lemma nth_upd_neqrev:
forall (vl : vallist) (n m : nat) (x y : val),
n <> m ->
nth_val n vl = Some y ->
nth_val n (update_nth_val m vl x) = Some y.
Definition prio_neq_cur tcbls curtid curprio :=
forall tid prio st m,
tid <> curtid ->
TcbMod.get tcbls tid = Some (prio, st, m) ->
prio <> curprio.
Lemma prio_neq_in_tbl:
forall prio0 prio rtbl grp,
0 <= Int.unsigned prio0 < 64 ->
0 <= Int.unsigned prio < 64 ->
prio0 <> prio ->
nth_val ∘(Int.unsigned (Int.shru prio ($ 3))) rtbl = Some (Vint32 grp) ->
prio_in_tbl prio0
(update_nth_val ∘(Int.unsigned (Int.shru prio ($ 3))) rtbl
(Vint32 (grp&Int.not ($ 1<<(prio&$ 7))))) ->
prio_in_tbl prio0 rtbl.
Lemma prio_neq_in_tbl_rev:
forall prio0 prio rtbl grp,
0 <= Int.unsigned prio0 < 64 ->
0 <= Int.unsigned prio < 64 ->
prio0 <> prio ->
nth_val ∘(Int.unsigned (Int.shru prio ($ 3))) rtbl = Some (Vint32 grp) ->
prio_in_tbl prio0 rtbl ->
prio_in_tbl prio0
(update_nth_val ∘(Int.unsigned (Int.shru prio ($ 3))) rtbl
(Vint32 (grp&Int.not ($ 1<<(prio&$ 7))))) .
Lemma prio_neq_not_in_tbl:
forall prio0 prio rtbl grp,
0 <= Int.unsigned prio0 < 64 ->
0 <= Int.unsigned prio < 64 ->
prio0 <> prio ->
nth_val ∘(Int.unsigned (Int.shru prio ($ 3))) rtbl = Some (Vint32 grp) ->
prio_not_in_tbl prio0
(update_nth_val ∘(Int.unsigned (Int.shru prio ($ 3))) rtbl
(Vint32 (grp&Int.not ($ 1<<(prio&$ 7))))) ->
prio_not_in_tbl prio0 rtbl.
Lemma prio_neq_not_in_tbl_rev:
forall prio0 prio rtbl grp,
0 <= Int.unsigned prio0 < 64 ->
0 <= Int.unsigned prio < 64 ->
prio0 <> prio ->
nth_val ∘(Int.unsigned (Int.shru prio ($ 3))) rtbl = Some (Vint32 grp) ->
prio_not_in_tbl prio0 rtbl ->
prio_not_in_tbl prio0
(update_nth_val ∘(Int.unsigned (Int.shru prio ($ 3))) rtbl
(Vint32 (grp&Int.not ($ 1<<(prio&$ 7))))) .
Lemma TcbMod_join_impl_prio_neq_cur_l :
forall tcbls1 tcbls2 tcbls curtid curprio,
prio_neq_cur tcbls curtid curprio ->
TcbMod.join tcbls1 tcbls2 tcbls ->
prio_neq_cur tcbls1 curtid curprio.
Lemma TcbMod_join_impl_prio_neq_cur_r :
forall tcbls1 tcbls2 tcbls curtid curprio,
prio_neq_cur tcbls curtid curprio ->
TcbMod.join tcbls1 tcbls2 tcbls ->
prio_neq_cur tcbls2 curtid curprio.
Lemma R_PrioTbl_P_impl_prio_neq_cur :
forall ptbl tcbls curtid curprio st m vhold,
0 <= Int.unsigned curprio < 64 ->
R_PrioTbl_P ptbl tcbls vhold ->
TcbMod.get tcbls curtid = Some (curprio, st, m) ->
prio_neq_cur tcbls curtid curprio.
Lemma idle_in_rtbl_hold:
forall v´10 p x2 x0 v´16 x7 m i6 i5 i3 i2 i1 i0,
array_type_vallist_match Int8u v´10 ->
prio_in_tbl ($ OS_IDLE_PRIO) v´10 ->
Int.eq p ($ OS_IDLE_PRIO) = false ->
nth_val´ (Z.to_nat (Int.unsigned i2)) v´10 = Vint32 x2 ->
Int.unsigned x2 <= 255 ->
RL_TCBblk_P
(x0
:: v´16
:: x7
:: m
:: Vint32 i6
:: Vint32 i5
:: Vint32 p
:: Vint32 i3
:: Vint32 i2 :: Vint32 i1 :: Vint32 i0 :: nil) ->
prio_in_tbl ($ OS_IDLE_PRIO)
(update_nth_val (Z.to_nat (Int.unsigned i2)) v´10
(Vint32 (x2&Int.not i1))).
Ltac invertsall :=
repeat progress match goal with
| H : Some _ = Some _ |-
_=> inverts H
end.
Lemma int_ltu_false_eq0:
forall x3,
Int.ltu ($ 0) x3 = false ->
Int.unsigned x3 = 0.
Lemma zof_nat_eq_zero_zero:
forall x , Z.of_nat x = 0 -> (x = 0)%nat.
Lemma sub_zero_eq_rev:
forall i1 i2 : int32,
i1 = i2 -> i1-ᵢi2 = Int.zero.
Lemma int_divu_zero:
forall x, Int.divu Int.zero x = Int.zero.
Lemma z_split:
forall x y,
x <= y -> x = y \/ x < y.
Lemma int_minus4_mod4 : forall x, Int.ltu x ($ 4) = false -> Int.modu (Int.sub x ($ 4)) ($ 4) = $ 0 ->(Int.unsigned x - 4) mod 4 = 0.
Lemma a_mult_b_ge_b : forall a b, 0<a -> 0<=b -> a*b >= b.
Lemma div_in_intrange: forall x a mx, 0<=x <=mx -> a>0 -> 0<=x/a<=mx.
Lemma math_le_xyz:
forall sin out start size,
start = $ 4 ->
Int.unsigned size <= OS_MAX_Q_SIZE ->
Int.ltu out start = false ->
Int.modu (out-ᵢstart) ($ 4) = $ 0 ->
Int.ltu sin start = false ->
Int.modu (sin-ᵢstart) ($ 4) = $ 0 ->
(∘(Int.unsigned (Int.divu (sin-ᵢstart) ($ 4))) < ∘(Int.unsigned size))%nat ->
(∘(Int.unsigned (Int.divu (out-ᵢ$ 4) ($ 4))) < ∘(Int.unsigned ($ Int.unsigned size)))%nat ->
∘(Int.unsigned (Int.divu ((out+ᵢ$ 4)-ᵢstart) ($ 4))) = ∘(Int.unsigned size) ->
Int.unsigned (Int.divu (sin-ᵢstart) ($ 4)) <= Int.unsigned (Int.divu (out-ᵢstart) ($ 4))/\
(S ∘(Int.unsigned (Int.divu (out-ᵢstart) ($ 4))) = ∘(Int.unsigned size))%nat /\
∘(Int.unsigned (Int.divu (out-ᵢstart) ($ 4))) =
(Z.to_nat ((Int.unsigned out - Int.unsigned start) / 4)).
Lemma isptr_length_nth:
forall n vl,
isptr (nth_val´ n vl) -> (S n <= length vl)%nat.
Lemma vallist_seg_eqnil :
forall n vl,
vallist_seg n n vl = nil.
Lemma vallist_seg_Sn :
forall n vl,
(S n <= length vl)%nat ->
vallist_seg n (S n) vl = nth_val´ n vl :: nil.
Lemma int_list_length_dec:
forall (hml : list val) x1,
Int.unsigned x1 = Z.pos (Pos.of_succ_nat (length hml)) ->
Int.unsigned (x1-ᵢ$ 1) = Z.of_nat (length hml).
Lemma vallistseg_n_m_split:
forall n m vl vl´,
(n >= m) %nat ->
(n <= length vl)%nat ->
vallist_seg m n vl = nth_val´ m vl :: vl´ ->
vallist_seg (S m) n vl = vl´.
Lemma list_append_split:
forall (ls1 ls2 : list val) x vl,
ls1 <> nil ->
ls1 ++ ls2 = x :: vl ->
exists l´, ls1 = x::l´ /\ vl = l´ ++ ls2.
Lemma vallist_seg_prop:
forall m size vl,
(m < size)%nat ->
(size <= length vl) %nat ->
vallist_seg m size vl <> nil.
Lemma vallist_seg_n_m_split´ :
forall m size vl vl´ ,
(m < size)%nat ->
(size <= length vl) %nat ->
vallist_seg m size vl = nth_val´ m vl :: vl´ ->
vallist_seg (S m) size vl = vl´.
Lemma vallist_seg_ltunm_prop:
forall m size vl vl´ x,
(m < size)%nat ->
(size <= length vl) %nat ->
vallist_seg m size vl ++ x = nth_val´ m vl :: vl´ ->
vallist_seg (S m) size vl ++ x = vl´.
Lemma le_change:
forall a b, (a <= b -> b >=a)%nat.
Lemma math_xyz_prop2 :
forall out start sin hsize,
start = $ 4 ->
Int.ltu out start = false ->
Int.ltu sin start = false ->
Int.modu (out-ᵢstart) ($ 4) = $ 0 ->
Int.modu (sin-ᵢstart) ($ 4) = $ 0 ->
(∘(Int.unsigned (Int.divu (sin-ᵢstart) ($ 4))) <
∘(Int.unsigned ($ Int.unsigned hsize)))%nat ->
(∘(Int.unsigned (Int.divu (out-ᵢstart) ($ 4))) <
∘(Int.unsigned ($ Int.unsigned hsize)))%nat ->
Int.unsigned ($ Int.unsigned hsize) <= OS_MAX_Q_SIZE ->
Int.unsigned (Int.divu (sin-ᵢstart) ($ 4)) >=
Int.unsigned (Int.divu ((out+ᵢ$ 4)-ᵢstart) ($ 4)) ->
Int.unsigned (Int.divu (sin-ᵢstart) ($ 4)) >=
Int.unsigned (Int.divu (out-ᵢstart) ($ 4))/\
(S ∘(Int.unsigned (Int.divu (out-ᵢstart) ($ 4))) =
∘(Int.unsigned (Int.divu ((out+ᵢ$ 4)-ᵢstart) ($ 4))))%nat /\
∘(Int.unsigned (Int.divu (out-ᵢstart) ($ 4))) =
(Z.to_nat ((Int.unsigned out - Int.unsigned start) / 4)).
Lemma math_xyz_prop3 :
forall out start sin hsize,
start = $ 4 ->
Int.ltu out start = false ->
Int.ltu sin start = false ->
Int.modu (out-ᵢstart) ($ 4) = $ 0 ->
Int.modu (sin-ᵢstart) ($ 4) = $ 0 ->
(∘(Int.unsigned (Int.divu (sin-ᵢstart) ($ 4))) <
∘(Int.unsigned ($ Int.unsigned hsize)))%nat ->
(∘(Int.unsigned (Int.divu (out-ᵢstart) ($ 4))) <
∘(Int.unsigned ($ Int.unsigned hsize)))%nat ->
Int.unsigned ($ Int.unsigned hsize) <= OS_MAX_Q_SIZE ->
Int.unsigned (Int.divu (sin-ᵢstart) ($ 4)) <
Int.unsigned (Int.divu ((out+ᵢ$ 4)-ᵢstart) ($ 4)) ->
(Int.unsigned (Int.divu (sin-ᵢstart) ($ 4)) <
Int.unsigned (Int.divu (out-ᵢstart) ($ 4)) \/
Int.unsigned (Int.divu (sin-ᵢstart) ($ 4)) =
Int.unsigned (Int.divu (out-ᵢstart) ($ 4)))/\
(S ∘(Int.unsigned (Int.divu (out-ᵢstart) ($ 4))) =
∘(Int.unsigned (Int.divu ((out+ᵢ$ 4)-ᵢstart) ($ 4))))%nat /\
∘(Int.unsigned (Int.divu (out-ᵢstart) ($ 4))) =
(Z.to_nat ((Int.unsigned out - Int.unsigned start) / 4)).
Lemma int_nat_ltu_lt:
forall x1 x,
Int.unsigned x1 = Z.of_nat x ->
Int.ltu ($ 0) x1 = true ->
(0 < x) %nat.
Lemma vallist_seg_prop_eq :
forall n m vl x ll,
vallist_seg n m vl = x :: ll ->
x = nth_val´ n vl.
Lemma list_length_lt:
forall l : list msg , (0 < length l)%nat
-> exists x l´, l = x ::l´.
Lemma math_out_start_eq:
forall out m,
Int.ltu out ($ 4) = false ->
Int.modu (out-ᵢ$4) ($ 4) = $ 0 ->
(∘(Int.unsigned (Int.divu (out-ᵢ$ 4) ($ 4))) <
∘(Int.unsigned ($ Int.unsigned m)))%nat ->
Int.unsigned ($ Int.unsigned m) <= OS_MAX_Q_SIZE ->
∘(Int.unsigned (Int.divu (out-ᵢ$4) ($ 4))) =
(Z.to_nat ((Int.unsigned out - Int.unsigned ($ 4)) / 4)).
Lemma math_lt_mod_lt :
forall i i0 x4,
Int.ltu i ($ 4) = false ->
Int.ltu i0 ($ 4) = false ->
Int.modu (i-ᵢ$ 4) ($ 4) = $ 0 ->
Int.modu (i0-ᵢ$ 4) ($ 4) = $ 0 ->
i0 <> i+ᵢ$ 4 ->
∘(Int.unsigned (Int.divu (i0-ᵢ$ 4) ($ 4))) = ∘(Int.unsigned x4) ->
(∘(Int.unsigned (Int.divu (i-ᵢ$ 4) ($ 4))) < ∘(Int.unsigned x4))%nat ->
Int.unsigned x4 <= OS_MAX_Q_SIZE ->
Int.ltu (i+ᵢ$ 4) ($ 4) = false /\ Int.modu ((i+ᵢ$ 4)-ᵢ$ 4) ($ 4) = $ 0 /\
(∘(Int.unsigned (Int.divu ((i+ᵢ$ 4)-ᵢ$ 4) ($ 4))) < ∘(Int.unsigned x4))%nat.
match vl with
| nil => Vundef
| v :: vl´ => match n with
| 0%nat => v
| S n´ => my_nth_val´ n´ vl´
end
end.
Lemma my_nth_val´_eql_yours:
forall n vl,
nth_val´ n vl = my_nth_val´ n vl.
Definition get_option_value (v : option val) : val :=
match v with
| None => Vundef
| Some v´ => v´
end.
Lemma my_nth_val´_and_nth_val:
forall n vl,
my_nth_val´ n vl = get_option_value (nth_val n vl).
Lemma nth_val´_and_nth_val:
forall n vl,
nth_val´ n vl = get_option_value (nth_val n vl).
Lemma prio_in_rtbl_has_tid:
forall rtbl ptbl p vhold,
0 <= Int.unsigned p < 64 ->
RL_RTbl_PrioTbl_P rtbl ptbl vhold->
prio_in_tbl p rtbl ->
exists x, nth_val´ (Z.to_nat (Int.unsigned p)) ptbl = Vptr x.
Lemma update_nth_val_length_eq:
forall n vl v, length vl = length (update_nth_val n vl v).
Lemma int_unsigned_or_prop´
: forall v´57 v´41 : int32,
Int.unsigned v´57 <= 255 ->
Int.unsigned v´41 <= 255 -> Int.unsigned (Int.or v´57 v´41) <= 255.
Lemma nth_val´_imp_nth_val_int:
forall z vl v,
nth_val´ (Z.to_nat z) vl = Vint32 v -> nth_val ∘z vl = Some (Vint32 v).
Lemma unsigned_to_z_eq: forall i, nat_of_Z (Int.unsigned i) =Z.to_nat (Int.unsigned i) .
Ltac clean_ptr H H´ v:=
let x:= fresh in
destruct H;
[assert (exists x,v=Vptr x) by pauto;mytac;clear H H´|
false;eapply isptr_val_inj_false;eauto].
Lemma Int_eq_false_Vptr_neq :
forall i1 i2 b,
Int.eq i1 i2 = false ->
Vptr (b, i1) <> Vptr (b, i2).
Lemma qentries_eq_zero :
forall (i:int32),
(val_inj
(if Int.ltu ($ 0) i
then Some (Vint32 Int.one)
else Some (Vint32 Int.zero)) = Vint32 Int.zero \/
val_inj
(if Int.ltu ($ 0) i
then Some (Vint32 Int.one)
else Some (Vint32 Int.zero)) = Vnull) ->
i = Int.zero.
Lemma update_nth_aux:
forall vl x a n,
update_nth_ectrls (x :: vl) (S n) a =
x :: (update_nth_ectrls vl n a).
Lemma upd_last_prop´:
forall v´40 v´51 v v0 x8,
v´40 <> nil ->
v´51 = upd_last_ectrls ((v, v0) :: v´40) x8 ->
exists vl, v´51 = ((v,v0) :: vl) /\
vl = upd_last_ectrls v´40 x8.
Lemma math_prop_and:
forall x0 n,
0 <= Int.unsigned x0 < 64 ->
(0 <= n < 8)%nat ->
n <> Z.to_nat (Int.unsigned (Int.shru x0 ($ 3))) ->
(Int.not ($ 1<<(Int.shru x0 ($ 3)))&($ 1<<$ Z.of_nat n)) = ($ 1<<$ Z.of_nat n).
Lemma math_prop_eq0:
forall x0,
0 <= Int.unsigned x0 < 64 ->
Int.not ($ 1<<(Int.shru x0 ($ 3)))&
($ 1<<$ Z.of_nat (Z.to_nat (Int.unsigned (Int.shru x0 ($ 3)
)))) = $ 0.
Lemma math_and_zero:
forall n x ,
0 <= Int.unsigned x < 64 ->
(0 <= n < 8)%nat ->
n <> Z.to_nat (Int.unsigned (Int.shru x ($ 3))) ->
($ 1<<$ Z.of_nat n)&($ 1<<(Int.shru x ($ 3))) = $ 0.
Lemma math_prop_neq_zero:
forall x,
0 <= Int.unsigned x < 64 ->
($ 1<<$ Z.of_nat (Z.to_nat (Int.unsigned (Int.shru x ($ 3)))))&($ 1<<(Int.shru x ($ 3))) <>
$ 0.
Lemma int_usigned_tcb_range:
forall x,
0 <= Int.unsigned x < 64 ->
0 <=Int.unsigned (x&$ 7) < 8 /\
0 <= Int.unsigned (Int.shru x ($ 3)) < 8.
Lemma prio_int_disj:
forall x y,
0 <= Int.unsigned x < 256 ->
0 <= Int.unsigned y < 8 ->
(x &($ 1<<y) = $ 1<<y) \/ (x&($ 1<<y) = $ 0).
Lemma nat_int64_range_eq:
forall x,
(0 <= Int.unsigned x < 64) ->
(0<=∘ (Int.unsigned x) < 64)% nat.
Lemma prio_neq_grpeq_prop :
forall prio0 prio,
0 <= Int.unsigned prio0 < 64 ->
0 <= Int.unsigned prio < 64 ->
prio0 <> prio ->
∘(Int.unsigned (Int.shru prio0 ($ 3))) = ∘(Int.unsigned (Int.shru prio ($ 3)))->
(Int.not ($ 1<<(prio&$ 7))&($ 1<<(prio0&$ 7))) =
$ 1<<(prio0&$ 7).
Lemma math_lshift_neq_zero:
forall x0,
0 <= Int.unsigned x0 < 64 ->
Int.zero <> $ 1<<$ Z.of_nat (Z.to_nat (Int.unsigned (Int.shru x0 ($ 3)))).
Ltac simpl_hyp :=
repeat progress
match goal with
| H : ?f _ = Some _ |- _ => unfold f in H; simpl in H; inverts H
end.
Ltac funfold H:=
match type of H with
| ?f _ =>
unfold f in H ;mytac; simpl_hyp
| ?f _ _ =>
unfold f in H ;mytac; simpl_hyp
| ?f _ _ _ =>
unfold f in H ;mytac; simpl_hyp
| ?f _ _ _ _ =>
unfold f in H ;mytac; simpl_hyp
| ?f _ _ _ _ _ =>
unfold f in H ;mytac; simpl_hyp
| _ => idtac
end.
Lemma nth_upd_neq :
forall vl n m x y,
n <> m ->
nth_val n (update_nth_val m vl x) = Some y ->
nth_val n vl = Some y.
Lemma nth_upd_eq :
forall vl n x y,
nth_val n (update_nth_val n vl x) = Some y ->
x = y.
Lemma int_unsigned_inj:
forall x,
0 <= x <= Int.max_unsigned -> $ x = $ 0 -> x = 0.
Lemma int_or_zero_split:
forall x y,
Int.or x y = $ 0 -> x = $0 /\ y = $ 0.
Lemma R_Prio_NoChange_Prio_hold:
forall tcb tid st msg prio st´ msg´,
R_Prio_No_Dup tcb ->
TcbMod.get tcb tid = Some (prio, st, msg) ->
R_Prio_No_Dup (TcbMod.set tcb tid (prio, st´, msg´)).
Lemma math_prop_neq_zero2:
forall x,
0 <= Int.unsigned x < 64 ->
$ 1<<(x&$ 7) <>
$ 0.
Lemma int_eq_false_ltu : forall x,
Int.eq x ($ 0) = false ->
Int.ltu ($ 0) x = true.
Lemma int_ltu_true:
forall x x0,
0 <= Int.unsigned x < 64 ->
Int.ltu ($ 0) (Int.or x0 ($ 1<<(x&$ 7))) = true.
Lemma math_prop_eq:
forall x ,
0 <= Int.unsigned x < 64 ->
($ 1<<$ Z.of_nat (Z.to_nat (Int.unsigned (Int.shru x ($ 3))))) =
$ 1<<(Int.shru x ($ 3)).
Lemma int8_range_nat:
forall z,
0 <= Int.unsigned z < 8 ->
(0<=Z.to_nat (Int.unsigned z) <8)%nat.
Lemma prio_rtbl_dec:
forall x rtbl,
0 <= Int.unsigned x < 64 ->
array_type_vallist_match Int8u rtbl ->
length rtbl = ∘OS_RDY_TBL_SIZE ->
prio_in_tbl x rtbl \/ prio_not_in_tbl x rtbl.
Lemma nat_of_Z_eq:
forall x y,
nat_of_Z (Int.unsigned x) = nat_of_Z (Int.unsigned y) ->
x = y.
Lemma nth_upd_neqrev:
forall (vl : vallist) (n m : nat) (x y : val),
n <> m ->
nth_val n vl = Some y ->
nth_val n (update_nth_val m vl x) = Some y.
Definition prio_neq_cur tcbls curtid curprio :=
forall tid prio st m,
tid <> curtid ->
TcbMod.get tcbls tid = Some (prio, st, m) ->
prio <> curprio.
Lemma prio_neq_in_tbl:
forall prio0 prio rtbl grp,
0 <= Int.unsigned prio0 < 64 ->
0 <= Int.unsigned prio < 64 ->
prio0 <> prio ->
nth_val ∘(Int.unsigned (Int.shru prio ($ 3))) rtbl = Some (Vint32 grp) ->
prio_in_tbl prio0
(update_nth_val ∘(Int.unsigned (Int.shru prio ($ 3))) rtbl
(Vint32 (grp&Int.not ($ 1<<(prio&$ 7))))) ->
prio_in_tbl prio0 rtbl.
Lemma prio_neq_in_tbl_rev:
forall prio0 prio rtbl grp,
0 <= Int.unsigned prio0 < 64 ->
0 <= Int.unsigned prio < 64 ->
prio0 <> prio ->
nth_val ∘(Int.unsigned (Int.shru prio ($ 3))) rtbl = Some (Vint32 grp) ->
prio_in_tbl prio0 rtbl ->
prio_in_tbl prio0
(update_nth_val ∘(Int.unsigned (Int.shru prio ($ 3))) rtbl
(Vint32 (grp&Int.not ($ 1<<(prio&$ 7))))) .
Lemma prio_neq_not_in_tbl:
forall prio0 prio rtbl grp,
0 <= Int.unsigned prio0 < 64 ->
0 <= Int.unsigned prio < 64 ->
prio0 <> prio ->
nth_val ∘(Int.unsigned (Int.shru prio ($ 3))) rtbl = Some (Vint32 grp) ->
prio_not_in_tbl prio0
(update_nth_val ∘(Int.unsigned (Int.shru prio ($ 3))) rtbl
(Vint32 (grp&Int.not ($ 1<<(prio&$ 7))))) ->
prio_not_in_tbl prio0 rtbl.
Lemma prio_neq_not_in_tbl_rev:
forall prio0 prio rtbl grp,
0 <= Int.unsigned prio0 < 64 ->
0 <= Int.unsigned prio < 64 ->
prio0 <> prio ->
nth_val ∘(Int.unsigned (Int.shru prio ($ 3))) rtbl = Some (Vint32 grp) ->
prio_not_in_tbl prio0 rtbl ->
prio_not_in_tbl prio0
(update_nth_val ∘(Int.unsigned (Int.shru prio ($ 3))) rtbl
(Vint32 (grp&Int.not ($ 1<<(prio&$ 7))))) .
Lemma TcbMod_join_impl_prio_neq_cur_l :
forall tcbls1 tcbls2 tcbls curtid curprio,
prio_neq_cur tcbls curtid curprio ->
TcbMod.join tcbls1 tcbls2 tcbls ->
prio_neq_cur tcbls1 curtid curprio.
Lemma TcbMod_join_impl_prio_neq_cur_r :
forall tcbls1 tcbls2 tcbls curtid curprio,
prio_neq_cur tcbls curtid curprio ->
TcbMod.join tcbls1 tcbls2 tcbls ->
prio_neq_cur tcbls2 curtid curprio.
Lemma R_PrioTbl_P_impl_prio_neq_cur :
forall ptbl tcbls curtid curprio st m vhold,
0 <= Int.unsigned curprio < 64 ->
R_PrioTbl_P ptbl tcbls vhold ->
TcbMod.get tcbls curtid = Some (curprio, st, m) ->
prio_neq_cur tcbls curtid curprio.
Lemma idle_in_rtbl_hold:
forall v´10 p x2 x0 v´16 x7 m i6 i5 i3 i2 i1 i0,
array_type_vallist_match Int8u v´10 ->
prio_in_tbl ($ OS_IDLE_PRIO) v´10 ->
Int.eq p ($ OS_IDLE_PRIO) = false ->
nth_val´ (Z.to_nat (Int.unsigned i2)) v´10 = Vint32 x2 ->
Int.unsigned x2 <= 255 ->
RL_TCBblk_P
(x0
:: v´16
:: x7
:: m
:: Vint32 i6
:: Vint32 i5
:: Vint32 p
:: Vint32 i3
:: Vint32 i2 :: Vint32 i1 :: Vint32 i0 :: nil) ->
prio_in_tbl ($ OS_IDLE_PRIO)
(update_nth_val (Z.to_nat (Int.unsigned i2)) v´10
(Vint32 (x2&Int.not i1))).
Ltac invertsall :=
repeat progress match goal with
| H : Some _ = Some _ |-
_=> inverts H
end.
Lemma int_ltu_false_eq0:
forall x3,
Int.ltu ($ 0) x3 = false ->
Int.unsigned x3 = 0.
Lemma zof_nat_eq_zero_zero:
forall x , Z.of_nat x = 0 -> (x = 0)%nat.
Lemma sub_zero_eq_rev:
forall i1 i2 : int32,
i1 = i2 -> i1-ᵢi2 = Int.zero.
Lemma int_divu_zero:
forall x, Int.divu Int.zero x = Int.zero.
Lemma z_split:
forall x y,
x <= y -> x = y \/ x < y.
Lemma int_minus4_mod4 : forall x, Int.ltu x ($ 4) = false -> Int.modu (Int.sub x ($ 4)) ($ 4) = $ 0 ->(Int.unsigned x - 4) mod 4 = 0.
Lemma a_mult_b_ge_b : forall a b, 0<a -> 0<=b -> a*b >= b.
Lemma div_in_intrange: forall x a mx, 0<=x <=mx -> a>0 -> 0<=x/a<=mx.
Lemma math_le_xyz:
forall sin out start size,
start = $ 4 ->
Int.unsigned size <= OS_MAX_Q_SIZE ->
Int.ltu out start = false ->
Int.modu (out-ᵢstart) ($ 4) = $ 0 ->
Int.ltu sin start = false ->
Int.modu (sin-ᵢstart) ($ 4) = $ 0 ->
(∘(Int.unsigned (Int.divu (sin-ᵢstart) ($ 4))) < ∘(Int.unsigned size))%nat ->
(∘(Int.unsigned (Int.divu (out-ᵢ$ 4) ($ 4))) < ∘(Int.unsigned ($ Int.unsigned size)))%nat ->
∘(Int.unsigned (Int.divu ((out+ᵢ$ 4)-ᵢstart) ($ 4))) = ∘(Int.unsigned size) ->
Int.unsigned (Int.divu (sin-ᵢstart) ($ 4)) <= Int.unsigned (Int.divu (out-ᵢstart) ($ 4))/\
(S ∘(Int.unsigned (Int.divu (out-ᵢstart) ($ 4))) = ∘(Int.unsigned size))%nat /\
∘(Int.unsigned (Int.divu (out-ᵢstart) ($ 4))) =
(Z.to_nat ((Int.unsigned out - Int.unsigned start) / 4)).
Lemma isptr_length_nth:
forall n vl,
isptr (nth_val´ n vl) -> (S n <= length vl)%nat.
Lemma vallist_seg_eqnil :
forall n vl,
vallist_seg n n vl = nil.
Lemma vallist_seg_Sn :
forall n vl,
(S n <= length vl)%nat ->
vallist_seg n (S n) vl = nth_val´ n vl :: nil.
Lemma int_list_length_dec:
forall (hml : list val) x1,
Int.unsigned x1 = Z.pos (Pos.of_succ_nat (length hml)) ->
Int.unsigned (x1-ᵢ$ 1) = Z.of_nat (length hml).
Lemma vallistseg_n_m_split:
forall n m vl vl´,
(n >= m) %nat ->
(n <= length vl)%nat ->
vallist_seg m n vl = nth_val´ m vl :: vl´ ->
vallist_seg (S m) n vl = vl´.
Lemma list_append_split:
forall (ls1 ls2 : list val) x vl,
ls1 <> nil ->
ls1 ++ ls2 = x :: vl ->
exists l´, ls1 = x::l´ /\ vl = l´ ++ ls2.
Lemma vallist_seg_prop:
forall m size vl,
(m < size)%nat ->
(size <= length vl) %nat ->
vallist_seg m size vl <> nil.
Lemma vallist_seg_n_m_split´ :
forall m size vl vl´ ,
(m < size)%nat ->
(size <= length vl) %nat ->
vallist_seg m size vl = nth_val´ m vl :: vl´ ->
vallist_seg (S m) size vl = vl´.
Lemma vallist_seg_ltunm_prop:
forall m size vl vl´ x,
(m < size)%nat ->
(size <= length vl) %nat ->
vallist_seg m size vl ++ x = nth_val´ m vl :: vl´ ->
vallist_seg (S m) size vl ++ x = vl´.
Lemma le_change:
forall a b, (a <= b -> b >=a)%nat.
Lemma math_xyz_prop2 :
forall out start sin hsize,
start = $ 4 ->
Int.ltu out start = false ->
Int.ltu sin start = false ->
Int.modu (out-ᵢstart) ($ 4) = $ 0 ->
Int.modu (sin-ᵢstart) ($ 4) = $ 0 ->
(∘(Int.unsigned (Int.divu (sin-ᵢstart) ($ 4))) <
∘(Int.unsigned ($ Int.unsigned hsize)))%nat ->
(∘(Int.unsigned (Int.divu (out-ᵢstart) ($ 4))) <
∘(Int.unsigned ($ Int.unsigned hsize)))%nat ->
Int.unsigned ($ Int.unsigned hsize) <= OS_MAX_Q_SIZE ->
Int.unsigned (Int.divu (sin-ᵢstart) ($ 4)) >=
Int.unsigned (Int.divu ((out+ᵢ$ 4)-ᵢstart) ($ 4)) ->
Int.unsigned (Int.divu (sin-ᵢstart) ($ 4)) >=
Int.unsigned (Int.divu (out-ᵢstart) ($ 4))/\
(S ∘(Int.unsigned (Int.divu (out-ᵢstart) ($ 4))) =
∘(Int.unsigned (Int.divu ((out+ᵢ$ 4)-ᵢstart) ($ 4))))%nat /\
∘(Int.unsigned (Int.divu (out-ᵢstart) ($ 4))) =
(Z.to_nat ((Int.unsigned out - Int.unsigned start) / 4)).
Lemma math_xyz_prop3 :
forall out start sin hsize,
start = $ 4 ->
Int.ltu out start = false ->
Int.ltu sin start = false ->
Int.modu (out-ᵢstart) ($ 4) = $ 0 ->
Int.modu (sin-ᵢstart) ($ 4) = $ 0 ->
(∘(Int.unsigned (Int.divu (sin-ᵢstart) ($ 4))) <
∘(Int.unsigned ($ Int.unsigned hsize)))%nat ->
(∘(Int.unsigned (Int.divu (out-ᵢstart) ($ 4))) <
∘(Int.unsigned ($ Int.unsigned hsize)))%nat ->
Int.unsigned ($ Int.unsigned hsize) <= OS_MAX_Q_SIZE ->
Int.unsigned (Int.divu (sin-ᵢstart) ($ 4)) <
Int.unsigned (Int.divu ((out+ᵢ$ 4)-ᵢstart) ($ 4)) ->
(Int.unsigned (Int.divu (sin-ᵢstart) ($ 4)) <
Int.unsigned (Int.divu (out-ᵢstart) ($ 4)) \/
Int.unsigned (Int.divu (sin-ᵢstart) ($ 4)) =
Int.unsigned (Int.divu (out-ᵢstart) ($ 4)))/\
(S ∘(Int.unsigned (Int.divu (out-ᵢstart) ($ 4))) =
∘(Int.unsigned (Int.divu ((out+ᵢ$ 4)-ᵢstart) ($ 4))))%nat /\
∘(Int.unsigned (Int.divu (out-ᵢstart) ($ 4))) =
(Z.to_nat ((Int.unsigned out - Int.unsigned start) / 4)).
Lemma int_nat_ltu_lt:
forall x1 x,
Int.unsigned x1 = Z.of_nat x ->
Int.ltu ($ 0) x1 = true ->
(0 < x) %nat.
Lemma vallist_seg_prop_eq :
forall n m vl x ll,
vallist_seg n m vl = x :: ll ->
x = nth_val´ n vl.
Lemma list_length_lt:
forall l : list msg , (0 < length l)%nat
-> exists x l´, l = x ::l´.
Lemma math_out_start_eq:
forall out m,
Int.ltu out ($ 4) = false ->
Int.modu (out-ᵢ$4) ($ 4) = $ 0 ->
(∘(Int.unsigned (Int.divu (out-ᵢ$ 4) ($ 4))) <
∘(Int.unsigned ($ Int.unsigned m)))%nat ->
Int.unsigned ($ Int.unsigned m) <= OS_MAX_Q_SIZE ->
∘(Int.unsigned (Int.divu (out-ᵢ$4) ($ 4))) =
(Z.to_nat ((Int.unsigned out - Int.unsigned ($ 4)) / 4)).
Lemma math_lt_mod_lt :
forall i i0 x4,
Int.ltu i ($ 4) = false ->
Int.ltu i0 ($ 4) = false ->
Int.modu (i-ᵢ$ 4) ($ 4) = $ 0 ->
Int.modu (i0-ᵢ$ 4) ($ 4) = $ 0 ->
i0 <> i+ᵢ$ 4 ->
∘(Int.unsigned (Int.divu (i0-ᵢ$ 4) ($ 4))) = ∘(Int.unsigned x4) ->
(∘(Int.unsigned (Int.divu (i-ᵢ$ 4) ($ 4))) < ∘(Int.unsigned x4))%nat ->
Int.unsigned x4 <= OS_MAX_Q_SIZE ->
Int.ltu (i+ᵢ$ 4) ($ 4) = false /\ Int.modu ((i+ᵢ$ 4)-ᵢ$ 4) ($ 4) = $ 0 /\
(∘(Int.unsigned (Int.divu ((i+ᵢ$ 4)-ᵢ$ 4) ($ 4))) < ∘(Int.unsigned x4))%nat.
end of handling div range
handle sub range
Lemma ecblist_p_compose:
forall qptrl1 p q msgqls1 mqls1 tcbls qptrl2 msgqls2 mqls2 mqls,
EcbMod.join mqls1 mqls2 mqls ->
ECBList_P p q qptrl1 msgqls1 mqls1 tcbls ->
ECBList_P q Vnull qptrl2 msgqls2 mqls2 tcbls ->
ECBList_P p Vnull (qptrl1 ++ qptrl2) (msgqls1 ++ msgqls2) mqls tcbls.
Definition auxand (P Q : Prop) := P /\ Q.
Lemma math_prop_int_modu:
forall x,
Int.ltu x ($ 4) = false ->
Int.modu (x-ᵢ$ 4) ($ 4) = $ 0 ->
(Int.unsigned x - Int.unsigned (Int.zero+ᵢ($ 4+ᵢInt.zero))) mod 4 = 0.
Lemma math_prop_ltu_20:
forall x x4,
Int.unsigned x4 <= OS_MAX_Q_SIZE ->
Int.ltu x ($ 4) = false ->
Int.modu (x-ᵢ$ 4) ($ 4) = $ 0 ->
(∘(Int.unsigned (Int.divu (x-ᵢ$ 4) ($ 4))) < ∘(Int.unsigned x4))%nat ->
(Int.unsigned x - Int.unsigned (Int.zero+ᵢ($ 4+ᵢInt.zero))) / 4 < 20.
Lemma nat_8_range_conver:
forall x, (0 <= Z.to_nat (Int.unsigned x) < 8)%nat <->
(Int.unsigned x < 8).
Lemma math_unmap_range:
forall x y,
Int.unsigned x <= 255 ->
nth_val´ (Z.to_nat (Int.unsigned x)) OSUnMapVallist = Vint32 y ->
(0<= Z.to_nat (Int.unsigned y) <8)%nat.
Lemma nth_val´_imply_nth_val:
forall n vl v,
(n < length vl)%nat ->
nth_val´ n vl = v ->
nth_val n vl = Some v.
Lemma shrl_eq :
forall x,
(0 <= Z.to_nat (Int.unsigned x) < 8)%nat ->
(Z.to_nat (Int.unsigned x)) =
∘(Int.unsigned (Int.shru ((x<<$ 3)+ᵢ$ 0) ($ 3))).
Lemma math_8_255_eq:
forall y v,
Int.unsigned v <= 255 ->
nth_val´ (Z.to_nat (Int.unsigned v)) OSUnMapVallist = Vint32 y ->
v <> $ 0 ->
v&($ 1<< y) = $ 1<< y.
Lemma math_prop_int_zero_eq :
forall rgrp x,
Int.unsigned rgrp <= 255->
nth_val´ (Z.to_nat (Int.unsigned rgrp)) OSUnMapVallist = Vint32 x ->
rgrp <> $ 0 ->
rgrp&($ 1<< x) = $ 0 ->
Int.zero = $ 1<<(((x<<$ 3))&$ 7).
Lemma math_64_le_8 :
forall y,
Int.unsigned y < 64 ->
Int.unsigned (Int.shru y ($ 3)) <8.
Lemma nat_x_prop_range:
forall x ,
(0 <= Z.to_nat (Int.unsigned x) < 8)%nat ->
0 <= Int.unsigned ((x<<$ 3)+ᵢ$ 0) < 64.
Lemma math_8range_eqy:
forall x y,
(0 <= Z.to_nat (Int.unsigned x) < 8)%nat ->
Int.unsigned y < 8 ->
(((x<<$ 3)+ᵢy)&$ 7) = y.
Lemma math_shrl_3_eq :
forall x y,
Int.unsigned y < 8 ->
(0 <= Z.to_nat (Int.unsigned x) < 8)%nat ->
(Int.shru ((x<<$ 3)+ᵢy) ($ 3)) = x.
Lemma math_88_prio_range:
forall x y,
Int.unsigned y < 8 ->
(0 <= Z.to_nat (Int.unsigned x) < 8)%nat ->
0 <= Int.unsigned ((x<<$ 3)+ᵢy) < 64.
Lemma math_unmap_get_y :
forall v y,
Int.unsigned v <= 255 ->
nth_val´ (Z.to_nat (Int.unsigned v)) OSUnMapVallist = Vint32 y ->
Int.unsigned y < 8.
Lemma prio_in_tbl_rgrp_neq_zero:
forall p rtbl rgrp,
0<= Int.unsigned p < 64 ->
array_type_vallist_match Int8u rtbl ->
length rtbl = ∘OS_RDY_TBL_SIZE->
prio_in_tbl p rtbl ->
RL_Tbl_Grp_P rtbl (Vint32 rgrp) ->
rgrp <> $ 0.
Lemma unmap_inrtbl´:
forall x y i i0 rtbl,
prio_in_tbl ($ OS_IDLE_PRIO) rtbl ->
array_type_vallist_match Int8u rtbl ->
length rtbl = ∘OS_RDY_TBL_SIZE->
RL_Tbl_Grp_P rtbl (Vint32 i) ->
(Int.unsigned i <= 255) ->
nth_val´ (Z.to_nat (Int.unsigned i)) OSUnMapVallist = Vint32 x ->
nth_val´ (Z.to_nat (Int.unsigned x)) rtbl = Vint32 i0 ->
nth_val´ (Z.to_nat (Int.unsigned i0)) OSUnMapVallist = Vint32 y ->
Int.unsigned ((x<<$ 3) +ᵢ y) < 64 /\
prio_in_tbl ((x<<$ 3) +ᵢ y) rtbl.
Lemma unmap_inrtbl:
forall x y i i0 rtbl,
prio_in_tbl ($ OS_IDLE_PRIO) rtbl ->
array_type_vallist_match Int8u rtbl ->
length rtbl = ∘OS_RDY_TBL_SIZE->
RL_Tbl_Grp_P rtbl (Vint32 i) ->
(Int.unsigned i <= 255) ->
nth_val´ (Z.to_nat (Int.unsigned i)) OSUnMapVallist = Vint32 x ->
nth_val´ (Z.to_nat (Int.unsigned x)) rtbl = Vint32 i0 ->
nth_val´ (Z.to_nat (Int.unsigned i0)) OSUnMapVallist = Vint32 y ->
prio_in_tbl (Int.repr (Int.unsigned ((x<<$ 3) +ᵢ y))) rtbl.
Lemma math_and_shf_ltu_true:
forall v x,
Int.unsigned x < 64 ->
v&($ 1<<(x&$ 7)) = $ 1<<(x&$ 7) ->
Int.ltu ($ 0) v = true.
Lemma nat_elim:
forall x,
Int.unsigned x < 8 ->
$ Z.of_nat (Z.to_nat (Int.unsigned x)) = x.
Lemma int_ltu_shru_ltu:
forall x prio´,
Int.unsigned x < 8 ->
Int.unsigned prio´ < 64 ->
Int.unsigned x < Int.unsigned (Int.shru prio´ ($ 3)) ->
Int.unsigned ((x<<$ 3)+ᵢ$7) < Int.unsigned prio´.
Lemma math_unmap_core_prop:
forall rgrp x y,
Int.unsigned rgrp <=255 ->
nth_val´ (Z.to_nat (Int.unsigned rgrp)) OSUnMapVallist = Vint32 x ->
Int.unsigned y < 8 ->
rgrp <> $ 0 ->
rgrp&($ 1<< y) = $ 1<< y ->
Int.unsigned x <= Int.unsigned y.
Lemma int_add_lt_max :
forall x y,
Int.unsigned x < 8 ->
Int.unsigned y < 8 ->
Int.unsigned ((x<<$ 3)+ᵢy) <= Int.unsigned ((x<<$ 3)+ᵢ$7).
Lemma math_prio_8_lt:
forall y prio´,
Int.unsigned y < 8 ->
Int.unsigned prio´ < 64 ->
Int.unsigned y <= Int.unsigned (prio´&$ 7) ->
Int.unsigned (((Int.shru prio´ ($ 3))<<$ 3)+ᵢy) <= Int.unsigned prio´.
Lemma math_highest_prio_select :
forall x y xv rgrp prio´ rtbl vy,
Int.unsigned x < 8 ->
Int.unsigned y < 8 ->
Int.unsigned (prio´&$ 7) < 8 ->
Int.unsigned prio´ < 64 ->
Int.unsigned (Int.shru prio´ ($ 3)) < 8 ->
Int.unsigned rgrp <=255 ->
Int.unsigned xv <=255 ->
nth_val´ (Z.to_nat (Int.unsigned xv)) OSUnMapVallist = Vint32 y ->
nth_val´ (Z.to_nat (Int.unsigned rgrp)) OSUnMapVallist = Vint32 x ->
nth_val (Z.to_nat (Int.unsigned x)) rtbl = Some (Vint32 xv) ->
nth_val (Z.to_nat (Int.unsigned (Int.shru prio´ ($ 3)))) rtbl = Some (Vint32 vy) ->
rgrp <> $ 0 ->
xv <> $ 0 ->
rgrp&($ 1<<(Int.shru prio´ ($ 3))) = $ 1<<(Int.shru prio´ ($ 3)) ->
vy&($ 1<<(prio´&$ 7)) = $ 1<<(prio´&$ 7) ->
Int.unsigned ((x<<$ 3)+ᵢy) <= Int.unsigned prio´.
Lemma tcbjoin_get_get2:
forall x t x3 x2 x1 z,
x <> t ->
TcbJoin x x3 x2 x1 ->
TcbMod.get x1 t = Some z ->
TcbMod.get x2 t = Some z.
Lemma TCBList_P_tcbmod_get:
forall l1 x1 t z p1 rtbl ,
TcbMod.get x1 t = Some z ->
TCBList_P p1 l1 rtbl x1 ->
(Vptr t = p1 /\ l1 <> nil) \/
(exists ll1 ll2 vl, l1 = ll1 ++ (vl :: ll2) /\ ll2 <> nil /\ V_OSTCBNext vl = Some (Vptr t)).
Lemma tcbjoin_join_ex:
forall x x3 x1 x4 x5 x2,
TcbJoin x x3 x2 x1 ->
TcbMod.join x4 x5 x2 ->
exists x´, TcbJoin x x3 x4 x´ /\ TcbMod.join x´ x5 x1.
Lemma TCBList_P_decompose:
forall l1 l2 p1 rtbl x1 a vp,
TCBList_P p1 ((l1++(a::nil))++l2) rtbl x1 ->
V_OSTCBNext a = Some vp ->
exists x y ,TCBList_P p1 (l1++(a::nil)) rtbl x /\
TCBList_P vp l2 rtbl y /\ TcbMod.join x y x1.
Lemma TCBList_get_TCBNode_P:
forall tcbls p1 p2 rtbl t x1 x x2 l1 l2 ,
TcbMod.get tcbls t = Some x ->
TcbMod.join x1 x2 tcbls ->
TCBList_P p1 l1 rtbl x1 ->
TCBList_P p2 l2 rtbl x2 ->
exists vl, TCBNode_P vl rtbl x.
Ltac sifthen :=
repeat progress
match goal with
| H : exists _, _ |- _ => destruct H
| H : _ /\ _ |- _ => destruct H
| H : context[if ?b then _ else _] |- _ =>
let x := fresh "B" in (remember b as x);
destruct x;
[match goal with
| H1 : true = (_ =? _)%positive |- _ =>
rewrite Pos2Z.inj_eqb in H1;
apply eq_sym in H1;
apply Z.eqb_eq in H1;
inverts H1
end | tryfalse]
end.
Ltac fsimpl :=
repeat progress
match goal with
| H : context[let (_, _) := ?x in _] |- _ => destruct x
| _ => idtac
end; sifthen;invertsall.
Lemma tcb_get_join:
forall tcs ptcb prio t m,
TcbMod.get tcs ptcb = Some (prio, t, m) ->
exists tcs´,
TcbMod.join (TcbMod.sig ptcb (prio, t, m)) tcs´ tcs.
Lemma math_prop_ltu_mod:
forall i,
Int.ltu i ($ 4) = false ->
Int.modu (i-ᵢ$ 4) ($ 4) = $ 0 ->
4 * ((Int.unsigned i - 4) / 4) = Int.unsigned i - 4.
Lemma math_prop_divu_zle:
forall x3 i,
Int.unsigned x3 <= OS_MAX_Q_SIZE ->
Int.ltu i ($ 4) = false ->
(∘(Int.unsigned (Int.divu (i-ᵢ$ 4) ($ 4))) < ∘(Int.unsigned x3))%nat ->
(Int.unsigned i - 4) / 4 < OS_MAX_Q_SIZE.
Lemma math_prop_divu_ltmod:
forall x3 i2,
0 < Int.unsigned x3 ->
Int.unsigned x3 <= OS_MAX_Q_SIZE ->
∘(Int.unsigned (Int.divu (i2-ᵢ$ 4) ($ 4))) = ∘(Int.unsigned x3) ->
Int.ltu i2 ($ 4) = false ->
Int.modu (i2-ᵢ$ 4) ($ 4) = $ 0 ->
i2 = Int.mul x3 ($ 4)+ᵢ$ 4.
Lemma math_prio_neq_zero:
forall prio pri,
0<=Int.unsigned prio < 64 ->
0<=Int.unsigned pri < 64 ->
prio <> pri ->
∘(Int.unsigned (Int.shru pri ($ 3))) = ∘(Int.unsigned (Int.shru prio ($ 3))) ->
(Int.one<<(pri&$ 7))&($ 1<<(prio&$ 7)) = $ 0.
Lemma prio_wt_inq_keep:
forall prio prio0 etbl ey,
Int.unsigned prio < 64 ->
prio <> $ prio0 ->
nth_val ∘(Int.unsigned (Int.shru prio ($ 3))) etbl = Some (Vint32 ey) ->
(PrioWaitInQ prio0
(update_nth_val ∘(Int.unsigned (Int.shru prio ($ 3))) etbl
(Vint32 (Int.or ey ($ 1<<(prio&$ 7))))) <->
PrioWaitInQ prio0 etbl).
Lemma ecbmod_joinsig_get_none:
forall x x0 x1 ecbls qid,
EcbMod.joinsig x x0 x1 ecbls ->
EcbMod.get ecbls qid = None ->
EcbMod.get x1 qid = None.
Lemma prio_update_self_not_in :
forall pri rtbl ry,
0 <= Int.unsigned pri < 64 ->
nth_val ∘(Int.unsigned (Int.shru pri ($ 3))) rtbl = Some (Vint32 ry) ->
~ prio_in_tbl pri
(update_nth_val ∘(Int.unsigned (Int.shru pri ($ 3))) rtbl
(Vint32 (ry&Int.not ($ 1<<(pri&$ 7))))).
Lemma math_xy_prio_cons:
forall x y,
Int.unsigned x < 8 ->
Int.unsigned y < 8 ->
0<= (Int.unsigned ((x<<$ 3)+ᵢy)) < 64.
Lemma nth_val´_imp_nth_val_vptr:
forall n (vl : list val) v,
nth_val´ n vl = Vptr v -> nth_val n vl = Some (Vptr v).
Lemma math_nth_8_neq_not:
forall x y n,
Int.unsigned x < 8 ->
nth_val´ (Z.to_nat (Int.unsigned x)) OSMapVallist = Vint32 y ->
(0 <= n < 8)%nat ->
n <> Z.to_nat (Int.unsigned x) ->
Int.not y &($ 1<<$ Z.of_nat n) = $ 1<<$ Z.of_nat n.
Lemma last_remain :
forall (y1 : list vallist) a,
y1 <> nil ->
last (a :: y1) nil = last y1 nil.
Lemma TCBList_merge_prop:
forall y1 x1 a b c z x2 y2,
TcbMod.join a b c ->
V_OSTCBNext (last y1 nil) = Some x2 ->
TCBList_P x1 y1 z a ->
TCBList_P x2 y2 z b ->
TCBList_P x1 (y1++y2) z c .
Lemma math_nth_8_neq_zero :
forall x y ,
Int.unsigned x < 8 ->
nth_val´ (Z.to_nat (Int.unsigned x)) OSMapVallist = Vint32 y ->
($ 1<<x)&y <> $ 0.
Lemma math_nth_8_neq_zero´ :
forall x y ,
Int.unsigned x < 8 ->
nth_val´ (Z.to_nat (Int.unsigned x)) OSMapVallist = Vint32 y ->
y <> $ 0 .
Lemma math_nth_8_gt_zero :
forall v´39 v´40 ,
Int.unsigned v´39 <= 7 ->
nth_val´ (Z.to_nat (Int.unsigned v´39)) OSMapVallist = Vint32 v´40 ->
0 < Int.unsigned v´40.
Lemma math_nth_8_eq_shl :
forall x y ,
Int.unsigned x < 8 ->
nth_val´ (Z.to_nat (Int.unsigned x)) OSMapVallist = Vint32 y ->
($ 1<<x)&y = ($ 1<<x).
Lemma math_nth_8_eq_zero:
forall x y n,
Int.unsigned x <= 7 ->
nth_val´ (Z.to_nat (Int.unsigned x)) OSMapVallist = Vint32 y ->
(0 <= n < 8)%nat ->
n <> Z.to_nat (Int.unsigned x) ->
y&($ 1<<$ Z.of_nat n) = Int.zero.
Lemma int_ltu_eq_false:
forall x1,
Int.ltu ($ 0) x1 = true ->
Int.eq x1 Int.zero = false.
Lemma Z2Nat_0: forall a, a<=0 -> Z.to_nat a =0%nat.
Lemma Zle_natle : forall a b, a<=b -> (Z.to_nat a <= Z.to_nat b)%nat.
Lemma math_le_trans:
forall x y n,
y <= Z.of_nat n ->
(∘x < ∘y)%nat ->
(∘x <= n)%nat.
Lemma math_xyz_prop2´
: forall out start sin hsize : int32,
start = $ 4 ->
Int.ltu out start = false ->
Int.ltu sin start = false ->
Int.modu (out-ᵢstart) ($ 4) = $ 0 ->
Int.modu (sin-ᵢstart) ($ 4) = $ 0 ->
(∘(Int.unsigned (Int.divu (sin-ᵢstart) ($ 4))) <
∘(Int.unsigned hsize))%nat ->
(∘(Int.unsigned (Int.divu (out-ᵢstart) ($ 4))) <
∘(Int.unsigned hsize))%nat ->
Int.unsigned hsize <= OS_MAX_Q_SIZE ->
Int.unsigned (Int.divu (sin-ᵢstart) ($ 4)) >
Int.unsigned (Int.divu ((out+ᵢ$ 4)-ᵢstart) ($ 4)) ->
Int.unsigned (Int.divu (sin-ᵢstart) ($ 4)) >
Int.unsigned (Int.divu (out-ᵢstart) ($ 4)) /\
S ∘(Int.unsigned (Int.divu (out-ᵢstart) ($ 4))) =
∘(Int.unsigned (Int.divu ((out+ᵢ$ 4)-ᵢstart) ($ 4))) /\
∘(Int.unsigned (Int.divu (out-ᵢstart) ($ 4))) =
Z.to_nat ((Int.unsigned out - Int.unsigned start) / 4).
Lemma math_xyz_prop3´
: forall out start sin hsize : int32,
start = $ 4 ->
Int.ltu out start = false ->
Int.ltu sin start = false ->
Int.modu (out-ᵢstart) ($ 4) = $ 0 ->
Int.modu (sin-ᵢstart) ($ 4) = $ 0 ->
(∘(Int.unsigned (Int.divu (sin-ᵢstart) ($ 4))) <
∘(Int.unsigned hsize))%nat ->
(∘(Int.unsigned (Int.divu (out-ᵢstart) ($ 4))) <
∘(Int.unsigned hsize))%nat ->
Int.unsigned hsize <= OS_MAX_Q_SIZE ->
Int.unsigned (Int.divu (sin-ᵢstart) ($ 4)) <
Int.unsigned (Int.divu ((out+ᵢ$ 4)-ᵢstart) ($ 4)) ->
(Int.unsigned (Int.divu (sin-ᵢstart) ($ 4)) <
Int.unsigned (Int.divu (out-ᵢstart) ($ 4)) \/
Int.unsigned (Int.divu (sin-ᵢstart) ($ 4)) =
Int.unsigned (Int.divu (out-ᵢstart) ($ 4))) /\
S ∘(Int.unsigned (Int.divu (out-ᵢstart) ($ 4))) =
∘(Int.unsigned (Int.divu ((out+ᵢ$ 4)-ᵢstart) ($ 4))) /\
∘(Int.unsigned (Int.divu (out-ᵢstart) ($ 4))) =
Z.to_nat ((Int.unsigned out - Int.unsigned start) / 4).
Lemma list_maxsize_le:
forall (ml : list val) hsize,
(length ml = ∘OS_MAX_Q_SIZE)%nat ->
Int.unsigned hsize <= OS_MAX_Q_SIZE ->
(∘(Int.unsigned hsize) <= length ml)%nat.
Lemma math_xyz_prop4´
: forall out start sin hsize : int32,
start = $ 4 ->
Int.ltu out start = false ->
Int.ltu sin start = false ->
Int.modu (out-ᵢstart) ($ 4) = $ 0 ->
Int.modu (sin-ᵢstart) ($ 4) = $ 0 ->
(∘(Int.unsigned (Int.divu (sin-ᵢstart) ($ 4))) <
∘(Int.unsigned hsize))%nat ->
(∘(Int.unsigned (Int.divu (out-ᵢstart) ($ 4))) <
∘(Int.unsigned hsize))%nat ->
Int.unsigned hsize <= OS_MAX_Q_SIZE ->
Int.unsigned (Int.divu (sin-ᵢstart) ($ 4)) =
Int.unsigned (Int.divu ((out+ᵢ$ 4)-ᵢstart) ($ 4)) ->
(Int.unsigned (Int.divu (sin-ᵢstart) ($ 4)) >
Int.unsigned (Int.divu (out-ᵢstart) ($ 4)) ) /\
S ∘(Int.unsigned (Int.divu (out-ᵢstart) ($ 4))) =
∘(Int.unsigned (Int.divu ((out+ᵢ$ 4)-ᵢstart) ($ 4))) /\
∘(Int.unsigned (Int.divu (out-ᵢstart) ($ 4))) =
Z.to_nat ((Int.unsigned out - Int.unsigned start) / 4).
Lemma math_out_start_eq´
: forall out m : int32,
Int.ltu out ($ 4) = false ->
Int.modu (out-ᵢ$ 4) ($ 4) = $ 0 ->
(∘(Int.unsigned (Int.divu (out-ᵢ$ 4) ($ 4))) <
∘(Int.unsigned m))%nat ->
Int.unsigned m <= OS_MAX_Q_SIZE ->
∘(Int.unsigned (Int.divu (out-ᵢ$ 4) ($ 4))) =
Z.to_nat ((Int.unsigned out - Int.unsigned ($ 4)) / 4).
Lemma prio_bit_and_zero:
forall prio prio0,
0 <= Int.unsigned prio0 < 64 ->
0 <= Int.unsigned prio < 64 ->
prio0 <> prio ->
Z.to_nat (Int.unsigned (Int.shru prio ($ 3))) = Z.to_nat (Int.unsigned (Int.shru prio0 ($ 3))) ->
($ 1<<(prio&$ 7))&($ 1<<(prio0&$ 7)) = Int.zero.
Lemma or_and_combine:
forall x y z,
x & z = z ->
y & z = Int.zero ->
(Int.or x y) & z = z.
Lemma or_and_distrib:
forall x y z,
(Int.or z x) & y = y ->
x & y = Int.zero ->
z & y = y.
Lemma or_and_distrib_zero:
forall x y z,
(Int.or z y) & x = Int.zero ->
y & x = Int.zero ->
z & x = Int.zero.
Lemma or_and_combine_zero:
forall x y z,
z & x = Int.zero ->
y & x = Int.zero ->
(Int.or z y) & x = Int.zero.
Lemma neq_comm:
forall T (a b:T),
a <> b ->
b <> a.
Lemma array_type_match_get_value:
forall rtbl Zpy,
0<=Zpy <= 7 ->
array_type_vallist_match Int8u rtbl ->
length rtbl = ∘OS_RDY_TBL_SIZE ->
(exists v, nth_val (Z.to_nat Zpy) rtbl = Some (Vint32 v)).
Lemma tcbjoin_tid_neq :
forall tid x y z tid0 a,
TcbJoin tid x y z ->
TcbMod.get y tid0 = Some a -> tid0 <> tid.
Lemma math_nth_8_eq_zero2:
forall (x y z: int32) ,
Int.unsigned x <= 7 ->
nth_val´ (Z.to_nat (Int.unsigned x)) OSMapVallist = Vint32 y ->
Int.unsigned z < 8 ->
z <> x -> Int.not y &($ 1<< z) = ($ 1<< z).
Lemma math_pry_neq_prio_neq:
forall x y z,
Int.unsigned x <= 7 ->
Int.unsigned y <= 7 ->
0 <= z < 64 ->
Int.shru ($ z) ($ 3) <> x ->
$ z <> (x<<$ 3)+ᵢy .
Lemma int_ltu_neq_zero:
forall x,
Int.ltu ($ 0) x = true -> x <> $ 0.
Lemma math_nth_8_eq_zero´:
forall (x y z: int32) ,
Int.unsigned x <= 7 ->
nth_val´ (Z.to_nat (Int.unsigned x)) OSMapVallist = Vint32 y ->
Int.unsigned z < 8 ->
z <> x -> y&($ 1<< z) = $ 0.
Lemma math_mapval_core_prop:
forall x y : int32,
Int.unsigned x < 8 ->
nth_val´ (Z.to_nat (Int.unsigned x)) OSMapVallist = Vint32 y ->
y = $ 1<<x.
Lemma int_not_shrl_and :
forall x y,
Int.unsigned x < 8 ->
Int.unsigned y < 8 ->
x <> y ->
(Int.not ($ 1 << x)) & ($1 << y) = $ 1 << y.
Lemma math_prio_eq:
forall prio ,
Int.unsigned prio < 64 ->
prio = Int.add (Int.shru prio ($ 3) << $ 3) (prio & $ 7).
Lemma joinsig_join_getnone:
forall x y v1 v2 v3 v4,
EcbMod.joinsig x y v4 v2 ->
EcbMod.join v1 v2 v3 ->
EcbMod.get v1 x = None.
Lemma joinsig_get_none:
forall x y v4 v2,
EcbMod.joinsig x y v4 v2 ->
EcbMod.get v4 x = None.
Lemma ecb_set_join_join:
forall (ml : EcbMod.map) (a : tidspec.A) (b : absecb.B)
(ml1 ml2 ml1´ : EcbMod.map) (b´ : absecb.B),
EcbMod.joinsig a b ml1´ ml1 ->
EcbMod.join ml2 ml1 ml ->
exists ml1n,
EcbMod.joinsig a b´ ml1´ ml1n /\ EcbMod.join ml2 ml1n (EcbMod.set ml a b´).
Lemma math_le_max_q :
forall x N M,
x <= OS_MAX_Q_SIZE ->
(M < ∘x)%nat ->
(S N = ∘x)%nat ->
(N < ∘OS_MAX_Q_SIZE)%nat /\ (N >= M)%nat.
Lemma math_len_le_and:
forall v2 a N M y,
length v2 = ∘OS_MAX_Q_SIZE ->
a <= OS_MAX_Q_SIZE ->
(M < ∘a)%nat ->
(S N = ∘ a)%nat ->
(M <= S N)%nat /\ (S N <= length (update_nth_val N v2 y))%nat.
Lemma math_length_int_eq:
forall x3 (x1 : list msg ) N x2,
Int.unsigned x3 = Z.of_nat (length x1) ->
((length x1 + 1)%nat = S N) %nat ->
S N = ∘(Int.unsigned x2) ->
Int.eq (x3+ᵢ$ 1) x2 = true.
Lemma math_max_le_q:
forall x M,
x <= OS_MAX_Q_SIZE ->
(M < ∘(x))%nat ->
(S M <= ∘OS_MAX_Q_SIZE)%nat.
Lemma math_inc_eq_ltu:
forall x2 x3 (x1 : list msg),
Int.unsigned x2 <= OS_MAX_Q_SIZE ->
Int.ltu x3 x2 = true ->
Int.unsigned x3 = Z.of_nat (length x1) ->
Int.unsigned (x3+ᵢ$ 1) = Z.of_nat (length x1 + 1) .
Lemma math_int_eq_len:
forall x3 (x1:list msg) x2,
(0 < Int.unsigned x2) ->
Int.unsigned x3 = Z.of_nat (length x1) ->
length x1 = (∘(Int.unsigned x2) - 1)%nat ->
Int.eq (x3+ᵢ$ 1) x2 = true.
Lemma math_int_lt_eq_split:
forall x i0 M N x2,
Int.ltu x ($ 4) = false ->
Int.ltu i0 ($ 4) = false ->
Int.modu (x-ᵢ$ 4) ($ 4) = $ 0 ->
Int.modu (i0-ᵢ$ 4) ($ 4) = $ 0 ->
(∘M < ∘(Int.unsigned x2))%nat ->
(∘N < ∘(Int.unsigned x2))%nat ->
Int.unsigned x2 <= OS_MAX_Q_SIZE ->
M = Int.unsigned (Int.divu (x-ᵢ$ 4) ($ 4)) ->
N = Int.unsigned (Int.divu (i0-ᵢ$ 4) ($ 4)) ->
Int.unsigned (Int.divu ((x+ᵢ$ 4)-ᵢ$ 4) ($ 4)) > N ->
(∘(Int.unsigned (Int.divu ((x+ᵢ$ 4)-ᵢ$ 4) ($ 4))) = S (∘M))%nat /\
(M > N \/ M = N)/\((Z.to_nat ((Int.unsigned x - 4) / 4)) = ∘M)%nat
/\ (∘M < ∘OS_MAX_Q_SIZE /\∘M>= ∘N )%nat .
Lemma math_int_lt_eq_split´:
forall x i0 M N x2,
Int.ltu x ($ 4) = false ->
Int.ltu i0 ($ 4) = false ->
Int.modu (x-ᵢ$ 4) ($ 4) = $ 0 ->
Int.modu (i0-ᵢ$ 4) ($ 4) = $ 0 ->
(∘M < ∘(Int.unsigned x2))%nat ->
(∘N < ∘(Int.unsigned x2))%nat ->
Int.unsigned x2 <= OS_MAX_Q_SIZE ->
M = Int.unsigned (Int.divu (x-ᵢ$ 4) ($ 4)) ->
N = Int.unsigned (Int.divu (i0-ᵢ$ 4) ($ 4)) ->
Int.unsigned (Int.divu ((x+ᵢ$ 4)-ᵢ$ 4) ($ 4)) < N ->
(∘(Int.unsigned (Int.divu ((x+ᵢ$ 4)-ᵢ$ 4) ($ 4))) = S (∘M))%nat /\
(M < N)/\((Z.to_nat ((Int.unsigned x - 4) / 4)) = ∘M)%nat
/\ (∘N < ∘OS_MAX_Q_SIZE /\∘M< ∘N /\ (∘(Int.unsigned x2) <= ∘OS_MAX_Q_SIZE ))%nat .
Lemma math_int_lt_eq_split´´:
forall x i0 M N x2,
Int.ltu x ($ 4) = false ->
Int.ltu i0 ($ 4) = false ->
Int.modu (x-ᵢ$ 4) ($ 4) = $ 0 ->
Int.modu (i0-ᵢ$ 4) ($ 4) = $ 0 ->
(∘M < ∘(Int.unsigned x2))%nat ->
(∘N < ∘(Int.unsigned x2))%nat ->
Int.unsigned x2 <= OS_MAX_Q_SIZE ->
M = Int.unsigned (Int.divu (x-ᵢ$ 4) ($ 4)) ->
N = Int.unsigned (Int.divu (i0-ᵢ$ 4) ($ 4)) ->
Int.unsigned (Int.divu ((x+ᵢ$ 4)-ᵢ$ 4) ($ 4)) = N ->
(∘(Int.unsigned (Int.divu ((x+ᵢ$ 4)-ᵢ$ 4) ($ 4))) = S (∘M))%nat /\
(M + 1 = N /\ M < N)/\((Z.to_nat ((Int.unsigned x - 4) / 4)) = ∘M)%nat
/\ (∘N < ∘OS_MAX_Q_SIZE /\S ∘(M)= ∘N /\ (∘(Int.unsigned x2) <= ∘OS_MAX_Q_SIZE ))%nat .
Lemma math_ltu_false_false:
forall x x4,
0 < Int.unsigned x4 ->
Int.unsigned x4 <= OS_MAX_Q_SIZE ->
Int.ltu x ($ 4) = false ->
(∘(Int.unsigned (Int.divu (x-ᵢ$ 4) ($ 4))) < ∘(Int.unsigned x4))%nat ->
Int.modu (x-ᵢ$ 4) ($ 4) = $ 0 ->
Int.ltu (x+ᵢ$ 4) ($ 4) = false /\ Int.modu ((x+ᵢ$ 4)-ᵢ$ 4) ($ 4) = $ 0.
Lemma join_indom_r : forall ma mb mab x, TcbMod.join ma mb mab -> TcbMod.indom mb x ->TcbMod.indom mab x.
Lemma join_indom_or : forall ma mb mab x, TcbMod.join ma mb mab -> TcbMod.indom mab x -> TcbMod.indom ma x \/ TcbMod.indom mb x.
Lemma tcblist_p_indom_eq : forall v x y l1 l2, TCBList_P v x y l1 -> TCBList_P v x y l2 -> (forall a, TcbMod.indom l1 a <-> TcbMod.indom l2 a).
Lemma tcbmod_get_or : forall ma a, TcbMod.get ma a = None \/ exists b, TcbMod.get ma a = Some b.
Lemma indom_eq_join_eq: forall ma mb ma´ mb´ mab, (forall a, TcbMod.indom ma a <-> TcbMod.indom ma´ a) -> TcbMod.join ma mb mab -> TcbMod.join ma´ mb´ mab -> ma = ma´.
Lemma tcblist_p_sub_eq:
forall l l1 l2 l1´ l2´ v x y,
TcbMod.join l1 l2 l ->
TCBList_P v x y l1 ->
TcbMod.join l1´ l2´ l ->
TCBList_P v x y l1´->
l2 = l2´.
Lemma math_le_int16:
forall x0 (l:list msg) m,
Int.unsigned x0 = Z.of_nat (length l) ->
(length l < ∘(Int.unsigned m))%nat ->
Int.unsigned m <= OS_MAX_Q_SIZE ->
Int.unsigned (x0+ᵢ$ 1) <= Int16.max_unsigned.
Lemma math_MN_max_prop:
forall M N m,
M < N ->
(∘M < ∘(Int.unsigned m))%nat ->
(∘N < ∘(Int.unsigned m))%nat ->
Int.unsigned m <= OS_MAX_Q_SIZE ->
(∘M <= ∘OS_MAX_Q_SIZE)%nat /\
(∘N <= ∘(Int.unsigned m))%nat/\(∘(Int.unsigned m) <= ∘OS_MAX_Q_SIZE)%nat.
Lemma math_MN_le_int16:
forall M N m x0,
M > N ->
(∘M < ∘(Int.unsigned m))%nat ->
(∘N < ∘(Int.unsigned m))%nat ->
Int.unsigned m <= OS_MAX_Q_SIZE ->
Int.unsigned x0 = Z.of_nat (∘M - ∘N) ->
Int.unsigned (x0+ᵢ$ 1) <= Int16.max_unsigned .
Lemma math_MN_le_max:
forall M N m ,
M > N ->
(∘M < ∘(Int.unsigned m))%nat ->
(∘N < ∘(Int.unsigned m))%nat ->
Int.unsigned m <= OS_MAX_Q_SIZE ->
(∘N <= ∘M)%nat /\ (∘M <= ∘ OS_MAX_Q_SIZE )%nat/\(∘N <= ∘(Int.unsigned m))%nat .
Lemma isptr_list_tail_add:
forall x1 x0,
isptr_list x1 ->
isptr_list (x1 ++ Vptr x0 :: nil).
Lemma list_gt_0_ex:
forall v2 : list val,
(0 < length v2)%nat ->
exists x y, v2 = x :: y.
Lemma vallist_seg_upd_prop:
forall N M v2 x1 y,
(N < length v2)%nat ->
(N >= M)%nat ->
vallist_seg M N v2 = x1 ->
vallist_seg M (S N) (update_nth_val N v2 y ) = x1 ++ (y :: nil).
Lemma vallist_pre_size_eq:
forall size v2 x,
(size <= length v2)%nat ->
vallist_pre size v2 = x ->
(length x = size).
Lemma vallist_seg_length_prop:
forall x y v2 ls,
(x <= y)%nat ->
(y <= length v2)%nat ->
vallist_seg x y v2 = ls ->
(length ls = y - x)%nat.
Lemma vallist_seg_length :
forall N v2 x1 size,
(S N < size) %nat ->
(size <= length v2) %nat ->
vallist_seg (S N) size v2 ++ vallist_seg 0 N v2 = x1 ->
(length x1 = size -1)%nat.
Lemma vallist_seg_upd_SM:
forall M v2 y,
(S M <= length v2)%nat ->
vallist_seg M (S M) (update_nth_val M v2 y) = y::nil.
Lemma vallist_seg_upd_irr:
forall N M size v2 y,
(M < N)%nat ->
(N < size)%nat ->
(size <= length v2)%nat ->
vallist_seg N size v2 =
vallist_seg N size (update_nth_val M v2 y).
Lemma disj_star_elim´´ :
forall p q x y p´ q´ x´ y´ p´´ q´´ x´´ y´´ r z : asrt,
((p \\// q \\// x \\// y \\// p´ \\// q´ \\// x´ \\// y´ \\// p´´ \\// q´´ \\// x´´ \\// y´´) ** z) ** r ==>
p ** z ** r \\// q ** z ** r \\// x ** z ** r \\// y ** z ** r \\// p´ ** z ** r \\// q´ ** z ** r \\// x´ ** z ** r \\// y´ ** z ** r \\// p´´ ** z ** r \\// q´´ ** z ** r \\// x´´ ** z ** r \\// y´´ ** z ** r.