Library mcertikos.devdrivers.DSerialIntroCode_serial_init
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_simpl :=
unfold_SerialState; unfold_DeviceData; unfold update_com1; simpl;
try (rewrite Int.unsigned_repr; [simpl | omega];
rewrite Int.unsigned_repr; [simpl | omega]).
Ltac serial_exists_unfold_simpl :=
unfold_SerialState; unfold_DeviceData; unfold update_com1, update_drv_serial; simpl.
Ltac solve_serial_in :=
unfold serial_in_spec; simpl;
rewrite Int.unsigned_repr; [reflexivity | omega].
Section SERIALINIT.
Let L: compatlayer (cdata RData) :=
set_serial_exists ↦ gensem set_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 SerialInitBody.
Context `{Hwb: WritableBlockOps}.
Variable (sc: stencil).
Variables (ge: genv)
(STENCIL_MATCHES: stencil_matches sc ge).
Function external_function arg_type ret_type cal_conv prim
:= Some (External (EF_external prim
(signature_of_type arg_type ret_type cal_conv))
arg_type ret_type cal_conv).
Variable (bset_serial_exists: block).
Hypothesis hset_serial_exists1 : Genv.find_symbol ge set_serial_exists = Some bset_serial_exists.
Hypothesis hset_serial_exists2 : Genv.find_funct_ptr ge bset_serial_exists =
Some (External (EF_external set_serial_exists
(signature_of_type (Tcons tuint Tnil) tvoid cc_default))
(Tcons tuint Tnil) tvoid 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).
Lemma serial_init_body_correct:
∀ m d d´ env le,
env = PTree.empty _ →
high_level_invariant d →
serial_init_spec d = Some d´ →
∃ le´,
exec_stmt ge env le ((m, d): mem) serial_init_body E0 le´ (m, d´)
Out_normal.
Proof.
generalize max_unsigned_val; intro muval.
intros m d d´ env le z Hinv Hspec.
unfold serial_init_body. functional inversion Hspec.
unfold update_com1, update_s, update_drv_serial in *; simpl in ×.
destruct d; destruct com1; destruct s; simpl in ×. inversion H3. clear H3.
clear Hinv H Hspec.
generalize (OracleInvariants.serial_recv_limit lrx str H4);
intros [Hstrnnil [Hstrlen [Hstrchar Hevent]]].
generalize (non_nil_list Hstrnnil); intros (h & tlstr & Hstr). subst.
generalize (forall_hd Hstrchar); intros Hstrhd.
subst.
esplit.
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.
}
d3 vcgen. repeat vcgen. serial_unfold_simpl.
d2 vcgen. repeat vcgen. serial_unfold_simpl.
d2 vcgen. repeat vcgen. serial_unfold_simpl.
d2 vcgen. repeat vcgen. serial_unfold_simpl.
d2 vcgen. repeat vcgen. serial_unfold_simpl.
d2 vcgen. repeat vcgen. serial_unfold_simpl.
d2 vcgen. repeat vcgen. serial_unfold_simpl.
d2 vcgen. repeat vcgen. serial_unfold_simpl.
d3 vcgen. vcgen. repeat vcgen. solve_serial_in.
repeat vcgen. serial_exists_unfold_simpl.
d2 vcgen. repeat vcgen. solve_serial_in. serial_unfold_simpl.
repeat vcgen. unfold serial_in_spec; simpl. serial_unfold_simpl.
rewrite Int.unsigned_repr. unfold ret; simpl.
repeat f_equal. rewrite update_baudrate_0_1_eq.
rewrite H4. unfold serial_trans_cpu; simpl. unfold_SerialState.
rewrite Hskiphw. reflexivity.
rewrite H4; simpl. unfold isChar in Hstrhd. rewrite Hskiphw. simpl. omega.
unfold update_com1, update_s, update_drv_serial in *; simpl in ×.
destruct d; destruct com1; destruct s; simpl in ×. inversion H3. clear H3.
clear Hinv H Hspec.
subst.
esplit.
d3 vcgen. repeat vcgen. serial_unfold_simpl.
d2 vcgen. repeat vcgen. serial_unfold_simpl.
d2 vcgen. repeat vcgen. serial_unfold_simpl.
d2 vcgen. repeat vcgen. serial_unfold_simpl.
d2 vcgen. repeat vcgen. serial_unfold_simpl.
d2 vcgen. repeat vcgen. serial_unfold_simpl.
d2 vcgen. repeat vcgen. serial_unfold_simpl.
d2 vcgen. repeat vcgen. serial_unfold_simpl.
d3 vcgen. vcgen. repeat vcgen. solve_serial_in.
repeat vcgen. serial_exists_unfold_simpl.
d2 vcgen. repeat vcgen. solve_serial_in. serial_unfold_simpl.
repeat vcgen. unfold serial_in_spec; simpl. serial_unfold_simpl.
rewrite Int.unsigned_repr. unfold ret; simpl.
repeat f_equal. rewrite update_baudrate_0_1_eq.
destruct (SerialEnv lrx) eqn: Henv.
- unfold serial_trans_cpu; simpl. unfold_SerialState. reflexivity.
- inversion H5.
- unfold serial_trans_cpu; simpl. unfold_SerialState. reflexivity.
- unfold serial_trans_cpu; simpl. unfold_SerialState. reflexivity.
- unfold serial_trans_cpu; simpl. unfold_SerialState.
destruct (SerialEnv lrx) eqn: Henv.
+ simpl. omega.
+ simpl. omega.
+ simpl. omega.
+ simpl. omega.
Qed.
End SerialInitBody.
Theorem serial_init_code_correct:
spec_le
(serial_init ↦ serial_init_spec_low)
(〚serial_init ↦ f_serial_init 〛L).
Proof.
set (L´ := L) in ×. unfold L in ×.
fbigstep_pre L´.
fbigstep
(serial_init_body_correct s
(Genv.globalenv p) makeglobalenv b0 Hb0fs Hb0fp b1 Hb1fs Hb1fp b2 Hb2fs Hb2fp m´0 labd labd´ (PTree.empty _)
(bind_parameter_temps´ (fn_params f_serial_init) (nil)
(create_undef_temps (fn_temps f_serial_init))
)
) H0.
Qed.
End SERIALINIT.
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_simpl :=
unfold_SerialState; unfold_DeviceData; unfold update_com1; simpl;
try (rewrite Int.unsigned_repr; [simpl | omega];
rewrite Int.unsigned_repr; [simpl | omega]).
Ltac serial_exists_unfold_simpl :=
unfold_SerialState; unfold_DeviceData; unfold update_com1, update_drv_serial; simpl.
Ltac solve_serial_in :=
unfold serial_in_spec; simpl;
rewrite Int.unsigned_repr; [reflexivity | omega].
Section SERIALINIT.
Let L: compatlayer (cdata RData) :=
set_serial_exists ↦ gensem set_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 SerialInitBody.
Context `{Hwb: WritableBlockOps}.
Variable (sc: stencil).
Variables (ge: genv)
(STENCIL_MATCHES: stencil_matches sc ge).
Function external_function arg_type ret_type cal_conv prim
:= Some (External (EF_external prim
(signature_of_type arg_type ret_type cal_conv))
arg_type ret_type cal_conv).
Variable (bset_serial_exists: block).
Hypothesis hset_serial_exists1 : Genv.find_symbol ge set_serial_exists = Some bset_serial_exists.
Hypothesis hset_serial_exists2 : Genv.find_funct_ptr ge bset_serial_exists =
Some (External (EF_external set_serial_exists
(signature_of_type (Tcons tuint Tnil) tvoid cc_default))
(Tcons tuint Tnil) tvoid 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).
Lemma serial_init_body_correct:
∀ m d d´ env le,
env = PTree.empty _ →
high_level_invariant d →
serial_init_spec d = Some d´ →
∃ le´,
exec_stmt ge env le ((m, d): mem) serial_init_body E0 le´ (m, d´)
Out_normal.
Proof.
generalize max_unsigned_val; intro muval.
intros m d d´ env le z Hinv Hspec.
unfold serial_init_body. functional inversion Hspec.
unfold update_com1, update_s, update_drv_serial in *; simpl in ×.
destruct d; destruct com1; destruct s; simpl in ×. inversion H3. clear H3.
clear Hinv H Hspec.
generalize (OracleInvariants.serial_recv_limit lrx str H4);
intros [Hstrnnil [Hstrlen [Hstrchar Hevent]]].
generalize (non_nil_list Hstrnnil); intros (h & tlstr & Hstr). subst.
generalize (forall_hd Hstrchar); intros Hstrhd.
subst.
esplit.
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.
}
d3 vcgen. repeat vcgen. serial_unfold_simpl.
d2 vcgen. repeat vcgen. serial_unfold_simpl.
d2 vcgen. repeat vcgen. serial_unfold_simpl.
d2 vcgen. repeat vcgen. serial_unfold_simpl.
d2 vcgen. repeat vcgen. serial_unfold_simpl.
d2 vcgen. repeat vcgen. serial_unfold_simpl.
d2 vcgen. repeat vcgen. serial_unfold_simpl.
d2 vcgen. repeat vcgen. serial_unfold_simpl.
d3 vcgen. vcgen. repeat vcgen. solve_serial_in.
repeat vcgen. serial_exists_unfold_simpl.
d2 vcgen. repeat vcgen. solve_serial_in. serial_unfold_simpl.
repeat vcgen. unfold serial_in_spec; simpl. serial_unfold_simpl.
rewrite Int.unsigned_repr. unfold ret; simpl.
repeat f_equal. rewrite update_baudrate_0_1_eq.
rewrite H4. unfold serial_trans_cpu; simpl. unfold_SerialState.
rewrite Hskiphw. reflexivity.
rewrite H4; simpl. unfold isChar in Hstrhd. rewrite Hskiphw. simpl. omega.
unfold update_com1, update_s, update_drv_serial in *; simpl in ×.
destruct d; destruct com1; destruct s; simpl in ×. inversion H3. clear H3.
clear Hinv H Hspec.
subst.
esplit.
d3 vcgen. repeat vcgen. serial_unfold_simpl.
d2 vcgen. repeat vcgen. serial_unfold_simpl.
d2 vcgen. repeat vcgen. serial_unfold_simpl.
d2 vcgen. repeat vcgen. serial_unfold_simpl.
d2 vcgen. repeat vcgen. serial_unfold_simpl.
d2 vcgen. repeat vcgen. serial_unfold_simpl.
d2 vcgen. repeat vcgen. serial_unfold_simpl.
d2 vcgen. repeat vcgen. serial_unfold_simpl.
d3 vcgen. vcgen. repeat vcgen. solve_serial_in.
repeat vcgen. serial_exists_unfold_simpl.
d2 vcgen. repeat vcgen. solve_serial_in. serial_unfold_simpl.
repeat vcgen. unfold serial_in_spec; simpl. serial_unfold_simpl.
rewrite Int.unsigned_repr. unfold ret; simpl.
repeat f_equal. rewrite update_baudrate_0_1_eq.
destruct (SerialEnv lrx) eqn: Henv.
- unfold serial_trans_cpu; simpl. unfold_SerialState. reflexivity.
- inversion H5.
- unfold serial_trans_cpu; simpl. unfold_SerialState. reflexivity.
- unfold serial_trans_cpu; simpl. unfold_SerialState. reflexivity.
- unfold serial_trans_cpu; simpl. unfold_SerialState.
destruct (SerialEnv lrx) eqn: Henv.
+ simpl. omega.
+ simpl. omega.
+ simpl. omega.
+ simpl. omega.
Qed.
End SerialInitBody.
Theorem serial_init_code_correct:
spec_le
(serial_init ↦ serial_init_spec_low)
(〚serial_init ↦ f_serial_init 〛L).
Proof.
set (L´ := L) in ×. unfold L in ×.
fbigstep_pre L´.
fbigstep
(serial_init_body_correct s
(Genv.globalenv p) makeglobalenv b0 Hb0fs Hb0fp b1 Hb1fs Hb1fp b2 Hb2fs Hb2fp m´0 labd labd´ (PTree.empty _)
(bind_parameter_temps´ (fn_params f_serial_init) (nil)
(create_undef_temps (fn_temps f_serial_init))
)
) H0.
Qed.
End SERIALINIT.
End WithPrimitives.
End DSERIALINTROCODE.