echidna/alloyiser.toml at main · hyperpolymath/echidna · 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
# SPDX-License-Identifier: PMPL-1.0-or-later
# alloyiser manifest for echidna
# Echidna has REST, GraphQL, and gRPC interfaces under src/interfaces/

[project]
name = "echidna"

[[specs]]
name = "echidna-rest"
source = "/var/mnt/eclipse/repos/verification-ecosystem/echidna/src/interfaces/rest/models.rs"
format = "openapi"

[[specs]]
name = "echidna-graphql"
source = "/var/mnt/eclipse/repos/verification-ecosystem/echidna/src/interfaces/graphql/schema.rs"
format = "graphql"

[[specs]]
name = "echidna-grpc"
source = "/var/mnt/eclipse/repos/verification-ecosystem/echidna/src/interfaces/grpc/proto/echidna.proto"
format = "openapi"

[[assertions]]
name = "no-orphan-records"
check = "all r: Record | some r.owner"
scope = 5

[[assertions]]
name = "proof-integrity"
check = "all p: Proof | p.status = Verified implies some p.theorem"
scope = 5

[[assertions]]
name = "rule-determinism"
check = "all r: Rule, s: State | lone r.apply[s]"
scope = 6

[alloy]
solver = "sat4j"
max-scope = 6