Library Complements

Corollaries of the main semantic preservation theorem.





Require Import Classical.

Require Import Coqlib.

Require Import AST.

Require Import Integers.

Require Import Values.

Require Import Events.

Require Import Globalenvs.

Require Import Smallstep.

Require Import Determinism.

Require Import Csyntax.

Require Import Csem.

Require Import Asm.

Require Import Compiler.

Require Import Errors.

Determinism of Asm semantics

In this section, we show that the semantics for the Asm language are deterministic, provided that the program is executed against a deterministic world, as formalized in module Determinism.





Remark extcall_arguments_deterministic:

  forall rs m sg args args',

  extcall_arguments rs m sg args ->

  extcall_arguments rs m sg args' -> args = args'.






Lemma step_internal_deterministic:

  forall ge s t1 s1 t2 s2,

  Asm.step ge s t1 s1 -> Asm.step ge s t2 s2 -> internal_determinism _ t1 s1 t2 s2.






Lemma initial_state_deterministic:

  forall p s1 s2,

  initial_state p s1 -> initial_state p s2 -> s1 = s2.






Lemma final_state_not_step:

  forall ge st r, final_state st r -> nostep step ge st.






Lemma final_state_deterministic:

  forall st r1 r2, final_state st r1 -> final_state st r2 -> r1 = r2.






Theorem asm_exec_program_deterministic:

  forall p w beh1 beh2,

  Asm.exec_program p beh1 -> Asm.exec_program p beh2 ->

  possible_behavior w beh1 -> possible_behavior w beh2 ->

  beh1 = beh2.

Additional semantic preservation property

Combining the semantic preservation theorem from module Compiler with the determinism of Asm executions, we easily obtain additional, stronger semantic preservation properties. The first property states that, when compiling a Clight program that has well-defined semantics, all possible executions of the resulting Asm code correspond to an execution of the source Clight program.





Theorem transf_c_program_is_refinement:

  forall p tp w,

  transf_c_program p = OK tp ->

  (exists b, Csem.exec_program p b /\ possible_behavior w b /\ not_wrong b) ->

  (forall b, Asm.exec_program tp b -> possible_behavior w b -> Csem.exec_program p b).






Section SPECS_PRESERVED.

The second additional results shows that if one execution of the source Clight program satisfies a given specification (a predicate on the observable behavior of the program), then all executions of the produced Asm program satisfy this specification as well.





Variable spec: program_behavior -> Prop.




Hypothesis spec_not_wrong: forall b, spec b -> not_wrong b.




Theorem transf_c_program_preserves_spec:

  forall p tp w,

  transf_c_program p = OK tp ->

  (exists b, Csem.exec_program p b /\ possible_behavior w b /\ spec b) ->

  (forall b, Asm.exec_program tp b -> possible_behavior w b -> spec b).






End SPECS_PRESERVED.