From aa0340d6bc613c1e987ed339cb585ff2a32a1ab1 Mon Sep 17 00:00:00 2001 From: Jason Gross Date: Mon, 2 Mar 2026 05:29:11 +0000 Subject: [PATCH] Update vc-current from upstream vc.tgz Update to latest version from softwarefoundations.cis.upenn.edu : Version 2.0 (2026-01-07 13:39, Rocq 9.0.0) Compatible with VST 2.16 --- vc-current/.devcontainer/.zshrc | 13 + vc-current/.devcontainer/Dockerfile | 58 + vc-current/.devcontainer/devcontainer.json | 70 +- vc-current/.devcontainer/hack.sh | 17 + vc-current/Bib.html | 4 +- vc-current/Bib.v | 2 +- vc-current/Hashfun.html | 150 +- vc-current/Hashfun.v | 2 +- vc-current/LICENSE | 2 +- vc-current/Makefile | 2 +- vc-current/Postscript.html | 36 +- vc-current/Postscript.v | 17 +- vc-current/Preface.html | 55 +- vc-current/Preface.v | 51 +- vc-current/README | 4 +- vc-current/Spec_stack.html | 42 +- vc-current/Spec_stack.v | 2 +- vc-current/Spec_stdlib.html | 126 +- vc-current/Spec_stdlib.v | 2 +- vc-current/Spec_triang.html | 16 +- vc-current/Spec_triang.v | 2 +- vc-current/VSU_intro.html | 14 +- vc-current/VSU_intro.v | 4 +- vc-current/VSU_main.html | 64 +- vc-current/VSU_main.v | 12 +- vc-current/VSU_main2.html | 34 +- vc-current/VSU_main2.v | 6 +- vc-current/VSU_stack.html | 76 +- vc-current/VSU_stack.v | 2 +- vc-current/VSU_stdlib.html | 51 +- vc-current/VSU_stdlib.v | 9 +- vc-current/VSU_stdlib2.html | 82 +- vc-current/VSU_stdlib2.v | 4 +- vc-current/VSU_triang.html | 24 +- vc-current/VSU_triang.v | 4 +- vc-current/Verif_append1.html | 108 +- vc-current/Verif_append1.v | 2 +- vc-current/Verif_append2.html | 68 +- vc-current/Verif_append2.v | 4 +- vc-current/Verif_hash.html | 250 +-- vc-current/Verif_hash.v | 2 +- vc-current/Verif_reverse.html | 108 +- vc-current/Verif_reverse.v | 12 +- vc-current/Verif_stack.html | 54 +- vc-current/Verif_stack.v | 2 +- vc-current/Verif_strlib.html | 289 ++- vc-current/Verif_strlib.v | 12 +- vc-current/Verif_sumarray.html | 100 +- vc-current/Verif_sumarray.v | 20 +- vc-current/Verif_triang.html | 248 +-- vc-current/Verif_triang.v | 16 +- vc-current/append.c | 60 +- vc-current/append.v | 405 ++-- vc-current/append32.v | 488 ----- vc-current/append64.v | 488 ----- vc-current/common/css/secf.css | 10 + vc-current/common/css/sf.css | 4 +- .../media/font/Open-Sans-300/LICENSE.txt | 404 ++-- .../font/Open-Sans-300italic/LICENSE.txt | 404 ++-- .../media/font/Open-Sans-600/LICENSE.txt | 404 ++-- .../font/Open-Sans-600italic/LICENSE.txt | 404 ++-- .../media/font/Open-Sans-700/LICENSE.txt | 404 ++-- .../font/Open-Sans-700italic/LICENSE.txt | 404 ++-- .../media/font/Open-Sans-800/LICENSE.txt | 404 ++-- .../font/Open-Sans-800italic/LICENSE.txt | 404 ++-- .../media/font/Open-Sans-italic/LICENSE.txt | 404 ++-- .../media/font/Open-Sans-regular/LICENSE.txt | 404 ++-- vc-current/common/media/image/secf_icon.jpg | Bin 0 -> 188756 bytes .../media/image/security_foundations_bg.jpg | Bin 0 -> 79541 bytes .../image/security_foundations_bg_unfaded.jpg | Bin 0 -> 51219 bytes vc-current/coqindex.html | 1854 +---------------- vc-current/hash.v | 534 +++-- vc-current/hash32.v | 886 -------- vc-current/hash64.v | 886 -------- vc-current/hints.v | 6 +- vc-current/index.html | 4 +- vc-current/main2.v | 441 ++-- vc-current/main232.v | 424 ---- vc-current/main264.v | 424 ---- vc-current/reverse.c | 80 +- vc-current/reverse.v | 386 ++-- vc-current/reverse32.v | 495 ----- vc-current/reverse64.v | 496 ----- vc-current/stack.v | 463 ++-- vc-current/stack2.v | 447 ++-- vc-current/stack232.v | 536 ----- vc-current/stack264.v | 536 ----- vc-current/stack32.v | 610 ------ vc-current/stack64.v | 610 ------ vc-current/stdlib.v | 366 ++-- vc-current/stdlib2.v | 416 ++-- vc-current/stdlib232.v | 502 ----- vc-current/stdlib264.v | 502 ----- vc-current/stdlib32.v | 392 ---- vc-current/stdlib64.v | 392 ---- vc-current/strlib.v | 426 ++-- vc-current/strlib32.v | 621 ------ vc-current/strlib64.v | 626 ------ vc-current/sumarray.c | 42 +- vc-current/sumarray.v | 399 ++-- vc-current/sumarray32.v | 435 ---- vc-current/sumarray64.v | 435 ---- vc-current/toc.html | 4 +- vc-current/triang2.v | 470 ++--- vc-current/triang232.v | 509 ----- vc-current/triang264.v | 509 ----- vc-current/vc.tgz | Bin 5930811 -> 6189426 bytes 107 files changed, 5706 insertions(+), 19307 deletions(-) create mode 100755 vc-current/.devcontainer/.zshrc create mode 100644 vc-current/.devcontainer/Dockerfile create mode 100644 vc-current/.devcontainer/hack.sh delete mode 100644 vc-current/append32.v delete mode 100644 vc-current/append64.v create mode 100644 vc-current/common/css/secf.css create mode 100644 vc-current/common/media/image/secf_icon.jpg create mode 100644 vc-current/common/media/image/security_foundations_bg.jpg create mode 100644 vc-current/common/media/image/security_foundations_bg_unfaded.jpg delete mode 100644 vc-current/hash32.v delete mode 100644 vc-current/hash64.v delete mode 100644 vc-current/main232.v delete mode 100644 vc-current/main264.v delete mode 100644 vc-current/reverse32.v delete mode 100644 vc-current/reverse64.v delete mode 100644 vc-current/stack232.v delete mode 100644 vc-current/stack264.v delete mode 100644 vc-current/stack32.v delete mode 100644 vc-current/stack64.v delete mode 100644 vc-current/stdlib232.v delete mode 100644 vc-current/stdlib264.v delete mode 100644 vc-current/stdlib32.v delete mode 100644 vc-current/stdlib64.v delete mode 100644 vc-current/strlib32.v delete mode 100644 vc-current/strlib64.v delete mode 100644 vc-current/sumarray32.v delete mode 100644 vc-current/sumarray64.v delete mode 100644 vc-current/triang232.v delete mode 100644 vc-current/triang264.v diff --git a/vc-current/.devcontainer/.zshrc b/vc-current/.devcontainer/.zshrc new file mode 100755 index 000000000..d38a73f47 --- /dev/null +++ b/vc-current/.devcontainer/.zshrc @@ -0,0 +1,13 @@ +autoload -U colors && colors +precmd() { + drawline="" + for i in {1..$COLUMNS}; drawline=" $drawline" + drawline="%U${drawline}%u" + PS1="%F{252}${drawline} +%B%F{124}%n:%~>%b%f " +} + +eval $(opam env) + +alias ls="ls --color" + diff --git a/vc-current/.devcontainer/Dockerfile b/vc-current/.devcontainer/Dockerfile new file mode 100644 index 000000000..10e717001 --- /dev/null +++ b/vc-current/.devcontainer/Dockerfile @@ -0,0 +1,58 @@ +FROM ubuntu:20.04 + +## BEGIN: RUNS AS ROOT + +# Create a user + +ARG USERNAME=cis5000 +ARG USER_UID=1000 +ARG USER_GID=$USER_UID + +RUN apt-get update -y + +RUN groupadd --gid $USER_GID $USERNAME \ + && useradd --uid $USER_UID --gid $USER_GID -m $USERNAME --shell /bin/zsh \ + # + # [Optional] Add sudo support. Omit if you don't need to install software after connecting. + && apt-get install -y sudo \ + && echo $USERNAME ALL=\(root\) NOPASSWD:ALL > /etc/sudoers.d/$USERNAME \ + && chmod 0440 /etc/sudoers.d/$USERNAME + +## Hack needs root permissions + +# See hack.sh +COPY hack.sh /tmp/hack.sh +RUN chmod +x /tmp/hack.sh +RUN /tmp/hack.sh + +RUN apt-get install -y build-essential +RUN apt-get install -y linux-libc-dev +RUN apt-get install -y m4 +RUN apt-get install -y opam +RUN apt-get install -y time +RUN apt-get install -y zip +RUN apt-get install -y zsh +RUN apt-get install -y libgmp3-dev +RUN DEBIAN_FRONTEND=noninteractive apt-get install -y pkg-config + +## Set up user environmnent +COPY .zshrc /home/$USERNAME/ + + +## Run in usermode + +# [Optional] Set the default user. Omit if you want to keep the default as root. +USER $USERNAME + +# Configure opam/ocaml +RUN opam init -y --disable-sandboxing --compiler=5.3.0 +RUN opam switch 5.3.0 +RUN opam install -y num +RUN opam repo add -y coq-released https://coq.inria.fr/opam/released +RUN opam pin add -y coq 9.0.0 +RUN opam install -y coq-simple-io +RUN opam install -y vscoq-language-server +RUN opam update -y +RUN opam upgrade -y +RUN eval `opam config env` + diff --git a/vc-current/.devcontainer/devcontainer.json b/vc-current/.devcontainer/devcontainer.json index 8202fd8e7..8cd956ad8 100644 --- a/vc-current/.devcontainer/devcontainer.json +++ b/vc-current/.devcontainer/devcontainer.json @@ -1,27 +1,49 @@ +// For format details, see https://aka.ms/devcontainer.json. For config options, see the +// README at: https://github.com/devcontainers/templates/tree/main/src/ubuntu { - "image": "bcpierce00/cis5000:8.17.1", - "customizations": { - "vscode": { - "extensions": ["maximedenes.vscoq"], - "settings": { - "coqtop.binPath" : "/home/coq/.opam/default/bin", - "files.exclude": { - "**/*.aux": true, - "**/*.glob": true, - "**/*.vo": true, - "**/*.vos": true, - "**/*.vok": true, - "**/*.html": true, - "**/.*.report": true, - "**/.*.cache": true - }, - "coq.loadCoqProject": true, - "coq.coqProjectRoot": ".", - "[coq]": { - "editor.tabSize": 2, - "editor.insertSpaces": true - } - } + "name": "Ubuntu", + // Or use a Dockerfile or Docker Compose file. More info: https://containers.dev/guide/dockerfile + "build": { + "dockerfile": "Dockerfile" + }, + + // Features to add to the dev container. More info: https://containers.dev/features. + // "features": {}, + + // Use 'forwardPorts' to make a list of ports inside the container available locally. + // "forwardPorts": [], + + // Use 'postCreateCommand' to run commands after the container is created. + // "postCreateCommand": "uname -a", + + // Configure tool-specific properties. + "customizations": { + "vscode": { + "extensions": [ + "maximedenes.vscoq" + ], + "settings": { + "coqtop.binPath" : "/home/cis5000/.opam/4.14.0/bin", + "files.exclude": { + "**/*.aux": true, + "**/*.glob": true, + "**/*.vo": true, + "**/*.vos": true, + "**/*.vok": true, + "**/*.html": true, + "**/.*.report": true, + "**/.*.cache": true + }, + "coq.loadCoqProject": true, + "coq.coqProjectRoot": ".", + "[coq]": { + "editor.tabSize": 2, + "editor.insertSpaces": true + } + } + } } - } + + // Uncomment to connect as root instead. More info: https://aka.ms/dev-containers-non-root. + // "remoteUser": "root" } diff --git a/vc-current/.devcontainer/hack.sh b/vc-current/.devcontainer/hack.sh new file mode 100644 index 000000000..b6d2c3f42 --- /dev/null +++ b/vc-current/.devcontainer/hack.sh @@ -0,0 +1,17 @@ +#!/usr/bin/env bash + +### HACK - workaround ubuntu libc6 version number bug see: https://forum.odroid.com/viewtopic.php?p=344373 + +mv /bin/uname /bin/uname.orig +tee -a /bin/uname <BibBibliography
-(* 2024-12-27 01:34 *)
+(* 2026-01-06 14:19 *)
diff --git a/vc-current/Bib.v b/vc-current/Bib.v index 4d96a92cb..99071ac18 100644 --- a/vc-current/Bib.v +++ b/vc-current/Bib.v @@ -89,4 +89,4 @@ *) -(* 2024-12-27 01:34 *) +(* 2026-01-06 14:19 *) diff --git a/vc-current/Hashfun.html b/vc-current/Hashfun.html index 0674e3773..0990a6de0 100644 --- a/vc-current/Hashfun.html +++ b/vc-current/Hashfun.html @@ -162,40 +162,40 @@

HashfunFunctional model of hash tabl
Require Import VST.floyd.functional_base.
-#[export] Instance EqDec_string: EqDec (list byte) := list_eq_dec Byte.eq_dec.
-Fixpoint hashfun_aux (h: Z) (s: list byte) : Z :=
+#[export] Instance EqDec_string: EqDec (list byte) := list_eq_dec Byte.eq_dec.
+Fixpoint hashfun_aux (h: Z) (s: list byte) : Z :=
 match s with
- | nil ⇒ h
- | c :: s' ⇒
-      hashfun_aux ((h × 65599 + Byte.signed c) mod Int.modulus) s'
+ | nil ⇒ h
+ | c :: s' ⇒
+      hashfun_aux ((h × 65599 + Byte.signed c) mod Int.modulus) s'
end.
-Definition hashfun (s: list byte) := hashfun_aux 0 s.
-Definition hashtable_contents := list (list (list byte × Z)).
+Definition hashfun (s: list byte) := hashfun_aux 0 s.
+Definition hashtable_contents := list (list (list byte × Z)).
Definition N := 109.
-Lemma N_eq : N = 109.
+Lemma N_eq : N = 109.
Proof. reflexivity. Qed.
#[export] Hint Rewrite N_eq : rep_lia.
Global Opaque N.
Definition empty_table : hashtable_contents :=
-  Zrepeat nil N.
-Fixpoint list_get (s: list byte) (al: list (list byte × Z)) : Z :=
+  Zrepeat nil N.
+Fixpoint list_get (s: list byte) (al: list (list byte × Z)) : Z :=
  match al with
- | (k,i) :: al' ⇒ if eq_dec s k then i else list_get s al'
- | nil ⇒ 0
+ | (k,i) :: al' ⇒ if eq_dec s k then i else list_get s al'
+ | nil ⇒ 0
 end.
-Fixpoint list_incr (s: list byte) (al: list (list byte × Z))
-              : list (list byte × Z) :=
+Fixpoint list_incr (s: list byte) (al: list (list byte × Z))
+              : list (list byte × Z) :=
  match al with
- | (k,i) :: al' ⇒ if eq_dec s k
-                      then (k, i +1)::al'
-                      else (k,i)::list_incr s al'
- | nil ⇒ (s, 1)::nil
+ | (k,i) :: al' ⇒ if eq_dec s k
+                      then (k, i +1)::al'
+                      else (k,i)::list_incr s al'
+ | nil ⇒ (s, 1)::nil
 end.
-Definition hashtable_get (s: list byte) (contents: hashtable_contents) : Z :=
-  list_get s (Znth (hashfun s mod (Zlength contents)) contents).
-Definition hashtable_incr (s: list byte) (contents: hashtable_contents)
+Definition hashtable_get (s: list byte) (contents: hashtable_contents) : Z :=
+  list_get s (Znth (hashfun s mod (Zlength contents)) contents).
+Definition hashtable_incr (s: list byte) (contents: hashtable_contents)
                      : hashtable_contents :=
-  let h := hashfun s mod (Zlength contents)
+  let h := hashfun s mod (Zlength contents)
  in let al := Znth h contents
  in upd_Znth h contents (list_incr s al).
@@ -205,7 +205,7 @@

HashfunFunctional model of hash tabl
-Lemma hashfun_inrange: ∀ s, 0 ≤ hashfun s ≤ Int.max_unsigned.
+Lemma hashfun_inrange: ∀ s, 0 ≤ hashfun s ≤ Int.max_unsigned.
Proof.
(* FILL IN HERE *) Admitted.
☐ @@ -219,9 +219,9 @@

HashfunFunctional model of hash tabl

Lemma hashtable_get_unfold:
- ∀ sigma (cts: list (list (list byte × Z) × val)),
- hashtable_get sigma (map fst cts) =
-  list_get sigma (Znth (hashfun sigma mod (Zlength cts)) (map fst cts)).
+ ∀ sigma (cts: list (list (list byte × Z) × val)),
+ hashtable_get sigma (map fst cts) =
+  list_get sigma (Znth (hashfun sigma mod (Zlength cts)) (map fst cts)).
Proof.
(* FILL IN HERE *) Admitted.
☐ @@ -236,8 +236,8 @@

HashfunFunctional model of hash tabl
Lemma Zlength_hashtable_incr:
 ∀ sigma cts,
-      0 < Zlength cts →
-      Zlength (hashtable_incr sigma cts) = Zlength cts.
+      0 < Zlength cts →
+      Zlength (hashtable_incr sigma cts) = Zlength cts.
Proof.
(* FILL IN HERE *) Admitted.
#[export] Hint Rewrite Zlength_hashtable_incr using list_solve : sublist.
@@ -253,9 +253,9 @@

HashfunFunctional model of hash tabl
Lemma Int_repr_eq_mod:
-   ∀ a, Int.repr (a mod Int.modulus) = Int.repr a.
+   ∀ a, Int.repr (a mod Int.modulus) = Int.repr a.
Proof.
-Print Int.eqm. (* This is a hint about how to prove the lemma *)
+Print Int.eqm. (* This is a hint about how to prove the lemma *)
Search Int.eqm. (* This is a hint about how to prove the lemma *)
(* FILL IN HERE *) Admitted.
@@ -267,18 +267,18 @@

HashfunFunctional model of hash tabl Lemma hashfun_aux_snoc:
  ∀ sigma h lo i,
-    0 ≤ lo →
-    lo ≤ i < Zlength sigma →
-  Int.repr (hashfun_aux h (sublist lo (i + 1) sigma)) =
-  Int.repr (hashfun_aux h (sublist lo i sigma) × 65599
-                                  + Byte.signed (Znth i sigma)).
+    0 ≤ lo →
+    lo ≤ i < Zlength sigma →
+  Int.repr (hashfun_aux h (sublist lo (i + 1) sigma)) =
+  Int.repr (hashfun_aux h (sublist lo i sigma) × 65599
+                                  + Byte.signed (Znth i sigma)).
Proof.
(* FILL IN HERE *) Admitted.
Lemma hashfun_snoc:
  ∀ sigma i,
-    0 ≤ i < Zlength sigma →
-  Int.repr (hashfun (sublist 0 (i + 1) sigma)) =
-  Int.repr (hashfun (sublist 0 i sigma) × 65599 + Byte.signed (Znth i sigma)).
+    0 ≤ i < Zlength sigma →
+  Int.repr (hashfun (sublist 0 (i + 1) sigma)) =
+  Int.repr (hashfun (sublist 0 i sigma) × 65599 + Byte.signed (Znth i sigma)).
Proof.
(* FILL IN HERE *) Admitted.
☐ @@ -307,14 +307,14 @@

HashfunFunctional model of hash tabl  Parameter table: Type.
 Parameter key : Type.
 Parameter empty: table.
- Parameter get: key → table → Z.
- Parameter incr: key → table → table.
- Axiom gempty: ∀ k, (* get-empty *)
-       get k empty = 0.
- Axiom gss: ∀ k t, (* get-set-same *)
-      get k (incr k t) = 1+(get k t).
- Axiom gso: ∀ j k t, (* get-set-other *)
-      j ≠ k → get j (incr k t) = get j t.
+ Parameter get: key → table → Z.
+ Parameter incr: key → table → table.
+ Axiom gempty: ∀ k, (* get-empty *)
+       get k empty = 0.
+ Axiom gss: ∀ k t, (* get-set-same *)
+      get k (incr k t) = 1+(get k t).
+ Axiom gso: ∀ j k t, (* get-set-other *)
+      j ≠ k → get j (incr k t) = get j t.
End COUNT_TABLE.

@@ -336,17 +336,17 @@

HashfunFunctional model of hash tabl
Module FunTable <: COUNT_TABLE.
- Definition table: Type := nat → Z.
- Definition key : Type := nat.
- Definition empty: table := fun k ⇒ 0.
- Definition get (k: key) (t: table) : Z := t k.
- Definition incr (k: key) (t: table) : table :=
-    fun k' ⇒ if Nat.eqb k' k then 1 + t k' else t k'.
- Lemma gempty: ∀ k, get k empty = 0.
+ Definition table: Type := nat → Z.
+ Definition key : Type := nat.
+ Definition empty: table := fun k ⇒ 0.
+ Definition get (k: key) (t: table) : Z := t k.
+ Definition incr (k: key) (t: table) : table :=
+    fun k' ⇒ if Nat.eqb k' k then 1 + t k' else t k'.
+ Lemma gempty: ∀ k, get k empty = 0.
(* FILL IN HERE *) Admitted.
- Lemma gss: ∀ k t, get k (incr k t) = 1+(get k t).
+ Lemma gss: ∀ k t, get k (incr k t) = 1+(get k t).
(* FILL IN HERE *) Admitted.
- Lemma gso: ∀ j k t, j ≠ k → get j (incr k t) = get j t.
+ Lemma gso: ∀ j k t, j ≠ k → get j (incr k t) = get j t.
(* FILL IN HERE *) Admitted.
End FunTable.
☐ @@ -371,33 +371,33 @@

HashfunFunctional model of hash tabl
Module IntHashTable <: COUNT_TABLE.
- Definition hashtable_invariant (cts: hashtable_contents) : Prop :=
-  Zlength cts = N ∧
-  ∀ i, 0 ≤ i < N →
-             list_norepet (map fst (Znth i cts))
-             ∧ Forall (fun s ⇒ hashfun s mod N = i) (map fst (Znth i cts)).
- Definition table := sig hashtable_invariant.
- Definition key := list byte.
+ Definition hashtable_invariant (cts: hashtable_contents) : Prop :=
+  Zlength cts = N ∧
+  ∀ i, 0 ≤ i < N →
+             list_norepet (map fst (Znth i cts))
+             ∧ Forall (fun s ⇒ hashfun s mod N = i) (map fst (Znth i cts)).
+ Definition table := sig hashtable_invariant.
+ Definition key := list byte.
 Lemma empty_invariant: hashtable_invariant empty_table.
 Proof.
(* FILL IN HERE *) Admitted.
-Lemma incr_invariant: ∀ k cts,
-      hashtable_invariant cts → hashtable_invariant (hashtable_incr k cts).
+Lemma incr_invariant: ∀ k cts,
+      hashtable_invariant cts → hashtable_invariant (hashtable_incr k cts).
Proof.
(* FILL IN HERE *) Admitted.
- Definition empty : table := exist _ _ empty_invariant.
- Definition get : key → table → Z :=
-                  fun k tbl ⇒ hashtable_get k (proj1_sig tbl).
- Definition incr : key → table → table :=
-       fun k tbl ⇒ exist _ _ (incr_invariant k _ (proj2_sig tbl)).
- Theorem gempty: ∀ k, get k empty = 0.
+ Definition empty : table := exist _ _ empty_invariant.
+ Definition get : key → table → Z :=
+                  fun k tbl ⇒ hashtable_get k (proj1_sig tbl).
+ Definition incr : key → table → table :=
+       fun k tbl ⇒ exist _ _ (incr_invariant k _ (proj2_sig tbl)).
+ Theorem gempty: ∀ k, get k empty = 0.
 Proof.
(* FILL IN HERE *) Admitted.
- Theorem gss: ∀ k t, get k (incr k t) = 1 + (get k t).
+ Theorem gss: ∀ k t, get k (incr k t) = 1 + (get k t).
 Proof.
(* FILL IN HERE *) Admitted.
- Theorem gso: ∀ j k t, (* get-set-other *)
-      j ≠ k → get j (incr k t) = get j t.
+ Theorem gso: ∀ j k t, (* get-set-other *)
+      j ≠ k → get j (incr k t) = get j t.
Proof.
(* FILL IN HERE *) Admitted.
☐ @@ -406,12 +406,12 @@

HashfunFunctional model of hash tabl
End IntHashTable.
-(* 2024-12-27 01:34 *)
+(* 2026-01-06 14:19 *)

diff --git a/vc-current/Hashfun.v b/vc-current/Hashfun.v index 053fe2643..c1996b2c1 100644 --- a/vc-current/Hashfun.v +++ b/vc-current/Hashfun.v @@ -328,4 +328,4 @@ Proof. End IntHashTable. -(* 2024-12-27 01:34 *) +(* 2026-01-06 14:19 *) diff --git a/vc-current/LICENSE b/vc-current/LICENSE index a332c0de1..733806a03 100644 --- a/vc-current/LICENSE +++ b/vc-current/LICENSE @@ -1,4 +1,4 @@ -Copyright (c) 2024 +Copyright (c) 2026 Permission is hereby granted, free of charge, to any person obtaining a copy of this software and associated documentation files (the "Software"), to deal diff --git a/vc-current/Makefile b/vc-current/Makefile index 95de0f388..a75efe266 100644 --- a/vc-current/Makefile +++ b/vc-current/Makefile @@ -10,7 +10,7 @@ clean:: $(RM) $(wildcard Makefile.coq Makefile.coq.conf) Makefile.coq: - coq_makefile $(COQMFFLAGS) -o Makefile.coq $(ALLVFILES) + rocq makefile $(COQMFFLAGS) -o Makefile.coq $(ALLVFILES) -include Makefile.coq diff --git a/vc-current/Postscript.html b/vc-current/Postscript.html index 00023c668..61051757d 100644 --- a/vc-current/Postscript.html +++ b/vc-current/Postscript.html @@ -56,7 +56,7 @@

PostscriptPostcript and bibliography
  • Bins-based malloc/free system [Appel and Naumann 2020]
    • -
  • AES encryption, B+Trees, Tries of B+ trees (unpublished +
  • AES encryption, B+Trees, Tries of B+ trees (unpublished master's or undergraduate theses).
    • @@ -74,7 +74,7 @@

    PostscriptPostcript and bibliography The first-draft version of VST's module system -- for verifying multimodule C programs with .c and .h files -- is described in [Beringer 2019]. The newer version, using Verified Software Units, - is demonstrated in progs/VSUpile distributed with VST. + is demonstrated in progs/VSUpile distributed with VST. The description in [Beringer 2019] mostly matches the proofs in progs/VSUpile, but the proofs handle data abstraction using the methods described in the the VSU chapters of this volume. @@ -82,7 +82,7 @@

    PostscriptPostcript and bibliography

    Input/output

    To prove I/O using our Verifiable C logic, we treat the state of the - outside world as a resource in the SEP clause, alongside (but separating from) + outside world as a resource in the SEP clause, alongside (but separating from) in-memory conjuncts. Proved examples are in progs/io.c, progs/io_mem.c, and their proof files progs/verif_io.v, progs/verif_io_mem.v. Research papers describing these concepts include [Koh 2020] and @@ -101,7 +101,7 @@

    PostscriptPostcript and bibliography There are many static analyzers -- too numerous to list here -- that attempt to check safety of your program: will it crash? Will it access an array out of bounds, or dereference an uninitialized pointer? Static - analyzers can be useful in software engineering, but they have two major + analyzers can be useful in software engineering, but they have two major limitations:
    • They don't verify functional correctness -- that is, does your program @@ -122,8 +122,8 @@

      PostscriptPostcript and bibliography functional program logic, and use higher-order logic to prove correctness. For example:
        -
      • Write pure functional programs in Coq, prove them correct in Coq, then - extract them from Coq to OCaml or Haskell. See Volume 3 of Software +
      • Write pure functional programs in Rocq, prove them correct in Rocq, then + extract them From Stdlib to OCaml or Haskell. See Volume 3 of Software Foundations: Verified Functional Algorithms.
        • @@ -131,11 +131,11 @@

        PostscriptPostcript and bibliography same thing: write functional programs, prove them correct, extract, compile. -
      • You can write Haskell programs, compile with ghc, and import into Coq +
      • You can write Haskell programs, compile with ghc, and import into Rocq for verification using hs-to-coq [Spector-Zabusky 2018].
        • -
      • ACL2 is an older system, that uses a first-order logic. That's less +
      • ACL2 is an older system, that uses a first-order logic. That's less expressive, you don't get polymorphism or quantification, but there have been many successful applications of ACL2 in industry.
        • @@ -165,7 +165,7 @@

        PostscriptPostcript and bibliography ML with mutable references and arrays is also a high-level imperative language. CFML is a system for reasoning about imperative ML - programs using separation logic in Coq [Chargueraud 2010], + programs using separation logic in Rocq [Chargueraud 2010], soon to be described in another volume of Software Foundations. CakeML is a system for proving (and correctly compiling) ML programs in HOL [Kumar 2014]. @@ -194,7 +194,7 @@

        PostscriptPostcript and bibliography Unlike VST, where (as you have seen) the proof script is separate from the program, in both Frama-C and VeriFast you prove the program by inserting assertions and invariants into the program. the tools complete the - verification automatically -- or else, point out which assertions + verification automatically -- or else, point out which assertions have failed, so you can adjust your assertions and invariants, and try again.
        @@ -203,17 +203,17 @@

        PostscriptPostcript and bibliography express your function specifications, assertions, and invariants.
        • In VST, as you have seen, that language is a separation language - (PROP/LOCAL/SEP) embedded in Coq, so that the PROP, LOCAL, and SEP + (PROP/LOCAL/SEP) embedded in Rocq, so that the PROP, LOCAL, and SEP clauses can all make use of the full expressive power of the Calculus of Inductive Constructions (CiC). You have seen a simple example of - the expressive power of this approach, where we can use ordinary Coq + the expressive power of this approach, where we can use ordinary Rocq proofs in Hashfun, and directly connect them to separation-logic proofs in Verif_hash.
        • Frama-C uses a weaker assertion language, expressed in C syntax. That's a much weaker logic to reason in, and it doesn't directly connect to - a general-purpose logic (and proof assistant) like Coq. Also, since + a general-purpose logic (and proof assistant) like Rocq. Also, since Frama-C is not a separation logic, it can be difficult to reason about data structures. @@ -222,7 +222,7 @@

          PostscriptPostcript and bibliography it is separation logic, not just Hoare logic. That means you can reason about data structures. There's no artificial limitation to a C-like syntax in the assertion language. Unfortunately, VeriFast's assertion language - is not connected to a general-purpose logic (and proof assistant); that + is not connected to a general-purpose logic (and proof assistant); that means you can do refinement proofs (this C program implements that functional model), but it's not so easy to reason about properties of your functional models. @@ -237,7 +237,7 @@

          PostscriptPostcript and bibliography Formal reasoning about source programs is a good thing -- but once you've proved your source program correct, how do you know that is compiled - correctly? That is, + correctly? That is,
          • the compiler must not have bugs, and @@ -264,13 +264,13 @@

            PostscriptPostcript and bibliography future software verification efforts.

    -
    -(* 2024-12-27 01:34 *)
    + +(* 2026-01-07 13:38 *)
    diff --git a/vc-current/Postscript.v b/vc-current/Postscript.v index aad1328bd..476e1e4f6 100644 --- a/vc-current/Postscript.v +++ b/vc-current/Postscript.v @@ -70,12 +70,12 @@ A good way to write proved-correct software is to program in a pure functional program logic, and use higher-order logic to prove correctness. For example: - - Write pure functional programs in Coq, prove them correct in Coq, then - extract them from Coq to OCaml or Haskell. See Volume 3 of Software + - Write pure functional programs in Rocq, prove them correct in Rocq, then + extract them From Stdlib to OCaml or Haskell. See Volume 3 of Software Foundations: Verified Functional Algorithms. - In HOL systems (Higher-order Logic) such as Isabelle/HOL, you can do the same thing: write functional programs, prove them correct, extract, compile. - - You can write Haskell programs, compile with [ghc], and import into Coq + - You can write Haskell programs, compile with [ghc], and import into Rocq for verification using hs-to-coq [Spector-Zabusky 2018] (in Bib.v). - ACL2 is an older system, that uses a first-order logic. That's less expressive, you don't get polymorphism or quantification, but there @@ -98,7 +98,7 @@ ML with mutable references and arrays is also a high-level imperative language. CFML is a system for reasoning about imperative ML - programs using separation logic in Coq [Chargueraud 2010] (in Bib.v), + programs using separation logic in Rocq [Chargueraud 2010] (in Bib.v), soon to be described in another volume of _Software Foundations_. CakeML is a system for proving (and correctly compiling) ML programs in HOL [Kumar 2014] (in Bib.v). *) @@ -121,15 +121,15 @@ Each of these three systems has an assertion language, in which you express your function specifications, assertions, and invariants. - In VST, as you have seen, that language is a separation language - (PROP/LOCAL/SEP) embedded in Coq, so that the PROP, LOCAL, and SEP + (PROP/LOCAL/SEP) embedded in Rocq, so that the PROP, LOCAL, and SEP clauses can all make use of the full expressive power of the Calculus of Inductive Constructions (CiC). You have seen a simple example of - the expressive power of this approach, where we can use ordinary Coq + the expressive power of this approach, where we can use ordinary Rocq proofs in [Hashfun], and directly connect them to separation-logic proofs in [Verif_hash]. - Frama-C uses a weaker assertion language, expressed in C syntax. That's a much weaker logic to reason in, and it doesn't directly connect to - a general-purpose logic (and proof assistant) like Coq. Also, since + a general-purpose logic (and proof assistant) like Rocq. Also, since Frama-C is not a separation logic, it can be difficult to reason about data structures. - VeriFast uses a capable Dafny-like logic -- even more capable, since @@ -164,5 +164,4 @@ expressive enough to allow to verify them. We wish you success in your future software verification efforts. *) - -(* 2024-12-27 01:34 *) +(* 2026-01-07 13:38 *) diff --git a/vc-current/Preface.html b/vc-current/Preface.html index b90c1845a..030347a1f 100644 --- a/vc-current/Preface.html +++ b/vc-current/Preface.html @@ -42,10 +42,10 @@

    Preface

    Here's a good way to build formally verified correct software: