Shahzad Bhatti Welcome to my ramblings and rants!

timeline
    title AI Paradigms and Verification Approaches
    section Logic Era (1970s–1990s)
        1972 : Prolog — logic programming and knowledge representation
        1979 : Boyer-Moore theorem prover
        1986 : Eiffel introduces Design by Contract
        1987 : TLA created by Leslie Lamport
    section Hybrid Era (2000s–2010s)
        1999 : Z3 SMT solver (Microsoft Research)
        2005 : Alloy model finder
        2009 : Dafny created (Microsoft Research)
        2014 : TLA+ used at AWS for S3 and DynamoDB
    section LLM Era (2020s)
        2022 : ChatGPT and Copilot — probabilistic code generation goes mainstream
        2024 : Agentic coding — 10× code throughput becomes normal
        2025 : Spec-driven development movement emerges
        2026 : Formal verification as AI guardrail

has_role(alice, viewer).
has_role(bob, editor).
role_inherits(editor, viewer).
role_grants(viewer, read, docs).
role_grants(editor, write, docs).

can_access(User, Action, Resource) :-
    has_role(User, Role),
    role_grants(Role, Action, Resource).
can_access(User, Action, Resource) :-
    has_role(User, Role),
    role_inherits(Role, Parent),
    role_grants(Parent, Action, Resource).

?- can_access(bob, read, docs).
% Yes — bob is editor, editor inherits viewer, viewer grants read:docs.

Example: (A v B) ^ (¬A v C) ^ (¬B v ¬C)
SAT solver: A=true, B=false, C=true

(assert (= (+ x y) 10))
(assert (> x 3))
(assert (> y 3))
(check-sat)
--> sat; x=4, y=6

from ortools.sat.python import cp_model
model = cp_model.CpModel()
x = model.new_int_var(0, 10, 'x')
y = model.new_int_var(0, 10, 'y')
model.add(x + y == 10)
model.add(x > 3)
model.add(y > 3)
solver = cp_model.CpSolver()
solver.solve(model)  # finds x=4, y=6

Admin A: check(submitter) --> no conflict --> intend to assign
Admin B: check(approver)  --> no conflict --> intend to assign
Admin A: assign(submitter) OK
Admin B: assign(approver)   <-- SoD violated: both roles now held

(* Safety: SoD never violated *)
SoDOK ==
  ~(\E r1, r2 \in assigned : r1 # r2 /\ <<r1,r2>> \in Conflicts)

(* Liveness: every pending assignment eventually completes *)
Liveness ==
  \A a \in Admins :
    [](phase[a] = "checking" => <>(phase[a] \in {"done", "idle"}))

Model checking completed. No error has been found.
2349 states generated, 1046 distinct states found, 0 states left on queue.

java -jar ~/tla2tools.jar -config tla/RBACPolicyChange.cfg tla/RBACPolicyChange.tla

method Divide(a: int, b: int) returns (result: int)
  requires b != 0           // precondition: caller must ensure this
  ensures result * b == a   // postcondition: callee guarantees this
{
  return a / b;
}

predicate ValidStore(s: RBACStore) {
  // No dangling principal references
  && (forall id :: id in s.principals ==>
        s.principals[id].orgId in s.orgs)
  // Tenant isolation: role parents must be in same org
  && (forall rid :: rid in s.roles ==>
        (forall pid :: pid in SeqToSet(s.roles[rid].parentIds) ==>
           s.roles[pid].orgId == s.roles[rid].orgId))
  // Claim resources must exist in the store
  && (forall rid :: rid in s.roles ==>
        (forall c :: c in s.roles[rid].claims ==>
           c.resourceId in s.resources))
  // ... (8 more invariants)
}

lemma EmptyStoreIsValid()
  ensures ValidStore(EmptyStore())
{}

SOUNDNESS:    If Evaluate returns Allow, a valid claim chain EXISTS.
              No phantom permissions. No false positives.

COMPLETENESS: If a valid claim chain exists, Evaluate returns Allow.
              No missed permissions. No false negatives.

// The specification — states what "correct" means mathematically
predicate PolicySpec(req: Request, store: RBACStore, ctx: EvalContext) {
  var principal := store.principals[req.principalId];
  exists c :: c in PrincipalClaims(principal, store.roles) &&
              ClaimGrants(c, req.action, req.resourceId, ctx)
}

// The implementation — Dafny proves it matches PolicySpec for all inputs
method Evaluate(req: Request, store: RBACStore, ctx: EvalContext)
    returns (decision: Decision)
  requires ValidStore(store)
  requires req.principalId in store.principals
  requires store.principals[req.principalId].orgId == req.orgId
  ensures decision == Allow ==> PolicySpec(req, store, ctx)    // SOUNDNESS
  ensures decision == Deny  ==> !PolicySpec(req, store, ctx)   // COMPLETENESS

while i < |claimSeq|
  invariant decision == Deny ==>
    forall j :: 0 <= j < i ==>
      !ClaimGrants(claimSeq[j], req.action, req.resourceId, ctx)
  decreases |claimSeq| - i
{
  if ClaimGrants(claimSeq[i], req.action, req.resourceId, ctx) {
    decision := Allow;
    return;
  }
  i := i + 1;
}

lemma MoreClaimsMonotonic(req, store1, store2, ctx)
  requires store1 has subset of claims of store2
  ensures PolicySpec(req, store1, ctx) ==> PolicySpec(req, store2, ctx)

method AddParent(child: RoleId, parent: RoleId, roles: map<RoleId, Role>)
    returns (result: map<RoleId, Role>, ok: bool)
  requires NoCycles(roles)
  ensures ok  ==> NoCycles(result)    // DAG invariant always preserved
  ensures !ok ==> result == roles     // rejection leaves the store unchanged
{
  var wouldCycle := child in Ancestors(parent, roles, |roles|);
  if wouldCycle { return roles, false; }
  // safe to add the parent edge
}

predicate SoDSatisfied(assignedRoles: set<RoleId>, conflicts: ConflictSet) {
  forall a, b ::
    a in assignedRoles && b in assignedRoles && a != b ==>
      (a, b) !in conflicts
}

method AssignRole(principal, newRole, conflicts)
  requires SoDSatisfied(SeqToSet(principal.roleIds), conflicts)
  ensures ok  ==> SoDSatisfied(SeqToSet(updated.roleIds), conflicts)
  ensures !ok ==> exists existing ::
    existing in SeqToSet(principal.roleIds) &&
    (existing, newRole) in conflicts   // proof witness for why it was rejected

rbac_separation_of_duty.dfy(42,4): Error: a postcondition could not be proved
  ensures ok ==> SoDSatisfied(SeqToSet(updated.roleIds), conflicts)

Counterexample:
  principal.roleIds = ["approver"]
  newRole = "submitter"
  conflicts = {("submitter", "approver")}  ? (new, existing) direction missed

// Adding constraints can only reduce access, never increase it
lemma AddingConstraintReducesAccess(base, extra, ctx)
  ensures AllConstraintsHold(base + [extra], ctx) ==>
          AllConstraintsHold(base, ctx)

// Empty constraint list always passes (vacuous truth — no constraints = no restrictions)
lemma EmptyConstraintsAlwaysHold(ctx)
  ensures AllConstraintsHold([], ctx)
{}

// Higher usage makes quota constraints harder to satisfy
lemma HigherUsageHarder(limit, usage1, usage2, ctx)
  requires usage1 <= usage2
  ensures ConstraintHolds(MaxUsage(limit), ctx[usage:=usage2]) ==>
          ConstraintHolds(MaxUsage(limit), ctx[usage:=usage1])

// go/pkg/types/types.go

type Claim struct {
    ID          ClaimID
    Action      string
    ResourceID  ResID
    Constraints []Constraint   // empty = always passes (vacuous truth, proved by EmptyConstraintsAlwaysHold)
}

// NewTimeWindow enforces the Dafny precondition ValidConstraint at construction time
func NewTimeWindow(start, end int) (Constraint, error) {
    if start >= end || end > 24 {
        return Constraint{}, fmt.Errorf("invalid time window: start < end <= 24 required")
    }
    return Constraint{Kind: TimeWindowKind, StartHour: start, EndHour: end}, nil
}

// NewGeoFence — Dafny requires |regions| > 0
func NewGeoFence(regions []string) (Constraint, error) {
    if len(regions) == 0 {
        return Constraint{}, fmt.Errorf("geo fence requires at least one region")
    }
    return Constraint{Kind: GeoFenceKind, Regions: regions}, nil
}

// NewMaxUsage — Dafny requires limit > 0
func NewMaxUsage(limit int) (Constraint, error) {
    if limit <= 0 {
        return Constraint{}, fmt.Errorf("max usage limit must be positive")
    }
    return Constraint{Kind: MaxUsageKind, MaxCount: limit}, nil
}

// go/pkg/constraints/constraints.go

// Holds mirrors Dafny's ConstraintHolds predicate exactly.
// Every case corresponds to a branch in the Dafny match expression.
func Holds(c types.Constraint, ctx types.EvalContext) bool {
    switch c.Kind {
    case types.TimeWindowKind:
        // Dafny: ctx.currentHour >= c.startHour && ctx.currentHour < c.endHour
        return ctx.CurrentHour >= c.StartHour && ctx.CurrentHour < c.EndHour
    case types.GeoFenceKind:
        // Dafny: ctx.currentRegion in c.allowedRegions
        for _, r := range c.Regions {
            if r == ctx.CurrentRegion {
                return true
            }
        }
        return false
    case types.MaxUsageKind:
        // Dafny: ctx.currentUsage < c.maxCount
        return ctx.CurrentUsage < c.MaxCount
    default:
        return false
    }
}

// AllHold evaluates a conjunction of constraints.
// Dafny proved: AllConstraintsHold([], ctx) == true (EmptyConstraintsAlwaysHold)
// Dafny proved: AllConstraintsHold(base + [extra], ctx) ==> AllConstraintsHold(base, ctx)
func AllHold(cs []types.Constraint, ctx types.EvalContext) bool {
    for _, c := range cs {
        if !Holds(c, ctx) {
            return false
        }
    }
    return true
}

// go/pkg/hierarchy/hierarchy.go

// HasCycle returns true if adding parent to child would create a cycle.
// Mirrors Dafny: child in Ancestors(parent, roles, |roles|)
func (r *Resolver) HasCycle(child, parent types.RoleID) bool {
    visited := map[types.RoleID]bool{}
    queue := []types.RoleID{parent}
    for len(queue) > 0 {
        current := queue[0]
        queue = queue[1:]
        if current == child {
            return true
        }
        if visited[current] {
            continue
        }
        visited[current] = true
        if role, ok := r.roles[current]; ok {
            queue = append(queue, role.ParentIDs...)
        }
    }
    return false
}

// AddParent adds a parent role with cycle guard.
// Mirrors Dafny: requires NoCycles, ensures NoCycles preserved or store unchanged.
func (r *Resolver) AddParent(child, parent types.RoleID) error {
    if r.HasCycle(child, parent) {
        return fmt.Errorf("adding parent %s to %s would create a cycle", parent, child)
    }
    role := r.roles[child]
    role.ParentIDs = append(role.ParentIDs, parent)
    r.roles[child] = role
    return nil
}

// TransitiveClaims collects all claims reachable through the role hierarchy.
// BFS bounded by number of roles — same as Dafny's fuel parameter.
func TransitiveClaims(roleID types.RoleID, roles map[types.RoleID]types.Role) []types.Claim {
    var claims []types.Claim
    visited := map[types.RoleID]bool{}
    queue := []types.RoleID{roleID}
    for len(queue) > 0 {
        current := queue[0]
        queue = queue[1:]
        if visited[current] {
            continue
        }
        visited[current] = true
        role, ok := roles[current]
        if !ok {
            continue
        }
        claims = append(claims, role.Claims...)
        queue = append(queue, role.ParentIDs...)
    }
    return claims
}

// go/pkg/store/store.go

// AssignRole mirrors Dafny AssignRole:
//   requires SoDSatisfied(current roles, conflicts)
//   ensures  SoDSatisfied(updated roles, conflicts) OR rejection with witness
func (s *Store) AssignRole(principalID types.PrinID, roleID types.RoleID) error {
    s.mu.Lock()
    defer s.mu.Unlock()

    principal, ok := s.principals[principalID]
    if !ok {
        return fmt.Errorf("principal %s not found", principalID)
    }
    role, ok := s.roles[roleID]
    if !ok {
        return fmt.Errorf("role %s not found", roleID)
    }
    // Tenant isolation — from Dafny ValidStore predicate
    if role.OrgID != principal.OrgID {
        return fmt.Errorf("tenant isolation: role org %s != principal org %s",
            role.OrgID, principal.OrgID)
    }
    // SoD conflict check — checks BOTH directions, per Dafny SoDSatisfied predicate
    for _, existingRoleID := range principal.RoleIDs {
        if s.hasConflict(existingRoleID, roleID) {
            return fmt.Errorf("separation of duty: role %q conflicts with existing role %q",
                roleID, existingRoleID)
        }
    }
    // Safe to assign — SoD preserved (Dafny ensures clause holds)
    principal.RoleIDs = append(principal.RoleIDs, roleID)
    s.principals[principalID] = principal
    return nil
}

// go/pkg/policy/policy.go

// Evaluate decides Allow or Deny for a request.
// Preconditions from Dafny requires clauses: request fields valid, principal exists, tenant matches.
// Postconditions from Dafny ensures clauses: Allow iff valid claim chain exists.
func (e *Engine) Evaluate(req types.Request, ctx types.EvalContext) (types.Decision, error) {
    if err := req.Validate(); err != nil {
        return types.Deny, fmt.Errorf("invalid request: %w", err)
    }
    principal, ok := e.store.GetPrincipal(req.PrincipalID)
    if !ok {
        return types.Deny, nil  // deny-by-default — proved by DenyByDefault lemma
    }
    if principal.OrgID != req.OrgID {
        return types.Deny, fmt.Errorf("tenant isolation violated")
    }
    // Walk transitive claims — same BFS algorithm as Dafny Evaluate method
    claims := hierarchy.PrincipalClaims(principal, e.store.AllRoles())
    for _, c := range claims {
        if constraints.ClaimGrants(c, req.Action, req.ResourceID, ctx) {
            return types.Allow, nil
        }
    }
    return types.Deny, nil
}

// go/pkg/policy/policy_test.go

// Mirrors: DenyByDefault lemma in rbac_invariants.dfy
func TestProp_NoRolesAlwaysDenied(t *testing.T) {
    props := gopter.NewProperties(gopter.DefaultTestParameters())
    props.Property("principal with no roles is always denied", prop.ForAll(
        func(action, resource string) bool {
            s := store.New()
            _ = s.AddOrg(types.Organization{ID: "org", Name: "org"})
            _ = s.AddResource(types.Resource{ID: resource, Name: resource, Kind: "api"})
            _ = s.AddPrincipal(types.Principal{ID: "p", OrgID: "org", Name: "P"})
            engine := policy.New(s)
            req := types.Request{OrgID: "org", PrincipalID: "p",
                Action: action, ResourceID: resource}
            decision, _ := engine.Evaluate(req, types.EvalContext{CurrentHour: 12})
            return decision == types.Deny
        },
        gen.AlphaString(), gen.AlphaString(),
    ))
    props.TestingRun(t, gopter.NewFormatedReporter(false, 80, os.Stdout))
}

// Mirrors: AddingConstraintReducesAccess lemma in rbac_constraints.dfy
func TestProp_ConstraintMonotonicity(t *testing.T) {
    props := gopter.NewProperties(gopter.DefaultTestParameters())
    props.Property("subset of constraints passing implies prefix passes", prop.ForAll(
        func(hour int, region string, usage int) bool {
            ctx := types.EvalContext{
                CurrentHour:   abs(hour) % 24,
                CurrentRegion: region,
                CurrentUsage:  abs(usage) % 100,
            }
            tw, _ := types.NewTimeWindow(9, 17)
            base := []types.Constraint{tw}
            geo, _ := types.NewGeoFence([]string{"us-east-1"})
            extended := append(base, geo)
            // If the extended (stricter) set passes, the base set MUST also pass
            if constraints.AllHold(extended, ctx) {
                return constraints.AllHold(base, ctx)
            }
            return true
        },
        gen.Int(), gen.AnyString(), gen.Int(),
    ))
    props.TestingRun(t, gopter.NewFormatedReporter(false, 80, os.Stdout))
}

// Mirrors: HigherUsageHarder lemma in rbac_constraints.dfy
func TestProp_QuotaMonotonicity(t *testing.T) {
    props := gopter.NewProperties(gopter.DefaultTestParameters())
    props.Property("higher usage never turns Deny into Allow for quota", prop.ForAll(
        func(limit int, lo int, delta int) bool {
            limit = abs(limit)%100 + 1
            lo = abs(lo) % 200
            hi := lo + abs(delta)%100   // hi >= lo guaranteed

            quota, _ := types.NewMaxUsage(limit)
            ctxLo := types.EvalContext{CurrentUsage: lo}
            ctxHi := types.EvalContext{CurrentUsage: hi}

            // If quota passes at HIGHER usage, it MUST pass at lower usage
            if constraints.Holds(quota, ctxHi) {
                return constraints.Holds(quota, ctxLo)
            }
            return true
        },
        gen.Int(), gen.Int(), gen.Int(),
    ))
    props.TestingRun(t, gopter.NewFormatedReporter(false, 80, os.Stdout))
}

// Mirrors: OwnClaimsIncluded lemma in rbac_role_hierarchy.dfy
func TestProp_OwnClaimsAlwaysIncluded(t *testing.T) {
    props := gopter.NewProperties(gopter.DefaultTestParameters())
    props.Property("role's own claims always appear in transitive claims", prop.ForAll(
        func(claimCount int) bool {
            claimCount = abs(claimCount)%5 + 1
            var claims []types.Claim
            for i := 0; i < claimCount; i++ {
                claims = append(claims, types.Claim{
                    ID:         types.ClaimID(fmt.Sprintf("c%d", i)),
                    Action:     fmt.Sprintf("action%d", i),
                    ResourceID: "res1",
                })
            }
            roles := map[types.RoleID]types.Role{
                "role1": {ID: "role1", OrgID: "org1", Claims: claims},
            }
            transitive := hierarchy.TransitiveClaims("role1", roles)
            for _, c := range claims {
                found := false
                for _, tc := range transitive {
                    if tc.ID == c.ID {
                        found = true
                        break
                    }
                }
                if !found {
                    return false
                }
            }
            return true
        },
        gen.Int(),
    ))
    props.TestingRun(t, gopter.NewFormatedReporter(false, 80, os.Stdout))
}

+ empty constraint list always passes: OK, passed 200 tests.
+ hour in [start,end) passes, hour outside fails: OK, passed 500 tests.
+ subset of constraints passing implies prefix passes: OK, passed 300 tests.
+ higher usage never turns Deny into Allow for quota: OK, passed 300 tests.
+ role's own claims always appear in transitive claims: OK, passed 200 tests.
+ adding a parent never reduces transitive claims: OK, passed 200 tests.
+ unknown principal is always denied: OK, passed 200 tests.
+ principal with no roles is always denied: OK, passed 200 tests.
PASS — 2300+ property-based test cases executed.

datatype ConstraintKind =
    | TimeWindow(startHour: nat, endHour: nat)
    | GeoFence(allowedRegions: seq<string>)
    | MaxUsage(maxCount: nat)
    | RateLimit(requestsPerMinute: nat)  // NEW

predicate ValidConstraint(c: ConstraintKind) {
    match c
    case TimeWindow(s, e) => 0 <= s < e <= 24
    case GeoFence(regions) => |regions| > 0
    case MaxUsage(max) => max > 0
    case RateLimit(rpm) => rpm > 0   // must be positive
}

predicate ConstraintHolds(c: ConstraintKind, ctx: EvalContext) {
    match c
    case TimeWindow(s, e) => s <= ctx.currentHour < e
    case GeoFence(regions) => ctx.currentRegion in regions
    case MaxUsage(max) => ctx.currentUsage < max
    case RateLimit(rpm) => ctx.currentRequestRate < rpm   // NEW
}

// Lower rate limit is harder to satisfy — proved automatically
lemma LowerRateLimitHarder(rpm1: nat, rpm2: nat, ctx: EvalContext)
    requires rpm1 <= rpm2
    requires rpm1 > 0 && rpm2 > 0
    ensures ConstraintHolds(RateLimit(rpm1), ctx) ==>
            ConstraintHolds(RateLimit(rpm2), ctx)
{
    // Dafny proves this in under a second: if rate < rpm1 <= rpm2 then rate < rpm2
}

$ dafny verify dafny/rbac_constraints.dfy
Dafny program verifier finished with 12 verified, 0 errors

func NewRateLimit(rpm int) (Constraint, error) {
    if rpm <= 0 {
        return Constraint{}, fmt.Errorf("rate limit must be positive")
    }
    return Constraint{Kind: RateLimitKind, MaxCount: rpm}, nil
}

// Add to Holds() in constraints.go:
case types.RateLimitKind:
    return ctx.CurrentRequestRate < c.MaxCount

func TestProp_LowerRateLimitHarder(t *testing.T) {
    props := gopter.NewProperties(gopter.DefaultTestParameters())
    props.Property("lower rate limit is harder to satisfy", prop.ForAll(
        func(rpm1, rpm2, rate int) bool {
            rpm1 = abs(rpm1)%100 + 1
            rpm2 = rpm1 + abs(rpm2)%100   // rpm2 >= rpm1 guaranteed
            ctx := types.EvalContext{CurrentRequestRate: abs(rate) % 200}
            c1, _ := types.NewRateLimit(rpm1)
            c2, _ := types.NewRateLimit(rpm2)
            if constraints.Holds(c1, ctx) {
                return constraints.Holds(c2, ctx)
            }
            return true
        },
        gen.Int(), gen.Int(), gen.Int(),
    ))
    props.TestingRun(t, gopter.NewFormatedReporter(false, 80, os.Stdout))
}

# Step 1: Verify formal specs
$ make verify-dafny
[DAFNY] Verifying rbac_types.dfy...              ? PASS
[DAFNY] Verifying rbac_policy.dfy...             ? PASS
[DAFNY] Verifying rbac_role_hierarchy.dfy...     ? PASS
[DAFNY] Verifying rbac_separation_of_duty.dfy... ? PASS
[DAFNY] Verifying rbac_constraints.dfy...        ? PASS
[DAFNY] Verifying rbac_invariants.dfy...         ? PASS
All 6 Dafny files verified successfully.

# Step 2: Model check concurrent protocol
$ make check-tla
[TLA+] Model checking RBACPolicyChange...
Model checking completed. No error has been found.
  2349 states generated, 1046 distinct states found.

# Step 3: Run property-based tests
$ make test
+ empty constraint list always passes: OK, passed 200 tests.
+ time window boundary conditions: OK, passed 500 tests.
+ constraint monotonicity: OK, passed 300 tests.
+ quota monotonicity: OK, passed 300 tests.
+ own claims in transitive closure: OK, passed 200 tests.
+ adding parent never removes claims: OK, passed 200 tests.
+ unknown principal always denied: OK, passed 200 tests.
+ no roles always denied: OK, passed 200 tests.
PASS — 2300+ property-based test cases executed.

# Step 4: Smoke-test the API
$ make run &
Server starting on :9090...

# alice can read docs (viewer role, time window 9-17, currently hour 10)
$ curl -s localhost:9090/evaluate -d '{
  "org_id":"acme", "principal_id":"alice",
  "action":"read", "resource_id":"docs",
  "hour":10, "region":"us-east-1", "usage":0
}' | jq .decision
"Allow"

# alice denied at 10pm — time constraint blocks access outside 9-17
$ curl -s localhost:9090/evaluate -d '{
  "org_id":"acme", "principal_id":"alice",
  "action":"read", "resource_id":"reports",
  "hour":22, "region":"us-east-1", "usage":0
}' | jq .decision
"Deny"

# bob can write docs from US (editor role + geo constraint us-east-1)
$ curl -s localhost:9090/evaluate -d '{
  "org_id":"acme", "principal_id":"bob",
  "action":"write", "resource_id":"docs",
  "hour":12, "region":"us-east-1", "usage":0
}' | jq .decision
"Allow"

# bob denied from EU — geo constraint blocks non-US regions
$ curl -s localhost:9090/evaluate -d '{
  "org_id":"acme", "principal_id":"bob",
  "action":"write", "resource_id":"docs",
  "hour":12, "region":"eu-west-1", "usage":0
}' | jq .decision
"Deny"

# SoD blocks carol (finance role) from also being submitter
$ curl -s localhost:9090/principals/carol/roles -d '{"role_id":"submitter"}'
{"error":"separation of duty: role \"submitter\" conflicts with existing role \"finance\""}

// Dafny lemma — proved by the verifier
lemma EmptyConstraintsAlwaysHold(ctx: EvalContext)
  ensures AllConstraintsHold([], ctx)
{}

// Matching gopter property — catches Go translation bugs
props.Property("empty constraint list always passes", prop.ForAll(
    func(hour int, region string) bool {
        ctx := types.EvalContext{CurrentHour: hour % 24, CurrentRegion: region}
        return constraints.AllHold(nil, ctx)
    },
    gen.Int(), gen.AnyString(),
))