Skip to content
GitLab
Projects
Groups
Snippets
Help
Loading...
Help
What's new
7
Help
Support
Community forum
Keyboard shortcuts
?
Submit feedback
Contribute to GitLab
Sign in / Register
Toggle navigation
Open sidebar
FP
Stacked Borrows Coq
Commits
d0716dc6
Commit
d0716dc6
authored
Sep 17, 2019
by
Ralf Jung
Browse files
Options
Browse Files
Download
Email Patches
Plain Diff
more edits
parent
1d6d9a6d
Changes
1
Hide whitespace changes
Inline
Sidebyside
Showing
1 changed file
with
7 additions
and
5 deletions
+7
5
README.md
README.md
+7
5
No files found.
README.md
View file @
d0716dc6
...
...
@@ 20,7 +20,9 @@ You can also run them in Miri via "Tools"  "Miri", which will show a Stacked Bo
We have given informal proof sketches of optimizations based on Stacked Borrows
in the paper. To further increase confidence in the semantics, we formalized
these arguments in Coq (about 14KLOC). We have carried out the proofs of the
transformations mentioned in the paper:
`example1`
,
`example2`
,
`example2_down`
,
`example3_down`
.
transformations mentioned in the paper:
`example1`
,
`example2`
,
`example2_down`
,
`example3_down`
; as well as two more variants to complete the picture,
`example1_down`
and
`example3`
.
### What to look for
...
...
@@ 36,10 +38,10 @@ The directory structure is as follows:

Adequacy (that the simulation implies behavior inclusion) is in
`sim/local_adequacy.v`
,
`sim/global_adequacy.v`
, and
`sim/program.v`
.

Properties of the simulation with respect to the operational semantics are
proven in
`sim/body.v`
,
`sim/refl_pure_step.v`
,
`sim/refl_mem_step.v`
,
`sim/left_step.v`
,
`sim/right_step.v`
,
`sim/simple.v`
.

The
fundamental property that the simulation
is
r
ef
lexive is proven in
`sim/refl.v`
.

The
main invariant needed for these properties is in
`sim/invariant
.v`
.
`sim/left_step.v`
,
`sim/right_step.v`
.

The
main invariant needed for these properties
is
d
ef
ined in
`sim/invariant.v`
.

In
`sim/simple.v`
, we define an easiertouse but less powerful derived simulation relation
.

The
fundamental property that the simulation is reflexive for wellformed terms is proven in
`sim/refl
.v`
.
*
`theories/opt`
: Proofs of optimizations.
For example, `theories/opt/ex1.v` provides the proof that the optimized
...
...
Write
Preview
Markdown
is supported
0%
Try again
or
attach a new file
.
Attach a file
Cancel
You are about to add
0
people
to the discussion. Proceed with caution.
Finish editing this message first!
Cancel
Please
register
or
sign in
to comment