remove comments (#3)

* Create README.md * Update SimMemInjC.v * Update README.md * Update README.md * Update README.md * delete comments * update ReadMe * update ReadMe * Update README.md
snu-sf · Oct 20, 2019 · da27882 · da27882
1 parent 19bf3b3
commit da27882
Show file tree

Hide file tree

Showing 24 changed files with 21 additions and 551 deletions.
diff --git a/README.md b/README.md
@@ -21,7 +21,7 @@ New directories are roughly as follows.
 - compose/: interaction semantics and its properties  
 - demo/: examples including Unreadglob, mutual-sum and utod
 - selfsim/: self-simulation of Clight and Assembly  
-- scripts/: scripts used for SLOC counting (Table 1, 2, 3)  
+- scripts/: scripts used for SLOC counting (_Table 1, 2, 3_)  
 - proof/: our meta theory
 
 
@@ -30,7 +30,7 @@ We list up few important definitions/proofs from the paper.
 **Semantics**  
 - Interaction Semantics _(Section 5)_ : [compose/Sem.v](compose/Sem.v)  
 - Module _(Page 18, Fig. 9)_: [compose/Mod.v](compose/Mod.v)  
-- Module Semantics _(Page 18, Fig. 9)_: [compose/ModSem.v](compose/ModSem.v#L140)  
+- Module Semantics _(Page 18, Fig. 9)_: [compose/ModSem.v](compose/ModSem.v#L138)  
 
 **Verification Techniques**  
 - RUSC Theory _(Section 2.3)_: [proof/RUSC.v](proof/RUSC.v)  
@@ -39,21 +39,21 @@ We list up few important definitions/proofs from the paper.
 - Parameter-SymbRel _(Page 20, Fig. 10)_: [proof/SimSymb.v](proof/SimSymb.v)  
 - Parameter-MemPred _(Page 20, Fig. 10)_: [proof/Sound.v](proof/Sound.v)  
 - Parameterized Open Simulation _(Page 21, Fig. 11)_: [proof/SimModSem.v](proof/SimModSem.v)  
-- Open Preservation _(Page 21, Fig. 11)_: [proof/Preservation.v](proof/Preservation.v) - [`local_preservation_standard`](proof/Preservation.v#L177)  
-- Adequacy of Parameterized Open Simulation _(Page 22, Theorem 6.2)_: [proof/AdequacyLocal.v](proof/AdequacyLocal.v) - [`Theorem adequacy_local`](proof/AdequacyLocal.v#729).  
+- Open Preservation _(Page 21, Fig. 11)_: [proof/Preservation.v](proof/Preservation.v) - [`local_preservation_standard`](proof/Preservation.v#L102)  
+- Adequacy of Parameterized Open Simulation _(Page 22, Theorem 6.2)_: [proof/AdequacyLocal.v](proof/AdequacyLocal.v) - [`Theorem adequacy_local`](proof/AdequacyLocal.v#L705).  
 
 **Correctness Theorems**  
 - Compiler cocrrectness theorem (main result): [driver/CompilerC.v](driver/CompilerC.v)
-  + Compositional Correctness I _(Page 23, Theorem 7.3)_: [`Theorem compiler_correct`](driver/CompilerC.v#L691)
+  + Compositional Correctness I _(Page 23, Theorem 7.3)_: [`Theorem compiler_correct`](driver/CompilerC.v#L633)
   + Compositional Correctness II _(Page 24, Theorem 7.5)_: [`Theorem compiler_correct_full`](driver/CompilerC.v#L712)  
-- Adequacy w.r.t. Assembly _(Page 24, Theorem 7.6)_: [bound/LowerBound.v](bound/LowerBound.v) - [`Theorem lower_bound_correct`](bound/LowerBound.v#L2398)
-- Adequacy w.r.t. C _(Page 24, Theorem 7.7)_: [bound/UpperBound_B.v](bound/UpperBound_B.v) - [`Theorem upper_bound_b_correct`](bound/UpperBound_B.v#L1360)  
+- Adequacy w.r.t. Assembly _(Page 24, Theorem 7.6)_: [bound/LowerBound.v](bound/LowerBound.v) - [`Theorem lower_bound_correct`](bound/LowerBound.v#L2395)
+- Adequacy w.r.t. C _(Page 24, Theorem 7.7)_: [bound/UpperBound_B.v](bound/UpperBound_B.v) - [`Theorem upper_bound_b_correct`](bound/UpperBound_B.v#L1349)  
 
 **Examples**  
 - Unreadglob example _(Section 4.1)_: [demo/unreadglob](demo/unreadglob) ([demo directory in CompCertR](https://github.com/snu-sf/CompCertR/tree/v3.5_adapt/demo) also contains actual optimization and proof files)  
 - mutual-sum example _(Section 4.2)_: [demo/mutrec](demo/mutrec)
-  + a.c, b.asm (Page 16, Fig. 7): [a.c](mutrec/a.c), [b.s](mutrec/b.s)
-  + a.spec, b.spec (Page 16, Fig. 7): [MutrecAspec.v](MutrecAspec.v), [MutrecBspec.v](MutrecBspec.v)
-  + ab.spec (Page 16, Fig. 7): [MutrecABspec.v](demo/mutrec/MutrecABspec.v)
+  + a.c, b.asm _(Page 16, Fig. 7)_: [a.c](demo/mutrec/a.c), [b.s](demo/mutrec/b.s)
+  + a.spec, b.spec _(Page 16, Fig. 7)_: [MutrecAspec.v](demo/mutrec/MutrecAspec.v), [MutrecBspec.v](demo/mutrec/MutrecBspec.v)
+  + ab.spec _(Page 16, Fig. 7)_: [MutrecABspec.v](demo/mutrec/MutrecABspec.v)
   + refinement proof: [MutrecRefinement.v](demo/mutrec/MutrecRefinement.v) - [`Theorem Mutrec_correct`](demo/mutrec/MutrecRefinement.v#L144)
 - utod example: [demo/utod](demo/utod)  
diff --git a/bound/LowerBound.v b/bound/LowerBound.v
@@ -140,7 +140,6 @@ Section PRESERVATION.
   Qed.
 
   Definition genv_le (ge_src ge_tgt: Genv.t fundef unit): Prop :=
-    (* sub_match_genvs eq ge_src ge_tgt. *)
     sub_match_genvs (@def_match _ _) ge_src ge_tgt.
 
   Lemma skenv_link_public_eq id:
@@ -1717,8 +1716,6 @@ Section PRESERVATION.
           * ii. ss. des; clarify. }
   Qed.
 
-  (* skenv_inject skenv_link j_callee (assign_junk_blocks m_src n) *)
-
 (** ********************* transf initial final  *********************************)
 
   Lemma transf_initial_states:

diff --git a/bound/UpperBound_B.v b/bound/UpperBound_B.v
@@ -43,17 +43,6 @@ Definition internal_function_state (ge: genv) (s: Csem.state) : Prop :=
 
 Section PRESERVATION.
 
-(* PLAN B-0*)
-
-(*
-B-0
-* : Physical
-+ : Logical
-c0 * empty
->=
-c0 + empty
-*)
-
   Inductive my_eq {A: Type} (x: A): A -> Prop :=
   | my_eq_refl: my_eq x x.
 

diff --git a/compose/Mod.v b/compose/Mod.v
@@ -25,7 +25,6 @@ Module Mod.
   (* 2) This definition will give an error when datatype is changed. *)
   Record t: Type := mk {
     datatype: Type;
-    (* skel: Skel.t; *)
     get_sk: datatype -> Sk.t;
     get_modsem: SkEnv.t -> datatype -> ModSem.t;
     data: datatype;

diff --git a/compose/ModSem.v b/compose/ModSem.v
@@ -141,35 +141,13 @@ Module ModSem.
     state: Type;
     genvtype: Type;
     step (se: Senv.t) (ge: genvtype) (st0: state) (tr: trace) (st1: state): Prop;
-    (* TOOD: is ge needed? I follow compcert for now. *)
-
-    (* set_mem (m0: mem) (st0: state): state; *) (* This is not used, after_external is enough *)
     at_external (st0: state) (args: Args.t): Prop;
     initial_frame (args: Args.t) (st0: state): Prop;
-    (* time: rs_arg >> st0 *)
-    final_frame (* (st_init: state) *) (st0: state) (retv: Retv.t): Prop;
-    (* time: st0 >> rs_arg *)
+    final_frame (st0: state) (retv: Retv.t): Prop;
     after_external (st0: state) (retv: Retv.t) (st1: state): Prop;
     globalenv: genvtype;
-    (* internals: list block; *)
-    (* internals: block -> Prop; *)
-    (* main_fptr: block; *)
-    (* Note: "internals" is not enough! A ModSemPair should be able to specify which SimMem it relys. *)
     skenv: SkEnv.t;
     skenv_link: SkEnv.t;
-    (* skenv: SkEnv.t; *)
-    (* ########################################## I added SkEnv.t only for defining "compat" in sim_mem. *)
-    (* If it is not used, remove it *)
-
-
-    (* good properties *)
-    (* We need to drop permission ! *)
-    (* initial_machine_get_mem: forall *)
-    (*     rs_arg m_arg st0 *)
-    (*     (INIT: initial_frame rs_arg m_arg st0) *)
-    (*   , *)
-    (*     <<MEM: st0.(get_mem) = m_arg>> *)
-    (* ; *)
 
     at_external_dtm: forall st args0 args1
         (AT0: at_external st args0)
@@ -180,13 +158,6 @@ Module ModSem.
         (FINAL0: final_frame st retv0)
         (FINAL1: final_frame st retv1),
         retv0 = retv1;
-    (* final_frame_dtm: forall *)
-    (*     rs_init st rs_ret0 m_ret0 rs_ret1 m_ret1 *)
-    (*     (FINAL0: final_frame rs_init st rs_ret0 m_ret0) *)
-    (*     (FINAL1: final_frame rs_init st rs_ret1 m_ret1) *)
-    (*   , *)
-    (*     rs_ret0 = rs_ret1 /\ m_ret0 = m_ret1 *)
-    (* ; *)
     after_external_dtm: forall st_call retv st0 st1
         (AFTER0: after_external st_call retv st0)
         (AFTER0: after_external st_call retv st1),
@@ -196,19 +167,12 @@ Module ModSem.
     is_call (st0: state): Prop := exists args, at_external st0 args;
     is_step (st0: state): Prop := exists tr st1, step skenv_link globalenv st0 tr st1;
     is_return (st0: state): Prop := exists retv, final_frame st0 retv;
-      (* exists rs_init rs_ret m_ret, final_frame rs_init st0 rs_ret m_ret; *)
-    (* Note: "forall" or "exists" for rs_init? *)
-    (* "forall" -> easy for opt/hard for meta *)
-    (* "exists" -> hard for opt/easy for meta *)
-    (* I think "exists" is OK here. *)
-    (* We can think of something like "forall rs_init (FUTURE: st0 is future of rs_init)", but is overkill. *)
 
     call_step_disjoint: is_call /1\ is_step <1= bot1;
     step_return_disjoint: is_step /1\ is_return <1= bot1;
     call_return_disjoint: is_call /1\ is_return <1= bot1;
   }.
 
-  (* Note: I didn't want to define this tactic. I wanted to use eauto + Hint Resolve, but it didn't work. *)
   Ltac tac :=
     try( let TAC := u; esplits; eauto in
          u in *; des_safe;
@@ -323,4 +287,3 @@ End ModSem.
 Hint Unfold ModSem.is_call ModSem.is_step ModSem.is_return.
 
 Coercion ModSem.to_semantics: ModSem.t >-> semantics.
-(* I want to use definitions like "Star" or "determinate_at" *)
diff --git a/compose/Sem.v b/compose/Sem.v
@@ -27,7 +27,6 @@ Module Frame.
 
   Record t: Type := mk {
     ms: ModSem.t;
-    (* st_init: ms.(ModSem.state); *)
     st: ms.(ModSem.state); (* local state *)
   }.
 
@@ -80,7 +79,6 @@ Inductive step (ge: Ge.t): state -> trace -> state -> Prop :=
 
 | step_internal
     fr0 frs tr st0
-    (* (INTERNAL: fr0.(Frame.is_internal)) *)
     (STEP: Step (fr0.(Frame.ms)) fr0.(Frame.st) tr st0):
     step ge (State (fr0 :: frs))
          tr (State ((fr0.(Frame.update_st) st0) :: frs))
@@ -97,14 +95,9 @@ Inductive step (ge: Ge.t): state -> trace -> state -> Prop :=
 Section SEMANTICS.
 
   Variable p: program.
-  (* Variable init_skel: Skel.t. *)
-  (* Hypothesis LINKED: link_list (List.map Mod.skel p) = Some init_skel. *)
 
   Definition link_sk: option Sk.t := link_list (List.map Mod.sk p).
 
-  (* Definition init_skenv: option SkEnv.t := option_map (@Genv.globalenv (fundef unit) unit) init_sk. *)
-  (* Definition init_skenv (init_sk: Sk.t): SkEnv.t := (@Genv.globalenv (fundef (option signature)) unit) init_sk. *)
-
   Definition skenv_fill_internals (skenv: SkEnv.t): SkEnv.t :=
     skenv.(Genv_map_defs) (fun _ gd => Some
                                       match gd with
@@ -118,11 +111,6 @@ Section SEMANTICS.
 
   Definition load_modsems (skenv: SkEnv.t): list ModSem.t := List.map ((flip Mod.modsem) skenv) p.
 
-  (* Definition init_mem: option mem := option_join (option_map (@Genv.init_mem (fundef unit) unit) init_sk). *)
-  (* Definition init_mem (init_sk: Sk.t): option mem := (@Genv.init_mem (fundef (option signature)) unit) init_sk. *)
-
-  (* Definition init_genv: option Ge.t := *)
-  (*   option_map (fun skenv => (Ge.mk skenv (init_modsem skenv))) init_skenv. *)
   Definition load_genv (init_skenv: SkEnv.t): Ge.t :=
     let (system, skenv) := load_system init_skenv in
     (system :: (load_modsems init_skenv), init_skenv).

diff --git a/demo/mutrec/MutrecABproof.v b/demo/mutrec/MutrecABproof.v
@@ -836,7 +836,7 @@ Section LXSIM.
                 econs 2; eauto; esplits.
                 -- eapply plus_two with (t1 := []) (t2 := []); ss.
                    ++ econs; eauto.
-                      { (* ez - determinate_at *)
+                      { 
                         eapply lift_determinate_at; ss; des_ifs; eauto.
                         econs; eauto.
                         - ii; ss. inv H; inv H0; ss.

diff --git a/demo/mutrec/MutrecABspec.v b/demo/mutrec/MutrecABspec.v
@@ -27,7 +27,6 @@ Section MODSEM.
   Variable skenv_link: SkEnv.t.
   Variable p: unit.
   Let skenv: SkEnv.t := skenv_link.(SkEnv.project) sk_link.
-  (* Let ge: genv := Build_genv (skenv.(SkEnv.revive) p) p.(prog_comp_env). *)
   Let ge: SkEnv.t := skenv.
 
   Inductive state: Type :=

diff --git a/demo/mutrec/MutrecAproof.v b/demo/mutrec/MutrecAproof.v
@@ -10,7 +10,6 @@ Require Import MutrecHeader.
 Require Import MutrecA MutrecAspec.
 Require Import Simulation.
 Require Import Skeleton Mod ModSem SimMod SimModSemLift SimSymb SimMemLift AsmregsC MatchSimModSem.
-(* Require SimMemInjC. *)
 Require SoundTop.
 Require SimMemInjC SimMemInjInvC.
 Require Import Clightdefs.
@@ -111,12 +110,11 @@ Inductive match_states_internal: nat -> MutrecAspec.state -> Clight.state -> Pro
 | match_callstate_nonzero
     idx i m_src m_tgt
     fptr
-    (* targs tres cconv *)
     (RANGE: 0 <= i.(Int.intval) < MAX)
     (FINDF: Genv.find_funct (Smallstep.globalenv (modsem2 skenv_link prog)) fptr = Some (Internal func_f))
     (IDX: (idx > 3)%nat)
   :
-    match_states_internal idx (Callstate i m_src) (Clight.Callstate fptr (Tfunction (* targs tres cconv) *)
+    match_states_internal idx (Callstate i m_src) (Clight.Callstate fptr (Tfunction
                                                                             (Tcons tint Tnil) tint cc_default)
                                                                     [Vint i] Kstop m_tgt)
 | match_returnstate
@@ -126,40 +124,6 @@ Inductive match_states_internal: nat -> MutrecAspec.state -> Clight.state -> Pro
 .
 
 
-(* Inductive match_states_internal: MutrecAspec.state -> Clight.state -> Prop := *)
-(* | match_callstate_nonzero_memoized *)
-(*     i m_src m_tgt *)
-(*     fptr blk memov *)
-(*     (* targs tres cconv *) *)
-(*     (FINDF: Genv.find_funct (Smallstep.globalenv (modsem2 skenv_link prog)) fptr = Some (Internal func_f)) *)
-(*     (SYMB: Genv.find_symbol skenv_link _memoized = Some blk) *)
-(*     (MEMOLD: Mem.loadv *)
-(*                Mint64 m_tgt *)
-(*                (Vptr blk (Ptrofs.repr (size_chunk Mint64 * i.(Int.intval)))) = Some (Vint memov)) *)
-(*     (MEMOIZED: memov = sum i) *)
-(*   : *)
-(*     match_states_internal (Callstate i m_src) (Clight.Callstate fptr (Tfunction (* targs tres cconv) *) *)
-(*                                                                         (Tcons tint Tnil) tint cc_default) *)
-(*                                                                 [Vint i] Kstop m_tgt) *)
-(* | match_callstate_nonzero_nonmemoized *)
-(*     i m_src m_tgt *)
-(*     fptr blk memov *)
-(*     (* targs tres cconv *) *)
-(*     (FINDF: Genv.find_funct (Smallstep.globalenv (modsem2 skenv_link prog)) fptr = Some (Internal func_f)) *)
-(*     (SYMB: Genv.find_symbol skenv_link _memoized = Some blk) *)
-(*     (MEMOLD: Mem.loadv *)
-(*                Mint64 m_tgt *)
-(*                (Vptr blk (Ptrofs.repr (size_chunk Mint64 * i.(Int.intval)))) = Some (Vint memov)) *)
-(*     (NONMEMOIZED: memov.(Int.intval) < 0) *)
-(*   : *)
-(*     match_states_internal (Callstate i m_src) (Clight.Callstate fptr (Tfunction (* targs tres cconv) *) *)
-(*                                                                         (Tcons tint Tnil) tint cc_default) *)
-(*                                                                 [Vint i] Kstop m_tgt) *)
-(* | match_returnstate *)
-(*     i m_src m_tgt *)
-(*   : *)
-(*     match_states_internal (Returnstate i m_src) (Clight.Returnstate (Vint i) Kstop m_tgt) *)
-(* . *)
 
 Inductive match_states (sm_init: SimMem.t)
           (idx: nat) (st_src0: MutrecAspec.state) (st_tgt0: Clight.state) (sm0: SimMem.t): Prop :=
@@ -169,7 +133,6 @@ Inductive match_states (sm_init: SimMem.t)
     (MCOMPATTGT: st_tgt0.(ClightC.get_mem) = sm0.(SimMem.tgt))
     (MWF: SimMem.wf sm0)
     (MLE: SimMem.le sm_init sm0)
-    (* (IDX: (idx > 3)%nat) *)
 .
 
 Lemma g_blk_exists
@@ -203,7 +166,6 @@ Proof.
   rename b into g_blk.
   eexists. splits; et.
   { unfold Genv.find_funct_ptr. des_ifs. }
-  (* exploit (@SkEnv.project_revive_precise _ _ skenv_link); eauto. *)
   { inv INCL.
     exploit (CSk.of_program_prog_defmap prog signature_of_function); et. rewrite T. intro S.
 
@@ -272,7 +234,6 @@ Proof.
         { apply Ord.lift_idx_spec.
           instantiate (1:=2%nat). nia. }
 
-        (* left. *)
         eapply plus_left with (t1 := E0) (t2 := E0); ss.
         { econs; eauto.
           { eapply modsem2_determinate; eauto. }
@@ -306,7 +267,6 @@ Proof.
 
         apply star_refl.
       * refl.
-      (* * refl. *)
       * right. eapply CIH; eauto. econs; ss; eauto.
         replace (Int.repr 0) with (sum Int.zero).
         { econs; eauto. }
@@ -485,7 +445,6 @@ Proof.
           clarify.
           eexists (Args.mk _ [Vint (Int.sub i (Int.repr 1))] _).
           exists sm0.
-          (* eexists (SimMemInjInv.mk minj _ _ (SimMemInjInv.mem_inv sm_init)). *)
           esplits; ss; eauto.
           { econs; ss; eauto.
             instantiate (1:=Vptr g_blk Ptrofs.zero).
@@ -514,11 +473,7 @@ Proof.
 
           esplits.
           { econs; eauto. }
-          { apply MLE2. (* eassumption. *)
-            (* etrans; eauto. refl. *)
-            (* eapply SimMemInjInv.unlift_spec; eauto. *)
-            (* econs; eauto. } *)
-          }
+          { apply MLE2. }
 
           left. pfold. econs; eauto. i; des. econs 2; eauto.
           {
@@ -626,7 +581,7 @@ Proof.
               econs 2.
             - etrans; eauto. etrans; eauto.
               eapply SimMemInjInvC.unlift_spec; eauto. econs; eauto.
-            (* - omega. *) }
+          }
       }
 
       { hexploit VAL; eauto. i. des. clarify.
@@ -819,17 +774,11 @@ Proof.
       * econs; eauto.
         { econs; eauto. omega. }
         { refl. }
-        (* { omega. } *)
 
   - (* init progress *)
     i.
     des. inv SAFESRC.
     inv SIMARGS; ss.
-    (* hexploit (SimMemInjC.skenv_inject_revive prog); et. { apply SIMSKENV. } intro SIMSKENV0; des. *)
-
-    (* exploit make_match_genvs; eauto. { apply SIMSKENV. } intro SIMGE. *)
-
-    (* hexploit (@fsim_external_inject_eq); try apply FINDF; eauto. clear FPTR. intro FPTR. *)
 
     esplits; eauto. econs; eauto.
     + instantiate (1:= func_f).

diff --git a/demo/mutrec/MutrecAspec.v b/demo/mutrec/MutrecAspec.v
@@ -19,7 +19,6 @@ Section MODSEM.
   Variable skenv_link: SkEnv.t.
   Variable p: unit.
   Let skenv: SkEnv.t := skenv_link.(SkEnv.project) prog.(CSk.of_program signature_of_function).
-  (* Let ge: genv := Build_genv (skenv.(SkEnv.revive) prog) prog.(prog_comp_env). *)
 
   Inductive state: Type :=
   | Callstate
@@ -47,8 +46,6 @@ Section MODSEM.
       (SYMB: Genv.find_symbol skenv f_id = Some blk)
       (FPTR: args.(Args.fptr) = Vptr blk Ptrofs.zero)
       (RANGE: 0 <= i.(Int.intval) < MAX)
-      (* (DEF: Genv.find_funct skenv args.(Args.fptr) = *)
-      (*         Some (AST.Internal (mksignature [AST.Tint] (Some AST.Tint) cc_default))) *)
       (VS: args.(Args.vs) = [Vint i])
       (M: args.(Args.m) = m)
     :