Skip to content

Commit 4bd92a4

Browse files
committed
feat: wire conflow config validation pipeline
1 parent 984342a commit 4bd92a4

6 files changed

Lines changed: 147 additions & 0 deletions

File tree

.conflow.yaml

Lines changed: 38 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,38 @@
1+
# conflow pipeline - Full generate → validate → export
2+
version: "1"
3+
name: "echidna"
4+
5+
stages:
6+
- name: "generate"
7+
description: "Generate configuration using Nickel"
8+
tool:
9+
type: nickel
10+
command: export
11+
file: configs/config.ncl
12+
format: json
13+
input: "configs/config.ncl"
14+
output: generated/config.json
15+
16+
- name: "validate"
17+
description: "Validate against CUE schema"
18+
tool:
19+
type: cue
20+
command: vet
21+
schemas:
22+
- schemas/config.cue
23+
input:
24+
from_stage: generate
25+
depends_on:
26+
- generate
27+
28+
- name: "export"
29+
description: "Export final configuration as YAML"
30+
tool:
31+
type: cue
32+
command: export
33+
out_format: yaml
34+
input:
35+
from_stage: generate
36+
output: deploy/config.yaml
37+
depends_on:
38+
- validate

alloyiser.toml

Lines changed: 40 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,40 @@
1+
# SPDX-License-Identifier: PMPL-1.0-or-later
2+
# alloyiser manifest for echidna
3+
# Echidna has REST, GraphQL, and gRPC interfaces under src/interfaces/
4+
5+
[project]
6+
name = "echidna"
7+
8+
[[specs]]
9+
name = "echidna-rest"
10+
source = "/var/mnt/eclipse/repos/echidna/src/interfaces/rest/models.rs"
11+
format = "openapi"
12+
13+
[[specs]]
14+
name = "echidna-graphql"
15+
source = "/var/mnt/eclipse/repos/echidna/src/interfaces/graphql/schema.rs"
16+
format = "graphql"
17+
18+
[[specs]]
19+
name = "echidna-grpc"
20+
source = "/var/mnt/eclipse/repos/echidna/src/interfaces/grpc/proto/echidna.proto"
21+
format = "openapi"
22+
23+
[[assertions]]
24+
name = "no-orphan-records"
25+
check = "all r: Record | some r.owner"
26+
scope = 5
27+
28+
[[assertions]]
29+
name = "proof-integrity"
30+
check = "all p: Proof | p.status = Verified implies some p.theorem"
31+
scope = 5
32+
33+
[[assertions]]
34+
name = "rule-determinism"
35+
check = "all r: Rule, s: State | lone r.apply[s]"
36+
scope = 6
37+
38+
[alloy]
39+
solver = "sat4j"
40+
max-scope = 6

configs/config.ncl

Lines changed: 11 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,11 @@
1+
# Configuration generation
2+
{
3+
name = "my-app",
4+
replicas =
5+
let env = "dev" in
6+
if env == "prod" then 5
7+
else if env == "staging" then 3
8+
else 1,
9+
port = 8080,
10+
env = "dev",
11+
}

generated/alloyiser/echidna.als

Lines changed: 21 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,21 @@
1+
module echidna
2+
3+
// Formal model generated by alloyiser from project 'echidna'.
4+
// Verify with: java -jar alloy.jar echidna.als
5+
assert no_orphan_records {
6+
all r: Record | some r.owner
7+
}
8+
check no_orphan_records for 5
9+
10+
assert proof_integrity {
11+
all p: Proof | p.status = Verified implies some p.theorem
12+
}
13+
check proof_integrity for 5
14+
15+
assert rule_determinism {
16+
all r: Rule, s: State | lone r.apply[s]
17+
}
18+
check rule_determinism for 6
19+
20+
// Visualise a sample instance
21+
run {} for 5
Lines changed: 28 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,28 @@
1+
#!/bin/sh
2+
# SPDX-License-Identifier: PMPL-1.0-or-later
3+
# Generated by alloyiser — Alloy analysis script
4+
# Requires: java, alloy.jar
5+
6+
ALLOY_JAR="alloy.jar"
7+
MODEL="/var/mnt/eclipse/repos/echidna/generated/alloyiser/echidna.als"
8+
SOLVER="sat4j"
9+
TIMEOUT="300"
10+
11+
echo "=== alloyiser analysis ==="
12+
echo "Model: $MODEL"
13+
echo "Solver: $SOLVER"
14+
echo "Assertions: 3"
15+
16+
echo "Checking: no_orphan_records..."
17+
timeout "$TIMEOUT" java -jar "$ALLOY_JAR" -batch -solver "$SOLVER" "$MODEL" 2>&1 | grep -A5 "no_orphan_records"
18+
echo ""
19+
20+
echo "Checking: proof_integrity..."
21+
timeout "$TIMEOUT" java -jar "$ALLOY_JAR" -batch -solver "$SOLVER" "$MODEL" 2>&1 | grep -A5 "proof_integrity"
22+
echo ""
23+
24+
echo "Checking: rule_determinism..."
25+
timeout "$TIMEOUT" java -jar "$ALLOY_JAR" -batch -solver "$SOLVER" "$MODEL" 2>&1 | grep -A5 "rule_determinism"
26+
echo ""
27+
28+
echo "=== analysis complete ==="

schemas/config.cue

Lines changed: 9 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,9 @@
1+
// Configuration schema
2+
package config
3+
4+
#Config: {
5+
name: string
6+
replicas: int & >=1
7+
port: int & >=1 & <=65535
8+
env: string
9+
}

0 commit comments

Comments
 (0)