cap_machine.linking
From iris Require Import base.
From iris.program_logic Require Import language ectx_language ectxi_language.
From stdpp Require Import gmap fin_maps fin_sets.
From cap_machine Require Import addr_reg.
Section Linking.
Variable Symbols: Type.
Variable Symbols_eq_dec: EqDecision Symbols.
Variable Symbols_countable: Countable Symbols.
Variable Word: Type.
Variable can_address_only: Word -> (gset Addr) -> Prop.
Variable is_main: Word -> Prop.
Definition imports: Type := gset (Symbols * Addr).
Definition exports: Type := gmap Symbols Word.
Definition segment: Type := gmap Addr Word.
Definition pre_component: Type := (segment * imports * exports).
Inductive component: Type :=
| Lib: pre_component -> component
| Main: pre_component -> Word -> component.
Inductive well_formed_pre_comp: pre_component -> Prop :=
| wf_pre_intro:
forall (ms : gmap Addr Word) imp (exp : gmap Symbols Word)
(Hdisj: forall s, is_Some (exp !! s) -> ~ exists a, (s, a) ∈ imp)
(Hexp: forall (s : Symbols) (w : Word), exp !! s = Some w -> can_address_only w (dom ms))
(Himp: forall s a, (s, a) ∈ imp -> is_Some (ms !! a))
(Himpdisj: forall s1 s2 a, (s1, a) ∈ imp -> (s2, a) ∈ imp -> s1 = s2)
(Hnpwl: forall (a : Addr) (w : Word), ms !! a = Some w -> can_address_only w (dom ms)),
well_formed_pre_comp (ms, imp, exp).
Inductive well_formed_comp: component -> Prop :=
| wf_lib:
forall comp
(Hwf_pre: well_formed_pre_comp comp),
well_formed_comp (Lib comp)
| wf_main:
forall comp w_main
(Hwf_pre: well_formed_pre_comp comp)
(Hw_main_addr: can_address_only w_main (dom (comp.1.1)))
(Hw_main: is_main w_main),
well_formed_comp (Main comp w_main).
Inductive is_program: component -> Prop :=
| is_program_intro:
forall ms imp exp w_main
(Hnoimports: imp = ∅)
(Hwfcomp: well_formed_comp (Main (ms, imp, exp) w_main)),
is_program (Main (ms,imp, exp) w_main).
Definition resolve_imports (imp: imports) (exp: exports) (ms: segment) :=
set_fold (fun '(s, a) m => match exp !! s with Some w => <[a:=w]> m | None => m end) ms imp.
Lemma resolve_imports_spec:
forall imp exp ms a
(Himpdisj: forall s1 s2 a, (s1, a) ∈ imp -> (s2, a) ∈ imp -> s1 = s2),
((~ exists s, (s, a) ∈ imp) ->
(resolve_imports imp exp ms) !! a = ms !! a) /\
(forall s, (s, a) ∈ imp ->
(exp !! s = None /\ (resolve_imports imp exp ms) !! a = ms !! a) \/ (exists wexp, exp !! s = Some wexp /\ (resolve_imports imp exp ms) !! a = Some wexp)).
Proof.
intros imp exp ms a. eapply (set_fold_ind_L (fun m imp => (forall s1 s2 a, (s1, a) ∈ imp -> (s2, a) ∈ imp -> s1 = s2) -> ((~ exists s, (s, a) ∈ imp) -> m !! a = ms !! a) /\ (forall s, (s, a) ∈ imp -> (exp !! s = None /\ m !! a = ms !! a) \/ (exists wexp, exp !! s = Some wexp /\ m !! a = Some wexp))) (fun '(s, a) m => match exp !! s with Some w => <[a:=w]> m | None => m end)); eauto.
{ intros. split; auto. intros.
eapply elem_of_empty in H0; elim H0; auto. }
intros. destruct x. split.
{ intros. destruct (exp !! s).
- rewrite lookup_insert_ne; auto.
+ apply H0.
* intros. eapply H1; eapply elem_of_union; right; eauto.
* intro Y. destruct Y as [sy Hiny].
eapply H2. exists sy. eapply elem_of_union. right; eauto.
+ intro; subst a. eapply H2. exists s.
eapply elem_of_union. left. eapply elem_of_singleton. reflexivity.
- apply H0.
+ intros. eapply H1; eapply elem_of_union; right; eauto.
+ intro Y. destruct Y as [sy Hiny].
eapply H2. exists sy. eapply elem_of_union. right; auto. }
{ intros; destruct (exp !! s) eqn:Hexp.
- destruct (decide (f = a)).
+ subst f; rewrite lookup_insert.
right. assert (s0 = s) as ->; eauto.
eapply elem_of_union in H2. destruct H2.
* generalize (proj1 (elem_of_singleton _ _) H2). inversion 1; subst; auto.
* eapply (H1 s0 s a); [eapply elem_of_union_r; auto|eapply elem_of_union_l; eapply elem_of_singleton; eauto].
+ rewrite lookup_insert_ne; auto.
eapply elem_of_union in H2; destruct H2.
* erewrite elem_of_singleton in H2. inversion H2; congruence.
* eapply H0; auto.
intros; eapply H1; eapply elem_of_union; right; eauto.
- eapply elem_of_union in H2. destruct H2.
+ erewrite elem_of_singleton in H2. inversion H2; subst; clear H2.
left; split; auto. eapply (proj1 (H0 ltac:(intros; eapply H1; eapply elem_of_union; right; eauto))).
intro Y. destruct Y as [sy Hsy].
eapply H. replace s with sy; auto.
eapply H1; [eapply elem_of_union_r; eauto| eapply elem_of_union_l; eapply elem_of_singleton; eauto].
+ eapply H0; auto.
intros; eapply H1; eapply elem_of_union_r; eauto. }
Unshelve. Fail idtac. Admitted.
Lemma resolve_imports_spec_in:
forall imp exp ms a s
(Himpdisj: forall s1 s2 a, (s1, a) ∈ imp -> (s2, a) ∈ imp -> s1 = s2),
(s, a) ∈ imp ->
(exp !! s = None /\ (resolve_imports imp exp ms) !! a = ms !! a) \/ (exists wexp, exp !! s = Some wexp /\ (resolve_imports imp exp ms) !! a = Some wexp).
Proof.
intros. eapply resolve_imports_spec; eauto.
Unshelve. Fail idtac. Admitted.
Lemma resolve_imports_spec_not_in:
forall imp exp ms a
(Himpdisj: forall s1 s2 a, (s1, a) ∈ imp -> (s2, a) ∈ imp -> s1 = s2),
((~ exists s, (s, a) ∈ imp) ->
(resolve_imports imp exp ms) !! a = ms !! a).
Proof.
intros. eapply resolve_imports_spec; eauto.
Unshelve. Fail idtac. Admitted.
Inductive link_pre_comp: pre_component -> pre_component -> pre_component -> Prop :=
| link_pre_comp_intro:
forall ms1 ms2 ms imp1 imp2 imp exp1 exp2 exp
(Hms_disj: forall a, is_Some (ms1 !! a) -> is_Some (ms2 !! a) -> False)
(Hexp: exp = merge (fun o1 o2 => match o1 with | Some _ => o1 | None => o2 end) exp1 exp2)
(Himp: forall s a, (s, a) ∈ imp <-> (((s, a) ∈ imp1 \/ (s, a) ∈ imp2) /\ exp !! s = None))
(Hms: ms = resolve_imports imp2 exp (resolve_imports imp1 exp (map_union ms1 ms2))),
link_pre_comp (ms1, imp1, exp1) (ms2, imp2, exp2) (ms, imp, exp).
Inductive link: component -> component -> component -> Prop :=
| link_lib_lib:
forall comp1 comp2 comp
(Hlink: link_pre_comp comp1 comp2 comp)
(Hwf_l: well_formed_comp (Lib comp1))
(Hwf_r: well_formed_comp (Lib comp2)),
link (Lib comp1) (Lib comp2) (Lib comp)
| link_lib_main:
forall comp1 comp2 comp w_main
(Hlink: link_pre_comp comp1 comp2 comp)
(Hwf_l: well_formed_comp (Lib comp1))
(Hwf_r: well_formed_comp (Main comp2 w_main)),
link (Lib comp1) (Main comp2 w_main) (Main comp w_main)
| link_main_lib:
forall comp1 comp2 comp w_main
(Hlink: link_pre_comp comp1 comp2 comp)
(Hwf_l: well_formed_comp (Main comp1 w_main))
(Hwf_r: well_formed_comp (Lib comp2)),
link (Main comp1 w_main) (Lib comp2) (Main comp w_main).
Inductive is_context (c comp p: component): Prop :=
| is_context_intro:
forall (His_program: link c comp p /\ is_program p),
is_context c comp p.
End Linking.
From iris.program_logic Require Import language ectx_language ectxi_language.
From stdpp Require Import gmap fin_maps fin_sets.
From cap_machine Require Import addr_reg.
Section Linking.
Variable Symbols: Type.
Variable Symbols_eq_dec: EqDecision Symbols.
Variable Symbols_countable: Countable Symbols.
Variable Word: Type.
Variable can_address_only: Word -> (gset Addr) -> Prop.
Variable is_main: Word -> Prop.
Definition imports: Type := gset (Symbols * Addr).
Definition exports: Type := gmap Symbols Word.
Definition segment: Type := gmap Addr Word.
Definition pre_component: Type := (segment * imports * exports).
Inductive component: Type :=
| Lib: pre_component -> component
| Main: pre_component -> Word -> component.
Inductive well_formed_pre_comp: pre_component -> Prop :=
| wf_pre_intro:
forall (ms : gmap Addr Word) imp (exp : gmap Symbols Word)
(Hdisj: forall s, is_Some (exp !! s) -> ~ exists a, (s, a) ∈ imp)
(Hexp: forall (s : Symbols) (w : Word), exp !! s = Some w -> can_address_only w (dom ms))
(Himp: forall s a, (s, a) ∈ imp -> is_Some (ms !! a))
(Himpdisj: forall s1 s2 a, (s1, a) ∈ imp -> (s2, a) ∈ imp -> s1 = s2)
(Hnpwl: forall (a : Addr) (w : Word), ms !! a = Some w -> can_address_only w (dom ms)),
well_formed_pre_comp (ms, imp, exp).
Inductive well_formed_comp: component -> Prop :=
| wf_lib:
forall comp
(Hwf_pre: well_formed_pre_comp comp),
well_formed_comp (Lib comp)
| wf_main:
forall comp w_main
(Hwf_pre: well_formed_pre_comp comp)
(Hw_main_addr: can_address_only w_main (dom (comp.1.1)))
(Hw_main: is_main w_main),
well_formed_comp (Main comp w_main).
Inductive is_program: component -> Prop :=
| is_program_intro:
forall ms imp exp w_main
(Hnoimports: imp = ∅)
(Hwfcomp: well_formed_comp (Main (ms, imp, exp) w_main)),
is_program (Main (ms,imp, exp) w_main).
Definition resolve_imports (imp: imports) (exp: exports) (ms: segment) :=
set_fold (fun '(s, a) m => match exp !! s with Some w => <[a:=w]> m | None => m end) ms imp.
Lemma resolve_imports_spec:
forall imp exp ms a
(Himpdisj: forall s1 s2 a, (s1, a) ∈ imp -> (s2, a) ∈ imp -> s1 = s2),
((~ exists s, (s, a) ∈ imp) ->
(resolve_imports imp exp ms) !! a = ms !! a) /\
(forall s, (s, a) ∈ imp ->
(exp !! s = None /\ (resolve_imports imp exp ms) !! a = ms !! a) \/ (exists wexp, exp !! s = Some wexp /\ (resolve_imports imp exp ms) !! a = Some wexp)).
Proof.
intros imp exp ms a. eapply (set_fold_ind_L (fun m imp => (forall s1 s2 a, (s1, a) ∈ imp -> (s2, a) ∈ imp -> s1 = s2) -> ((~ exists s, (s, a) ∈ imp) -> m !! a = ms !! a) /\ (forall s, (s, a) ∈ imp -> (exp !! s = None /\ m !! a = ms !! a) \/ (exists wexp, exp !! s = Some wexp /\ m !! a = Some wexp))) (fun '(s, a) m => match exp !! s with Some w => <[a:=w]> m | None => m end)); eauto.
{ intros. split; auto. intros.
eapply elem_of_empty in H0; elim H0; auto. }
intros. destruct x. split.
{ intros. destruct (exp !! s).
- rewrite lookup_insert_ne; auto.
+ apply H0.
* intros. eapply H1; eapply elem_of_union; right; eauto.
* intro Y. destruct Y as [sy Hiny].
eapply H2. exists sy. eapply elem_of_union. right; eauto.
+ intro; subst a. eapply H2. exists s.
eapply elem_of_union. left. eapply elem_of_singleton. reflexivity.
- apply H0.
+ intros. eapply H1; eapply elem_of_union; right; eauto.
+ intro Y. destruct Y as [sy Hiny].
eapply H2. exists sy. eapply elem_of_union. right; auto. }
{ intros; destruct (exp !! s) eqn:Hexp.
- destruct (decide (f = a)).
+ subst f; rewrite lookup_insert.
right. assert (s0 = s) as ->; eauto.
eapply elem_of_union in H2. destruct H2.
* generalize (proj1 (elem_of_singleton _ _) H2). inversion 1; subst; auto.
* eapply (H1 s0 s a); [eapply elem_of_union_r; auto|eapply elem_of_union_l; eapply elem_of_singleton; eauto].
+ rewrite lookup_insert_ne; auto.
eapply elem_of_union in H2; destruct H2.
* erewrite elem_of_singleton in H2. inversion H2; congruence.
* eapply H0; auto.
intros; eapply H1; eapply elem_of_union; right; eauto.
- eapply elem_of_union in H2. destruct H2.
+ erewrite elem_of_singleton in H2. inversion H2; subst; clear H2.
left; split; auto. eapply (proj1 (H0 ltac:(intros; eapply H1; eapply elem_of_union; right; eauto))).
intro Y. destruct Y as [sy Hsy].
eapply H. replace s with sy; auto.
eapply H1; [eapply elem_of_union_r; eauto| eapply elem_of_union_l; eapply elem_of_singleton; eauto].
+ eapply H0; auto.
intros; eapply H1; eapply elem_of_union_r; eauto. }
Unshelve. Fail idtac. Admitted.
Lemma resolve_imports_spec_in:
forall imp exp ms a s
(Himpdisj: forall s1 s2 a, (s1, a) ∈ imp -> (s2, a) ∈ imp -> s1 = s2),
(s, a) ∈ imp ->
(exp !! s = None /\ (resolve_imports imp exp ms) !! a = ms !! a) \/ (exists wexp, exp !! s = Some wexp /\ (resolve_imports imp exp ms) !! a = Some wexp).
Proof.
intros. eapply resolve_imports_spec; eauto.
Unshelve. Fail idtac. Admitted.
Lemma resolve_imports_spec_not_in:
forall imp exp ms a
(Himpdisj: forall s1 s2 a, (s1, a) ∈ imp -> (s2, a) ∈ imp -> s1 = s2),
((~ exists s, (s, a) ∈ imp) ->
(resolve_imports imp exp ms) !! a = ms !! a).
Proof.
intros. eapply resolve_imports_spec; eauto.
Unshelve. Fail idtac. Admitted.
Inductive link_pre_comp: pre_component -> pre_component -> pre_component -> Prop :=
| link_pre_comp_intro:
forall ms1 ms2 ms imp1 imp2 imp exp1 exp2 exp
(Hms_disj: forall a, is_Some (ms1 !! a) -> is_Some (ms2 !! a) -> False)
(Hexp: exp = merge (fun o1 o2 => match o1 with | Some _ => o1 | None => o2 end) exp1 exp2)
(Himp: forall s a, (s, a) ∈ imp <-> (((s, a) ∈ imp1 \/ (s, a) ∈ imp2) /\ exp !! s = None))
(Hms: ms = resolve_imports imp2 exp (resolve_imports imp1 exp (map_union ms1 ms2))),
link_pre_comp (ms1, imp1, exp1) (ms2, imp2, exp2) (ms, imp, exp).
Inductive link: component -> component -> component -> Prop :=
| link_lib_lib:
forall comp1 comp2 comp
(Hlink: link_pre_comp comp1 comp2 comp)
(Hwf_l: well_formed_comp (Lib comp1))
(Hwf_r: well_formed_comp (Lib comp2)),
link (Lib comp1) (Lib comp2) (Lib comp)
| link_lib_main:
forall comp1 comp2 comp w_main
(Hlink: link_pre_comp comp1 comp2 comp)
(Hwf_l: well_formed_comp (Lib comp1))
(Hwf_r: well_formed_comp (Main comp2 w_main)),
link (Lib comp1) (Main comp2 w_main) (Main comp w_main)
| link_main_lib:
forall comp1 comp2 comp w_main
(Hlink: link_pre_comp comp1 comp2 comp)
(Hwf_l: well_formed_comp (Main comp1 w_main))
(Hwf_r: well_formed_comp (Lib comp2)),
link (Main comp1 w_main) (Lib comp2) (Main comp w_main).
Inductive is_context (c comp p: component): Prop :=
| is_context_intro:
forall (His_program: link c comp p /\ is_program p),
is_context c comp p.
End Linking.