Library mcertikos.devdrivers.DSerialIntroCode_serial_getc
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 SERIALGETC.
Let L: compatlayer (cdata RData) :=
get_serial_exists ↦ gensem get_serial_exists_spec
⊕ serial_in ↦ gensem serial_in_spec
⊕ cons_buf_write ↦ gensem cons_buf_write_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 SerialGetcBody.
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 bcons_buf_write: block.
Hypothesis hcons_buf_write1: Genv.find_symbol ge cons_buf_write = Some bcons_buf_write.
Hypothesis hcons_buf_write2: Genv.find_funct_ptr ge bcons_buf_write =
Some (External (EF_external cons_buf_write
(signature_of_type (Tcons tuint Tnil) tvoid cc_default))
(Tcons tuint Tnil) tvoid cc_default).
Lemma serial_getc_body_correct:
∀ m r d d´ env le,
env = PTree.empty _ →
high_level_invariant d →
serial_getc_spec d = Some (d´, Int.unsigned r) →
∃ le´,
exec_stmt ge env le ((m, d): mem) serial_getc_body E0 le´ (m, d´)
(Out_return (Some (Vint r, tuint))).
Proof.
generalize max_unsigned_val; intro muval.
intros m r d d´ env le Henv Hinv Hspec.
generalize (serial_calc_com1_base d Hinv); intro Hcom1Base.
inversion Hinv.
functional inversion Hspec; clear Hspec;
try (unfold rxbuf´ in *; unfold tl´ in *; unfold c´ in *); subst;
unfold update_com1; simpl; unfold_DeviceData; unfold_SerialState;
(try on_eq_left (com1 d) act (fun Hx ⇒ rename Hx into Hd));
try (destruct d; destruct com1, drv_serial; simpl in *; try destruct s; simpl in × );
try (inversion Hd; subst; clear Hd); clear Hinv; unfold serial_getc_body; clear H4.
- Case "serial_exists = true， RxBuf = nil, Env = SerialRecv str".
intro_env_instances lrx str H8.
assert (Hr: r = Int.repr 1). rewrite H0; rewrite Int.repr_unsigned; reflexivity.
assert (Hskiphw: skipn (length tlstr - 11) (h :: tlstr) = h :: tlstr).
{
assert (Hlen: (0 ≤ length tlstr ≤ 11)%nat).
repeat toZ. generalize Hstrlen. solve_list. unfold Z.succ. intros. omega.
replace (length tlstr - 11)%nat with 0%nat by omega. simpl. reflexivity.
}
subst. unfold update_console; simpl.
esplit.
repeat vcgen. rewrite Int.unsigned_repr. reflexivity. omega.
discharge_cmp.
repeat vcgen.
unfold serial_in_spec; simpl. rewrite H8.
serial_unfold_simpl. rewrite Hskiphw. reflexivity.
omega.
vcgen. omega. omega.
discharge_cmp.
repeat vcgen.
unfold serial_in_spec; simpl. rewrite H7.
serial_unfold_simpl. reflexivity.
omega.
unfold cons_buf_write_spec; simpl. unfold update_console; simpl.
replace (lrx + 1 + 1) with (lrx + 2). rewrite Int.unsigned_repr.
reflexivity.
omega.
omega.
ptreesolve.
- Case "serial_exists = true， RxBuf = nil, Env = NullEvent".
assert (Hr: r = Int.repr 0). rewrite H0; rewrite Int.repr_unsigned; reflexivity.
subst.
esplit.
repeat vcgen.
rewrite Int.unsigned_repr. reflexivity.
omega.
discharge_cmp.
d2 vcgen.
d5 vcgen.
unfold Int.one. rewrite Int.unsigned_repr.
unfold serial_in_spec; simpl. rewrite H8; simpl.
serial_unfold_refl.
omega. omega.
repeat vcgen. discharge_cmp. ptreesolve.
- Case "serial_exists = true, RxBuf = c :: tl, Env = SerialRecv str".
intro_env_instances lrx str H8.
assert (Hr: r = Int.repr 1). rewrite H0; rewrite Int.repr_unsigned; reflexivity.
fold rxbuf´.
assert (Hrxbuf´: rxbuf´ = rxbuf´). reflexivity. unfold rxbuf´ in Hrxbuf´ at 1.
assert (Hc´: c´ = c´). reflexivity. unfold c´ in Hc´ at 1.
assert (Htl´: tl´ = tl´). reflexivity. unfold tl´ in Htl´ at 1.
fold rxbuf´ in c´, tl´. fold c´. fold tl´.
assert (Hh´tl´: ∃ h´ tl´, rxbuf´ = h´ :: tl´).
{
generalize (skipn_remains (c :: t ++ h :: tlstr) 12). intros Hremains.
unfold rxbuf´. apply Hremains. omega. intros Habsurd. inversion Habsurd.
}
destruct Hh´tl´ as (hx & tlx & Hxtlx).
assert (c´ = hx).
{
unfold c´. rewrite Hxtlx. simpl. reflexivity.
}
assert (tl´ = tlx).
{
unfold tl´. rewrite Hxtlx. simpl. reflexivity.
}
unfold rxbuf´ in Hxtlx.
unfold update_console; simpl.
esplit.
repeat vcgen.
rewrite Int.unsigned_repr. reflexivity.
omega.
discharge_cmp.
repeat vcgen.
unfold serial_in_spec; simpl. rewrite H8; simpl.
serial_unfold_refl.
rewrite Hxtlx. rewrite Int.unsigned_repr. reflexivity.
omega.
calc. simpl. discharge_cmp. omega. omega.
simpl. repeat vcgen.
unfold serial_in_spec; simpl. rewrite H7; simpl.
serial_unfold_refl.
rewrite Int.unsigned_repr. unfold cons_buf_write_spec; simpl.
unfold update_console; simpl.
calc. rewrite Z.add_comm. rewrite H, H1.
reflexivity. rewrite <- H. unfold c´. unfold rxbuf´. omega.
ptreesolve. rewrite Hr. reflexivity.
- Case "serial_exists = true, RxBuf = c :: tl, Env = NullEvent, Env + 1 = SerialRecv".
intro_env_instances (lrx + 1) str H7.
assert (Hr: r = Int.repr 1). rewrite H0; rewrite Int.repr_unsigned; reflexivity.
fold rxbuf´.
assert (Hrxbuf´: rxbuf´ = rxbuf´). reflexivity. unfold rxbuf´ in Hrxbuf´ at 1.
assert (Hc´: c´ = c´). reflexivity. unfold c´ in Hc´ at 1.
assert (Htl´: tl´ = tl´). reflexivity. unfold tl´ in Htl´ at 1.
fold rxbuf´ in c´, tl´. fold c´. fold tl´.
assert (Hh´tl´: ∃ h´ tl´, rxbuf´ = h´ :: tl´).
{
generalize (skipn_remains (c :: t ++ h :: tlstr) 12). intros Hremains.
unfold rxbuf´. apply Hremains. omega. intros Habsurd. inversion Habsurd.
}
destruct Hh´tl´ as (hx & tlx & Hxtlx).
assert (c´ = hx).
{
unfold c´. rewrite Hxtlx. simpl. reflexivity.
}
assert (tl´ = tlx).
{
unfold tl´. rewrite Hxtlx. simpl. reflexivity.
}
unfold rxbuf´ in Hxtlx.
unfold update_console; simpl.
subst.
esplit.
repeat vcgen.
rewrite Int.unsigned_repr. reflexivity. omega.
discharge_cmp.
repeat vcgen.
unfold serial_in_spec; simpl. rewrite H8; simpl.
serial_unfold_refl.
calc. discharge_cmp. omega. omega.
discharge_cmp.
repeat vcgen.
rewrite Int.unsigned_repr.
unfold serial_in_spec; simpl. rewrite H7; simpl.
serial_unfold_refl. rewrite Hxtlx. simpl. reflexivity.
omega. unfold cons_buf_write_spec; simpl.
unfold update_console; simpl.
calc. rewrite Z.add_comm. rewrite Int.unsigned_repr. rewrite <- H1, H. reflexivity.
rewrite <- H. omega.
discharge_cmp. repeat vcgen.
- Case "serial_exists = true, RxBuf = c :: tl, Env = NullEvent, Env + 1 = NullEvent".
assert (Hr: r = Int.repr 1). rewrite H0; rewrite Int.repr_unsigned; reflexivity.
unfold update_console; simpl.
subst.
esplit.
repeat vcgen.
rewrite Int.unsigned_repr. reflexivity. omega.
discharge_cmp.
repeat vcgen.
unfold serial_in_spec; simpl. rewrite H8; simpl.
serial_unfold_refl.
calc. discharge_cmp. omega. omega.
discharge_cmp.
d2 vcgen.
d5 vcgen.
rewrite Int.unsigned_repr.
unfold serial_in_spec; simpl. rewrite H7; simpl.
serial_unfold_refl.
omega. omega.
repeat vcgen.
unfold update_console; simpl.
calc. rewrite Z.add_comm.
repeat vcgen.
ptreesolve.
- Case "serial_exists = false".
assert (Hr: r = Int.repr 0). rewrite H0; rewrite Int.repr_unsigned; reflexivity.
subst.
destruct valid_serial_exists.
esplit.
repeat vcgen.
unfold get_serial_exists_spec.
rewrite H1, H2, H3, H; simpl.
rewrite Int.unsigned_repr; [reflexivity | omega].
discharge_cmp.
repeat vcgen. discharge_cmp. ptreesolve.
+ rewrite H in _x. contradiction _x. omega.
Qed.
End SerialGetcBody.
Theorem serial_getc_code_correct:
spec_le
(serial_getc ↦ serial_getc_spec_low)
(〚serial_getc ↦ f_serial_getc 〛L).
Proof.
set (L´ := L) in ×. unfold L in ×.
fbigstep_pre L´.
fbigstep
(serial_getc_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_getc) (nil)
(create_undef_temps (fn_temps f_serial_getc))
)
) H0.
Qed.
End SERIALGETC.
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 SERIALGETC.
Let L: compatlayer (cdata RData) :=
get_serial_exists ↦ gensem get_serial_exists_spec
⊕ serial_in ↦ gensem serial_in_spec
⊕ cons_buf_write ↦ gensem cons_buf_write_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 SerialGetcBody.
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 bcons_buf_write: block.
Hypothesis hcons_buf_write1: Genv.find_symbol ge cons_buf_write = Some bcons_buf_write.
Hypothesis hcons_buf_write2: Genv.find_funct_ptr ge bcons_buf_write =
Some (External (EF_external cons_buf_write
(signature_of_type (Tcons tuint Tnil) tvoid cc_default))
(Tcons tuint Tnil) tvoid cc_default).
Lemma serial_getc_body_correct:
∀ m r d d´ env le,
env = PTree.empty _ →
high_level_invariant d →
serial_getc_spec d = Some (d´, Int.unsigned r) →
∃ le´,
exec_stmt ge env le ((m, d): mem) serial_getc_body E0 le´ (m, d´)
(Out_return (Some (Vint r, tuint))).
Proof.
generalize max_unsigned_val; intro muval.
intros m r d d´ env le Henv Hinv Hspec.
generalize (serial_calc_com1_base d Hinv); intro Hcom1Base.
inversion Hinv.
functional inversion Hspec; clear Hspec;
try (unfold rxbuf´ in *; unfold tl´ in *; unfold c´ in *); subst;
unfold update_com1; simpl; unfold_DeviceData; unfold_SerialState;
(try on_eq_left (com1 d) act (fun Hx ⇒ rename Hx into Hd));
try (destruct d; destruct com1, drv_serial; simpl in *; try destruct s; simpl in × );
try (inversion Hd; subst; clear Hd); clear Hinv; unfold serial_getc_body; clear H4.
- Case "serial_exists = true， RxBuf = nil, Env = SerialRecv str".
intro_env_instances lrx str H8.
assert (Hr: r = Int.repr 1). rewrite H0; rewrite Int.repr_unsigned; reflexivity.
assert (Hskiphw: skipn (length tlstr - 11) (h :: tlstr) = h :: tlstr).
{
assert (Hlen: (0 ≤ length tlstr ≤ 11)%nat).
repeat toZ. generalize Hstrlen. solve_list. unfold Z.succ. intros. omega.
replace (length tlstr - 11)%nat with 0%nat by omega. simpl. reflexivity.
}
subst. unfold update_console; simpl.
esplit.
repeat vcgen. rewrite Int.unsigned_repr. reflexivity. omega.
discharge_cmp.
repeat vcgen.
unfold serial_in_spec; simpl. rewrite H8.
serial_unfold_simpl. rewrite Hskiphw. reflexivity.
omega.
vcgen. omega. omega.
discharge_cmp.
repeat vcgen.
unfold serial_in_spec; simpl. rewrite H7.
serial_unfold_simpl. reflexivity.
omega.
unfold cons_buf_write_spec; simpl. unfold update_console; simpl.
replace (lrx + 1 + 1) with (lrx + 2). rewrite Int.unsigned_repr.
reflexivity.
omega.
omega.
ptreesolve.
- Case "serial_exists = true， RxBuf = nil, Env = NullEvent".
assert (Hr: r = Int.repr 0). rewrite H0; rewrite Int.repr_unsigned; reflexivity.
subst.
esplit.
repeat vcgen.
rewrite Int.unsigned_repr. reflexivity.
omega.
discharge_cmp.
d2 vcgen.
d5 vcgen.
unfold Int.one. rewrite Int.unsigned_repr.
unfold serial_in_spec; simpl. rewrite H8; simpl.
serial_unfold_refl.
omega. omega.
repeat vcgen. discharge_cmp. ptreesolve.
- Case "serial_exists = true, RxBuf = c :: tl, Env = SerialRecv str".
intro_env_instances lrx str H8.
assert (Hr: r = Int.repr 1). rewrite H0; rewrite Int.repr_unsigned; reflexivity.
fold rxbuf´.
assert (Hrxbuf´: rxbuf´ = rxbuf´). reflexivity. unfold rxbuf´ in Hrxbuf´ at 1.
assert (Hc´: c´ = c´). reflexivity. unfold c´ in Hc´ at 1.
assert (Htl´: tl´ = tl´). reflexivity. unfold tl´ in Htl´ at 1.
fold rxbuf´ in c´, tl´. fold c´. fold tl´.
assert (Hh´tl´: ∃ h´ tl´, rxbuf´ = h´ :: tl´).
{
generalize (skipn_remains (c :: t ++ h :: tlstr) 12). intros Hremains.
unfold rxbuf´. apply Hremains. omega. intros Habsurd. inversion Habsurd.
}
destruct Hh´tl´ as (hx & tlx & Hxtlx).
assert (c´ = hx).
{
unfold c´. rewrite Hxtlx. simpl. reflexivity.
}
assert (tl´ = tlx).
{
unfold tl´. rewrite Hxtlx. simpl. reflexivity.
}
unfold rxbuf´ in Hxtlx.
unfold update_console; simpl.
esplit.
repeat vcgen.
rewrite Int.unsigned_repr. reflexivity.
omega.
discharge_cmp.
repeat vcgen.
unfold serial_in_spec; simpl. rewrite H8; simpl.
serial_unfold_refl.
rewrite Hxtlx. rewrite Int.unsigned_repr. reflexivity.
omega.
calc. simpl. discharge_cmp. omega. omega.
simpl. repeat vcgen.
unfold serial_in_spec; simpl. rewrite H7; simpl.
serial_unfold_refl.
rewrite Int.unsigned_repr. unfold cons_buf_write_spec; simpl.
unfold update_console; simpl.
calc. rewrite Z.add_comm. rewrite H, H1.
reflexivity. rewrite <- H. unfold c´. unfold rxbuf´. omega.
ptreesolve. rewrite Hr. reflexivity.
- Case "serial_exists = true, RxBuf = c :: tl, Env = NullEvent, Env + 1 = SerialRecv".
intro_env_instances (lrx + 1) str H7.
assert (Hr: r = Int.repr 1). rewrite H0; rewrite Int.repr_unsigned; reflexivity.
fold rxbuf´.
assert (Hrxbuf´: rxbuf´ = rxbuf´). reflexivity. unfold rxbuf´ in Hrxbuf´ at 1.
assert (Hc´: c´ = c´). reflexivity. unfold c´ in Hc´ at 1.
assert (Htl´: tl´ = tl´). reflexivity. unfold tl´ in Htl´ at 1.
fold rxbuf´ in c´, tl´. fold c´. fold tl´.
assert (Hh´tl´: ∃ h´ tl´, rxbuf´ = h´ :: tl´).
{
generalize (skipn_remains (c :: t ++ h :: tlstr) 12). intros Hremains.
unfold rxbuf´. apply Hremains. omega. intros Habsurd. inversion Habsurd.
}
destruct Hh´tl´ as (hx & tlx & Hxtlx).
assert (c´ = hx).
{
unfold c´. rewrite Hxtlx. simpl. reflexivity.
}
assert (tl´ = tlx).
{
unfold tl´. rewrite Hxtlx. simpl. reflexivity.
}
unfold rxbuf´ in Hxtlx.
unfold update_console; simpl.
subst.
esplit.
repeat vcgen.
rewrite Int.unsigned_repr. reflexivity. omega.
discharge_cmp.
repeat vcgen.
unfold serial_in_spec; simpl. rewrite H8; simpl.
serial_unfold_refl.
calc. discharge_cmp. omega. omega.
discharge_cmp.
repeat vcgen.
rewrite Int.unsigned_repr.
unfold serial_in_spec; simpl. rewrite H7; simpl.
serial_unfold_refl. rewrite Hxtlx. simpl. reflexivity.
omega. unfold cons_buf_write_spec; simpl.
unfold update_console; simpl.
calc. rewrite Z.add_comm. rewrite Int.unsigned_repr. rewrite <- H1, H. reflexivity.
rewrite <- H. omega.
discharge_cmp. repeat vcgen.
- Case "serial_exists = true, RxBuf = c :: tl, Env = NullEvent, Env + 1 = NullEvent".
assert (Hr: r = Int.repr 1). rewrite H0; rewrite Int.repr_unsigned; reflexivity.
unfold update_console; simpl.
subst.
esplit.
repeat vcgen.
rewrite Int.unsigned_repr. reflexivity. omega.
discharge_cmp.
repeat vcgen.
unfold serial_in_spec; simpl. rewrite H8; simpl.
serial_unfold_refl.
calc. discharge_cmp. omega. omega.
discharge_cmp.
d2 vcgen.
d5 vcgen.
rewrite Int.unsigned_repr.
unfold serial_in_spec; simpl. rewrite H7; simpl.
serial_unfold_refl.
omega. omega.
repeat vcgen.
unfold update_console; simpl.
calc. rewrite Z.add_comm.
repeat vcgen.
ptreesolve.
- Case "serial_exists = false".
assert (Hr: r = Int.repr 0). rewrite H0; rewrite Int.repr_unsigned; reflexivity.
subst.
destruct valid_serial_exists.
esplit.
repeat vcgen.
unfold get_serial_exists_spec.
rewrite H1, H2, H3, H; simpl.
rewrite Int.unsigned_repr; [reflexivity | omega].
discharge_cmp.
repeat vcgen. discharge_cmp. ptreesolve.
+ rewrite H in _x. contradiction _x. omega.
Qed.
End SerialGetcBody.
Theorem serial_getc_code_correct:
spec_le
(serial_getc ↦ serial_getc_spec_low)
(〚serial_getc ↦ f_serial_getc 〛L).
Proof.
set (L´ := L) in ×. unfold L in ×.
fbigstep_pre L´.
fbigstep
(serial_getc_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_getc) (nil)
(create_undef_temps (fn_temps f_serial_getc))
)
) H0.
Qed.
End SERIALGETC.
End WithPrimitives.
End DSERIALINTROCODE.