Giter VIP home page Giter VIP logo

ccr's Introduction

Conditional Contextual Refinement

This is the artifact for the paper "Conditional Contextual Refinement".

List of Claims

We claim that the artifact provides Coq development for the results in the paper (modulo small simplifications for expository purposes) and compiles without any problem.

Download, installation, and sanity-testing

The artifact is presented as a Docker image ("CCR-docker.tar"), but we are also submitting the latest source code ("CCR.tar.gz") just in case. Both of these are also publicly available here and here. If there is a need to update our artifact in the middle of the review process, we will make the latest version available on those links.

Installing via Docker image

  1. Install Docker (version 20.10.14 is tested).

Now, you can either use the Docker image from the Docker Hub (make sure you have internet connection):

  1. Run sudo docker run -it alxest/popl23ae /bin/bash

or, you can use the Docker image that we submitted:

  1. Run sudo docker load < CCR.tar && sudo docker run -it alxest/popl23ae /bin/bash.

Installing manually with raw source code

  1. Install opam in your system with the version at least 2.1.0.
  2. Make a fresh directorcy, install a local opam switch and install the dependencies:
mkdir fresh_directory && cd fresh_directory &&
opam switch create . ocaml.4.13.0 &&
eval $(opam env) &&
opam repo add coq-released "https://coq.inria.fr/opam/released" &&
opam config env &&
opam pin add coq 8.15.2 -y &&
opam pin add coq-paco 4.1.2 -y &&
opam pin add coq-itree 4.0.0 -y &&
opam pin add coq-ordinal 0.5.2 -y &&
opam pin add coq-stdpp 1.7.0 -y &&
opam pin add coq-iris 3.6.0 -y &&
opam pin add coq-compcert 3.11 -y &&
opam pin add ocamlbuild 0.14.1 -y

Now, you can either use the source code from the Github (make sure you have internet connection):

  1. Run git clone [email protected]:alxest/CCR.git && cd CCR && make

or you can use the raw source code that we submitted:

  1. Run mv CCR.tar.gz fresh_directory && tar -xvf CCR.tar.gz && cd CCR && make.

Evaluation Instructions

To evaluate this artifact, we propose the following steps:

  1. Confirm that the Coq development compiles without any problem. To do so, type git clean -xf . in the project root directory if you have previously built the Coq development or are using the Docker image. Check that no .vo file remains (e.g., typing find . -iname "*.vo" in the project root should print nothing). Then, run make -jN where N is the number of cores you wish to use.
  2. Check that the source code does not contain any admit or Admitted. (e.g., typing grep -ri "admit" --include="*.v" . in the project root should print nothing).
  3. Read the Section "Mapping from the paper to the Coq development" and check that the Coq development indeed corresponds to the paper's presentation
  4. Check that the project is hosted in the public repository (including an issue tracker) with open source license. We have also setup public chat room to accommodate collaboration with others.
  5. Check that the development supports extraction of examples to OCaml, which can actually be executed. The script below runs "echo" example (in the tech report) which takes (scanf) integers indefinitely, and when you put -1, it will print the integers you entered so far in a reverse order. You can run the scripts as follows in the project root directory.
    • "cd ./extract; ./run.sh; cd .." extracts and runs examples written in EMS (abstractions and implementation of Echo, etc) using the extraction mechanism of Interaction Trees.
    • "cd ./imp/compiler_extract; ./run.sh; cd .." builds IMP compiler, compiles an example down to the assembly using CompCert, and runs it.
  6. (optional) Check that the development is not using any more axioms than the ones specified in Section "Axioms". You can execute Print Assumptions THEOREM after a theorem. (e.g., try Print Assumptions adequacy_type2 at the end of the spc/Hoare.v.)

Mapping from the paper to the Coq development

Fig. 1 (in examples/map directory)

  • module I_Map --> MapI.v
  • module A_Map --> MapA.v
  • pre/post conditions S_Map --> MapStb in MapHeader.v
  • module M_Map (L200) --> MapM.v

Sec. 2.4 Incremental and modular verification of the running example (in examples/map directory)

  • proof of I_Map ⊑_ctx <S0_Map ⊢ M_Map > -> MapIAproof.v
  • proof of <S0_Map ⊢ M_Map > ⊑_ctx <S_Map ⊢ A_Map > -> MapMAproof.v
  • proof of end-to-end refinement (I_Map ⊑_ctx <S_Map ⊢ A_Map >) -> MapIAproof.v

Fig. 3 (in ems/ directory)

  • E_P --> eventE in ModSem.v
  • E_EMS --> Es in ModSem.v
  • Mod --> Mod.t in ModSem.v
  • Mi ≤ctx Ma --> refines2 in ModSem.v
  • Vertical composition of contextual refinements --> refines2_PreOrder in ModSem.v
  • Horizontal composition of contextual refinements --> refines2_add in ModSem.v

Fig. 4 (in ems/ directory)

  • Trace --> Tr.t in Behavior.v
  • beh --> Beh.of_program in Behavior.v
  • concat --> ModL.compile in ModSem.v

Fig. 5

  • simulation relation --> sim_itree in SimModSem.v

Fig. 6 (in spc/ directory)

  • PCM --> URA.t in PCM.v
  • rProp --> iProp' in IProp.v
  • Cond --> fspec in HoarDef.v
  • Conds --> (alist gname fspec)
  • <S |-a M> --> Module SMod in HoareDef.v
  • WrapC --> HoareCall in HoardDef.v
  • WrapF --> HoareFun in HoardDef.v

Note: the gap between Coq development and paper's presentation of Fig. 6 originates from the additional features in Section 5, which are just briefly mentioned. Specifically, the ordinals comes from the extension on Section 5.1 and the additional arguments to pre/post conditions (varg_src, vret_src) comes from the extension on Section 5.3.

Fig. 7

  • 𝜎_Mem --> SModSem.initial_mr field of SMemSem in mem/Mem1.v
  • S_Mem --> MemStb in mem/Mem1.v

Fig. 8 (in examples/repeat directory)

  • repeat --> repeatF in Repeat0.v
  • succ, main --> succF and addF in Add0.v
  • H_RP --> repeat_spec in Repeat1.v
  • S_SC --> succ_spec in Add1.v
  • end-to-end refinement --> correct in RepeatAll.v

Theorem 3.1 (Adequacy)

  • adequacy_local2 in ems/SimModSem.v

Theorem 4.1 (Assumption Cancellation Theorem (ACT))

  • adequacy_type2 in spc/Hoare.v

Theorem 4.2 (Extensionality)

  • adequacy_weaken in spc/Weakening.v

Note: Indeed, we are proving stronger property than a mere extensionality here. stb_weaker in spc/STB.v allows not just extension of the specs, but also weakening/strengthening of the pre/post-conditions.

Lemma 4.3 (Safety)

  • safe_mods_safe in spc/Safe.v

Theorem 6.1 (Separate Compilation Correctness)

  • compile_behavior_improves in imp/compiler_proof/Imp2AsmProof.v

Axioms

The development uses the following non-constructive axioms (most of them are in lib/Axioms.v).

  • Functional form of the (non extensional) Axiom of Choice. (technically, it appears as relational_choice here and dependent_unique_choice here. However, combination of these two axioms are known to be equivalent to Functional form of the (non extensional) Axiom of Choice. Specifically, see Reification of dependent and non dependent functional relation are equivalent, and AC_rel + AC! = AC_fun here.)
  • System call semantics, following the style of CompCert
  • Propositional Extensionality. (prop_extensinality here)
  • Proof Irrelevance. (proof_irrelevance here)
  • Functional Extensionality. (functional_extensionality_dep here)
  • Invariance by Substitution of Reflexive Equality Proofs, UIP. (eq_rect_eq here)
  • Constructive form of definite description. constructive_definite_description here
  • Excluded middle. (classic here)
  • Bisimulation on itree implies Leibniz equality. (bisimulation_is_eq here)

Chat Room

If you are involved in this project in any way -- either the user or the developer -- you are encouraged to join the CCR-project discord server for chat.

ccr's People

Contributors

alxest avatar minkiminki avatar dongjaelee1 avatar merhs avatar prooooveit avatar tomtomjhj avatar

Stargazers

SoonWon Moon avatar avatar Jiho Lee avatar

Watchers

Jeehoon Kang avatar avatar avatar Chung-Kil Hur avatar avatar SoonWon Moon avatar avatar avatar avatar

Forkers

hilyun07 ppapill0n petrosyh damhiya goldenrabbit-23 rememberiom lunawood

ccr's Issues

Minor Refactorings

  • simplify mainpre Type
  • rename SMod -> ModS (parallel with ModL)
  • main_body / mainBody / mainbody
  • main_spec mainspec
  • Give a name to ((flip ModL.get_modsem) skenv)? it is used in Hoare.v and might be frequently used in other places too.
  • The need for Echo2 is somewhat awkward; put APC inside hCallE so that it can be wholly removed?

Relaxing equiv

df29abd
It turns out the proof becomes quite annoying; let's do this when it is definitely needed.

Idea: define extensionality lemmas for possible speedup? 

Let eq_ext: forall X (x0 x1 ctx: X), x0 = x1 -> x1 = ctx -> x0 = ctx. Proof. intros. subst; eauto. Qed.
Goal 0 =1. Time do 1000 (erewrite f_equal; [|reflexivity]). Show Proof. Abort.
Goal 0 =1. Time do 1000 (eapply Red._einit; [Red._ctx 0|reflexivity]). Show Proof. Abort.
Goal 0 =1. Time do 1000 (eapply eq_ext; [reflexivity|]). Show Proof. Abort.

Bug on ired_r case

| [ |- (gpaco3 (_sim_itree ) _ _ _ _ _ (, ITree.bind' _ (Ret _))) ] =>
apply sim_r_bind_ret_l

add recursion

Global Environment translation

Generating global environment when linking modules, Imp just appends lists but compcert performs ptree acrobatics, and the order of the pointers may not be preserved. To translate, need some injection/permutation.

  1. When proving the whole program refinement, insert a layer between Imp-compcert, Imp', which is Imp with nondeterministic genv.
  2. When generating Imp genv, apply the ptree-order.
  3. Do not use ptree_combine when generating compcert genv.
  4. Reorder compcert genv after ptree_combine.

Engineering PCM 

Structure cmraT := CmraT' {
  cmra_car :> Type;
}.
Variable A: cmraT.
Let b: Type := A.
Set Printing All.

works, but if we use Class instead of Structure, it doesn't work...

  • Using Op/Valid typeclasses - It is good that I can reuse these operators again, but it mandated too much unfolding during the proof...
  • mixin structure (why does it work, even though it is not a class??)

TODO: add WSeal 

Section TEST.
  Variable A: Type.
  Let A' := Seal.sealing "my_seal" A.
  Variable a: A.
  Fail Check (a: A').
End TEST.

Module WSeal.
  Definition sealing (_: string) X (x: X) := x.
  Lemma sealing_eq key X (x: X): sealing key x = x.
  Proof. refl. Qed.
End WSeal.
Opaque WSeal.sealing.

Ltac seal_with key x :=
  replace x with (WSeal.sealing key x); [|eapply WSeal.sealing_eq].
Ltac seal x :=
  let key := fresh "key" in
  assert (key:= "_deafult_");
  seal_with key x.
Ltac unseal x :=
  match (type of x) with
  | string => repeat rewrite (@WSeal.sealing_eq x) in *; try clear x
  | _ => repeat rewrite (@WSeal.sealing_eq _ _ x) in *;
         repeat match goal with
                | [ H: string |- _ ] => try clear H
                end
  end
.

Notation "☃ y" := (WSeal.sealing _ y) (at level 60, only printing).
Goal forall x, 5 + 5 = x. i. seal 5. seal x. Fail progress cbn. unseal key0. unseal 5. progress cbn. Abort.
Goal forall x y z, x + y = z. i. seal x. seal y. unseal y. unseal key. Abort.
Goal forall x y z, x + y = z. i. seal_with "a" x. seal_with "b" y. unseal "a". unseal "b". Abort.

Section TEST.
  Variable A: Type.
  Let A' := WSeal.sealing "my_seal" A.
  Variable a: A.
  Check (a: A').
End TEST.

TODO: simplify rE

In order to impose certain well-behavior (e.g., fp-update) mechanically, current definition of rE is somewhat sophisticated.
Now, however, such condition is already imposed by hCall event infrastructure (user doesn't have direct access to resources).
Therefore, we can simplify rE so that it just has get/set events (then, the simulation relation will become simpler too).

e.g., current Put event is interpreted this way:

| Put mn mr fr =>
          guarantee(URA.updatable (URA.add (mrs mn) hd) (URA.add mr fr));;
          Ret (((update mrs mn mr), fr :: tl), tt)

but, we can remove the guarantee condition here, and put it in the "decoration" part of hCallE

Remove admits in ModSem.v

Goal: ditto.
Description:
Define equivalence class between ModSem.t, prove that this equivalence relation preserves behavior, and finally prove that LHS/RHS of add_comm (and add_assoc) are in equivalence class.
Read the code, ask @alxest in offline if needed.

Refactor/revise

  • Hoare01proof.v performance
  • Stack01proof.v proof & performance && merge Minki's work
  • Echo01proof.v proof minor fixes
  • Add iGuard
  • Add entry resource
  • better cosmetics in fspec (meta-variable)
  • tactic for hiding the itree except for the first command
  • Add "Seal" in GRA.to_URA so that user doesn't need to use Local Transparent/Opaque

Revert "alloc to malloc changed" commit

The main branch has "alloc to malloc changed" commit (e981f37), which renames alloc to malloc. I think I reverted it before, but somehow this commit exists in the main branch...
As suggested by @alxest before, I think we should use alloc in the development, not malloc.

Simulation Transitivity

Let foo be o <- Choose Ord;; do sth finishes in o steps.
There are simulations between foo;; foo;; tau Ret 0 and foo;; tau Ret 0,
and between foo;; tau Ret 0 and tau;; Ret 0.
However, foo;; foo;; tau Ret 0 ~ tau Ret 0 is not true. i.e. simulation is not transitive!

The problem is that there is no upper bound of possible simulation indexes.
If each index is smaller than kappa, or if we allow an itree to branch only with a set less than Ord (which is not possible due to Hoareproof1),
we may be able to prove transitivity.
(Roughly saying, if itr0 ~ itr1 with an index i0 and itr1 ~ itr2 with an index i1,
itr0 ~ itr2 with the kappa * i0 + i1)

Or, we can use transitivity of behavioral refinement directly, instead of transitivity of simulation.
Then, we should define intermediate interaction trees.

Imp2Csharpminor compiler proof

I shared some idea with @alxest on Imp2Clight compiler correctness proof.

We want to prove the following:

Theorem Imp2ClightCorrect: for all I1, I2, ..., In : Imp program,
beh(link(mem, I1, ..., In)) > mapBeh(c_beh(c_link(i2c(I1), ..., i2c(In)))).

Main problem is that the definitions of data are different between Imp and CompCert(CC):

  1. memory: malloc in Imp is nondeterministic / malloc in CC gives next empty memory
  2. global environment: link in Imp is just concatenation / link in CC uses PTree.combine
  3. value: Imp uses Z / CC uses int64 (for our case)

This inequality makes the main proof more complex.
To resolve 1 and 2, current idea is to define a layer between Imp and CC, using mem* and link*, which follows CC:

Theorem Imp2ClightCorrect: for all I1, I2, ..., In : Imp program,
beh(link(mem, I1, ..., In)) > beh(link*(mem*, I1, ..., In)) > mapBeh(c_beh(c_link(i2c(I1), ..., i2c(In)))).

There is no clear solution to 3. value for now; we are considering changing the definition of Imp's value to follow CC.

Some other details to consider:

  • Defining an (partial)inverse function of mapBeh and proving some kind of 'weak bijection'. This can be postponed; I think mapBeh can be defined in an convincing way.
  • String to positive conversion is needed. Currently, a parameter s2p is declared and used, and realized in extracted using CC's function. We can actually define a bijective function from string to positive and use it.
  • Event definition is different. Imp's Syscall do not record memory, but CC does record Syscall-memory interaction. Two ideas: 1. assumes that syscalls we treat do not change memory, 2. change Imp's Syscall definition.
  • Value is different, as mentioned earlier. Using CC's value model is current idea.

TODO:

  • define src semantics (mem*, link*); correctness proof can be postponed
  • define mapBeh.
  • define simulation relations; refer CC's match_states.

Minor discussions

  • Change the definition of Impure
  • Fix bug in YPM
  • Add notation for entails-update?
  Goal forall P Q, ⌞(P -* Q)⌟ <-> (P ⊢ Q).
  Proof.
    split; i.
    - rr in H. r. ii. specialize (H ε). hexploit1 H.
      { eapply URA.wf_unit. }
      hexploit1 H; ss.
      specialize (H r).
      rewrite URA.unit_idl in H.
      eapply H; et.
    - rr. rr in H. ii.
      eapply H; eauto. rr in H0.
  Abort.
  Goal forall P Q, (P -* Q) ε <-> (P ⊢ Q).
  Proof.
    split; i.
    - rr in H. r. ii. specialize (H r). rewrite URA.unit_idl in H. eapply H; et.
    - rr. rr in H. ii. rewrite URA.unit_idl in *. eapply H; et.
  Qed.
  Goal forall P Q, iHyp ((P ** Q) -* ( |=> P)) ε.
    i. iIntro. iDestruct A. unfold iHyp in *. r. rewrite URA.unit_idl. esplits. i.
    esplits; try apply A; et.
    admit "ez".
  Qed.

Include return value to 'event_sys'

Current 'event_sys' do not include return value, and STS of a 'vis' state is deterministic.
Including return value to 'event_sys' should make it nondeterministic*.
(cf. CompCert's 'Event_syscall' do include return value)
edit: *Including return value do not necessarily make 'vis' nondeterministic.

Recommend Projects

  • React photo React

    A declarative, efficient, and flexible JavaScript library for building user interfaces.

  • Vue.js photo Vue.js

    🖖 Vue.js is a progressive, incrementally-adoptable JavaScript framework for building UI on the web.

  • Typescript photo Typescript

    TypeScript is a superset of JavaScript that compiles to clean JavaScript output.

  • TensorFlow photo TensorFlow

    An Open Source Machine Learning Framework for Everyone

  • Django photo Django

    The Web framework for perfectionists with deadlines.

  • D3 photo D3

    Bring data to life with SVG, Canvas and HTML. 📊📈🎉

Recommend Topics

  • javascript

    JavaScript (JS) is a lightweight interpreted programming language with first-class functions.

  • web

    Some thing interesting about web. New door for the world.

  • server

    A server is a program made to process requests and deliver data to clients.

  • Machine learning

    Machine learning is a way of modeling and interpreting data that allows a piece of software to respond intelligently.

  • Game

    Some thing interesting about game, make everyone happy.

Recommend Org

  • Facebook photo Facebook

    We are working to build community through open source technology. NB: members must have two-factor auth.

  • Microsoft photo Microsoft

    Open source projects and samples from Microsoft.

  • Google photo Google

    Google ❤️ Open Source for everyone.

  • D3 photo D3

    Data-Driven Documents codes.