verity/Contracts/Specs.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
/-
  Contracts.Specs: Declarative Contract Specifications

  Shipped compiler inputs are the macro-generated `CompilationModel` values
  emitted by `verity_contract`. This module keeps the manual `cryptoHashSpec`
  special case (external-library linking demo) plus the canonical `allSpecs`
  list of macro-generated specs.
-/

import Compiler.CompilationModel
import Contracts.Counter
import Contracts.SimpleStorage
import Contracts.Owned
import Contracts.OwnedCounter
import Contracts.SafeCounter
import Contracts.Ledger
import Contracts.Vault
import Contracts.SimpleToken
import Contracts.ERC20

namespace Compiler.Specs

open Compiler.CompilationModel

/-!
## CryptoHash Specification (External Library Linking Demo)

Demonstrates `Expr.externalCall` for linking external Yul libraries at
compile time. The EDSL placeholder in `Contracts/CryptoHash/Contract.lean`
uses simple addition; the `CompilationModel` below calls the real library
functions (`PoseidonT3_hash`, `PoseidonT4_hash`) which are injected by
the Linker when you pass `--link examples/external-libs/PoseidonT3.yul`.
-/

def cryptoHashSpec : CompilationModel := {
  name := "CryptoHash"
  fields := [
    { name := "lastHash", ty := FieldType.uint256 }
  ]
  «constructor» := none
  externals := [
    { name := "PoseidonT3_hash"
      params := [ParamType.uint256, ParamType.uint256]
      returnType := some ParamType.uint256
      axiomNames := ["poseidon_t3_deterministic", "poseidon_t3_collision_resistant"] },
    { name := "PoseidonT4_hash"
      params := [ParamType.uint256, ParamType.uint256, ParamType.uint256]
      returnType := some ParamType.uint256
      axiomNames := ["poseidon_t4_deterministic", "poseidon_t4_collision_resistant"] }
  ]
  functions := [
    { name := "storeHashTwo"
      params := [
        { name := "a", ty := ParamType.uint256 },
        { name := "b", ty := ParamType.uint256 }
      ]
      returnType := none
      body := [
        Stmt.letVar "h" (Expr.externalCall "PoseidonT3_hash" [Expr.param "a", Expr.param "b"]),
        Stmt.setStorage "lastHash" (Expr.localVar "h"),
        Stmt.stop
      ]
    },
    { name := "storeHashThree"
      params := [
        { name := "a", ty := ParamType.uint256 },
        { name := "b", ty := ParamType.uint256 },
        { name := "c", ty := ParamType.uint256 }
      ]
      returnType := none
      body := [
        Stmt.letVar "h" (Expr.externalCall "PoseidonT4_hash" [Expr.param "a", Expr.param "b", Expr.param "c"]),
        Stmt.setStorage "lastHash" (Expr.localVar "h"),
        Stmt.stop
      ]
    },
    { name := "getLastHash"
      params := []
      returnType := some FieldType.uint256
      body := [
        Stmt.return (Expr.storage "lastHash")
      ]
    }
  ]
}

/-!
## Generate All Contracts

`allSpecs` lists every contract that compiles without external dependencies.
`cryptoHashSpec` is excluded because it requires `--link` flags for external
Yul libraries (PoseidonT3/T4). Use `lake exe verity-compiler --link ...` to
compile it separately.

**Adding a new contract (canonical path)**: add a `verity_contract` declaration
in `Contracts/<Name>/<Name>.lean`, then add the generated `<Name>.spec`
to `allSpecs` below.

Selectors are still auto-computed by `computeSelectors`.
-/

def allSpecs : List CompilationModel := [
  Contracts.SimpleStorage.spec,
  Contracts.Counter.spec,
  Contracts.Owned.spec,
  Contracts.Ledger.spec,
  Contracts.Vault.spec,
  Contracts.OwnedCounter.spec,
  Contracts.SimpleToken.spec,
  Contracts.SafeCounter.spec,
  Contracts.ERC20.spec
]

end Compiler.Specs