pl/frap
1
0
Fork 0
mirror of https://github.com/achlipala/frap.git synced 2024-09-19 19:57:13 +00:00
Code Issues Projects Releases Packages Wiki Activity Actions

Revising for Wednesday's lecture

Browse source
This commit is contained in:
Adam Chlipala 2021-04-24 15:55:15 -04:00
parent 513e01bd3b
commit 7e4068d5db
2 changed files with 10 additions and 12 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

14
Connecting.v
View file

@ -110,7 +110,7 @@ Proof.
intros; apply (shatter_word a).
Qed.
Hint Resolve shatter_word_0 : core.
Local Hint Resolve shatter_word_0 : core.
Require Import Coq.Logic.Eqdep_dec.
@ -182,7 +182,7 @@ End BIT_WIDTH.
(** * A modification of last chapter's language, to use words instead of naturals *)
(* There actually isn't much to say about this language and its separation
* logic. We are almost just copying and pasting word operations for [nat]
* logic. We are almost just copying and pasting with word operations for [nat]
* operations. Also, we drop failure and dynamic memory allocation, since they
* would just distract from the main point. *)
@ -314,7 +314,7 @@ Module MixedEmbedded(Import BW : BIT_WIDTH).
t.
Qed.
Hint Resolve split_empty_bwd' : core.
Local Hint Resolve split_empty_bwd' : core.
Theorem extra_lift : forall (P : Prop) p,
P
@ -457,7 +457,7 @@ Module MixedEmbedded(Import BW : BIT_WIDTH).
unfold star, himp in *; simp; eauto 7.
Qed.
Hint Constructors hoare_triple : core.
Global Hint Constructors hoare_triple : core.
Lemma invert_Bind : forall {result' result} (c1 : cmd result') (c2 : result' -> cmd result) P Q,
hoare_triple P (Bind c1 c2) Q
@ -658,7 +658,7 @@ Module MixedEmbedded(Import BW : BIT_WIDTH).
unfold ptsto; reflexivity.
Qed.
Hint Constructors step : core.
Global Hint Constructors step : core.
Lemma progress : forall {result} (c : cmd result) P Q,
hoare_triple P c Q
@ -2732,7 +2732,7 @@ Module MixedToDeep(Import BW : BIT_WIDTH).
equality.
Qed.
Hint Constructors eval DE.step : core.
Local Hint Constructors eval DE.step : core.
Lemma translate_exp_sound' : forall V v e,
translate_exp V v e
@ -2751,7 +2751,7 @@ Module MixedToDeep(Import BW : BIT_WIDTH).
induct 1; simplify; eauto.
Qed.
Hint Resolve translate_exp_sound translate_exp_sound' : core.
Local Hint Resolve translate_exp_sound translate_exp_sound' : core.
Lemma not_stuck_loop : forall V (c : cmd (wrd * wrd)) s,
translate (rt := TwoWords) translate_loop_body V c s

8
frap_book.tex
View file

@ -4592,7 +4592,7 @@ We also go into more detail on one avant-garde approach, of verified compilation
\section{Where Does the Buck Stop?}
For any system where we really care about correctness (or its special case of security\index{security}), it is common to delineate a \emph{trusted code base (TCB)}\index{trusted code base}\index{TCB}: the parts of the system where bugs could invalidate correctness.
By implication, system components outside the TCB can be arbitarily buggy without endangering correctness.
By implication, system components outside the TCB can be arbitrarily buggy without endangering correctness.
When we use Coq, the Coq proof checker itself is in the TCB.
Implicitly, all the infrastructure below the proof checker is also trusted.
@ -4623,7 +4623,7 @@ Oversimplifying a bit, we are considering what is the ``last level'' of a proof
The easiest ``last level'' connection is via \emph{extraction}\index{extraction}, which translates Gallina programs into functional programs in languages like OCaml\index{OCaml}, Haskell\index{Haskell}, and Scheme\index{Scheme}.
Other proof assistants than Coq tend to include similar extraction facilities.
When the formal object of study is already a purely functional program, extraction is a very natural fit.
Its main downside are TCB size and performance.
Its main downsides are TCB size and performance.
On the TCB front, a variety of compilers, including the one for extraction itself, remain trusted.
On the performance front, it is often possible to make a functional program run much faster or use much less memory by translating it to, say, a C program that doesn't rely on garbage collection.
@ -4671,7 +4671,7 @@ These connections across languages may enlarge the TCB significantly, but we can
We may also want to give modules first-class status in Coq and prove the correctness of linking mechanisms.
In concert with verified compilers\index{compiler verification}, possibilities open up to do linking across languages without expanding the TCB.
All languages can be compiled to some common format, like assembly language, and the compiled version of each libary can be given a specification in a common logical format, like a particular Hoare logic.
All languages can be compiled to some common format, like assembly language, and the compiled version of each library can be given a specification in a common logical format, like a particular Hoare logic.
With all the pieces in place, we wind up with the semantics of the common language in the TCB, but the compilers and all aspects of their source languages stay outside the TCB.
@ -4772,7 +4772,6 @@ More involved and raising new complications is the rule for loops; see the Coq c
\begin{proof}
In other words, every execution of the target-language system can be mimicked by one of the source-language system, where the states are connected throughout by some relation that we choose.
A good choice is the relation $\sim$ defined by this inference rule.
$$\infer{(h, v \uplus v', s) \sim (h, c)}{
\dscomp{v}{c}{s}
}$$
@ -4784,7 +4783,6 @@ More involved and raising new complications is the rule for loops; see the Coq c
Actually, we need to modify our translation judgment so that it also applies to ``silly'' intermediate states of execution in the target language.
For instance, we wind up with $\skipe$s that are quickly stepped away, yet those configurations must be related to source configurations by $\sim$.
Here is one example of the extra rules that we need to add to make our induction hypothsis strong enough.
$$\infer{\dscomp{v}{x \leftarrow \mt{Return} \; n; c(x)}{\mt{skip}; s}}{
v(y) = n
& \dscomp{v}{c(n)}{s}