Library mcertikos.devdrivers.DSerialIntroCode_serial_putc
Require Import Coqlib.
Require Import Maps.
Require Import AST.
Require Import Integers.
Require Import Floats.
Require Import Values.
Require Import MemoryX.
Require Import EventsX.
Require Import Globalenvs.
Require Import Locations.
Require Import Smallstep.
Require Import ClightBigstep.
Require Import Cop.
Require Import ZArith.Zwf.
Require Import RealParams.
Require Import LoopProof.
Require Import VCGen.
Require Import liblayers.compcertx.Stencil.
Require Import liblayers.compcertx.MakeProgram.
Require Import liblayers.compat.CompatLayers.
Require Import liblayers.compat.CompatGenSem.
Require Import CompatClightSem.
Require Import PrimSemantics.
Require Import Clight.
Require Import CDataTypes.
Require Import Ctypes.
Require Import CLemmas.
Require Import FutureTactic.
Require Import AbstractDataType.
Require Import DSerialIntroCSource.
Require Import SerialGenSpec.
Require Import ObjSerialDriver.
Require Import ObjSerialDevice.
Require Import DSerialIntro.
Require Import INVLemmaDevice.
Require Import TacticsForTesting.
Require Import OracleInstances.
Import DeviceStateDataType.
Lemma serial_calc_com1_base:
∀ d,
high_level_invariant d →
Base (s (com1 d)) = 1016.
Proof.
intros d Hinv.
generalize (valid_com1_port d); intros Hport; apply Hport in Hinv.
rewrite Hinv. reflexivity.
Qed.
Module DSERIALINTROCODE.
Section WithPrimitives.
Context `{real_params: RealParams}.
Context `{oracle_prop: MultiOracleProp}.
Context {memb} `{Hmemx: Mem.MemoryModelX memb}.
Context `{Hmwd: UseMemWithData memb}.
Let mem := mwd (cdata RData).
Context `{Hstencil: Stencil}.
Context `{make_program_ops: !MakeProgramOps Clight.function type Clight.fundef type}.
Context `{Hmake_program: !MakeProgram Clight.function type Clight.fundef type}.
Local Open Scope Z_scope.
Ltac serial_unfold_refl :=
unfold_SerialState; unfold_DeviceData; unfold update_com1; simpl;
try (rewrite Int.unsigned_repr; [reflexivity | omega]).
Ltac serial_unfold_simpl :=
unfold_SerialState; unfold_DeviceData; unfold update_com1, update_drv_serial; simpl;
rewrite Int.unsigned_repr; simpl.
Ltac solve_serial_in :=
unfold serial_in_spec; simpl;
rewrite Int.unsigned_repr; [reflexivity | omega].
Ltac intro_env_instances lrx str H :=
generalize (OracleInvariants.serial_recv_limit lrx str H);
intros [Hstrnnil [Hstrlen [Hstrchar Hevent]]];
generalize (non_nil_list Hstrnnil); intros (h & tlstr & Hstr); subst;
generalize (forall_hd Hstrchar); intros Hstrhd; subst; unfold isChar in Hstrhd;
generalize (forall_tl Hstrchar); intros Hstrtl; subst.
Section SERIALPUTC.
Let L: compatlayer (cdata RData) :=
get_serial_exists ↦ gensem get_serial_exists_spec
⊕ serial_in ↦ gensem serial_in_spec
⊕ serial_out ↦ gensem serial_out_spec.
Local Instance: ExternalCallsOps mem := CompatExternalCalls.compatlayer_extcall_ops L.
Local Instance: CompilerConfigOps mem := CompatExternalCalls.compatlayer_compiler_config_ops L.
Local Open Scope Z_scope.
Section SerialPutcBody.
Context `{Hwb: WritableBlockOps}.
Variable (sc: stencil).
Variables (ge: genv)
(STENCIL_MATCHES: stencil_matches sc ge).
Variable (bget_serial_exists: block).
Hypothesis hget_serial_exists1 : Genv.find_symbol ge get_serial_exists = Some bget_serial_exists.
Hypothesis hget_serial_exists2 : Genv.find_funct_ptr ge bget_serial_exists =
Some (External (EF_external get_serial_exists
(signature_of_type Tnil tuint cc_default))
Tnil tuint cc_default).
Variable bserial_in: block.
Hypothesis hserial_in1: Genv.find_symbol ge serial_in = Some bserial_in.
Hypothesis hserial_in2: Genv.find_funct_ptr ge bserial_in =
Some (External (EF_external serial_in
(signature_of_type (Tcons tuint (Tcons tuint Tnil)) tuint cc_default))
(Tcons tuint (Tcons tuint Tnil)) tuint cc_default).
Variable bserial_out: block.
Hypothesis hserial_out1: Genv.find_symbol ge serial_out = Some bserial_out.
Hypothesis hserial_out2: Genv.find_funct_ptr ge bserial_out =
Some (External (EF_external serial_out
(signature_of_type (Tcons tuint (Tcons tuint Tnil)) tvoid cc_default))
(Tcons tuint (Tcons tuint Tnil)) tvoid cc_default).
Section serial_putc_loop_proof.
Variable m_init: memb.
Variable abd: RData.
Variable t: Z.
Variable h : Z.
Variable tl: list Z.
Variable c: int.
Hypothesis Htrange: 0 ≤ t < 12800.
Hypothesis Htevent: SerialEnv (l2 (com1 abd) + t) = SerialSendComplete.
Hypothesis Htinv: ∀ n, 0 ≤ n < t →
SerialEnv (l2 (com1 abd) + n) = NullEvent.
Hypothesis Hinv: high_level_invariant abd.
Hypothesis Hon: SerialOn (s (com1 abd)) = true.
Hypothesis Hrx: RxBuf (s (com1 abd)) = nil.
Hypothesis Htx: TxBuf (s (com1 abd)) = h :: tl.
Function serial_putc_loop_body_P (le: temp_env) (m: mem): Prop :=
le ! _lsr = Some (Vint (Int.repr 0)) ∧
le ! _i = Some (Vint Int.zero) ∧
le ! _c = Some (Vint c) ∧
0 ≤ t ∧
m = (m_init, abd).
Definition d_end :=
(abd {com1 / l2: (l2 (com1 abd)) + t + 1}
{com1 / s / TxBuf: nil}).
Function d_mid (i: Z) := (abd {com1 / l2: (l2 (com1 abd)) + i}).
Function serial_putc_loop_body_Q (le : temp_env) (m: mem): Prop :=
le ! _i = Some (Vint (Int.repr (t + 1))) ∧
le ! _lsr = Some (Vint (Int.repr 1)) ∧
le ! _c = Some (Vint c) ∧
m = (m_init, d_end).
Lemma Zlt_le_trans:
∀ n m p,
n < m → m ≤ p → n < p.
Proof.
intros n m p Hnm Hmp.
omega.
Qed.
Lemma serial_putc_loop_correct_aux:
LoopProofSimpleWhile.t
serial_putc_loop_condition
serial_putc_loop_body
ge (PTree.empty _)
serial_putc_loop_body_P
serial_putc_loop_body_Q.
Proof.
generalize max_unsigned_val; intro muval.
apply LoopProofSimpleWhile.make with
(W := Z)
(lt := fun z1 z2 ⇒ (0 ≤ z2 ∧ z1 < z2)%Z)
(I := fun le m w ⇒ ∃ i,
le ! _i = Some (Vint (Int.repr i)) ∧
le ! _c = Some (Vint c) ∧
w = t - i ∧
((
0 ≤ i ≤ t ∧
m = (m_init, abd {com1 / l2: (l2 (com1 abd)) + i}) ∧
le ! _lsr = Some (Vint (Int.repr 0))
) ∨ (
i = t + 1 ∧
m = (m_init, d_end) ∧
le ! _lsr = Some (Vint (Int.repr 1))
))
).
apply Zwf_well_founded.
intros le m Hp.
destruct Hp as (Hp1 & Hp2 & Hpc & Hp3 & Hp4).
∃ t, 0.
rewrite Hp4. rewrite Z.add_0_r; unfold update_com1, update_l2; simpl.
destruct abd; destruct com1; subst; simpl.
repeat constructor; discharge_cmp.
intros le m w Hi.
destruct Hi as (i & Hlei & Hlec & Hiw & Hit).
destruct Hit as [Hilt | Hit].
Case "i <= t, in loop".
{
destruct Hilt as (Hirange & Him & Hle).
rewrite Him.
assert (casei: 0 ≤ i < t ∨ i = t) by omega.
Caseeq casei.
{
intros Hirange´.
generalize (Htinv i Hirange´); intros Horacle.
destruct abd; destruct com1; destruct s eqn: s_eq; simpl in *; subst.
unfold update_com1, update_l2; simpl.
esplit. esplit.
split; [|split; [| split]].
- SCase "loop condition".
unfold serial_putc_loop_condition.
repeat vcgen.
- SCase "bool val".
repeat vcgen.
- SCase "out case".
inversion 1.
- intros H; clear H.
esplit. esplit.
split.
+ SCase "loop body".
unfold serial_putc_loop_body.
repeat vcgen.
unfold serial_in_spec; rewrite serial_calc_com1_base; simpl.
rewrite Horacle; simpl.
serial_unfold_refl.
inversion Hinv; econstructor; eauto.
+ SCase "loop invariants holds".
∃ (t - i - 1).
split. split; omega.
∃ (i + 1).
split. repeat vcgen.
split. repeat vcgen.
split. omega.
left.
split. omega.
split. rewrite Z.add_assoc. reflexivity.
repeat vcgen.
}
{
intros Hirange´.
unfold serial_putc_loop_body_Q, d_end.
subst. destruct abd; destruct com1; destruct s eqn: s_eq; simpl in *; subst.
unfold update_com1; simpl; unfold_DeviceData; unfold_SerialState.
esplit. esplit.
split; [|split; [| split]].
- SCase "loop condition".
unfold serial_putc_loop_condition.
repeat vcgen.
- SCase "bool val".
repeat vcgen.
- SCase "out case".
inversion 1.
- intros H; clear H.
esplit. esplit.
split.
+ SCase "loop body".
unfold serial_putc_loop_body.
repeat vcgen.
unfold serial_in_spec; rewrite serial_calc_com1_base; simpl.
rewrite Htevent; simpl.
unfold update_com1; simpl; unfold_DeviceData; unfold_SerialState.
rewrite Int.unsigned_repr; [reflexivity | omega].
inversion Hinv; econstructor; eauto.
+ SCase "loop invariants hold".
∃ (-1).
split. split; omega.
∃ (t + 1).
split. repeat vcgen.
split. repeat vcgen.
split. rewrite Z.sub_add_distr. omega.
right.
split. trivial.
split. reflexivity.
repeat vcgen.
}
}
Case "i = t + 1, out".
{
destruct Hit as (Hirange & Him & Hlsr).
rewrite Him.
unfold serial_putc_loop_body_Q, d_end.
subst. destruct abd; destruct com1; destruct s eqn: s_eq; simpl in *; subst.
unfold update_com1; simpl; unfold_DeviceData; unfold_SerialState.
esplit. esplit.
split; [|split; [| split]].
- SCase "loop condition".
unfold serial_putc_loop_condition.
repeat vcgen.
- SCase "bool val".
repeat vcgen.
- SCase "out case".
intros H; clear H.
split. repeat vcgen.
split. repeat vcgen.
split. repeat vcgen.
reflexivity.
- SCase "loop invariants holds".
inversion 1.
}
Qed.
End serial_putc_loop_proof.
Lemma serial_putc_loop_correct:
∀ m d le t h tl c,
0 ≤ t < 12800 →
SerialEnv ((l2 (com1 d)) + t) = SerialSendComplete →
(∀ n, 0 ≤ n < t → SerialEnv ((l2 (com1 d)) + n) = NullEvent) →
high_level_invariant d →
SerialOn (s (com1 d)) = true →
RxBuf (s (com1 d)) = nil →
TxBuf (s (com1 d)) = h :: tl →
le ! _lsr = Some (Vint (Int.repr 0)) →
le ! _i = Some (Vint Int.zero) →
le ! _c = Some (Vint c) →
∃ le´, exec_stmt ge (PTree.empty _) le ((m, d): mem)
(Swhile serial_putc_loop_condition serial_putc_loop_body)
E0 le´ (m, (d_end d t)) Out_normal ∧
le´ ! _i = Some (Vint (Int.repr (t + 1))) ∧
le´ ! _lsr = Some (Vint (Int.repr 1)) ∧
le´ ! _c = Some (Vint c).
Proof.
intros m d le t h tl c Htrange Hevent Hnop Hinv Hon Hrx Htx Hlelsr Hlei Hlec.
generalize (serial_putc_loop_correct_aux m d t h tl c Htrange Hevent Hnop Hinv Hon Hrx Htx).
unfold serial_putc_loop_body_P, serial_putc_loop_body_Q.
intro Hlp.
refine (_ (LoopProofSimpleWhile.termination _ _ _ _ _ _ Hlp le (m, d) _)).
intro pre.
destruct pre as (le´ & m´ & Hexec & Hle´i & Hle´lsr & Hle´c & Hd_end).
∃ le´. subst.
split. assumption.
repeat split; try assumption.
repeat split; try assumption.
omega.
Qed.
Lemma div_mod2_eq1:
∀ n, n ≠ 0 → (n / n) mod 2 = 1.
Proof.
intros n Hneq.
rewrite Z.div_same. rewrite Z.mod_small; omega. assumption.
Qed.
Lemma div32_mod2_eq1:
(32 / 32) mod 2 = 1.
Proof.
apply div_mod2_eq1; omega.
Qed.
Lemma div_mod2_eq0:
∀ n m, 0 ≤ n < m →
(n / m) mod 2 = 0.
Proof.
intros n m H.
rewrite Z.div_small. rewrite Z.mod_small; omega.
assumption.
Qed.
Lemma div32_mod2_eq0:
(0 / 32) mod 2 = 0.
Proof.
apply div_mod2_eq0 with (n:=0) (m:=32).
omega.
Qed.
Lemma attach_some:
∀ A (a b: A),
a = b →
Some a = Some b.
Proof.
intros.
rewrite H. reflexivity.
Qed.
Lemma detach_some:
∀ A (a b: A),
Some a = Some b →
a = b.
Proof.
intros. inversion H. trivial.
Qed.
Tactic Notation "extract_abd" "act" tactic(t) :=
match goal with
| [|-ClightBigstep.exec_stmt _ _ _ _ (_, ?d) _ _ _ _ _] ⇒ t d
| _ ⇒ fail "cannot find abd in the current goal."
end.
Tactic Notation "extract_le" "act" tactic(t) :=
match goal with
| [|-ClightBigstep.exec_stmt _ _ _ ?le (_, _) _ _ _ _ _] ⇒ t le
| _ ⇒ fail "cannot find le in the current goal"
end.
Lemma serial_putc_body_correct:
∀ m c d d´ env le,
env = PTree.empty _ →
PTree.get _c le = Some (Vint c) →
high_level_invariant d →
serial_putc_spec (Int.unsigned c) d = Some d´ →
∃ le´,
exec_stmt ge env le ((m, d): mem) serial_putc_body E0 le´ (m, d´)
Out_normal.
Proof.
generalize max_unsigned_val; intro muval.
intros m c d d´ env le Henv Hcle Hinv Hspec.
generalize (serial_calc_com1_base d Hinv); intro Hcom1Base.
generalize (OracleInvariants.serial_send_complete_bound d); intro Heit.
functional inversion Hspec; subst; clear H3;
try (destruct d; destruct com1, drv_serial; destruct s eqn: s_eq; simpl in *; subst;
simpl in *; unfold update_com1; unfold_DeviceData; unfold_SerialState; subst
); clear Hspec.
- Case "serial_exists = true, txbuf = nil, c = '\r'".
inversion H4; subst.
esplit.
unfold serial_putc_body.
repeat vcgen.
rewrite Int.unsigned_repr; [reflexivity | omega].
discharge_cmp.
repeat vcgen.
unfold serial_in_spec; simpl.
destruct (SerialEnv ltx); serial_unfold_refl.
calc. discharge_cmp.
omega. omega. calc; omega. omega. omega. calc; omega. omega.
omega.
discharge_cmp.
repeat vcgen.
calc; omega.
ptreesolve.
discharge_cmp.
discharge_cmp.
discharge_cmp.
repeat vcgen.
- Case "serial_exists = true, txbuf = nil, c <> '\r'".
inversion H4; subst.
esplit.
unfold serial_putc_body.
repeat vcgen.
rewrite Int.unsigned_repr; [reflexivity | omega].
discharge_cmp.
repeat vcgen.
unfold serial_in_spec; simpl.
destruct (SerialEnv ltx); serial_unfold_refl.
calc. discharge_cmp.
omega. omega. calc; omega. omega. omega. calc; omega. omega.
omega.
discharge_cmp.
repeat vcgen.
calc; omega.
ptreesolve.
discharge_cmp.
discharge_cmp.
discharge_cmp.
repeat vcgen.
- Case "serial_exists = true, txbuf = c :: tl, c = '\r'".
destruct _x11 as [| z tl] eqn: Hx11. inversion H6.
inversion H4; subst.
assert (Heit´: z :: tl ≠ nil) by inversion 1.
apply Heit in Heit´. destruct Heit´ as (t & Htrange & Horacle & Hevent).
assert (caseevent: t = 0 ∨ 0 < t < 12800) by omega.
Caseeq (caseevent).
+ SCase "SerialSendComplete immediately".
intros Ht. subst. rewrite Z.add_0_r in Hevent.
esplit.
unfold serial_putc_body.
repeat vcgen.
unfold get_serial_exists_spec; simpl. rewrite Int.unsigned_repr. reflexivity.
omega.
discharge_cmp. repeat vcgen.
unfold serial_in_spec; rewrite serial_calc_com1_base; simpl.
rewrite Hevent; simpl.
serial_unfold_refl.
inversion Hinv; econstructor; eauto.
calc. discharge_cmp.
omega. omega. calc; omega. omega. omega. calc; omega. omega. omega.
discharge_cmp.
repeat vcgen. calc. omega. calc. ptreesolve. reflexivity.
discharge_cmp.
discharge_cmp.
× SSCase "the sending part".
repeat vcgen. unfold serial_out_spec; simpl.
unfold update_com1; simpl; unfold_DeviceData; unfold_SerialState.
unfold ret; simpl. repeat f_equal.
rewrite next_sendcomplete_eq_t with (t´ := 0). omega.
omega. rewrite Z.add_0_r. assumption. assumption.
+ SCase "not send at ts".
intros Htrange´.
generalize (next_sendcomplete_eq_t ltx t Htrange Hevent Horacle); intros Hts.
exec_pre_abd dpre.
set (Hd := dpre {com1 / l2: ltx + 1}).
set (Hle := (PTree.set _i (Vint Int.zero)
(PTree.set _lsr (Vint Int.zero)
(PTree.set 41 (Vint Int.zero) (PTree.set 44 (Vint Int.one) le))))).
exploit (serial_putc_loop_correct m Hd Hle (t - 1) z tl c);
simpl; try auto; try omega; try discharge_cmp.
× calc. simpl. assumption.
× intros. generalize (Horacle (n + 1)). calc. intros Ho.
assert (Har: ltx + 1 + n = ltx + n + 1) by omega.
rewrite Har. rewrite Ho. reflexivity. omega.
× econstructor; inversion Hinv; eauto.
× unfold Hle. ptreesolve.
× unfold Hle. ptreesolve.
× unfold Hle. ptreesolve.
× intros Hloop.
destruct Hloop as (le_after_loop & Hloopexec & Hle´i & Hle´lsr & Hle´c).
esplit.
unfold serial_putc_body.
repeat vcgen.
rewrite Int.unsigned_repr; [reflexivity | omega].
assert (Hevent0: 0 ≤ 0 < t) by omega.
generalize (Horacle 0). rewrite Z.add_0_r. intros Horacle0.
discharge_cmp. repeat vcgen.
unfold serial_in_spec; subst; simpl.
rewrite Horacle0.
serial_unfold_refl.
omega. calc. discharge_cmp. omega. omega. calc; reflexivity. omega.
omega. calc; omega. omega. omega.
discharge_cmp.
d2 vcgen. calc. discharge_cmp. repeat vcgen.
{ SSCase "loop proof".
eapply Hloopexec.
}
calc. omega.
eassumption.
repeat vcgen.
repeat vcgen.
{ SSCase "after loop".
discharge_cmp. repeat vcgen.
unfold d_end, Hd; unfold update_com1; unfold_DeviceData; unfold_SerialState.
replace (ltx + 1 + (t - 1) + 1) with (ltx + t + 1) by omega.
unfold serial_out_spec; simpl.
serial_unfold_refl. rewrite Hts.
reflexivity.
}
- Case "serial_exists = true, txbuf = c :: tl, c <> '\r'".
destruct _x11 as [| z tl] eqn: Hx11. inversion H6.
inversion H4; subst; simpl in ×. clear H4.
assert (Heit´: z :: tl ≠ nil) by inversion 1.
apply Heit in Heit´. destruct Heit´ as (t & Htrange & Horacle & Hevent).
assert (caseevent: t = 0 ∨ 0 < t < 12800) by omega.
Caseeq (caseevent).
+ SCase "SerialSendComplete immediately".
intros Ht. subst. rewrite Z.add_0_r in Hevent.
esplit.
unfold serial_putc_body.
repeat vcgen.
rewrite Int.unsigned_repr; [reflexivity | omega].
discharge_cmp. repeat vcgen.
unfold serial_in_spec; rewrite serial_calc_com1_base; simpl.
rewrite Hevent; simpl.
serial_unfold_refl.
inversion Hinv; econstructor; eauto.
calc. discharge_cmp.
omega. omega. calc; omega. omega. omega. calc; omega.
omega. omega.
discharge_cmp.
repeat vcgen.
calc. omega.
ptreesolve.
discharge_cmp.
discharge_cmp.
discharge_cmp.
× SSCase "the sending part".
repeat vcgen.
unfold serial_out_spec; simpl.
serial_unfold_refl.
rewrite next_sendcomplete_eq_t with (t´ := 0). calc.
replace (1 + ltx) with (ltx + 1) by omega.
reflexivity.
omega.
rewrite Z.add_0_r. assumption.
intros. rewrite (Horacle n0). reflexivity. omega.
+ SCase "not send at ts".
intros Htrange´.
generalize (next_sendcomplete_eq_t ltx t Htrange Hevent Horacle); intros Hts.
exec_pre_abd dpre.
set (Hd := dpre {com1 / l2: ltx + 1}).
set (Hle := (PTree.set _i (Vint Int.zero)
(PTree.set _lsr (Vint Int.zero)
(PTree.set 41 (Vint Int.zero) (PTree.set 44 (Vint Int.one) le))))).
exploit (serial_putc_loop_correct m Hd Hle (t - 1) z tl c);
simpl; try auto; try omega; try discharge_cmp.
replace (ltx + 1 + (t - 1)) with (ltx + t) by omega. assumption.
intros n0 Hnrange. generalize (Horacle (n0 + 1)). intros Hn0oracle.
replace (ltx + (n0 + 1)) with (ltx + 1 + n0) in Hn0oracle by omega.
rewrite Hn0oracle. reflexivity. omega.
inversion Hinv; econstructor; eauto.
unfold Hle. ptreesolve.
unfold Hle. ptreesolve.
unfold Hle. ptreesolve.
intros Hloop.
destruct Hloop as (le_after_loop & Hloopexec & Hle´i & Hle´lsr & Hle´c).
esplit.
unfold serial_putc_body.
repeat vcgen.
rewrite Int.unsigned_repr; [reflexivity | omega].
discharge_cmp. repeat vcgen.
generalize (Horacle 0); intro Horacle0.
assert (Hevent0: 0 ≤ 0 < t) by omega.
apply Horacle0 in Hevent0. clear Horacle0. rewrite Z.add_0_r in Hevent0.
unfold serial_in_spec; rewrite serial_calc_com1_base; simpl.
rewrite Hevent0.
serial_unfold_refl.
inversion Hinv; econstructor; eauto.
calc. simpl. discharge_cmp.
omega. omega. calc; omega. omega. omega. calc; omega. omega.
omega.
d2 vcgen. repeat vcgen.
× SSCase "loop proof".
eapply Hloopexec.
× eassumption.
× repeat vcgen.
× repeat vcgen.
× SSCase "after loop".
discharge_cmp. repeat vcgen.
unfold serial_out_spec; simpl.
unfold d_end, Hd; unfold update_com1; simpl; unfold_DeviceData; unfold_SerialState.
replace (ltx + 1 + (t - 1) + 1) with (ltx + t + 1) by omega.
rewrite Hts.
reflexivity.
- Case "serial_exists = false".
esplit. unfold serial_putc_body.
repeat vcgen. unfold get_serial_exists_spec.
rewrite H0, H1, H2.
inversion Hinv. destruct valid_serial_exists.
rewrite H. rewrite Int.unsigned_repr; [reflexivity | omega].
rewrite H in _x. contradiction _x. reflexivity.
discharge_cmp. repeat vcgen.
Qed.
End SerialPutcBody.
Theorem serial_putc_code_correct:
spec_le
(serial_putc ↦ serial_putc_spec_low)
(〚serial_putc ↦ f_serial_putc 〛L).
Proof.
set (L´ := L) in ×. unfold L in ×.
fbigstep_pre L´.
fbigstep
(serial_putc_body_correct
s
(Genv.globalenv p)
makeglobalenv b0 Hb0fs Hb0fp b1 Hb1fs Hb1fp b2 Hb2fs Hb2fp m´0 c labd labd´ (PTree.empty _)
(bind_parameter_temps´ (fn_params f_serial_putc) (Vint c :: nil)
(create_undef_temps (fn_temps f_serial_putc))
)
) H0.
Qed.
End SERIALPUTC.
End WithPrimitives.
End DSERIALINTROCODE.
Require Import Maps.
Require Import AST.
Require Import Integers.
Require Import Floats.
Require Import Values.
Require Import MemoryX.
Require Import EventsX.
Require Import Globalenvs.
Require Import Locations.
Require Import Smallstep.
Require Import ClightBigstep.
Require Import Cop.
Require Import ZArith.Zwf.
Require Import RealParams.
Require Import LoopProof.
Require Import VCGen.
Require Import liblayers.compcertx.Stencil.
Require Import liblayers.compcertx.MakeProgram.
Require Import liblayers.compat.CompatLayers.
Require Import liblayers.compat.CompatGenSem.
Require Import CompatClightSem.
Require Import PrimSemantics.
Require Import Clight.
Require Import CDataTypes.
Require Import Ctypes.
Require Import CLemmas.
Require Import FutureTactic.
Require Import AbstractDataType.
Require Import DSerialIntroCSource.
Require Import SerialGenSpec.
Require Import ObjSerialDriver.
Require Import ObjSerialDevice.
Require Import DSerialIntro.
Require Import INVLemmaDevice.
Require Import TacticsForTesting.
Require Import OracleInstances.
Import DeviceStateDataType.
Lemma serial_calc_com1_base:
∀ d,
high_level_invariant d →
Base (s (com1 d)) = 1016.
Proof.
intros d Hinv.
generalize (valid_com1_port d); intros Hport; apply Hport in Hinv.
rewrite Hinv. reflexivity.
Qed.
Module DSERIALINTROCODE.
Section WithPrimitives.
Context `{real_params: RealParams}.
Context `{oracle_prop: MultiOracleProp}.
Context {memb} `{Hmemx: Mem.MemoryModelX memb}.
Context `{Hmwd: UseMemWithData memb}.
Let mem := mwd (cdata RData).
Context `{Hstencil: Stencil}.
Context `{make_program_ops: !MakeProgramOps Clight.function type Clight.fundef type}.
Context `{Hmake_program: !MakeProgram Clight.function type Clight.fundef type}.
Local Open Scope Z_scope.
Ltac serial_unfold_refl :=
unfold_SerialState; unfold_DeviceData; unfold update_com1; simpl;
try (rewrite Int.unsigned_repr; [reflexivity | omega]).
Ltac serial_unfold_simpl :=
unfold_SerialState; unfold_DeviceData; unfold update_com1, update_drv_serial; simpl;
rewrite Int.unsigned_repr; simpl.
Ltac solve_serial_in :=
unfold serial_in_spec; simpl;
rewrite Int.unsigned_repr; [reflexivity | omega].
Ltac intro_env_instances lrx str H :=
generalize (OracleInvariants.serial_recv_limit lrx str H);
intros [Hstrnnil [Hstrlen [Hstrchar Hevent]]];
generalize (non_nil_list Hstrnnil); intros (h & tlstr & Hstr); subst;
generalize (forall_hd Hstrchar); intros Hstrhd; subst; unfold isChar in Hstrhd;
generalize (forall_tl Hstrchar); intros Hstrtl; subst.
Section SERIALPUTC.
Let L: compatlayer (cdata RData) :=
get_serial_exists ↦ gensem get_serial_exists_spec
⊕ serial_in ↦ gensem serial_in_spec
⊕ serial_out ↦ gensem serial_out_spec.
Local Instance: ExternalCallsOps mem := CompatExternalCalls.compatlayer_extcall_ops L.
Local Instance: CompilerConfigOps mem := CompatExternalCalls.compatlayer_compiler_config_ops L.
Local Open Scope Z_scope.
Section SerialPutcBody.
Context `{Hwb: WritableBlockOps}.
Variable (sc: stencil).
Variables (ge: genv)
(STENCIL_MATCHES: stencil_matches sc ge).
Variable (bget_serial_exists: block).
Hypothesis hget_serial_exists1 : Genv.find_symbol ge get_serial_exists = Some bget_serial_exists.
Hypothesis hget_serial_exists2 : Genv.find_funct_ptr ge bget_serial_exists =
Some (External (EF_external get_serial_exists
(signature_of_type Tnil tuint cc_default))
Tnil tuint cc_default).
Variable bserial_in: block.
Hypothesis hserial_in1: Genv.find_symbol ge serial_in = Some bserial_in.
Hypothesis hserial_in2: Genv.find_funct_ptr ge bserial_in =
Some (External (EF_external serial_in
(signature_of_type (Tcons tuint (Tcons tuint Tnil)) tuint cc_default))
(Tcons tuint (Tcons tuint Tnil)) tuint cc_default).
Variable bserial_out: block.
Hypothesis hserial_out1: Genv.find_symbol ge serial_out = Some bserial_out.
Hypothesis hserial_out2: Genv.find_funct_ptr ge bserial_out =
Some (External (EF_external serial_out
(signature_of_type (Tcons tuint (Tcons tuint Tnil)) tvoid cc_default))
(Tcons tuint (Tcons tuint Tnil)) tvoid cc_default).
Section serial_putc_loop_proof.
Variable m_init: memb.
Variable abd: RData.
Variable t: Z.
Variable h : Z.
Variable tl: list Z.
Variable c: int.
Hypothesis Htrange: 0 ≤ t < 12800.
Hypothesis Htevent: SerialEnv (l2 (com1 abd) + t) = SerialSendComplete.
Hypothesis Htinv: ∀ n, 0 ≤ n < t →
SerialEnv (l2 (com1 abd) + n) = NullEvent.
Hypothesis Hinv: high_level_invariant abd.
Hypothesis Hon: SerialOn (s (com1 abd)) = true.
Hypothesis Hrx: RxBuf (s (com1 abd)) = nil.
Hypothesis Htx: TxBuf (s (com1 abd)) = h :: tl.
Function serial_putc_loop_body_P (le: temp_env) (m: mem): Prop :=
le ! _lsr = Some (Vint (Int.repr 0)) ∧
le ! _i = Some (Vint Int.zero) ∧
le ! _c = Some (Vint c) ∧
0 ≤ t ∧
m = (m_init, abd).
Definition d_end :=
(abd {com1 / l2: (l2 (com1 abd)) + t + 1}
{com1 / s / TxBuf: nil}).
Function d_mid (i: Z) := (abd {com1 / l2: (l2 (com1 abd)) + i}).
Function serial_putc_loop_body_Q (le : temp_env) (m: mem): Prop :=
le ! _i = Some (Vint (Int.repr (t + 1))) ∧
le ! _lsr = Some (Vint (Int.repr 1)) ∧
le ! _c = Some (Vint c) ∧
m = (m_init, d_end).
Lemma Zlt_le_trans:
∀ n m p,
n < m → m ≤ p → n < p.
Proof.
intros n m p Hnm Hmp.
omega.
Qed.
Lemma serial_putc_loop_correct_aux:
LoopProofSimpleWhile.t
serial_putc_loop_condition
serial_putc_loop_body
ge (PTree.empty _)
serial_putc_loop_body_P
serial_putc_loop_body_Q.
Proof.
generalize max_unsigned_val; intro muval.
apply LoopProofSimpleWhile.make with
(W := Z)
(lt := fun z1 z2 ⇒ (0 ≤ z2 ∧ z1 < z2)%Z)
(I := fun le m w ⇒ ∃ i,
le ! _i = Some (Vint (Int.repr i)) ∧
le ! _c = Some (Vint c) ∧
w = t - i ∧
((
0 ≤ i ≤ t ∧
m = (m_init, abd {com1 / l2: (l2 (com1 abd)) + i}) ∧
le ! _lsr = Some (Vint (Int.repr 0))
) ∨ (
i = t + 1 ∧
m = (m_init, d_end) ∧
le ! _lsr = Some (Vint (Int.repr 1))
))
).
apply Zwf_well_founded.
intros le m Hp.
destruct Hp as (Hp1 & Hp2 & Hpc & Hp3 & Hp4).
∃ t, 0.
rewrite Hp4. rewrite Z.add_0_r; unfold update_com1, update_l2; simpl.
destruct abd; destruct com1; subst; simpl.
repeat constructor; discharge_cmp.
intros le m w Hi.
destruct Hi as (i & Hlei & Hlec & Hiw & Hit).
destruct Hit as [Hilt | Hit].
Case "i <= t, in loop".
{
destruct Hilt as (Hirange & Him & Hle).
rewrite Him.
assert (casei: 0 ≤ i < t ∨ i = t) by omega.
Caseeq casei.
{
intros Hirange´.
generalize (Htinv i Hirange´); intros Horacle.
destruct abd; destruct com1; destruct s eqn: s_eq; simpl in *; subst.
unfold update_com1, update_l2; simpl.
esplit. esplit.
split; [|split; [| split]].
- SCase "loop condition".
unfold serial_putc_loop_condition.
repeat vcgen.
- SCase "bool val".
repeat vcgen.
- SCase "out case".
inversion 1.
- intros H; clear H.
esplit. esplit.
split.
+ SCase "loop body".
unfold serial_putc_loop_body.
repeat vcgen.
unfold serial_in_spec; rewrite serial_calc_com1_base; simpl.
rewrite Horacle; simpl.
serial_unfold_refl.
inversion Hinv; econstructor; eauto.
+ SCase "loop invariants holds".
∃ (t - i - 1).
split. split; omega.
∃ (i + 1).
split. repeat vcgen.
split. repeat vcgen.
split. omega.
left.
split. omega.
split. rewrite Z.add_assoc. reflexivity.
repeat vcgen.
}
{
intros Hirange´.
unfold serial_putc_loop_body_Q, d_end.
subst. destruct abd; destruct com1; destruct s eqn: s_eq; simpl in *; subst.
unfold update_com1; simpl; unfold_DeviceData; unfold_SerialState.
esplit. esplit.
split; [|split; [| split]].
- SCase "loop condition".
unfold serial_putc_loop_condition.
repeat vcgen.
- SCase "bool val".
repeat vcgen.
- SCase "out case".
inversion 1.
- intros H; clear H.
esplit. esplit.
split.
+ SCase "loop body".
unfold serial_putc_loop_body.
repeat vcgen.
unfold serial_in_spec; rewrite serial_calc_com1_base; simpl.
rewrite Htevent; simpl.
unfold update_com1; simpl; unfold_DeviceData; unfold_SerialState.
rewrite Int.unsigned_repr; [reflexivity | omega].
inversion Hinv; econstructor; eauto.
+ SCase "loop invariants hold".
∃ (-1).
split. split; omega.
∃ (t + 1).
split. repeat vcgen.
split. repeat vcgen.
split. rewrite Z.sub_add_distr. omega.
right.
split. trivial.
split. reflexivity.
repeat vcgen.
}
}
Case "i = t + 1, out".
{
destruct Hit as (Hirange & Him & Hlsr).
rewrite Him.
unfold serial_putc_loop_body_Q, d_end.
subst. destruct abd; destruct com1; destruct s eqn: s_eq; simpl in *; subst.
unfold update_com1; simpl; unfold_DeviceData; unfold_SerialState.
esplit. esplit.
split; [|split; [| split]].
- SCase "loop condition".
unfold serial_putc_loop_condition.
repeat vcgen.
- SCase "bool val".
repeat vcgen.
- SCase "out case".
intros H; clear H.
split. repeat vcgen.
split. repeat vcgen.
split. repeat vcgen.
reflexivity.
- SCase "loop invariants holds".
inversion 1.
}
Qed.
End serial_putc_loop_proof.
Lemma serial_putc_loop_correct:
∀ m d le t h tl c,
0 ≤ t < 12800 →
SerialEnv ((l2 (com1 d)) + t) = SerialSendComplete →
(∀ n, 0 ≤ n < t → SerialEnv ((l2 (com1 d)) + n) = NullEvent) →
high_level_invariant d →
SerialOn (s (com1 d)) = true →
RxBuf (s (com1 d)) = nil →
TxBuf (s (com1 d)) = h :: tl →
le ! _lsr = Some (Vint (Int.repr 0)) →
le ! _i = Some (Vint Int.zero) →
le ! _c = Some (Vint c) →
∃ le´, exec_stmt ge (PTree.empty _) le ((m, d): mem)
(Swhile serial_putc_loop_condition serial_putc_loop_body)
E0 le´ (m, (d_end d t)) Out_normal ∧
le´ ! _i = Some (Vint (Int.repr (t + 1))) ∧
le´ ! _lsr = Some (Vint (Int.repr 1)) ∧
le´ ! _c = Some (Vint c).
Proof.
intros m d le t h tl c Htrange Hevent Hnop Hinv Hon Hrx Htx Hlelsr Hlei Hlec.
generalize (serial_putc_loop_correct_aux m d t h tl c Htrange Hevent Hnop Hinv Hon Hrx Htx).
unfold serial_putc_loop_body_P, serial_putc_loop_body_Q.
intro Hlp.
refine (_ (LoopProofSimpleWhile.termination _ _ _ _ _ _ Hlp le (m, d) _)).
intro pre.
destruct pre as (le´ & m´ & Hexec & Hle´i & Hle´lsr & Hle´c & Hd_end).
∃ le´. subst.
split. assumption.
repeat split; try assumption.
repeat split; try assumption.
omega.
Qed.
Lemma div_mod2_eq1:
∀ n, n ≠ 0 → (n / n) mod 2 = 1.
Proof.
intros n Hneq.
rewrite Z.div_same. rewrite Z.mod_small; omega. assumption.
Qed.
Lemma div32_mod2_eq1:
(32 / 32) mod 2 = 1.
Proof.
apply div_mod2_eq1; omega.
Qed.
Lemma div_mod2_eq0:
∀ n m, 0 ≤ n < m →
(n / m) mod 2 = 0.
Proof.
intros n m H.
rewrite Z.div_small. rewrite Z.mod_small; omega.
assumption.
Qed.
Lemma div32_mod2_eq0:
(0 / 32) mod 2 = 0.
Proof.
apply div_mod2_eq0 with (n:=0) (m:=32).
omega.
Qed.
Lemma attach_some:
∀ A (a b: A),
a = b →
Some a = Some b.
Proof.
intros.
rewrite H. reflexivity.
Qed.
Lemma detach_some:
∀ A (a b: A),
Some a = Some b →
a = b.
Proof.
intros. inversion H. trivial.
Qed.
Tactic Notation "extract_abd" "act" tactic(t) :=
match goal with
| [|-ClightBigstep.exec_stmt _ _ _ _ (_, ?d) _ _ _ _ _] ⇒ t d
| _ ⇒ fail "cannot find abd in the current goal."
end.
Tactic Notation "extract_le" "act" tactic(t) :=
match goal with
| [|-ClightBigstep.exec_stmt _ _ _ ?le (_, _) _ _ _ _ _] ⇒ t le
| _ ⇒ fail "cannot find le in the current goal"
end.
Lemma serial_putc_body_correct:
∀ m c d d´ env le,
env = PTree.empty _ →
PTree.get _c le = Some (Vint c) →
high_level_invariant d →
serial_putc_spec (Int.unsigned c) d = Some d´ →
∃ le´,
exec_stmt ge env le ((m, d): mem) serial_putc_body E0 le´ (m, d´)
Out_normal.
Proof.
generalize max_unsigned_val; intro muval.
intros m c d d´ env le Henv Hcle Hinv Hspec.
generalize (serial_calc_com1_base d Hinv); intro Hcom1Base.
generalize (OracleInvariants.serial_send_complete_bound d); intro Heit.
functional inversion Hspec; subst; clear H3;
try (destruct d; destruct com1, drv_serial; destruct s eqn: s_eq; simpl in *; subst;
simpl in *; unfold update_com1; unfold_DeviceData; unfold_SerialState; subst
); clear Hspec.
- Case "serial_exists = true, txbuf = nil, c = '\r'".
inversion H4; subst.
esplit.
unfold serial_putc_body.
repeat vcgen.
rewrite Int.unsigned_repr; [reflexivity | omega].
discharge_cmp.
repeat vcgen.
unfold serial_in_spec; simpl.
destruct (SerialEnv ltx); serial_unfold_refl.
calc. discharge_cmp.
omega. omega. calc; omega. omega. omega. calc; omega. omega.
omega.
discharge_cmp.
repeat vcgen.
calc; omega.
ptreesolve.
discharge_cmp.
discharge_cmp.
discharge_cmp.
repeat vcgen.
- Case "serial_exists = true, txbuf = nil, c <> '\r'".
inversion H4; subst.
esplit.
unfold serial_putc_body.
repeat vcgen.
rewrite Int.unsigned_repr; [reflexivity | omega].
discharge_cmp.
repeat vcgen.
unfold serial_in_spec; simpl.
destruct (SerialEnv ltx); serial_unfold_refl.
calc. discharge_cmp.
omega. omega. calc; omega. omega. omega. calc; omega. omega.
omega.
discharge_cmp.
repeat vcgen.
calc; omega.
ptreesolve.
discharge_cmp.
discharge_cmp.
discharge_cmp.
repeat vcgen.
- Case "serial_exists = true, txbuf = c :: tl, c = '\r'".
destruct _x11 as [| z tl] eqn: Hx11. inversion H6.
inversion H4; subst.
assert (Heit´: z :: tl ≠ nil) by inversion 1.
apply Heit in Heit´. destruct Heit´ as (t & Htrange & Horacle & Hevent).
assert (caseevent: t = 0 ∨ 0 < t < 12800) by omega.
Caseeq (caseevent).
+ SCase "SerialSendComplete immediately".
intros Ht. subst. rewrite Z.add_0_r in Hevent.
esplit.
unfold serial_putc_body.
repeat vcgen.
unfold get_serial_exists_spec; simpl. rewrite Int.unsigned_repr. reflexivity.
omega.
discharge_cmp. repeat vcgen.
unfold serial_in_spec; rewrite serial_calc_com1_base; simpl.
rewrite Hevent; simpl.
serial_unfold_refl.
inversion Hinv; econstructor; eauto.
calc. discharge_cmp.
omega. omega. calc; omega. omega. omega. calc; omega. omega. omega.
discharge_cmp.
repeat vcgen. calc. omega. calc. ptreesolve. reflexivity.
discharge_cmp.
discharge_cmp.
× SSCase "the sending part".
repeat vcgen. unfold serial_out_spec; simpl.
unfold update_com1; simpl; unfold_DeviceData; unfold_SerialState.
unfold ret; simpl. repeat f_equal.
rewrite next_sendcomplete_eq_t with (t´ := 0). omega.
omega. rewrite Z.add_0_r. assumption. assumption.
+ SCase "not send at ts".
intros Htrange´.
generalize (next_sendcomplete_eq_t ltx t Htrange Hevent Horacle); intros Hts.
exec_pre_abd dpre.
set (Hd := dpre {com1 / l2: ltx + 1}).
set (Hle := (PTree.set _i (Vint Int.zero)
(PTree.set _lsr (Vint Int.zero)
(PTree.set 41 (Vint Int.zero) (PTree.set 44 (Vint Int.one) le))))).
exploit (serial_putc_loop_correct m Hd Hle (t - 1) z tl c);
simpl; try auto; try omega; try discharge_cmp.
× calc. simpl. assumption.
× intros. generalize (Horacle (n + 1)). calc. intros Ho.
assert (Har: ltx + 1 + n = ltx + n + 1) by omega.
rewrite Har. rewrite Ho. reflexivity. omega.
× econstructor; inversion Hinv; eauto.
× unfold Hle. ptreesolve.
× unfold Hle. ptreesolve.
× unfold Hle. ptreesolve.
× intros Hloop.
destruct Hloop as (le_after_loop & Hloopexec & Hle´i & Hle´lsr & Hle´c).
esplit.
unfold serial_putc_body.
repeat vcgen.
rewrite Int.unsigned_repr; [reflexivity | omega].
assert (Hevent0: 0 ≤ 0 < t) by omega.
generalize (Horacle 0). rewrite Z.add_0_r. intros Horacle0.
discharge_cmp. repeat vcgen.
unfold serial_in_spec; subst; simpl.
rewrite Horacle0.
serial_unfold_refl.
omega. calc. discharge_cmp. omega. omega. calc; reflexivity. omega.
omega. calc; omega. omega. omega.
discharge_cmp.
d2 vcgen. calc. discharge_cmp. repeat vcgen.
{ SSCase "loop proof".
eapply Hloopexec.
}
calc. omega.
eassumption.
repeat vcgen.
repeat vcgen.
{ SSCase "after loop".
discharge_cmp. repeat vcgen.
unfold d_end, Hd; unfold update_com1; unfold_DeviceData; unfold_SerialState.
replace (ltx + 1 + (t - 1) + 1) with (ltx + t + 1) by omega.
unfold serial_out_spec; simpl.
serial_unfold_refl. rewrite Hts.
reflexivity.
}
- Case "serial_exists = true, txbuf = c :: tl, c <> '\r'".
destruct _x11 as [| z tl] eqn: Hx11. inversion H6.
inversion H4; subst; simpl in ×. clear H4.
assert (Heit´: z :: tl ≠ nil) by inversion 1.
apply Heit in Heit´. destruct Heit´ as (t & Htrange & Horacle & Hevent).
assert (caseevent: t = 0 ∨ 0 < t < 12800) by omega.
Caseeq (caseevent).
+ SCase "SerialSendComplete immediately".
intros Ht. subst. rewrite Z.add_0_r in Hevent.
esplit.
unfold serial_putc_body.
repeat vcgen.
rewrite Int.unsigned_repr; [reflexivity | omega].
discharge_cmp. repeat vcgen.
unfold serial_in_spec; rewrite serial_calc_com1_base; simpl.
rewrite Hevent; simpl.
serial_unfold_refl.
inversion Hinv; econstructor; eauto.
calc. discharge_cmp.
omega. omega. calc; omega. omega. omega. calc; omega.
omega. omega.
discharge_cmp.
repeat vcgen.
calc. omega.
ptreesolve.
discharge_cmp.
discharge_cmp.
discharge_cmp.
× SSCase "the sending part".
repeat vcgen.
unfold serial_out_spec; simpl.
serial_unfold_refl.
rewrite next_sendcomplete_eq_t with (t´ := 0). calc.
replace (1 + ltx) with (ltx + 1) by omega.
reflexivity.
omega.
rewrite Z.add_0_r. assumption.
intros. rewrite (Horacle n0). reflexivity. omega.
+ SCase "not send at ts".
intros Htrange´.
generalize (next_sendcomplete_eq_t ltx t Htrange Hevent Horacle); intros Hts.
exec_pre_abd dpre.
set (Hd := dpre {com1 / l2: ltx + 1}).
set (Hle := (PTree.set _i (Vint Int.zero)
(PTree.set _lsr (Vint Int.zero)
(PTree.set 41 (Vint Int.zero) (PTree.set 44 (Vint Int.one) le))))).
exploit (serial_putc_loop_correct m Hd Hle (t - 1) z tl c);
simpl; try auto; try omega; try discharge_cmp.
replace (ltx + 1 + (t - 1)) with (ltx + t) by omega. assumption.
intros n0 Hnrange. generalize (Horacle (n0 + 1)). intros Hn0oracle.
replace (ltx + (n0 + 1)) with (ltx + 1 + n0) in Hn0oracle by omega.
rewrite Hn0oracle. reflexivity. omega.
inversion Hinv; econstructor; eauto.
unfold Hle. ptreesolve.
unfold Hle. ptreesolve.
unfold Hle. ptreesolve.
intros Hloop.
destruct Hloop as (le_after_loop & Hloopexec & Hle´i & Hle´lsr & Hle´c).
esplit.
unfold serial_putc_body.
repeat vcgen.
rewrite Int.unsigned_repr; [reflexivity | omega].
discharge_cmp. repeat vcgen.
generalize (Horacle 0); intro Horacle0.
assert (Hevent0: 0 ≤ 0 < t) by omega.
apply Horacle0 in Hevent0. clear Horacle0. rewrite Z.add_0_r in Hevent0.
unfold serial_in_spec; rewrite serial_calc_com1_base; simpl.
rewrite Hevent0.
serial_unfold_refl.
inversion Hinv; econstructor; eauto.
calc. simpl. discharge_cmp.
omega. omega. calc; omega. omega. omega. calc; omega. omega.
omega.
d2 vcgen. repeat vcgen.
× SSCase "loop proof".
eapply Hloopexec.
× eassumption.
× repeat vcgen.
× repeat vcgen.
× SSCase "after loop".
discharge_cmp. repeat vcgen.
unfold serial_out_spec; simpl.
unfold d_end, Hd; unfold update_com1; simpl; unfold_DeviceData; unfold_SerialState.
replace (ltx + 1 + (t - 1) + 1) with (ltx + t + 1) by omega.
rewrite Hts.
reflexivity.
- Case "serial_exists = false".
esplit. unfold serial_putc_body.
repeat vcgen. unfold get_serial_exists_spec.
rewrite H0, H1, H2.
inversion Hinv. destruct valid_serial_exists.
rewrite H. rewrite Int.unsigned_repr; [reflexivity | omega].
rewrite H in _x. contradiction _x. reflexivity.
discharge_cmp. repeat vcgen.
Qed.
End SerialPutcBody.
Theorem serial_putc_code_correct:
spec_le
(serial_putc ↦ serial_putc_spec_low)
(〚serial_putc ↦ f_serial_putc 〛L).
Proof.
set (L´ := L) in ×. unfold L in ×.
fbigstep_pre L´.
fbigstep
(serial_putc_body_correct
s
(Genv.globalenv p)
makeglobalenv b0 Hb0fs Hb0fp b1 Hb1fs Hb1fp b2 Hb2fs Hb2fp m´0 c labd labd´ (PTree.empty _)
(bind_parameter_temps´ (fn_params f_serial_putc) (Vint c :: nil)
(create_undef_temps (fn_temps f_serial_putc))
)
) H0.
Qed.
End SERIALPUTC.
End WithPrimitives.
End DSERIALINTROCODE.