Strata/Strata.lean at main · strata-org/Strata · GitHub

1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
/-
  Copyright Strata Contributors

  SPDX-License-Identifier: Apache-2.0 OR MIT
-/

-- This module serves as the root of the `Strata` library.
-- In each category, imports are sorted by alphabetical order.
module
/- DDM -/
import StrataDDM.Integration.Lean
import StrataDDM.Ion

/- Dialect Library -/
import Strata.DL.SMT
import Strata.DL.Lambda
import Strata.DL.Imperative

/- Utilities -/
import Strata.Util.NameProofs
import Strata.Util.Sarif

/- Strata Languages -/
import Strata.Languages.Core.FactoryWF
import Strata.Languages.Core.SeqModel
import Strata.Languages.Core.StatementSemantics
import Strata.Languages.Core.SarifOutput

import Strata.Languages.Laurel.Grammar
import Strata.Languages.Laurel.LaurelCompilationPipeline

/- Code Transforms -/
import Strata.Transform.CallElimCorrect
import Strata.Transform.CoreSpecification
import Strata.Transform.DetToKleeneCorrect
import Strata.Transform.ProcBodyVerifyCorrect

/- Strata Languages — additional -/
import Strata.Languages.B3
import Strata.Languages.C_Simp.C_Simp
import Strata.Languages.C_Simp.Verify
import Strata.Languages.Core.EntryPoint
import Strata.Languages.Core.VerifierProofs
import Strata.Languages.Dyn.Dyn
import Strata.Languages.Dyn.Verify
import Strata.Languages.Laurel.FilterPrelude

/- DDM -/
import StrataDDM

/- Backends -/
import Strata.Backends.CBMC

/- Dialect Library — additional (can't go in aggregates due to cycles) -/
import Strata.DL.Imperative.CFGToCProverGOTO
import Strata.DL.Imperative.ToCProverGOTO
import Strata.DL.SMT.Denote
import Strata.DL.SMT.FactoryCorrect
import Strata.DL.SMT.Translate

/- Code Transforms — additional -/
import Strata.Transform.StructuredToUnstructured

/- Other -/
import Strata.MetaVerifier

/- Pipeline -/
import Strata.Pipeline.Diagnostic

/- Simple API -/
import Strata.SimpleAPI

/- CLI -/
import Strata.Cli.Framework
import Strata.Cli.VerifyOptions

 -- deletion candidates: nothing imports these modules:

-- noimport:
import Strata.DL.Imperative.CFGSemantics
import Strata.DL.Lambda.Denote.Assumptions
import Strata.DL.Lambda.Denote.CallOfLFuncDenote
import Strata.DL.Lambda.Denote.LExprDenote
import Strata.DL.Lambda.Denote.LExprDenoteConstrs
import Strata.DL.Lambda.Denote.LExprDenoteEq
import Strata.DL.Lambda.Denote.LExprDenoteProps
import Strata.DL.Lambda.Denote.LExprDenoteSubst
import Strata.DL.Lambda.Denote.LExprDenoteTySubst
import Strata.DL.Lambda.Denote.LExprSemanticsConsistent
import Strata.DL.Lambda.LExprTypeSpec
import Strata.DL.Lambda.MetaData
import Strata.DL.Lambda.Reflect
import Strata.DL.Lambda.Semantics
import Strata.DL.Lambda.TypeFactoryWF
import Strata.DL.Util.HList
import Strata.Languages.Core.ProgramWF
import Strata.Languages.Core.StatementWF
import Strata.Languages.Dyn.DDMTransform.Parse
import Strata.Languages.Dyn.DDMTransform.Translate
import Strata.Util.Random


-- noimport: Strata.Util.IOTests (used for tests)