-
Notifications
You must be signed in to change notification settings - Fork 0
/
doc.html
100 lines (93 loc) · 6.03 KB
/
doc.html
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
<!DOCTYPE html PUBLIC "-//W3C//DTD XHTML 1.0 Strict//EN" "http://www.w3.org/TR/xhtml1/DTD/xhtml1-strict.dtd">
<html xmlns="http://www.w3.org/1999/xhtml">
<head>
<title>Mechanized Logical Relations for Termination-Insensitive Noninterference</title>
<meta http-equiv="Content-Type" content="text/html;charset=utf-8" />
<link href="html/coqdoc.css" rel="stylesheet" type="text/css" />
<link href="html/coqdocjs.css" rel="stylesheet" type="text/css"/>
</head>
<body onload="document.getElementById('content').focus()">
<div id="header">
<span class="left">
<span class="modulename"> <script> document.write(document.title) </script> </span>
</span>
<span class="button" id="toggle-proofs"></span>
<span class="right">
<a href="">Project Page</a>
<a href="vendor/modal-weakestpre/html/indexpage.html"> Index (MWP) </a>
<a href="vendor/modal-weakestpre/html/toc.html"> Table of Contents (MWP) </a>
<a href="html/indexpage.html"> Index (TINI) </a>
<a href="html/toc.html"> Table of Contents (TINI) </a>
</span>
</div>
<div id="content" tabindex="-1" onblur="document.getElementById('content').focus()">
<div id="main">
This document contains an entry point and overview of the documentation
for the development generated by the coqdoc
tool. See <a href="README.md#documentation">README.md</a> for
instructions on how to generate it if not already present.
<h2 id="modal-weakest-precondition-theory">Modal Weakest Precondition (MWP) Theory</h2>
Below we highlight definitions and lemmas that are important for logical relations model.
<ul>
<li>The general definition of the MWP predicate (Definition 3.4) is defined in
<a href="vendor/modal-weakestpre/html/mwp.mwp.html">mwp.v</a>.</li>
<li>All general derived proof rules for program reasoning are defined in
<a href="vendor/modal-weakestpre/html/mwp.mwp_lifting.html">mwp_lifting.v</a>.</li>
<li>The generic adequacy statement is stated and proved in
<a href="vendor/modal-weakestpre/html/mwp.mwp_adequacy.html">mwp_adequacy.v</a>.</li>
<li>The unary update-modality MWP instance (Example 3.1) is defined
in <a href="vendor/modal-weakestpre/html/mwp.mwp_modalities.mwp_fupd.html">mwp_fupd.v</a>.</li>
<li>The unary step-taking update-modality MWP instance (Example 3.2)
used in our unary logical-relations model is defined in
<a href="vendor/modal-weakestpre/html/mwp.mwp_modalities.mwp_step_fupd.html">mwp_step_fupd.v</a>.</li>
<li>The binary predicate (Example 3.5) used in our logical-relations model is
defined in
<a href="vendor/modal-weakestpre/html/mwp.mwp_modalities.ni_logrel.mwp_left.html">mwp_left.v</a>;
the inner predicate in
<a href="vendor/modal-weakestpre/html/mwp.mwp_modalities.ni_logrel.mwp_right.html">mwp_right.v</a></li>
<li>The binary predicate used in Section 5 is defined in
<a href="vendor/modal-weakestpre/html/mwp.mwp_modalities.ni_logrel.mwp_logrel_fupd.html">mwp_logrel_fupd.v</a></li>
<li>Lemmas about the interactions between the unary and binary predicates
(e.g. Lemma 3.7 and Lemma 5.1) are found in
<a href="vendor/modal-weakestpre/html/mwp.mwp_modalities.ni_logrel.ni_logrel_lemmas.html">ni_logrel_lemmas.v</a>
and
<a href="vendor/modal-weakestpre/html/mwp.mwp_modalities.ni_logrel.ni_logrel_fupd_lemmas.html">ni_logrel_fupd_lemmas.v</a></li>
</ul>
<h2 id="noninterference-development">Language, Type System and Logical Relations Model</h2>
<ul>
<li>A general theory of join semilattices, including the induced ordering
<a href="html/logrel_ifc.lambda_sec.lattice.html">lattice.v</a>.</li>
<li>Our language of study is defined in
<a href="html/logrel_ifc.lambda_sec.lang.html">lang.v</a>.</li>
<li>The types and type system are defined in
<a href="html/logrel_ifc.lambda_sec.types.html">types.v</a> and
<a href="html/logrel_ifc.lambda_sec.typing.html">typing.v</a>, respectively.</li>
<li>The unary logical relation is defined in
<a href="html/logrel_ifc.lambda_sec.logrel_unary.html">logrel_unary.v</a> and
its fundamental theorem is stated and proved in
<a href="html/logrel_ifc.lambda_sec.fundamental_unary.html">fundamental_unary.v</a>.</li>
<li>The binary logical relation is defined in
<a href="html/logrel_ifc.lambda_sec.logrel_binary.html">logrel_binary.v</a> and
its fundamental theorem is stated and proved in
<a href="html/logrel_ifc.lambda_sec.fundamental_binary.html">fundamental_binary.v</a>.</li>
<li>Termination-insensitive noninterference is proved in
<a href="html/logrel_ifc.lambda_sec.noninterference.html">noninterference.v</a>.</li>
<li>The introductory examples are found in
<a href="html/logrel_ifc.examples.arith.html">arith.v</a>,
<a href="html/logrel_ifc.examples.refs.html">refs.v</a>, and
<a href="html/logrel_ifc.examples.refs_implicit.html">refs_implicit.v</a>.</li>
<li>The example from Section 5.1 is found in
<a href="html/logrel_ifc.examples.report.html">report.v</a>.</li>
<li>The examples from Section 5.2 are found in
<a href="html/logrel_ifc.examples.value_dependent.html">value_dependent.v</a>
and
<a href="html/logrel_ifc.examples.value_dependent_pack.html">value_dependent_pack.v</a>.</li>
<li>The example from Section 5.3 is found in
<a href="html/logrel_ifc.examples.compute_with_cache.html">compute_with_cache.v</a>.</li>
<li>The parametricity theorems from Section 5.4 are shown in
<a href="html/logrel_ifc.examples.parametricity.html">parametricity.v</a>.</li>
</ul>
</div>
</div>
</body>
</html>