This is the artifact for the paper "Conditional Contextual Refinement".
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.
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.
Now, you can either use the Docker image from the Docker Hub (make sure you have internet connection):
sudo docker run -it alxest/popl23ae /bin/bash
or, you can use the Docker image that we submitted:
sudo docker load < CCR.tar && sudo docker run -it alxest/popl23ae /bin/bash
.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):
git clone git@github.com:alxest/CCR.git && cd CCR && make
or you can use the raw source code that we submitted:
mv CCR.tar.gz fresh_directory && tar -xvf CCR.tar.gz && cd CCR && make
.To evaluate this artifact, we propose the following steps:
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.admit
or
Admitted.
(e.g., typing grep -ri "admit" --include="*.v" .
in
the project root should print nothing).-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.
Print Assumptions THEOREM
after a theorem. (e.g., try Print Assumptions adequacy_type2
at the end of the spc/Hoare.v
.)Fig. 1 (in examples/map directory)
MapStb
in MapHeader.vSec. 2.4 Incremental and modular verification of the running example
(in examples/map
directory)
Fig. 3 (in ems/ directory)
eventE
in ModSem.vEs
in ModSem.vMod.t
in ModSem.vrefines2
in ModSem.vrefines2_PreOrder
in ModSem.vrefines2_add
in ModSem.vFig. 4 (in ems/ directory)
Tr.t
in Behavior.v
Beh.of_program
in Behavior.v
ModL.compile
in ModSem.v
Fig. 5
sim_itree
in SimModSem.vFig. 6 (in spc/ directory)
URA.t
in PCM.viProp'
in IProp.vfspec
in HoarDef.v(alist gname fspec)
Module SMod
in HoareDef.vHoareCall
in HoardDef.vHoareFun
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
SModSem.initial_mr
field of SMemSem
in mem/Mem1.vMemStb
in mem/Mem1.vFig. 8 (in examples/repeat directory)
repeatF
in Repeat0.vsuccF
and addF
in Add0.vrepeat_spec
in Repeat1.vsucc_spec
in Add1.vcorrect
in RepeatAll.vTheorem 3.1 (Adequacy)
adequacy_local2
in ems/SimModSem.vTheorem 4.1 (Assumption Cancellation Theorem (ACT))
adequacy_type2
in spc/Hoare.vTheorem 4.2 (Extensionality)
adequacy_weaken
in spc/Weakening.vNote: 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.vTheorem 6.1 (Separate Compilation Correctness)
compile_behavior_improves
in imp/compiler_proof/Imp2AsmProof.vThe development uses the following non-constructive axioms (most of them are in lib/Axioms.v
).
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.)prop_extensinality
here)proof_irrelevance
here)functional_extensionality_dep
here)eq_rect_eq
here)constructive_definite_description
hereclassic
here)bisimulation_is_eq
here)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.