Merge branch 'global-funcs'

mit-pdos · Feb 7, 2025 · ed86efb · ed86efb
2 parents e9ffeac + 57d2e3d
commit ed86efb
Show file tree

Hide file tree

Showing 207 changed files with 28,005 additions and 17,900 deletions.
diff --git a/.gitattributes b/.gitattributes
@@ -1 +1,3 @@
 external/Goose/** linguist-generated
+new/code/**/*.v linguist-generated
+new/generatedproof/**/*.v linguist-generated
diff --git a/Makefile b/Makefile
@@ -1,4 +1,4 @@
-SRC_DIRS := 'src' 'external' 'new' 'new_trusted_code' 'new_code_axioms' 'new_partial_axioms'
+SRC_DIRS := 'src' 'external' 'new' 
 ALL_VFILES := $(shell find $(SRC_DIRS) -not -path "external/coqutil/etc/coq-scripts/*" -name "*.v")
 VFILES := $(shell find 'src' -name "*.v")
 QUICK_CHECK_FILES := $(shell find 'src/program_proof/examples' -name "*.v")

diff --git a/_CoqProject b/_CoqProject
@@ -29,7 +29,4 @@
 -Q external/record-update/src RecordUpdate
 -Q external/coq-tactical/src Tactical
 -Q external/iris-named-props/src iris_named_props
--Q new_trusted_code New.code
--Q new_code_axioms New.code
--Q new_partial_axioms New.code_axioms
 -Q new New
diff --git a/external/coqutil b/external/coqutil
diff --git a/new/code/bytes.v b/new/code/bytes.v
diff --git a/new/code/bytes.v.toml b/new/code/bytes.v.toml
@@ -0,0 +1,3 @@
+axiomatize = [
+  "Buffer",
+]
diff --git a/new/code/context.v b/new/code/context.v
diff --git a/new/code/context.v.toml b/new/code/context.v.toml
@@ -0,0 +1,7 @@
+axiomatize = [
+  "Context",
+]
+
+translate = [
+  "CancelFunc",
+]
diff --git a/new/code/crypto/rand.v b/new/code/crypto/rand.v
diff --git a/new/code/crypto/rand.v.toml b/new/code/crypto/rand.v.toml
@@ -0,0 +1,3 @@
+Imports = []
+ToTranslate = []
+ToAxiomatize = []
diff --git a/new/code/errors.v b/new/code/errors.v
diff --git a/new/code/errors.v.toml b/new/code/errors.v.toml
@@ -0,0 +1,3 @@
+Imports = []
+ToTranslate = []
+ToAxiomatize = []
diff --git a/new/code/etcdclient.v b/new/code/etcdclient.v
diff --git a/new/code/fmt.v b/new/code/fmt.v
diff --git a/new/code/fmt.v.toml b/new/code/fmt.v.toml
@@ -0,0 +1,4 @@
+trusted = [
+  "Print",
+  "Printf"
+]
+0 −28		src/coqutil/Lift1Prop.v
+0 −24		src/coqutil/Map/Separation.v
+0 −927		src/coqutil/Map/SeparationLogic.v