Skip to content

Commit 908a446

Browse files
lukaszczlukaszcz
authored
Verified compilation prototype: generation of Lean verification statements (#3344)
* Adds the `--verify` option which causes the compiler to emit a Lean project with statements of compilation correctness. Currently, the verification statements are generated only for a part of the Core pipeline in the main optimization phase. * Adds `examples/verification` with two simple compiler run verification examples.
1 parent adc3b81 commit 908a446

File tree

53 files changed

+1335
-96
lines changed

Some content is hidden

Large Commits have some content hidden by default. Use the searchbox below for content that may be hidden.

53 files changed

+1335
-96
lines changed

‎app/Commands/Dev/Core/Asm.hs

+2-1
Original file line numberDiff line numberDiff line change
@@ -5,6 +5,7 @@ import Commands.Base
55
import Commands.Dev.Core.Asm.Options
66
import Juvix.Compiler.Asm qualified as Asm
77
import Juvix.Compiler.Core qualified as Core
8+
import Juvix.Compiler.Verification.Dumper
89

910
runCommand ::
1011
forall r a.
@@ -16,7 +17,7 @@ runCommand opts = do
1617
ep <- getEntryPoint (Just sinputFile)
1718
s' <- readFile inputFile
1819
tab <- getRight (Core.runParserMain inputFile defaultModuleId mempty s')
19-
r <- runReader ep . runError @JuvixError $ coreToAsm (Core.moduleFromInfoTable tab)
20+
r <- runReader ep . runError @JuvixError . ignoreDumper $ coreToAsm (Core.moduleFromInfoTable tab)
2021
md' <- getRight r
2122
if
2223
| project opts ^. coreAsmPrint ->

‎app/Commands/Dev/Core/Compile/Base.hs

+9
Original file line numberDiff line numberDiff line change
@@ -19,6 +19,7 @@ import Juvix.Compiler.Reg.Data.Module qualified as Reg
1919
import Juvix.Compiler.Reg.Pretty qualified as Reg
2020
import Juvix.Compiler.Tree.Data.Module qualified as Tree
2121
import Juvix.Compiler.Tree.Pretty qualified as Tree
22+
import Juvix.Compiler.Verification.Dumper
2223

2324
data PipelineArg = PipelineArg
2425
{ _pipelineArgOptions :: CompileOptions,
@@ -74,6 +75,7 @@ runCPipeline pa@PipelineArg {..} = do
7475
. run
7576
. runReader entryPoint
7677
. runError @JuvixError
78+
. ignoreDumper
7779
$ coreToMiniC _pipelineArgModule
7880
inputfile <- getMainFile (Just (_pipelineArgOptions ^. compileInputFile))
7981
cFile <- inputCFile inputfile
@@ -98,6 +100,7 @@ runAsmPipeline pa@PipelineArg {..} = do
98100
r <-
99101
runReader entryPoint
100102
. runError @JuvixError
103+
. ignoreDumper
101104
. coreToAsm
102105
$ _pipelineArgModule
103106
md' <- getRight r
@@ -111,6 +114,7 @@ runRegPipeline pa@PipelineArg {..} = do
111114
r <-
112115
runReader entryPoint
113116
. runError @JuvixError
117+
. ignoreDumper
114118
. coreToReg
115119
$ _pipelineArgModule
116120
md' <- getRight r
@@ -124,6 +128,7 @@ runTreePipeline pa@PipelineArg {..} = do
124128
r <-
125129
runReader entryPoint
126130
. runError @JuvixError
131+
. ignoreDumper
127132
. coreToTree Core.IdentityTrans
128133
$ _pipelineArgModule
129134
md' <- getRight r
@@ -137,6 +142,7 @@ runAnomaPipeline pa@PipelineArg {..} = do
137142
r <-
138143
runReader entryPoint
139144
. runError @JuvixError
145+
. ignoreDumper
140146
. coreToAnoma
141147
$ _pipelineArgModule
142148
res <- getRight r
@@ -149,6 +155,7 @@ runCasmPipeline pa@PipelineArg {..} = do
149155
r <-
150156
runReader entryPoint
151157
. runError @JuvixError
158+
. ignoreDumper
152159
. coreToCasm
153160
$ _pipelineArgModule
154161
Casm.Result {..} <- getRight r
@@ -161,6 +168,7 @@ runCairoPipeline pa@PipelineArg {..} = do
161168
r <-
162169
runReader entryPoint
163170
. runError @JuvixError
171+
. ignoreDumper
164172
. coreToCairo
165173
$ _pipelineArgModule
166174
res <- getRight r
@@ -173,6 +181,7 @@ runRiscZeroRustPipeline pa@PipelineArg {..} = do
173181
r <-
174182
runReader entryPoint
175183
. runError @JuvixError
184+
. ignoreDumper
176185
. coreToRiscZeroRust
177186
$ _pipelineArgModule
178187
Rust.Result {..} <- getRight r

‎app/Commands/Dev/Core/FromConcrete.hs

+1-1
Original file line numberDiff line numberDiff line change
@@ -20,7 +20,7 @@ runCommand coreOpts = do
2020
run
2121
. runReader (project @GlobalOptions @Core.CoreOptions gopts)
2222
. runError @JuvixError
23-
$ Core.applyTransformations (Core.CombineInfoTables : project coreOpts ^. coreFromConcreteTransformations) md
23+
$ Core.applyTransformations' (Core.CombineInfoTables : project coreOpts ^. coreFromConcreteTransformations) md
2424
tab0 :: InfoTable <- Core.computeCombinedInfoTable <$> getRight r
2525
let tab' :: InfoTable = if coreOpts ^. coreFromConcreteNoDisambiguate then tab0 else disambiguateNames' tab0
2626
inInputModule :: IdentifierInfo -> Bool

‎app/Commands/Dev/Core/Read.hs

+1-1
Original file line numberDiff line numberDiff line change
@@ -24,7 +24,7 @@ runCommand opts = do
2424
inputFile :: Path Abs File <- fromAppPathFile sinputFile
2525
s' <- readFile inputFile
2626
tab <- getRight (Core.runParserMain inputFile defaultModuleId mempty s')
27-
let r = run $ runReader (project @GlobalOptions @Core.CoreOptions gopts) $ runError @JuvixError $ Core.applyTransformations (project opts ^. coreReadTransformations) (Core.moduleFromInfoTable tab)
27+
let r = run $ runReader (project @GlobalOptions @Core.CoreOptions gopts) $ runError @JuvixError $ Core.applyTransformations' (project opts ^. coreReadTransformations) (Core.moduleFromInfoTable tab)
2828
tab0 <- getRight r
2929
let tab' = Core.computeCombinedInfoTable $ if project opts ^. coreReadNoDisambiguate then tab0 else Core.disambiguateNames tab0
3030
Scoper.scopeTrace tab'

‎app/Commands/Dev/Core/Strip.hs

+2
Original file line numberDiff line numberDiff line change
@@ -5,6 +5,7 @@ import Commands.Dev.Core.Strip.Options
55
import Juvix.Compiler.Core qualified as Core
66
import Juvix.Compiler.Core.Pretty qualified as Core
77
import Juvix.Compiler.Core.Translation.Stripped.FromCore qualified as Stripped
8+
import Juvix.Compiler.Verification.Dumper
89

910
runCommand :: forall r a. (Members '[EmbedIO, TaggedLock, App] r, CanonicalProjection a Core.Options, CanonicalProjection a CoreStripOptions) => a -> Sem r ()
1011
runCommand opts = do
@@ -18,6 +19,7 @@ runCommand opts = do
1819
run
1920
. runReader ep
2021
. runError @JuvixError
22+
. ignoreDumper
2123
$ Core.toStripped Core.IdentityTrans (Core.moduleFromInfoTable tab)
2224
tab' <-
2325
getRight $

‎app/Commands/Dev/DevCompile/Core.hs

+1-1
Original file line numberDiff line numberDiff line change
@@ -24,7 +24,7 @@ runCommand opts = do
2424
res :: Core.Module <-
2525
( runError @JuvixError
2626
. runReader (project' @Core.CoreOptions gopts)
27-
. Core.applyTransformations compileTransformations
27+
. Core.applyTransformations' compileTransformations
2828
$ coremodule
2929
)
3030
>>= getRight

‎app/Commands/Eval.hs

+1-1
Original file line numberDiff line numberDiff line change
@@ -18,7 +18,7 @@ runCommand opts@EvalOptions {..} = do
1818
case mevalNode of
1919
Just evalNode -> do
2020
evopts <- evalOptionsToEvalOptions opts
21-
md <- getRight . run . runError @JuvixError . runReader @Core.CoreOptions (project gopts) $ Core.applyTransformations Core.toEvalTransformations (Core.moduleFromInfoTable tab)
21+
md <- getRight . run . runError @JuvixError . runReader @Core.CoreOptions (project gopts) $ Core.applyTransformations' Core.toEvalTransformations (Core.moduleFromInfoTable tab)
2222
let tab' = Core.computeCombinedInfoTable md
2323
Eval.evalAndPrint' (project gopts) (project opts) evopts tab' evalNode
2424
Nothing -> do

‎app/GlobalOptions.hs

+13-4
Original file line numberDiff line numberDiff line change
@@ -14,7 +14,8 @@ import Juvix.Data.Error.GenericError qualified as E
1414
import Juvix.Data.Field
1515

1616
data GlobalOptions = GlobalOptions
17-
{ _globalNoColors :: Bool,
17+
{ _globalVerify :: Bool,
18+
_globalNoColors :: Bool,
1819
_globalVSCode :: Bool,
1920
_globalShowNameIds :: Bool,
2021
_globalBuildDir :: Maybe (AppPath Dir),
@@ -55,13 +56,15 @@ instance CanonicalProjection GlobalOptions Core.CoreOptions where
5556
Core._optUnrollLimit = defaultUnrollLimit,
5657
Core._optFieldSize = fromMaybe defaultFieldSize _globalFieldSize,
5758
Core._optOptimizationLevel = defaultOptimizationLevel,
58-
Core._optInliningDepth = defaultInliningDepth
59+
Core._optInliningDepth = defaultInliningDepth,
60+
Core._optVerify = _globalVerify
5961
}
6062

6163
defaultGlobalOptions :: GlobalOptions
6264
defaultGlobalOptions =
6365
GlobalOptions
64-
{ _globalNoColors = False,
66+
{ _globalVerify = False,
67+
_globalNoColors = False,
6568
_globalVSCode = False,
6669
_globalNumThreads = defaultNumThreads,
6770
_globalShowNameIds = False,
@@ -84,6 +87,11 @@ defaultGlobalOptions =
8487
-- the input boolean
8588
parseGlobalFlags :: Parser GlobalOptions
8689
parseGlobalFlags = do
90+
_globalVerify <-
91+
switch
92+
( long "verify"
93+
<> help "Generate Lean verification statements"
94+
)
8795
_globalNoColors <-
8896
switch
8997
( long "no-colors"
@@ -229,7 +237,8 @@ entryPointFromGlobalOptions root mainFile opts = do
229237
_entryPointGenericOptions = project opts,
230238
_entryPointBuildDir = maybe (e ^. entryPointBuildDir) (CustomBuildDir . Abs) mabsBuildDir,
231239
_entryPointOffline = opts ^. globalOffline,
232-
_entryPointFieldSize = fromMaybe defaultFieldSize $ opts ^. globalFieldSize
240+
_entryPointFieldSize = fromMaybe defaultFieldSize $ opts ^. globalFieldSize,
241+
_entryPointVerify = opts ^. globalVerify
233242
}
234243

235244
entryPointFromGlobalOptionsNoFile :: (Members '[EmbedIO, TaggedLock] r) => Root -> GlobalOptions -> Sem r EntryPoint

‎examples/verification/Package.juvix

+8
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,8 @@
1+
module Package;
2+
3+
import PackageDescription.V2 open;
4+
5+
package : Package :=
6+
defaultPackage@{
7+
name := "verification";
8+
};

‎examples/verification/Program1.juvix

+9
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,9 @@
1+
module Program1;
2+
3+
import Stdlib.Prelude open;
4+
5+
f (x : Nat) : Nat := x + 7;
6+
7+
g (x : Nat) : Nat := x * 2;
8+
9+
main : Nat := f (g 3);

‎examples/verification/Program1_lean_completed/.gitignore

+1
Original file line numberDiff line numberDiff line change
@@ -0,0 +1 @@
1+
.lake

‎examples/verification/Program1_lean_completed/Program1.lean

+66
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,66 @@
1+
import Juvix.Core.Main
2+
open Juvix.Core.Main
3+
4+
lemma step_0_constant_folding : Expr.save (Expr.binop BinaryOp.add_int (Expr.binop BinaryOp.mul_int (Expr.const (Constant.int 3)) (Expr.const (Constant.int 2))) (Expr.const (Constant.int 7))) (Expr.var 0) ≈ Expr.save (Expr.const (Constant.int 13)) (Expr.var 0) := by
5+
congr'
6+
eval_const'
7+
8+
lemma step_1_inlining : Expr.save (Expr.const (Constant.int 13)) (Expr.var 0) ≈ Expr.save (Expr.const (Constant.int 13)) (Expr.var 0) := by
9+
rfl
10+
11+
lemma step_2_simplification : Expr.save (Expr.const (Constant.int 13)) (Expr.var 0) ≈ Expr.save (Expr.const (Constant.int 13)) (Expr.var 0) := by
12+
rfl
13+
14+
lemma step_3_specialize_args : Expr.save (Expr.const (Constant.int 13)) (Expr.var 0) ≈ Expr.save (Expr.const (Constant.int 13)) (Expr.var 0) := by
15+
rfl
16+
17+
lemma step_4_simplification : Expr.save (Expr.const (Constant.int 13)) (Expr.var 0) ≈ Expr.save (Expr.const (Constant.int 13)) (Expr.var 0) := by
18+
rfl
19+
20+
lemma step_5_constant_folding : Expr.save (Expr.const (Constant.int 13)) (Expr.var 0) ≈ Expr.save (Expr.const (Constant.int 13)) (Expr.var 0) := by
21+
rfl
22+
23+
lemma step_6_inlining : Expr.save (Expr.const (Constant.int 13)) (Expr.var 0) ≈ Expr.save (Expr.const (Constant.int 13)) (Expr.var 0) := by
24+
rfl
25+
26+
lemma step_7_simplification : Expr.save (Expr.const (Constant.int 13)) (Expr.var 0) ≈ Expr.save (Expr.const (Constant.int 13)) (Expr.var 0) := by
27+
rfl
28+
29+
lemma step_8_specialize_args : Expr.save (Expr.const (Constant.int 13)) (Expr.var 0) ≈ Expr.save (Expr.const (Constant.int 13)) (Expr.var 0) := by
30+
rfl
31+
32+
lemma step_9_simplification : Expr.save (Expr.const (Constant.int 13)) (Expr.var 0) ≈ Expr.save (Expr.const (Constant.int 13)) (Expr.var 0) := by
33+
rfl
34+
35+
lemma step_10_constant_folding : Expr.save (Expr.const (Constant.int 13)) (Expr.var 0) ≈ Expr.save (Expr.const (Constant.int 13)) (Expr.var 0) := by
36+
rfl
37+
38+
lemma step_11_inlining : Expr.save (Expr.const (Constant.int 13)) (Expr.var 0) ≈ Expr.save (Expr.const (Constant.int 13)) (Expr.var 0) := by
39+
rfl
40+
41+
lemma step_12_simplification : Expr.save (Expr.const (Constant.int 13)) (Expr.var 0) ≈ Expr.save (Expr.const (Constant.int 13)) (Expr.var 0) := by
42+
rfl
43+
44+
lemma step_13_specialize_args : Expr.save (Expr.const (Constant.int 13)) (Expr.var 0) ≈ Expr.save (Expr.const (Constant.int 13)) (Expr.var 0) := by
45+
rfl
46+
47+
lemma step_14_simplification : Expr.save (Expr.const (Constant.int 13)) (Expr.var 0) ≈ Expr.save (Expr.const (Constant.int 13)) (Expr.var 0) := by
48+
rfl
49+
50+
lemma step_15_constant_folding : Expr.save (Expr.const (Constant.int 13)) (Expr.var 0) ≈ Expr.save (Expr.const (Constant.int 13)) (Expr.var 0) := by
51+
rfl
52+
53+
lemma step_16_inlining : Expr.save (Expr.const (Constant.int 13)) (Expr.var 0) ≈ Expr.save (Expr.const (Constant.int 13)) (Expr.var 0) := by
54+
rfl
55+
56+
lemma step_17_simplification : Expr.save (Expr.const (Constant.int 13)) (Expr.var 0) ≈ Expr.save (Expr.const (Constant.int 13)) (Expr.var 0) := by
57+
rfl
58+
59+
lemma step_18_specialize_args : Expr.save (Expr.const (Constant.int 13)) (Expr.var 0) ≈ Expr.save (Expr.const (Constant.int 13)) (Expr.var 0) := by
60+
rfl
61+
62+
lemma step_19_simplification : Expr.save (Expr.const (Constant.int 13)) (Expr.var 0) ≈ Expr.save (Expr.const (Constant.int 13)) (Expr.var 0) := by
63+
rfl
64+
65+
lemma step_20_constant_folding : Expr.save (Expr.const (Constant.int 13)) (Expr.var 0) ≈ Expr.save (Expr.const (Constant.int 13)) (Expr.var 0) := by
66+
rfl

0 commit comments

Comments
 (0)