Skip to content

Commit bf07bb5

Browse files
atombandrewmwells-amazonshigoel
authored
Add opaque definitions for a simple API (#388)
These opaque definitions will allow us to discuss and agree on a simple, high-level API that could be used to implement CLI commands and other Strata clients that live at a similar level of abstraction. Most of these APIs can easily be implemented based on direct calls to existing code. One, at least, will require a little more work, however. By submitting this pull request, I confirm that you can use, modify, copy, and redistribute this contribution, under the terms of your choice. --------- Co-authored-by: Andrew Wells <130512013+andrewmwells-amazon@users.noreply.github.com> Co-authored-by: Shilpi Goel <shigoel@gmail.com>
1 parent 6effd4d commit bf07bb5

2 files changed

Lines changed: 192 additions & 0 deletions

File tree

‎Strata.lean‎

Lines changed: 3 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -30,3 +30,6 @@ import Strata.Transform.DetToNondetCorrect
3030

3131
/- Backends -/
3232
import Strata.Backends.CBMC.CProver
33+
34+
/- Simple API -/
35+
import Strata.SimpleAPI

‎Strata/SimpleAPI.lean‎

Lines changed: 189 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,189 @@
1+
/-
2+
Copyright Strata Contributors
3+
4+
SPDX-License-Identifier: Apache-2.0 OR MIT
5+
-/
6+
7+
import Strata.DDM.Elab
8+
import Strata.DDM.Ion
9+
import Strata.DDM.Util.ByteArray
10+
import Strata.Util.IO
11+
12+
import Strata.DDM.Integration.Java.Gen
13+
import Strata.Languages.Python.Python
14+
import Strata.Transform.CoreTransform
15+
import Strata.Transform.ProcedureInlining
16+
17+
import Strata.Languages.Laurel.Grammar.LaurelGrammar
18+
import Strata.Languages.Laurel.Grammar.ConcreteToAbstractTreeTranslator
19+
import Strata.Languages.Laurel.LaurelToCoreTranslator
20+
21+
/-! ## Simple Strata API
22+
23+
A simple API for reading, writing, transforming, and analyzing Strata programs.
24+
25+
This API allows clients of Strata to perform its basic operations as directly as
26+
possible. It is intended for use cases that are essentially equivalent to more
27+
fine-grained or more structured equivalents of what the `strata` CLI can
28+
currently do.
29+
30+
**Note:** All definitions are opaque for the moment, so that we can discuss the
31+
structure. Most can be implemented straightforwardly by calling existing code.
32+
Those that can't are noted explicitly.
33+
34+
It involves several key types:
35+
36+
* `Strata.Dialect`: The formal description of a Strata dialect. Used only to
37+
describe which dialects are available when reading or writing files.
38+
39+
* `Strata.Program`: The generic AST for a Strata program in any dialect.
40+
Generally used just as an interim representation before serializing or after
41+
deserializing a program. Before using a `Strata.Program`, it will usually
42+
make sense to translate it into the custom AST for a specific dialect.
43+
44+
* `Laurel.Program`: A dialect-specific AST for a program in the Laurel dialect.
45+
46+
* `Core.Program`: A dialect-specific AST for a program in the Core dialect.
47+
48+
* `Core.VCResults`: The results of attempting to prove each verification condition
49+
that arises from deductive verification of a Core program.
50+
-/
51+
52+
namespace Strata
53+
54+
/-! ### File I/O -/
55+
56+
/--
57+
Either a Strata dialect description or a Strata program in a specific dialect.
58+
This is represented in a single type because an arbitrary Ion file could contain
59+
either one.
60+
-/
61+
inductive DialectOrProgram
62+
| dialect (d : Strata.Dialect)
63+
| program (pgm : Strata.Program)
64+
65+
/--
66+
Parse a Strata dialect or program in textual format, possibly loading other
67+
dialects as needed along the way. The `DialectFileMap` indicates where to find
68+
the definitions of other dialects. The `FilePath` indicates the name of the file
69+
to be parsed. And the `ByteArray` includes the contents of that file. TODO:
70+
should it take just a file name and read it directly?
71+
-/
72+
opaque readStrataText :
73+
Strata.DialectFileMap →
74+
System.FilePath →
75+
ByteArray →
76+
IO (Strata.Elab.LoadedDialects × DialectOrProgram)
77+
78+
/--
79+
Parse a Strata dialect or program in Ion format, possibly loading other
80+
dialects as needed along the way. The `DialectFileMap` indicates where to find
81+
the definitions of other dialects. The `FilePath` indicates the name of the file
82+
to be parsed. And the `ByteArray` includes the contents of that file. TODO:
83+
should it take just a file name and read it directly?
84+
-/
85+
opaque readStrataIon :
86+
Strata.DialectFileMap →
87+
System.FilePath →
88+
ByteArray →
89+
IO (Strata.Elab.LoadedDialects × DialectOrProgram)
90+
91+
/--
92+
Parse a Strata dialect or program in either textual or Ion format, possibly
93+
loading other dialects as needed along the way. The `DialectFileMap` indicates
94+
where to find the definitions of other dialects. The `FilePath` indicates the
95+
name of the file to be loaded.
96+
-/
97+
opaque readStrataFile :
98+
Strata.DialectFileMap →
99+
System.FilePath →
100+
IO (Strata.Elab.LoadedDialects × DialectOrProgram)
101+
102+
/--
103+
Serialize a Strata program in textual format. Returns a byte array rather than
104+
writing directly to a file.
105+
-/
106+
opaque writeStrataText : Strata.Program → ByteArray
107+
108+
/--
109+
Serialize a Strata program in Ion format. Returns a byte array rather than
110+
writing directly to a file.
111+
-/
112+
opaque writeStrataIon : Strata.Program → ByteArray
113+
114+
/-! ### Transformation between generic and dialect-specific representation -/
115+
116+
/--
117+
Translate a program in the dialect-specific AST for Core into the generic Strata
118+
AST. Usually useful as a step before serialization. TODO: we can't yet implement
119+
this, but will be able to once we use DDM-generated translation between the
120+
generic and Strata-specific ASTs.
121+
-/
122+
opaque coreToGeneric : Core.Program → Strata.Program
123+
124+
/--
125+
Translate a program in the generic AST for Strata into the dialect-specific AST
126+
for Core. This can fail with an error message if the input is not a
127+
well-structured instance of the Core dialect.
128+
-/
129+
opaque genericToCore : Strata.Program → Except String Core.Program
130+
131+
/--
132+
Translate a program in the dialect-specific AST for Laurel into the generic Strata
133+
AST. Usually useful as a step before serialization.
134+
-/
135+
opaque laurelToGeneric : Laurel.Program → Strata.Program
136+
137+
/--
138+
Translate a program in the generic AST for Strata into the dialect-specific AST
139+
for Laurel. This can fail with an error message if the input is not a
140+
well-structured instance of the Core dialect.
141+
-/
142+
opaque genericToLaurel : Strata.Program → Except String Laurel.Program
143+
144+
/-! ### Transformation between dialects -/
145+
146+
/--
147+
Translate a program represented in the dialect-specific AST for the Laurel
148+
dialect into the dialect-specific AST for the Core dialect. This can fail with
149+
an error message if the input program contains constructs that are not yet
150+
supported.
151+
-/
152+
opaque laurelToCore : Laurel.Program → Except String Core.Program
153+
154+
/-! ### Transformation of Core programs -/
155+
156+
/--
157+
Options to control the behavior of inlining procedure calls in a Core program.
158+
-/
159+
opaque Core.InlineTransformOptions : Type
160+
161+
/--
162+
Transform a Core program to inline some or all procedure calls.
163+
-/
164+
opaque Core.inlineProcedures : Core.Program → Core.InlineTransformOptions → Core.Program
165+
166+
/--
167+
Transform a Core program to replace each loop with assertions and assumptions about
168+
its invariants.
169+
-/
170+
opaque Core.loopElimWithContract : Core.Program → Core.Program
171+
172+
/--
173+
Transform a Core program to replace each procedure call with assertions and
174+
assumptions about its contract.
175+
-/
176+
opaque Core.callElimWithContract : Core.Program → Core.Program
177+
178+
/-! ### Analysis of Core programs -/
179+
180+
/--
181+
Options to control the behavior of deductive verification of Core programs.
182+
-/
183+
opaque Core.VerifyOptions : Type
184+
185+
/--
186+
Do deductive verification of a Core program, including any external solver
187+
invocation that is necessary.
188+
-/
189+
opaque Core.verify : Core.Program → Core.VerifyOptions → IO Core.VCResults

0 commit comments

Comments
 (0)