1
+ { system
2
+ , compiler
3
+ , flags
4
+ , pkgs
5
+ , hsPkgs
6
+ , pkgconfPkgs
7
+ , errorHandler
8
+ , config
9
+ , ... } :
10
+ {
11
+ flags = { } ;
12
+ package = {
13
+ specVersion = "2.2" ;
14
+ identifier = { name = "copilot-verifier" ; version = "4.2" ; } ;
15
+ license = "BSD-3-Clause" ;
16
+ copyright = "(c) Galois, Inc 2021-2024" ;
17
+
18
+ author = "Galois Inc." ;
19
+ homepage = "" ;
20
+ url = "" ;
21
+ synopsis = "System for verifying the correctness of generated Copilot programs" ;
22
+ description = "@copilot-verifier@ is an add-on to the [Copilot Stream\n DSL](https://copilot-language.github.io) for verifying the correctness of C\n code generated by the @copilot-c99@ package.\n \n @copilot-verifier@ uses the [Crucible symbolic\n simulator](https://github.com/galoisinc/crucible) to interpret the semantics\n of the generated C program and and to produce verification conditions\n sufficient to guarantee that the meaning of the generated program corresponds\n in a precise way to the meaning of the original stream specification. The\n generated verification conditions are then dispatched to SMT solvers to be\n automatically solved." ;
23
+ buildType = "Simple" ;
24
+ } ;
25
+ components = {
26
+ "library" = {
27
+ depends = [
28
+ ( hsPkgs . "aeson" or ( errorHandler . buildDepError "aeson" ) )
29
+ ( hsPkgs . "base" or ( errorHandler . buildDepError "base" ) )
30
+ ( hsPkgs . "bv-sized" or ( errorHandler . buildDepError "bv-sized" ) )
31
+ ( hsPkgs . "bytestring" or ( errorHandler . buildDepError "bytestring" ) )
32
+ ( hsPkgs . "containers" or ( errorHandler . buildDepError "containers" ) )
33
+ ( hsPkgs . "copilot-c99" or ( errorHandler . buildDepError "copilot-c99" ) )
34
+ ( hsPkgs . "copilot-core" or ( errorHandler . buildDepError "copilot-core" ) )
35
+ ( hsPkgs . "copilot-theorem" or ( errorHandler . buildDepError "copilot-theorem" ) )
36
+ ( hsPkgs . "crucible" or ( errorHandler . buildDepError "crucible" ) )
37
+ ( hsPkgs . "crucible-llvm" or ( errorHandler . buildDepError "crucible-llvm" ) )
38
+ ( hsPkgs . "crux" or ( errorHandler . buildDepError "crux" ) )
39
+ ( hsPkgs . "crux-llvm" or ( errorHandler . buildDepError "crux-llvm" ) )
40
+ ( hsPkgs . "filepath" or ( errorHandler . buildDepError "filepath" ) )
41
+ ( hsPkgs . "lens" or ( errorHandler . buildDepError "lens" ) )
42
+ ( hsPkgs . "llvm-pretty" or ( errorHandler . buildDepError "llvm-pretty" ) )
43
+ ( hsPkgs . "mtl" or ( errorHandler . buildDepError "mtl" ) )
44
+ ( hsPkgs . "panic" or ( errorHandler . buildDepError "panic" ) )
45
+ ( hsPkgs . "parameterized-utils" or ( errorHandler . buildDepError "parameterized-utils" ) )
46
+ ( hsPkgs . "prettyprinter" or ( errorHandler . buildDepError "prettyprinter" ) )
47
+ ( hsPkgs . "text" or ( errorHandler . buildDepError "text" ) )
48
+ ( hsPkgs . "transformers" or ( errorHandler . buildDepError "transformers" ) )
49
+ ( hsPkgs . "vector" or ( errorHandler . buildDepError "vector" ) )
50
+ ( hsPkgs . "what4" or ( errorHandler . buildDepError "what4" ) )
51
+ ] ;
52
+ buildable = true ;
53
+ } ;
54
+ sublibs = {
55
+ "copilot-verifier-examples" = {
56
+ depends = [
57
+ ( hsPkgs . "aeson" or ( errorHandler . buildDepError "aeson" ) )
58
+ ( hsPkgs . "base" or ( errorHandler . buildDepError "base" ) )
59
+ ( hsPkgs . "bv-sized" or ( errorHandler . buildDepError "bv-sized" ) )
60
+ ( hsPkgs . "bytestring" or ( errorHandler . buildDepError "bytestring" ) )
61
+ ( hsPkgs . "containers" or ( errorHandler . buildDepError "containers" ) )
62
+ ( hsPkgs . "copilot-c99" or ( errorHandler . buildDepError "copilot-c99" ) )
63
+ ( hsPkgs . "copilot-core" or ( errorHandler . buildDepError "copilot-core" ) )
64
+ ( hsPkgs . "copilot-theorem" or ( errorHandler . buildDepError "copilot-theorem" ) )
65
+ ( hsPkgs . "crucible" or ( errorHandler . buildDepError "crucible" ) )
66
+ ( hsPkgs . "crucible-llvm" or ( errorHandler . buildDepError "crucible-llvm" ) )
67
+ ( hsPkgs . "crux" or ( errorHandler . buildDepError "crux" ) )
68
+ ( hsPkgs . "crux-llvm" or ( errorHandler . buildDepError "crux-llvm" ) )
69
+ ( hsPkgs . "filepath" or ( errorHandler . buildDepError "filepath" ) )
70
+ ( hsPkgs . "lens" or ( errorHandler . buildDepError "lens" ) )
71
+ ( hsPkgs . "llvm-pretty" or ( errorHandler . buildDepError "llvm-pretty" ) )
72
+ ( hsPkgs . "mtl" or ( errorHandler . buildDepError "mtl" ) )
73
+ ( hsPkgs . "panic" or ( errorHandler . buildDepError "panic" ) )
74
+ ( hsPkgs . "parameterized-utils" or ( errorHandler . buildDepError "parameterized-utils" ) )
75
+ ( hsPkgs . "prettyprinter" or ( errorHandler . buildDepError "prettyprinter" ) )
76
+ ( hsPkgs . "text" or ( errorHandler . buildDepError "text" ) )
77
+ ( hsPkgs . "transformers" or ( errorHandler . buildDepError "transformers" ) )
78
+ ( hsPkgs . "vector" or ( errorHandler . buildDepError "vector" ) )
79
+ ( hsPkgs . "what4" or ( errorHandler . buildDepError "what4" ) )
80
+ ( hsPkgs . "case-insensitive" or ( errorHandler . buildDepError "case-insensitive" ) )
81
+ ( hsPkgs . "copilot" or ( errorHandler . buildDepError "copilot" ) )
82
+ ( hsPkgs . "copilot-language" or ( errorHandler . buildDepError "copilot-language" ) )
83
+ ( hsPkgs . "copilot-prettyprinter" or ( errorHandler . buildDepError "copilot-prettyprinter" ) )
84
+ ( hsPkgs . "copilot-verifier" or ( errorHandler . buildDepError "copilot-verifier" ) )
85
+ ] ;
86
+ buildable = true ;
87
+ } ;
88
+ } ;
89
+ exes = {
90
+ "verify-examples" = {
91
+ depends = [
92
+ ( hsPkgs . "aeson" or ( errorHandler . buildDepError "aeson" ) )
93
+ ( hsPkgs . "base" or ( errorHandler . buildDepError "base" ) )
94
+ ( hsPkgs . "bv-sized" or ( errorHandler . buildDepError "bv-sized" ) )
95
+ ( hsPkgs . "bytestring" or ( errorHandler . buildDepError "bytestring" ) )
96
+ ( hsPkgs . "containers" or ( errorHandler . buildDepError "containers" ) )
97
+ ( hsPkgs . "copilot-c99" or ( errorHandler . buildDepError "copilot-c99" ) )
98
+ ( hsPkgs . "copilot-core" or ( errorHandler . buildDepError "copilot-core" ) )
99
+ ( hsPkgs . "copilot-theorem" or ( errorHandler . buildDepError "copilot-theorem" ) )
100
+ ( hsPkgs . "crucible" or ( errorHandler . buildDepError "crucible" ) )
101
+ ( hsPkgs . "crucible-llvm" or ( errorHandler . buildDepError "crucible-llvm" ) )
102
+ ( hsPkgs . "crux" or ( errorHandler . buildDepError "crux" ) )
103
+ ( hsPkgs . "crux-llvm" or ( errorHandler . buildDepError "crux-llvm" ) )
104
+ ( hsPkgs . "filepath" or ( errorHandler . buildDepError "filepath" ) )
105
+ ( hsPkgs . "lens" or ( errorHandler . buildDepError "lens" ) )
106
+ ( hsPkgs . "llvm-pretty" or ( errorHandler . buildDepError "llvm-pretty" ) )
107
+ ( hsPkgs . "mtl" or ( errorHandler . buildDepError "mtl" ) )
108
+ ( hsPkgs . "panic" or ( errorHandler . buildDepError "panic" ) )
109
+ ( hsPkgs . "parameterized-utils" or ( errorHandler . buildDepError "parameterized-utils" ) )
110
+ ( hsPkgs . "prettyprinter" or ( errorHandler . buildDepError "prettyprinter" ) )
111
+ ( hsPkgs . "text" or ( errorHandler . buildDepError "text" ) )
112
+ ( hsPkgs . "transformers" or ( errorHandler . buildDepError "transformers" ) )
113
+ ( hsPkgs . "vector" or ( errorHandler . buildDepError "vector" ) )
114
+ ( hsPkgs . "what4" or ( errorHandler . buildDepError "what4" ) )
115
+ ( hsPkgs . "case-insensitive" or ( errorHandler . buildDepError "case-insensitive" ) )
116
+ ( hsPkgs . "copilot-verifier" or ( errorHandler . buildDepError "copilot-verifier" ) )
117
+ ( hsPkgs . "copilot-verifier" . components . sublibs . copilot-verifier-examples or ( errorHandler . buildDepError "copilot-verifier:copilot-verifier-examples" ) )
118
+ ( hsPkgs . "optparse-applicative" or ( errorHandler . buildDepError "optparse-applicative" ) )
119
+ ] ;
120
+ buildable = true ;
121
+ } ;
122
+ } ;
123
+ tests = {
124
+ "copilot-verifier-test" = {
125
+ depends = [
126
+ ( hsPkgs . "aeson" or ( errorHandler . buildDepError "aeson" ) )
127
+ ( hsPkgs . "base" or ( errorHandler . buildDepError "base" ) )
128
+ ( hsPkgs . "bv-sized" or ( errorHandler . buildDepError "bv-sized" ) )
129
+ ( hsPkgs . "bytestring" or ( errorHandler . buildDepError "bytestring" ) )
130
+ ( hsPkgs . "containers" or ( errorHandler . buildDepError "containers" ) )
131
+ ( hsPkgs . "copilot-c99" or ( errorHandler . buildDepError "copilot-c99" ) )
132
+ ( hsPkgs . "copilot-core" or ( errorHandler . buildDepError "copilot-core" ) )
133
+ ( hsPkgs . "copilot-theorem" or ( errorHandler . buildDepError "copilot-theorem" ) )
134
+ ( hsPkgs . "crucible" or ( errorHandler . buildDepError "crucible" ) )
135
+ ( hsPkgs . "crucible-llvm" or ( errorHandler . buildDepError "crucible-llvm" ) )
136
+ ( hsPkgs . "crux" or ( errorHandler . buildDepError "crux" ) )
137
+ ( hsPkgs . "crux-llvm" or ( errorHandler . buildDepError "crux-llvm" ) )
138
+ ( hsPkgs . "filepath" or ( errorHandler . buildDepError "filepath" ) )
139
+ ( hsPkgs . "lens" or ( errorHandler . buildDepError "lens" ) )
140
+ ( hsPkgs . "llvm-pretty" or ( errorHandler . buildDepError "llvm-pretty" ) )
141
+ ( hsPkgs . "mtl" or ( errorHandler . buildDepError "mtl" ) )
142
+ ( hsPkgs . "panic" or ( errorHandler . buildDepError "panic" ) )
143
+ ( hsPkgs . "parameterized-utils" or ( errorHandler . buildDepError "parameterized-utils" ) )
144
+ ( hsPkgs . "prettyprinter" or ( errorHandler . buildDepError "prettyprinter" ) )
145
+ ( hsPkgs . "text" or ( errorHandler . buildDepError "text" ) )
146
+ ( hsPkgs . "transformers" or ( errorHandler . buildDepError "transformers" ) )
147
+ ( hsPkgs . "vector" or ( errorHandler . buildDepError "vector" ) )
148
+ ( hsPkgs . "what4" or ( errorHandler . buildDepError "what4" ) )
149
+ ( hsPkgs . "case-insensitive" or ( errorHandler . buildDepError "case-insensitive" ) )
150
+ ( hsPkgs . "copilot-verifier" or ( errorHandler . buildDepError "copilot-verifier" ) )
151
+ ( hsPkgs . "copilot-verifier" . components . sublibs . copilot-verifier-examples or ( errorHandler . buildDepError "copilot-verifier:copilot-verifier-examples" ) )
152
+ ( hsPkgs . "silently" or ( errorHandler . buildDepError "silently" ) )
153
+ ( hsPkgs . "tasty" or ( errorHandler . buildDepError "tasty" ) )
154
+ ( hsPkgs . "tasty-expected-failure" or ( errorHandler . buildDepError "tasty-expected-failure" ) )
155
+ ( hsPkgs . "tasty-hunit" or ( errorHandler . buildDepError "tasty-hunit" ) )
156
+ ] ;
157
+ buildable = true ;
158
+ } ;
159
+ } ;
160
+ } ;
161
+ }
0 commit comments