verity/lakefile.lean at main · lfglabs-dev/verity · 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
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
import Lake
open Lake DSL

package «verity» where
  version := v!"1.0.0"

require evmyul from git
  "https://github.com/lfglabs-dev/EVMYulLean.git"@"f7e4ee0dc8f8d5265ce822a937ab5be771f182e9"

@[default_target]
lean_lib «Verity» where
  globs := #[
    .one `Verity,
    .andSubmodules `Verity.Core,
    .submodules `Verity.EVM,
    .andSubmodules `Verity.Macro,
    .submodules `Verity.Stdlib,
    .andSubmodules `Verity.Specs.Common,
    .one `Verity.Specs.Composition,
    .submodules `Verity.Proofs.Stdlib,
    .one `Verity.Proofs.LoopSimulation,
    .one `Verity.Proofs.LoopSimulationResultAware
  ]

lean_lib «Contracts» where
  globs := #[
    .one `Contracts,
    .one `Contracts.Common,
    .one `Contracts.Specs,
    .one `Contracts.Interpreter,
    .submodules `Contracts.Examples,
    .andSubmodules `Contracts.Smoke,
    .andSubmodules `Contracts.Counter,
    .andSubmodules `Contracts.SimpleStorage,
    .andSubmodules `Contracts.Owned,
    .andSubmodules `Contracts.Ownable,
    .andSubmodules `Contracts.OwnedCounter,
    .andSubmodules `Contracts.OwnedCounterComposed,
    .andSubmodules `Contracts.SafeCounter,
    .andSubmodules `Contracts.Ledger,
    .one `Contracts.Vault, .one `Contracts.Vault.Vault,
    .one `Contracts.Vault.Spec, .one `Contracts.Vault.Invariants,
    .one `Contracts.Vault.SpecProofs, .one `Contracts.Vault.Proofs.Basic,
    .one `Contracts.Vault.Proofs.Correctness, .one `Contracts.Vault.Proofs.Conservation,
    .one `Contracts.Vault.Proofs.Native,
    .andSubmodules `Contracts.ERC20,
    .andSubmodules `Contracts.ERC721,
    .andSubmodules `Contracts.SimpleToken,
    .andSubmodules `Contracts.CryptoHash,
    .andSubmodules `Contracts.ReentrancyExample,
    .andSubmodules `Contracts.ReentrancyRelyGuarantee
  ]

/-- Solidity read by `solidity_import`: editing it rebuilds the import. -/
input_dir solidityImportSmokeSources where
  path := "Contracts/SolidityImportSmoke"
  filter := .extension "sol"
  text := true

lean_lib «SolidityImportSmoke» where
  globs := #[.one `Contracts.SolidityImportSmoke.Smoke,
    .one `Contracts.SolidityImportSmoke.Transactions,
    .one `Contracts.SolidityImportSmoke.SequenceModel,
    .one `Contracts.SolidityImportSmoke.EventSequenceModel,
    .one `Contracts.SolidityImportSmoke.EnvironmentSequenceModel,
    .one `Contracts.SolidityImportSmoke.StorageSequenceModel,
    .one `Contracts.SolidityImportSmoke.MappingSequenceModel,
    .one `Contracts.SolidityImportSmoke.MappingDirtySequenceModel,
    .one `Contracts.SolidityImportSmoke.StorageVoidSequenceModel,
    .one `Contracts.SolidityImportSmoke.StorageBytesSequenceModel,
    .one `Contracts.SolidityImportSmoke.StorageTraceChecks,
    .one `Contracts.SolidityImportSmoke.EventRejections,
    .one `Contracts.SolidityImportSmoke.ErrorPayloads,
    .one `Contracts.SolidityImportSmoke.ErrorSequenceModel,
    .one `Contracts.SolidityImportSmoke.Require,
    .one `Contracts.SolidityImportSmoke.RequireCustom]
  needs := #[solidityImportSmokeSources]

lean_lib «Compiler» where
  globs := #[.andSubmodules `Compiler]

-- Axiom dependency audit: imports all proof modules so `lake build PrintAxioms`
-- compiles them, then `lake env lean PrintAxioms.lean` can run #print axioms.
lean_lib «PrintAxioms» where
  globs := #[.one `PrintAxioms]

lean_exe «verity-compiler» where
  root := `Compiler.Main
  -- interpreter eval of ecm/interface specs forces init/std decls (e.g. `UInt64.ofNatLT`). (#1951)
  supportInterpreter := true

lean_exe «difftest-interpreter» where
  root := `Contracts.Interpreter

lean_exe «random-gen» where
  root := `Compiler.RandomGen

lean_exe «gas-report» where
  root := `Compiler.Gas.Report
  -- Static gas reporting evaluates compiled terms that may depend on init/std
  -- interpreter support through typed-interface ECMs.
  supportInterpreter := true

lean_exe «compiler-main-test» where
  root := `Compiler.MainTestRunner
  -- Mirrors `verity-compiler`: CLI regression tests evaluate typed-interface ECMs
  -- through the Lean interpreter.
  supportInterpreter := true

-- Emits the canonical storage-layout audit artifact (#1897). Lives at the
-- package root because it imports both Compiler and Contracts, which the
-- Compiler -> Contracts boundary forbids inside `Compiler/`.
lean_lib «StorageLayoutReport» where
  globs := #[.one `StorageLayoutReport]

lean_exe «verity-storage-layout-report» where
  root := `StorageLayoutReport
  supportInterpreter := true