Fix #249: [Milestone 3 prerequisite] Create and populate bench/policy-compliance-fixtures with 6 verification tasks

bench/policy-compliance-fixtures/README.md

@@ -0,0 +1,153 @@
+# policy-compliance-fixtures
+
+Six policy-compliance verification tasks that serve as the shared input corpus
+for the Milestone 3 comparative analysis in `bench/symbolic-comparison.md`
+(parent issue: `bench/symbolic-comparison.md`). Each task describes a single
+authorization / resource-access / data-protection policy together with:
+
+- its **policy rules** (the declarative invariant the verifier must enforce),
+- its **known paths / branches** (the reachable verdict branches, each with a
+  concrete witness input that exercises it),
+- a **concrete representation** (a CEL boolean expression runnable today via
+  `POST /v1/verify/criterion` with `verify_method: "cel_expr"`), and
+- a **symbolic representation** (an SMT-LIB2 formula runnable today via
+  `POST /v1/verify/z3`, and the future symbolic-execution engine).
+
+The two representations express the *same* allow-path condition so that
+concrete testing and symbolic execution can be compared apples-to-apples on
+path coverage and constraint-solving time.
+
+This sub-issue only ships the fixtures. Running both engines over them and
+writing the comparison document is the parent issue's job.
+
+## Fixture set
+
+The six tasks are ordered by increasing structural complexity, spanning the
+range required by the acceptance criteria (simple condition → complex nested
+policy):
+
+| # | File | Domain | Complexity | Branches | Construct introduced |
+|---|------|--------|------------|----------|-----------------------|
+| 1 | [`auth-minimum-age.json`](auth-minimum-age.json)         | authorization | simple    | 2 | single relational condition |
+| 2 | [`rbac-role-check.json`](rbac-role-check.json)           | authorization | simple    | 3 | disjunction / set membership |
+| 3 | [`resource-quota.json`](resource-quota.json)             | resource-access | moderate | 2 | linear arithmetic over 3 vars |
+| 4 | [`time-window-access.json`](time-window-access.json)     | resource-access | moderate | 3 | nested conjunction of bounds |
+| 5 | [`tiered-rate-limit.json`](tiered-rate-limit.json)       | resource-access | complex  | 3 | mixed disjunction + conjunction |
+| 6 | [`data-residency-geo.json`](data-residency-geo.json)     | data-protection | complex  | 4 | conjunctive predicate set + negated membership |
+
+Every task carries a `complexity` field; together they cover simple
+conditions, moderate constraints, and complex nested policies.
+
+## Per-task summary
+
+### 1. `auth-minimum-age` — Minimum-age authorization gate (simple)
+**Policy.** Principal age MUST be >= 18.
+**Paths.** `allow` (`age >= 18`, witness `age=18`) · `deny` (`age < 18`, witness `age=12`).
+**CEL.** `age >= 18`  ·  **SMT.** `(assert (>= age 18))` → `sat`.
+**Expected behavior.** Boundary `age == 18` is allowed (closed lower bound); both branches are independently feasible.
+
+### 2. `rbac-role-check` — Role-based access control (simple, disjunctive)
+**Policy.** Role MUST be in `{admin, editor}`.
+**Paths.** `allow-admin` (`admin`) · `allow-editor` (`editor`) · `deny-other` (witness `viewer`).
+**CEL.** `role == "admin" || role == "editor"`  ·  **SMT.** `(assert (or (= role 1) (= role 2)))` → `sat` (role codes admin=1, editor=2).
+**Expected behavior.** Three feasible paths: one per allow-set member plus default deny.
+
+### 3. `resource-quota` — Capacity-arithmetic gate (moderate)
+**Policy.** `used + requested <= limit`.
+**Paths.** `allow-within-quota` (witness `used=30,requested=20,limit=100`) · `deny-over-quota` (witness `used=90,requested=20,limit=100`).
+**CEL.** `used + requested <= limit`  ·  **SMT.** `(assert (<= (+ used requested) limit))` → `sat`.
+**Expected behavior.** Boundary (`used + requested == limit`) is allowed; tests additive capacity reasoning rather than equality.
+
+### 4. `time-window-access` — Business-hours window (moderate, nested)
+**Policy.** `9 <= hour <= 17` AND `1 <= day <= 5` (Mon–Fri).
+**Paths.** `allow-business-hours` (witness `hour=12,day=3`) · `deny-off-hours` (witness `hour=23,day=3`) · `deny-weekend` (witness `hour=12,day=7`).
+**CEL.** `hour >= 9 && hour <= 17 && day >= 1 && day <= 5`  ·  **SMT.** conjunction of four bounds → `sat`.
+**Expected behavior.** Two independent ranged predicates; each fails on its own sub-path. `day` is 1..7 (1=Mon…7=Sun).
+
+### 5. `tiered-rate-limit` — Tiered limit with burst (complex, mixed)
+**Policy.** `request_count <= 100` OR (`request_count <= 200` AND `tier == "premium"`).
+**Paths.** `allow-under-base` (witness `count=50,tier=free`) · `allow-premium-burst` (witness `count=150,tier=premium`) · `deny-over-limit` (witness `count=250,tier=premium`).
+**CEL.** `request_count <= 100 || (request_count <= 200 && tier == "premium")`  ·  **SMT.** mixed disjunction/conjunction → `sat` (tier code premium=1).
+**Expected behavior.** The burst path is reachable only through the nested conjunction; richest branching in the set.
+
+### 6. `data-residency-geo` — Geo-fencing compliance (complex, conjunctive)
+**Policy.** `region == "EU"` AND `country` NOT in `{"X","Y"}` AND `encrypted == true`.
+**Paths.** `allow-compliant` · `deny-wrong-region` · `deny-blocked-country` · `deny-unencrypted` (witnesses in the file).
+**CEL.** `region == "EU" && !(country in ["X", "Y"]) && encrypted == true`  ·  **SMT.** conjunction of equality + two negated equalities + boolean → `sat` (region EU=1; blocked X=10, Y=11).
+**Expected behavior.** Most predicate-dense policy; three independent deny sub-paths plus one allow path.
+
+## File format
+
+Each `<task-id>.json` is a self-contained task with this shape:
+
+```jsonc
+{
+  "id": "auth-minimum-age",            // stable identifier, matches file stem
+  "title": "...",
+  "category": "authorization",          // authorization | resource-access | data-protection
+  "complexity": "simple",               // simple | moderate | complex
+  "description": "...",                 // prose: what the policy enforces and why
+  "policy_rules": ["..."],              // declarative rules the verifier must enforce
+  "expected_behavior": "...",           // allow/deny semantics + boundary behaviour
+  "paths": [                            // reachable verdict branches (path coverage map)
+    { "id": "allow", "condition": "...", "verdict": "allow"|"deny",
+      "feasible": true, "witness": { "...": ... } }
+  ],
+  "representations": {
+    "cel":  { "endpoint": "POST /v1/verify/criterion", "verify_method": "cel_expr",
+              "expr": "...", "context_template": { "...": ... } },
+    "smt2": { "endpoint": "POST /v1/verify/z3",
+              "declarations": "(declare-const ...)", "policy_assertion": "(assert ...)",
+              "expected_check_sat": "sat", "notes": "..." }
+  },
+  "samples": [                          // concrete inputs + expected verdicts (golden cases)
+    { "name": "...", "context": { "...": ... }, "expected_cel": true, "expected_path": "allow" }
+  ]
+}
+```
+
+`paths[].witness` and `samples[].context` are concrete inputs that exercise a
+specific branch; the symbolic explorer uses the `paths` to enumerate coverage
+while the concrete tester uses `samples` (and the CEL `expr`) as golden cases.
+
+## Running the fixtures
+
+### Concrete testing (CEL — available today)
+
+POST a task's CEL representation to the criterion endpoint:
+
+```bash
+curl -s localhost:8080/v1/verify/criterion -d '{
+  "criterion": {
+    "id": "auth-minimum-age",
+    "verify_method": "cel_expr",
+    "arg": {"expr": "age >= 18", "context": {"age": 25}},
+    "level": "hard", "category": "security"
+  }
+}'
+# => {"ok":true,"criterionId":"auth-minimum-age"}
+```
+
+`bench/policy_compliance_fixtures_test.go` automates this: it loads every
+`*.json` in this directory, then runs each task's CEL `expr` against every
+`samples[].context` through the real `internal/cel` evaluator and asserts the
+result equals `samples[].expected_cel`. This is the concrete-testing
+acceptance criterion, pinned so it cannot silently regress.
+
+### Symbolic execution (SMT-LIB2 — available today via Z3; full engine pending)
+
+POST a task's SMT-LIB2 to the Z3 endpoint:
+
+```bash
+curl -s localhost:8080/v1/verify/z3 -d '{
+  "input": {"constraints_smt2": "(declare-const age Int) (assert (>= age 18))"}
+}'
+# => check-sat: sat
+```
+
+Each task's `representations.smt2` is pre-shaped for this endpoint
+(`declarations` + `policy_assertion`); the documented `expected_check_sat` is
+the result for the allow-path formula. Encoding notes (role/region/country
+integer codes, day-of-week numbering) are recorded in each file's `smt2.notes`
+and in the per-task summaries above so the future `internal/symbolic`
+path-explorer can consume them without re-deriving the mapping.

bench/policy-compliance-fixtures/auth-minimum-age.json

@@ -0,0 +1,37 @@
+{
+  "id": "auth-minimum-age",
+  "title": "Minimum-age authorization gate",
+  "category": "authorization",
+  "complexity": "simple",
+  "description": "A principal may access a resource only if their declared age is at least the minimum threshold (18). This is the smallest meaningful policy: a single relational condition with two reachable branches (grant / deny). It is the baseline against which the more complex fixtures are compared.",
+  "policy_rules": [
+    "The principal's age MUST be greater than or equal to 18 to be authorized.",
+    "Any age below 18 MUST be denied regardless of other attributes."
+  ],
+  "expected_behavior": "An access request evaluates to allow when age >= 18 and to deny when age < 18. The boundary value age == 18 must be allowed (closed lower bound). Both branches are independently feasible, so a symbolic explorer must enumerate two paths and a concrete tester must observe both verdicts.",
+  "paths": [
+    { "id": "allow", "condition": "age >= 18", "verdict": "allow", "feasible": true, "witness": { "age": 18 } },
+    { "id": "deny", "condition": "age < 18", "verdict": "deny", "feasible": true, "witness": { "age": 12 } }
+  ],
+  "representations": {
+    "cel": {
+      "endpoint": "POST /v1/verify/criterion",
+      "verify_method": "cel_expr",
+      "expr": "age >= 18",
+      "context_template": { "age": 0 }
+    },
+    "smt2": {
+      "endpoint": "POST /v1/verify/z3",
+      "declarations": "(declare-const age Int)",
+      "policy_assertion": "(assert (>= age 18))",
+      "expected_check_sat": "sat",
+      "notes": "Integer age; the policy assertion is the allow-path condition, so check-sat is sat with model age=18."
+    }
+  },
+  "samples": [
+    { "name": "adult", "context": { "age": 25 }, "expected_cel": true, "expected_path": "allow" },
+    { "name": "boundary-min", "context": { "age": 18 }, "expected_cel": true, "expected_path": "allow" },
+    { "name": "one-below-min", "context": { "age": 17 }, "expected_cel": false, "expected_path": "deny" },
+    { "name": "minor", "context": { "age": 12 }, "expected_cel": false, "expected_path": "deny" }
+  ]
+}

bench/policy-compliance-fixtures/data-residency-geo.json

@@ -0,0 +1,43 @@
+{
+  "id": "data-residency-geo",
+  "title": "Data-residency / geo-fencing compliance (conjunctive predicate set with negated membership)",
+  "category": "data-protection",
+  "complexity": "complex",
+  "description": "A record may be persisted only when ALL of the following hold: it is stored in the EU residency region, it is not in a blocked-country set, and it is encrypted at rest. This fixture exercises a conjunction of heterogeneous predicates (equality on an enumerated region, negated membership over a country blocklist, and a boolean flag), which is the most predicate-dense policy in the set and stresses both path enumeration and the solver's conjunction reasoning.",
+  "policy_rules": [
+    "region MUST equal \"EU\".",
+    "country MUST NOT be a member of the blocked set {\"X\", \"Y\"}.",
+    "encrypted MUST be true.",
+    "The record is allowed only when ALL three rules hold simultaneously."
+  ],
+  "expected_behavior": "The record is allowed only when region == EU AND country is not blocked AND encrypted == true. Each predicate fails independently, so there are three deny sub-paths (wrong region, blocked country, unencrypted) in addition to the single allow path. In the SMT-LIB encoding, region is mapped to an integer code (EU=1) and country to integer codes (blocked: X=10, Y=11).",
+  "paths": [
+    { "id": "allow-compliant", "condition": "region == \"EU\" && !(country in [\"X\", \"Y\"]) && encrypted == true", "verdict": "allow", "feasible": true, "witness": { "region": "EU", "country": "DE", "encrypted": true } },
+    { "id": "deny-wrong-region", "condition": "region != \"EU\" && !(country in [\"X\", \"Y\"]) && encrypted == true", "verdict": "deny", "feasible": true, "witness": { "region": "US", "country": "DE", "encrypted": true } },
+    { "id": "deny-blocked-country", "condition": "region == \"EU\" && country in [\"X\", \"Y\"] && encrypted == true", "verdict": "deny", "feasible": true, "witness": { "region": "EU", "country": "X", "encrypted": true } },
+    { "id": "deny-unencrypted", "condition": "region == \"EU\" && !(country in [\"X\", \"Y\"]) && encrypted == false", "verdict": "deny", "feasible": true, "witness": { "region": "EU", "country": "DE", "encrypted": false } }
+  ],
+  "representations": {
+    "cel": {
+      "endpoint": "POST /v1/verify/criterion",
+      "verify_method": "cel_expr",
+      "expr": "region == \"EU\" && !(country in [\"X\", \"Y\"]) && encrypted == true",
+      "context_template": { "region": "", "country": "", "encrypted": false }
+    },
+    "smt2": {
+      "endpoint": "POST /v1/verify/z3",
+      "declarations": "(declare-const region Int)(declare-const country Int)(declare-const encrypted Bool)",
+      "policy_assertion": "(assert (and (= region 1) (not (= country 10)) (not (= country 11)) encrypted))",
+      "expected_check_sat": "sat",
+      "notes": "Conjunction over equality, two negated equalities, and a boolean; region EU=1, blocked countries X=10/Y=11. Satisfiable (e.g. region=1, country=5, encrypted=true)."
+    }
+  },
+  "samples": [
+    { "name": "eu-de-encrypted", "context": { "region": "EU", "country": "DE", "encrypted": true }, "expected_cel": true, "expected_path": "allow-compliant" },
+    { "name": "eu-fr-encrypted", "context": { "region": "EU", "country": "FR", "encrypted": true }, "expected_cel": true, "expected_path": "allow-compliant" },
+    { "name": "us-de-encrypted", "context": { "region": "US", "country": "DE", "encrypted": true }, "expected_cel": false, "expected_path": "deny-wrong-region" },
+    { "name": "eu-x-encrypted", "context": { "region": "EU", "country": "X", "encrypted": true }, "expected_cel": false, "expected_path": "deny-blocked-country" },
+    { "name": "eu-y-encrypted", "context": { "region": "EU", "country": "Y", "encrypted": true }, "expected_cel": false, "expected_path": "deny-blocked-country" },
+    { "name": "eu-de-plaintext", "context": { "region": "EU", "country": "DE", "encrypted": false }, "expected_cel": false, "expected_path": "deny-unencrypted" }
+  ]
+}

bench/policy-compliance-fixtures/rbac-role-check.json

@@ -0,0 +1,38 @@
+{
+  "id": "rbac-role-check",
+  "title": "Role-based access control (disjunctive membership)",
+  "category": "authorization",
+  "complexity": "simple",
+  "description": "A write operation is permitted only when the principal holds one of the privileged roles in the allow-set {admin, editor}. This fixture introduces a disjunction over an enumerated domain, exercising the membership-check path that symbolic execution must split into one branch per allow-set member plus a default deny branch.",
+  "policy_rules": [
+    "The principal's role MUST be a member of the allow-set {admin, editor} to write.",
+    "Any role outside the allow-set MUST be denied write access."
+  ],
+  "expected_behavior": "Write is allowed for role == admin or role == editor and denied for every other role. The allow-set has two members, so the symbolic explorer must enumerate three feasible paths (admin, editor, other). In the SMT-LIB encoding, roles are mapped to integer codes: admin=1, editor=2, all other roles=0.",
+  "paths": [
+    { "id": "allow-admin", "condition": "role == \"admin\"", "verdict": "allow", "feasible": true, "witness": { "role": "admin" } },
+    { "id": "allow-editor", "condition": "role == \"editor\"", "verdict": "allow", "feasible": true, "witness": { "role": "editor" } },
+    { "id": "deny-other", "condition": "role != \"admin\" && role != \"editor\"", "verdict": "deny", "feasible": true, "witness": { "role": "viewer" } }
+  ],
+  "representations": {
+    "cel": {
+      "endpoint": "POST /v1/verify/criterion",
+      "verify_method": "cel_expr",
+      "expr": "role == \"admin\" || role == \"editor\"",
+      "context_template": { "role": "" }
+    },
+    "smt2": {
+      "endpoint": "POST /v1/verify/z3",
+      "declarations": "(declare-const role Int)",
+      "policy_assertion": "(assert (or (= role 1) (= role 2)))",
+      "expected_check_sat": "sat",
+      "notes": "Role codes: admin=1, editor=2. The disjunction is satisfiable (e.g. role=1)."
+    }
+  },
+  "samples": [
+    { "name": "admin", "context": { "role": "admin" }, "expected_cel": true, "expected_path": "allow-admin" },
+    { "name": "editor", "context": { "role": "editor" }, "expected_cel": true, "expected_path": "allow-editor" },
+    { "name": "viewer", "context": { "role": "viewer" }, "expected_cel": false, "expected_path": "deny-other" },
+    { "name": "empty", "context": { "role": "" }, "expected_cel": false, "expected_path": "deny-other" }
+  ]
+}

bench/policy-compliance-fixtures/resource-quota.json

@@ -0,0 +1,37 @@
+{
+  "id": "resource-quota",
+  "title": "Resource quota / capacity-arithmetic gate",
+  "category": "resource-access",
+  "complexity": "moderate",
+  "description": "A provisioning request is accepted only when current usage plus the requested amount stays within the tenant's quota limit. This fixture introduces linear integer arithmetic over three variables, exercising the solver's ability to reason about additive capacity rather than simple equality/membership.",
+  "policy_rules": [
+    "used + requested MUST NOT exceed the tenant quota limit.",
+    "The request MUST be denied when used + requested > limit."
+  ],
+  "expected_behavior": "The request is allowed when (used + requested) <= limit and denied when (used + requested) > limit. The boundary case (used + requested == limit) is allowed. Both branches are feasible: a small request against a fresh tenant is allowed; an over-large request is denied.",
+  "paths": [
+    { "id": "allow-within-quota", "condition": "used + requested <= limit", "verdict": "allow", "feasible": true, "witness": { "used": 30, "requested": 20, "limit": 100 } },
+    { "id": "deny-over-quota", "condition": "used + requested > limit", "verdict": "deny", "feasible": true, "witness": { "used": 90, "requested": 20, "limit": 100 } }
+  ],
+  "representations": {
+    "cel": {
+      "endpoint": "POST /v1/verify/criterion",
+      "verify_method": "cel_expr",
+      "expr": "used + requested <= limit",
+      "context_template": { "used": 0, "requested": 0, "limit": 0 }
+    },
+    "smt2": {
+      "endpoint": "POST /v1/verify/z3",
+      "declarations": "(declare-const used Int)(declare-const requested Int)(declare-const limit Int)",
+      "policy_assertion": "(assert (<= (+ used requested) limit))",
+      "expected_check_sat": "sat",
+      "notes": "Linear arithmetic over non-negative integers; satisfiable (e.g. used=0, requested=0, limit=1)."
+    }
+  },
+  "samples": [
+    { "name": "well-within", "context": { "used": 30, "requested": 20, "limit": 100 }, "expected_cel": true, "expected_path": "allow-within-quota" },
+    { "name": "exactly-at-limit", "context": { "used": 80, "requested": 20, "limit": 100 }, "expected_cel": true, "expected_path": "allow-within-quota" },
+    { "name": "one-over-limit", "context": { "used": 81, "requested": 20, "limit": 100 }, "expected_cel": false, "expected_path": "deny-over-quota" },
+    { "name": "far-over-limit", "context": { "used": 90, "requested": 50, "limit": 100 }, "expected_cel": false, "expected_path": "deny-over-quota" }
+  ]
+}