stave-z3.md

gistfile1.txt

```go
obs, err := stave.LoadObservation(path)
facts, err := stave.ExtractFacts(obs)
```

Your intent is:

```text
Use Stave as a library.
Bring your own solver.
Write your own analysis program.
```


```text
stave CLI
  deterministic checks
  reports
  fixtures
  no solver dependency

stave Go library
  load snapshots
  expose facts
  expose evidence model
  expose finding model

developer examples
  Stave + Z3
  Stave + custom policy engine
  Stave + graph analysis
```


```text
Stave facts + Z3 constraints = custom security reasoning
```

`cvc5` is an SMT solver. It supports many SMT theories and combinations of theories. 

```text
Developer project
→ imports Stave Go library
→ uses cvc5 or Z3
→ writes custom reasoning programs
```

```text
Stave = cloud configuration facts and evidence model
Z3/cvc5 = SMT solvers
Developer code = custom security reasoning
```

make Stave easy to use with both.

Developers can choose:

| Solver | Role                                         |
| ------ | -------------------------------------------- |
| Z3     | Common SMT solver, broad ecosystem           |
| cvc5   | SMT solver, strong support for many theories |
| Stave  | Provides normalized cloud/security facts     |

The Stave CLI stays simple.

```text
stave apply
stave validate
stave report
```

The developer extension path is separate.

```text
stave facts + z3 constraints
stave facts + cvc5 constraints
```

## Repository organization

Use examples:

```text
examples/solver/
  z3/
    s3-public-read/
  cvc5/
    s3-public-read/
```

Each example should show the same question:

```text
Can any public principal read this S3 bucket?
```

That lets developers compare Z3 and cvc5 without making either part of Stave.

```text
cvc5 is an SMT solver developers can use with Stave, similar to Z3.
```

Z3 adds a **reasoning engine beside the evaluation layer**.

```text
Executive layer    stave report    stave plan     stave monitor
                        ↓               ↓               ↓
Analytical layer   stave score     stave rank     stave trend
                        ↓               ↓               ↓
Evaluation layer   stave apply     stave map      stave coverage
                        ↓               ↓               ↓
Reasoning adapter  CEL evaluator   graph engine   Z3/cvc5 program
                        ↓               ↓               ↓
Data layer         snapshot JSON   controls YAML  chains YAML
```

Reasoning adapter is an implementation/developer layer.

Before Z3:

```text
Stave checks known rules against known facts.
```

After Z3:

```text
Developers can ask if unsafe states are logically possible.
```

### `stave apply`

Answers:

```text
Does this snapshot violate this invariant?
```

Example:

```text
This bucket allows public read.
```

### Z3 program using Stave

Answers:

```text
Is there any possible principal/action/resource path that violates this invariant?
```

Example:

```text
There exists a public principal that can perform s3:GetObject on this PHI bucket.
```

So Z3 is not just another command.

It is a way to write custom reasoning programs over Stave facts.

## Better hierarchy with developer extension

I would model it like this:

```text
Executive layer
  stave report
  stave plan
  stave monitor

Analytical layer
  stave score
  stave rank
  stave trend

Evaluation layer
  stave apply
  stave map
  stave coverage

Developer reasoning layer
  Stave facts + Z3
  Stave facts + cvc5
  Stave facts + graph analysis
  Stave facts + custom Go programs

Data layer
  snapshot JSON
  controls YAML
  chains YAML
```

This makes the boundary clear.

The Stave CLI remains productized.
The solver path remains programmable.

## What Z3 adds conceptually

Z3 adds **existential reasoning**.

That means questions like:

```text
Is there any path?
Is there any principal?
Is there any action?
Is there any resource?
Is there any configuration combination?
```

Examples:

```text
Can any external principal read this bucket?
Can any role write outside the allowed prefix?
Can any policy statement bypass this deny?
Can any chain reach sensitive data?
Can any exception make this control ineffective?
```

This is different from normal evaluation.

Normal evaluation checks facts.

Z3 searches the space of possibilities.

## Where it fits in your commands

### Data layer

No big change.

```text
snapshot JSON
controls YAML
chains YAML
```

But you may add a derived form:

```text
facts JSON
```

So the data layer becomes:

```text
snapshot JSON
controls YAML
chains YAML
facts JSON
```

`facts JSON` is useful because both Z3 and cvc5 examples can consume it.

## Evaluation layer

`stave apply` still uses normal deterministic rules.

```text
stave apply
```

This should remain the main command.

Z3 should not replace it.

Instead, Z3 programs can reuse Stave parsing and fact extraction.

```text
stave apply = built-in evaluation
custom Z3 program = custom reasoning
```

## Analytical layer

This is where Z3 output can feed value.

A Z3 program can produce:

```text
counterexample
reachable path
violating assignment
minimal unsafe condition
```

Then Stave can turn that into:

```text
score
rank
trend
```

Example:

```text
Z3 proves public read is reachable
→ Stave marks exposure as reachable
→ score increases
→ rank moves higher
→ trend shows recurrence
```

## Executive layer

Executives should not see Z3.

They should see the result:

```text
This unsafe access path is reachable.
This control prevents recurrence.
This exception creates exposure.
This remediation closes the path.
```

So the executive layer remains stable.

## Revised abstraction hierarchy

This is the version I would use:

```text
Executive layer
  report       plan        monitor
  "What matters?"
  "What should change?"
  "Is it staying fixed?"

Analytical layer
  score        rank        trend
  "How bad?"
  "What first?"
  "Is it improving?"

Evaluation layer
  apply        map         coverage
  "What failed?"
  "What is connected?"
  "What is protected?"

Developer reasoning layer
  facts API    solver API  examples
  "What can be proven?"
  "What is reachable?"
  "What counterexample exists?"

Data layer
  snapshots    controls    chains
  "What is observed?"
  "What is required?"
  "What path exists?"
```

```text
examples/solver/z3/
examples/solver/cvc5/
```

This says:

```text
Stave is programmable.
Bring your own solver.
```

Expose this from Stave:

```go
obs := stave.LoadSnapshot(path)
facts := stave.BuildFacts(obs)
```

Then developer programs do:

```go
solver := z3.NewSolver()
solver.Assert(...)
solver.Check()
```

The stable Stave abstraction is:

```text
facts
```

Z3 changes Stave from this:

```text
configuration checker
```

to this:

```text
configuration reasoning substrate
```

But only at the developer layer.

For users:

```text
stave apply
stave score
stave report
```

For developers:

```text
Stave facts + Z3/cvc5 = custom proof programs
```

```text
Blast radius = how far the damage can spread.

Impact analysis = what the damage means.
```

## In cloud security

### Blast radius asks

```text
What can this compromised identity, bucket, key, role, or workload reach?
```

Examples:

```text
Can this IAM role access one S3 bucket or all buckets?

Can this exposed key read only logs or also production data?

Can this public bucket expose one prefix or the whole bucket?
```

Blast radius is about **scope**.

## Impact analysis asks

```text
Why does this matter to the business, security, compliance, or operations?
```

Examples:

```text
Does the exposed bucket contain PHI?

Does it affect regulated healthcare data?

Does it create HIPAA reporting risk?

Does it expose customer records?

Does it allow data modification, not just reading?
```

Impact is about **consequence**.

## Example

Misconfiguration:

```text
An S3 bucket policy allows public read.
```

Blast radius:

```text
Public users can read objects under s3://patient-records/*
```

Impact analysis:

```text
The bucket may expose patient data.
This may create disclosure risk.
This may require investigation, notification, and remediation.
```

```text
Blast radius = reachable cloud resources and permissions

Impact analysis = business/security meaning of that reachability
```

```text
configuration defect
→ reachable access path
→ blast radius
→ impact
→ remediation priority
```

Blast radius is the **technical spread**.

Impact analysis is the **meaning and severity** of that spread.