Configure some packages as trusted for goose

Author: upamanyus

Makefile

@@ -1,4 +1,4 @@
-SRC_DIRS := 'src' 'external' 'new' 'new_trusted_code'
+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")

_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

new/code/bytes.v

@@ -16,11 +16,22 @@ Axiom asciiSpace'init : val.
 
 Definition pkg_name' : go_string := "bytes".
 
-Definition vars' : list (go_string * go_type) := [("ErrTooLarge"%go, error); ("errNegativeRead"%go, error); ("errUnreadByte"%go, error); ("asciiSpace"%go, arrayT 256 uint8T)].
+Definition vars' : list (go_string * go_type) := [].
 
 Definition functions' : list (go_string * val) := [].
 
 Definition msets' : list (go_string * (list (go_string * val))) := [].
 
+Axiom _'init : val.
+
+Definition initialize' : val :=
+  rec: "initialize'" <> :=
+    globals.package_init pkg_name' vars' functions' msets' (λ: <>,
+      exception_do (do:  (ErrTooLarge'init #());;;
+      do:  (errNegativeRead'init #());;;
+      do:  (errUnreadByte'init #());;;
+      do:  (asciiSpace'init #()))
+      ).
+
 End code.
 End bytes.

new/code/context.v

@@ -18,12 +18,21 @@ Axiom closedchan'init : val.
 
 Definition pkg_name' : go_string := "context".
 
-Definition vars' : list (go_string * go_type) := [("Canceled"%go, error); ("DeadlineExceeded"%go, error); ("goroutines"%go, atomic.Int32); ("cancelCtxKey"%go, intT); ("closedchan"%go, chanT (structT [
-             ]))].
+Definition vars' : list (go_string * go_type) := [].
 
 Definition functions' : list (go_string * val) := [].
 
 Definition msets' : list (go_string * (list (go_string * val))) := [].
 
+Axiom _'init : val.
+
+Definition initialize' : val :=
+  rec: "initialize'" <> :=
+    globals.package_init pkg_name' vars' functions' msets' (λ: <>,
+      exception_do (do:  (Canceled'init #());;;
+      do:  (DeadlineExceeded'init #());;;
+      do:  (closedchan'init #()))
+      ).
+
 End code.
 End context.

new/code/crypto/rand.v

@@ -12,11 +12,19 @@ Axiom altGetRandom'init : val.
 
 Definition pkg_name' : go_string := "crypto/rand".
 
-Definition vars' : list (go_string * go_type) := [("Reader"%go, io.Reader); ("altGetRandom"%go, funcT)].
+Definition vars' : list (go_string * go_type) := [].
 
 Definition functions' : list (go_string * val) := [].
 
 Definition msets' : list (go_string * (list (go_string * val))) := [].
 
+Axiom _'init : val.
+
+Definition initialize' : val :=
+  rec: "initialize'" <> :=
+    globals.package_init pkg_name' vars' functions' msets' (λ: <>,
+      exception_do (do:  #())
+      ).
+
 End code.
 End rand.

new/code/errors.v

@@ -12,11 +12,20 @@ Axiom errorType'init : val.
 
 Definition pkg_name' : go_string := "errors".
 
-Definition vars' : list (go_string * go_type) := [("ErrUnsupported"%go, error); ("errorType"%go, reflectlite.Type)].
+Definition vars' : list (go_string * go_type) := [].
 
 Definition functions' : list (go_string * val) := [].
 
 Definition msets' : list (go_string * (list (go_string * val))) := [].
 
+Axiom _'init : val.
+
+Definition initialize' : val :=
+  rec: "initialize'" <> :=
+    globals.package_init pkg_name' vars' functions' msets' (λ: <>,
+      exception_do (do:  (ErrUnsupported'init #());;;
+      do:  (errorType'init #()))
+      ).
+
 End code.
 End errors.

new/code/etcdclient.v

@@ -150,5 +150,11 @@ Definition functions' : list (go_string * val) := [].
 
 Definition msets' : list (go_string * (list (go_string * val))) := [("KeyValue"%go, []); ("KeyValue'ptr"%go, []); ("ResponseHeader"%go, []); ("ResponseHeader'ptr"%go, []); ("PutRequest"%go, []); ("PutRequest'ptr"%go, []); ("PutResponse"%go, []); ("PutResponse'ptr"%go, []); ("opType"%go, []); ("opType'ptr"%go, []); ("Op"%go, []); ("Op'ptr"%go, []); ("OpOption"%go, []); ("OpOption'ptr"%go, []); ("SortTarget"%go, []); ("SortTarget'ptr"%go, []); ("SortOrder"%go, []); ("SortOrder'ptr"%go, []); ("SortOption"%go, []); ("SortOption'ptr"%go, []); ("LeaseID"%go, []); ("LeaseID'ptr"%go, []); ("Cmp"%go, []); ("Cmp'ptr"%go, []); ("Compare"%go, []); ("Compare'ptr"%go, []); ("Compare_CompareResult"%go, []); ("Compare_CompareResult'ptr"%go, []); ("Compare_CompareTarget"%go, []); ("Compare_CompareTarget'ptr"%go, [])].
 
+Definition initialize' : val :=
+  rec: "initialize'" <> :=
+    globals.package_init pkg_name' vars' functions' msets' (λ: <>,
+      exception_do (do:  #())
+      ).
+
 End code.
 End etcdclient.

new/code/fmt.v

@@ -1,28 +1,5 @@
 (* autogenerated from fmt *)
 From New.golang Require Import defn.
 
-Module fmt.
-Section code.
-Context `{ffi_syntax}.
+Require Export New.trusted_code.fmt.
 
-
-Axiom ppFree'init : val.
-
-Axiom space'init : val.
-
-Axiom ssFree'init : val.
-
-Axiom errComplex'init : val.
-
-Axiom errBool'init : val.
-
-Definition pkg_name' : go_string := "fmt".
-
-Definition vars' : list (go_string * go_type) := [("ppFree"%go, sync.Pool); ("space"%go, sliceT); ("ssFree"%go, sync.Pool); ("errComplex"%go, error); ("errBool"%go, error)].
-
-Definition functions' : list (go_string * val) := [].
-
-Definition msets' : list (go_string * (list (go_string * val))) := [].
-
-End code.
-End fmt.

new/code/fmt.v.toml

@@ -1,3 +1 @@
-Imports = []
-ToTranslate = []
-ToAxiomatize = []
+trusted = true

new/code/github_com/goose_lang/goose/testdata/examples/append_log.v

@@ -1,8 +1,8 @@
 (* autogenerated from github.com/goose-lang/goose/testdata/examples/append_log *)
 From New.golang Require Import defn.
-From New.code Require Import github_com.goose_lang.primitive.disk.
-From New.code Require Import github_com.tchajed.marshal.
-From New.code Require Import sync.
+Require Import New.code.github_com.goose_lang.primitive.disk.
+Require Import New.code.github_com.tchajed.marshal.
+Require Import New.code.sync.
 
 From New Require Import disk_prelude.
 Module append_log.
@@ -193,5 +193,13 @@ Definition functions' : list (go_string * val) := [("Init"%go, Init); ("Open"%go
 
 Definition msets' : list (go_string * (list (go_string * val))) := [("Log"%go, []); ("Log'ptr"%go, [("Append"%go, Log__Append); ("Get"%go, Log__Get); ("Reset"%go, Log__Reset); ("append"%go, Log__append); ("get"%go, Log__get); ("mkHdr"%go, Log__mkHdr); ("reset"%go, Log__reset); ("writeHdr"%go, Log__writeHdr)])].
 
+Definition initialize' : val :=
+  rec: "initialize'" <> :=
+    globals.package_init pkg_name' vars' functions' msets' (λ: <>,
+      exception_do (do:  disk.initialize';;;
+      do:  marshal.initialize';;;
+      do:  sync.initialize')
+      ).
+
 End code.
 End append_log.

new/code/github_com/goose_lang/goose/testdata/examples/semantics.v

@@ -1,8 +1,8 @@
 (* autogenerated from github.com/goose-lang/goose/testdata/examples/semantics *)
 From New.golang Require Import defn.
-From New.code Require Import github_com.goose_lang.primitive.
-From New.code Require Import github_com.goose_lang.primitive.disk.
-From New.code Require Import sync.
+Require Import New.code.github_com.goose_lang.primitive.
+Require Import New.code.github_com.goose_lang.primitive.disk.
+Require Import New.code.sync.
 
 From New Require Import disk_prelude.
 Module semantics.
@@ -2872,5 +2872,13 @@ Definition msets' : list (go_string * (list (go_string * val))) := [("unit"%go,
                  method_call #pkg_name' #"Log" #"unlock" (![Log] "$recvAddr")
                  )%V)])].
 
+Definition initialize' : val :=
+  rec: "initialize'" <> :=
+    globals.package_init pkg_name' vars' functions' msets' (λ: <>,
+      exception_do (do:  disk.initialize';;;
+      do:  sync.initialize';;;
+      do:  primitive.initialize')
+      ).
+
 End code.
 End semantics.