Update contents as of 2020 Oct.

.gitignore

@@ -6,4 +6,9 @@
 *.rej
 *.toc
 *.vo
+*.vos
+*.vok
+.lia.cache
 Makefile.conf
+Makefile.coq
+Makefile.coq.conf

Makefile

@@ -1,11 +1,12 @@
-all: lf plf vfa qc
+all: lf plf vfa qc vc
 
-.PHONY: lf plf vfa qc
+.PHONY: lf plf vfa qc vc
 
 lf: doc/pdf/lf.pdf
 plf: doc/pdf/plf.pdf
 vfa: doc/pdf/vfa.pdf
 qc: doc/pdf/qc.pdf
+vc: doc/pdf/vc.pdf
 
 doc/pdf/lf.pdf: src/lf/all.pdf
 	mkdir -p doc/pdf
@@ -23,24 +24,45 @@ doc/pdf/qc.pdf: src/qc/all.pdf
 	mkdir -p doc/pdf
 	mv src/qc/all.pdf doc/pdf/qc.pdf
 
+doc/pdf/vc.pdf: src/vc/all.pdf
+	mkdir -p doc/pdf
+	mv src/vc/all.pdf doc/pdf/vc.pdf
+
 src/lf/all.pdf:
-	make -C src/lf all
+	-patch -N -d src/lf < src/lf-Preface.v.patch
+	make -C src/lf
 	-patch -N -d src/lf < src/Makefile.patch
-	make -C src/lf all.pdf
+	make -C src/lf -f Makefile.coq all.pdf
 
 src/plf/all.pdf:
-	make -C src/plf all
+	-patch -N -d src/plf < src/plf-Preface.v.patch
+	-patch -N -d src/plf < src/Hoare.v.patch
+	make -C src/plf
 	-patch -N -d src/plf < src/Makefile.patch
-	make -C src/plf all.pdf
+	make -C src/plf -f Makefile.coq all.pdf
 
 src/vfa/all.pdf:
-	make -C src/vfa all
+	-patch -N -d src/vfa < src/vfa-Preface.v.patch
+	-patch -N -d src/vfa < src/Extract.v.patch
+	-patch -N -d src/vfa < src/Redblack.v.patch
+	make -C src/vfa
 	-patch -N -d src/vfa < src/Makefile.patch
-	make -C src/vfa all.pdf
+	make -C src/vfa -f Makefile.coq all.pdf
 
 src/qc/all.pdf:
+	-patch -N -d src/qc < src/qc-Preface.v.patch
 	-patch -N -d src/qc < src/Typeclasses.v.patch
 	-patch -N -d src/qc < src/QuickChickTool.v.patch
-	make -C src/qc all
+	make -C src/qc
 	-patch -N -d src/qc < src/Makefile.patch
-	make -C src/qc all.pdf	
+	make -C src/qc -f Makefile.coq all.pdf
+
+src/vc/all.pdf:
+	-patch -N -d src/vc < src/vc-Preface.v.patch
+	-patch -N -d src/vc < src/Verif_sumarray.v.patch
+	-patch -N -d src/vc < src/Verif_reverse.v.patch
+	-patch -N -d src/vc < src/Verif_strlib.v.patch
+	-patch -N -d src/vc < src/Verif_hash.v.patch
+	make -C src/vc
+	-patch -N -d src/vc < src/Makefile.patch
+	make -C src/vc -f Makefile.coq all.pdf

README.md

@@ -3,23 +3,26 @@ _sf_
 
 Mirror of the [Software Foundations](http://softwarefoundations.cis.upenn.edu/) series of books.  Includes generated PDFs.
 
-- B. Pierce, et al. (2019) [“Logical Foundations”](doc/pdf/lf.pdf)  
-  _Version 5.6 (09 Jan 2019, Coq 8.8.2)_
+- B. Pierce, et al. (2020) [“Logical Foundations”](doc/pdf/lf.pdf)  
+  _Version 5.8 (2020-09-09 20:57, Coq 8.12)_
 
-- B. Pierce, et al. (2019) [“Programming Language Foundations”](doc/pdf/plf.pdf)  
-  _Version 5.7 (08 Feb 2019, Coq 8.8.2)_
+- B. Pierce, et al. (2020) [“Programming Language Foundations”](doc/pdf/plf.pdf)  
+  _Version 5.8 (2020-09-09 21:10, Coq 8.12)_
 
-- A. Appel (2018) [“Verified Functional Algorithms”](doc/pdf/vfa.pdf)  
-  _Version 1.4 (25 Aug 2018, Coq 8.8.2)_
+- A. Appel (2020) [“Verified Functional Algorithms”](doc/pdf/vfa.pdf)  
+  _Version 1.4 (2020-08-07 17:12, Coq 8.9.1 or later)_
 
-- L. Lampropoulos and B. Pierce (2018) [“QuickChick: Property-Based Testing in Coq”](doc/pdf/qc.pdf)  
-  _Version 1.0 (09 Oct 2018, Coq 8.8.2)_
+- L. Lampropoulos and B. Pierce (2020) [“QuickChick: Property-Based Testing in Coq”](doc/pdf/qc.pdf)  
+  _Version 1.1 (2020-10-14 10:24, Coq 8.12)_
+
+- A. Appel and Q. Cao (2020) [“Verifiable C”](doc/pdf/vc.pdf)  
+  _Version 0.9.7 (2020-09-18 15:40, Coq 8.12) Compatible with VST 2.6 (July 2020)_
 
 
 Usage
 -----
 
-To regenerate the PDFs, ensure Coq, QuickChick, and LaTeX are installed, then:
+To regenerate the PDFs, ensure Coq, QuickChick, VST and LaTeX are installed, then:
 
 ```
 $ make
@@ -29,7 +32,26 @@ $ make
 
 The [Makefiles](src/Makefile.patch) are patched during the build process, so that chapters are generated in the right order, and the LaTeX nesting limit is not reached.
 
-Similarly, the [Typeclasses](src/Typeclasses.v.patch) and [QuickChickTool](src/QuickChickTool.v.patch) chapters of the QuickChick book are patched, so that a diacritic does not confuse LaTeX, and code listings appear in the output as intended.
+Similarly, the following chapters are patched:
+
+- Logical Foundation book
+  - [Preface](src/lf-Preface.v.patch) _To fill BibTeX info_
+- Programming Language Foundation book
+  - [Preface](src/plf-Preface.v.patch) _To fill BibTeX info_
+- Verified Functional Algorithms book
+  - [Preface](src/vfa-Preface.v.patch) _To fill BibTeX info_
+  - [Extract](src/Extract.v.patch) _To escape code listings_
+  - [Redblack](src/Redblack.v.patch) _To escape code listings_
+- QuickChick book
+  - [Preface](src/qc-Preface.v.patch) _To fill BibTeX info_
+  - [Typeclasses](src/Typeclasses.v.patch) _To combine diacritic mark to avoid LaTeX confusion_
+  - [QuickChickTool](src/QuickChickTool.v.patch) _To escape code listings_
+- Verifiable C book
+  - [Preface](src/vc-Preface.v.patch) _To fill BibTeX info_
+  - [Verif_sumarray](src/Verif_sumarray.v.patch) _To escape code listings_
+  - [Verif_reverse](src/Verif_reverse.v.patch) _To escape code listings_
+  - [Verif_strlib](src/Verif_strlib.v.patch) _To escape code listings_
+  - [Verif_hash](src/Verif_hash.v.patch) _To escape code listings_
 
 
 About

src/Extract.v.patch

@@ -0,0 +1,25 @@
+--- Extract.v.orig	2020-11-03 14:07:26.986781600 +0900
++++ Extract.v	2020-11-03 17:51:52.039637300 +0900
+@@ -356,8 +356,10 @@
+     you will find the file [test_searchtree.ml]. You can
+     run it using the OCaml toplevel with these commands:
+
++<<
+ # #use "searchtree.ml";;
+ # #use "test_searchtree.ml";;
++>>
+
+ On a recent machine with a 2.9 GHz Intel Core i9 that prints:
+
+@@ -368,9 +370,11 @@
+ That execution uses the bytecode interpreter.  The native compiler
+ will have better performance:
+
++<<
+ $ ocamlopt -c searchtree.mli searchtree.ml
+ $ ocamlopt searchtree.cmx -open Searchtree test_searchtree.ml -o test_searchtree
+ $ ./test_searchtree
++>>
+
+ On the same machine that prints,
+

src/Hoare.v.patch

@@ -0,0 +1,11 @@
+--- Hoare.v.orig	2020-11-03 13:34:32.671636100 +0900
++++ Hoare.v	2020-11-03 13:35:40.251175700 +0900
+@@ -461,7 +461,7 @@
+       X := 3
+       {{ X = 3 }}
+
+-      {{ (0 <= X /\ X <= 5) [X |-> 3]  (that is, 0 <= 3 /\ 3 <= 5)
++      {{ (0 <= X /\ X <= 5) [X |-> 3] }} (that is, 0 <= 3 /\ 3 <= 5)
+       X := 3
+       {{ 0 <= X /\ X <= 5 }}
+ *)

src/Makefile.patch

@@ -1,8 +1,8 @@
---- Makefile
-+++ Makefile
-@@ -16,14 +16,17 @@
+--- Makefile.coq.orig	2020-11-03 12:37:48.421365500 +0900
++++ Makefile.coq	2020-11-03 12:41:37.736258200 +0900
+@@ -19,14 +19,17 @@
  # definitions, like the list of .v files or the path to Coq
- include Makefile.conf
+ include Makefile.coq.conf
 
 +# Generate chapters in the right order
 +reverse=$(if $1,$(call reverse,$(wordlist 2,$(words $1),$1))) $(firstword $1)
@@ -12,22 +12,21 @@
 +VFILES            := $(call reverse,$(COQMF_VFILES))
  MLIFILES          := $(COQMF_MLIFILES)
  MLFILES           := $(COQMF_MLFILES)
- ML4FILES          := $(COQMF_ML4FILES)
+ MLGFILES          := $(COQMF_MLGFILES)
  MLPACKFILES       := $(COQMF_MLPACKFILES)
  MLLIBFILES        := $(COQMF_MLLIBFILES)
 -CMDLINE_VFILES    := $(COQMF_CMDLINE_VFILES)
 +CMDLINE_VFILES    := $(call reverse,$(COQMF_CMDLINE_VFILES))
  INSTALLCOQDOCROOT := $(COQMF_INSTALLCOQDOCROOT)
  OTHERFLAGS        := $(COQMF_OTHERFLAGS)
  COQ_SRC_SUBDIRS   := $(COQMF_COQ_SRC_SUBDIRS)
-@@ -170,7 +173,9 @@
-
- COQFLAGS?=-q $(OPT) $(COQLIBS) $(OTHERFLAGS)
- COQCHKFLAGS?=-silent -o $(COQLIBS)
--COQDOCFLAGS?=-interpolate -utf8
-+
+@@ -191,7 +194,8 @@
+ # these variables are meant to be overridden if you want to add *extra* flags
+ COQEXTRAFLAGS?=
+ COQCHKEXTRAFLAGS?=
+-COQDOCEXTRAFLAGS?=
 +# Work around the LaTeX nesting limit
-+COQDOCFLAGS?=-interpolate -utf8 -p '\usepackage{enumitem}\setlistdepth{9}\setlist[itemize,1]{label=$$\bullet$$}\setlist[itemize,2]{label=$$\bullet$$}\setlist[itemize,3]{label=$$\bullet$$}\setlist[itemize,4]{label=$$\bullet$$}\setlist[itemize,5]{label=$$\bullet$$}\setlist[itemize,6]{label=$$\bullet$$}\setlist[itemize,7]{label=$$\bullet$$}\setlist[itemize,8]{label=$$\bullet$$}\setlist[itemize,9]{label=$$\bullet$$}\renewlist{itemize}{itemize}{9}'
- COQDOCLIBS?=$(COQLIBS_NOML)
++COQDOCEXTRAFLAGS?=-p '\usepackage{enumitem}\setlistdepth{9}\setlist[itemize,1]{label=$$\bullet$$}\setlist[itemize,2]{label=$$\bullet$$}\setlist[itemize,3]{label=$$\bullet$$}\setlist[itemize,4]{label=$$\bullet$$}\setlist[itemize,5]{label=$$\bullet$$}\setlist[itemize,6]{label=$$\bullet$$}\setlist[itemize,7]{label=$$\bullet$$}\setlist[itemize,8]{label=$$\bullet$$}\setlist[itemize,9]{label=$$\bullet$$}\renewlist{itemize}{itemize}{9}'
 
- # The version of Coq being run and the version of coq_makefile that
+ # these flags do NOT contain the libraries, to make them easier to overwrite
+ COQFLAGS?=-q $(OTHERFLAGS) $(COQEXTRAFLAGS)

src/Redblack.v.patch

@@ -0,0 +1,14 @@
+--- Redblack.v.orig	2020-11-03 17:26:46.995120800 +0900
++++ Redblack.v	2020-11-03 17:53:01.108931700 +0900
+@@ -799,9 +799,11 @@
+     That execution uses the bytecode interpreter.  The native compiler
+     will have better performance:
+
++<<
+       $ ocamlopt -c redblack.mli redblack.ml
+       $ ocamlopt redblack.cmx -open Redblack test_searchtree.ml -o test_redblack
+       $ ./test_redblack
++>>
+
+ On the same machine that prints,
+

src/Typeclasses.v.patch

@@ -5,7 +5,7 @@
      [Transitive], etc.) and [Proper].  They are described in the
      second half of _A Gentle Introduction to Type Classes and
 -    Relations in Coq_, by Castéran and Sozeau.
-+    Relations in Coq_, by Casteran and Sozeau.
-     http://www.labri.fr/perso/casteran/CoqArt/TypeClassesTut/typeclassestut.pdf.
++    Relations in Coq_, by Castéran and Sozeau.
+     https://www.labri.fr/perso/casteran/CoqArt/TypeClassesTut/typeclassestut.pdf.
 
      A much larger collection of typeclasses for formalizing

src/Verif_hash.v.patch

@@ -0,0 +1,44 @@
+--- Verif_hash.v.orig	2020-11-04 17:33:32.700145200 +0900
++++ Verif_hash.v	2020-11-04 17:34:23.357208300 +0900
+@@ -284,11 +284,15 @@
+     [0 <= i <= Zlength contents].
+   In the LOCAL part of your loop invariant, try to use something like
+
++[[
+     temp _c (Vbyte (Znth i (contents ++ [Byte.zero]))
++]]
+
+   instead of 
+
++[[
+     temp _c (Znth i (map Vbyte (...)))
++]]
+
+   The reason is that [temp _c (Vint x)] or [temp _c (Vbyte y)] is much 
+   easier for Floyd to handle than [temp _c X]
+@@ -653,7 +657,9 @@
+
+   We will describe variable [r] something like this:
+
++[[
+   PROP() LOCAL(temp _r r) SEP(data_at Ews (tptr tcell) q r).
++]]
+
+   That is, pointer to a single word containing [q].  But when
+   we do [r = &(p->next)] we will have [r] pointing into the middle
+@@ -972,6 +978,7 @@
+
+ (**
+
++<<
+   void incr_list (struct cell **r0, char *s);
+
+   void incr (struct hashtable *table, char *s) {
+@@ -979,6 +986,7 @@
+     unsigned int b = h % N;
+     incr_list (& table->buckets[b], s);
+   }
++>>
+
+   The difficult part here is the function-argument, [ & table->buckets[b] ].
+   The precondition of the [incr_list] function requires just a single

src/Verif_reverse.v.patch

@@ -0,0 +1,17 @@
+--- Verif_reverse.v.orig	2020-11-03 20:52:56.284178000 +0900
++++ Verif_reverse.v	2020-11-03 20:54:09.738201600 +0900
+@@ -714,12 +714,14 @@
+   abbreviate_semax.
+ (** Now, our proof goal is:
+
++[[
+   semax Delta
+     (PROP ( )
+      LOCAL (temp _t y; temp _w w; temp _v v)
+      SEP (listrep s1 w; data_at Tsh t_list (h, y) v; listrep r y))
+     ((_v -> _tail) = _w; MORE_COMMANDS)
+     POSTCONDITION.
++]]
+
+ The next [forward] tactic will do symbolic execution of [v->tail = w]. *)
+    forward. (* v->tail = w;

src/Verif_strlib.v.patch

@@ -0,0 +1,12 @@
+--- Verif_strlib.v.orig	2020-11-03 20:54:56.722608400 +0900
++++ Verif_strlib.v	2020-11-03 20:55:20.647973000 +0900
+@@ -270,7 +270,9 @@
+ start_function.
+ (** Look at the proof goal below the line.  We have the assertion,
+
++[[
+   PROP ( )  LOCAL (temp _str str)  SEP (cstring sh s str))
++]]
+
+  When proving things about a string-manipulating function, the
+   first decision is:  Does this function treat the string _abstractly_

src/Verif_sumarray.v.patch

@@ -0,0 +1,14 @@
+--- Verif_sumarray.v.orig	2020-11-03 20:28:55.259059700 +0900
++++ Verif_sumarray.v	2020-11-03 20:51:38.352547500 +0900
+@@ -715,9 +715,11 @@
+   and we can see its SEP assertion in the precondition of the
+   current proof goal:
+
++[[
+    data_at Ews (tarray tuint 4)
+            (map Vint [Int.repr 1; Int.repr 2; Int.repr 3; Int.repr 4])
+            (gv _four)
++]]
+ *)
+
+ (** SEE ALSO: VC.pdf Chapter 20 (_Function calls_)

src/lf-Preface.v.patch

@@ -0,0 +1,23 @@
+--- Preface.v.orig	2020-11-03 13:07:54.400253800 +0900
++++ Preface.v	2020-11-03 19:04:14.280718100 +0900
+@@ -350,14 +350,14 @@
+ (** If you want to refer to this volume in your own writing, please
+     do so as follows:
+
+-   @book            {$FIRSTAUTHOR:SF$VOLUMENUMBER,
+-   author       =   {$AUTHORS},
+-   title        =   "$VOLUMENAME",
++   @book            {Pierce:SF1,
++   author       =   {Benjamin C. Pierce, Arthur Azevedo de Amorim, Chris Casinghino, Marco Gaboardi, Michael Greenberg, Cătălin Hriţcu, Vilhelm Sjöberg, Brent Yorgey},
++   title        =   "Logical Foundations",
+    series       =   "Software Foundations",
+-   volume       =   "$VOLUMENUMBER",
+-   year         =   "$VOLUMEYEAR",
++   volume       =   "1",
++   year         =   "2020",
+    publisher    =   "Electronic textbook",
+-   note         =   {Version $VERSION, \URLhttp://softwarefoundations.cis.upenn.edu },
++   note         =   {Version 5.8, \URLhttp://softwarefoundations.cis.upenn.edu },
+    }
+ *)
+