> For the complete documentation index, see [llms.txt](https://dsg-3.gitbook.io/dsg-docs/llms.txt). Markdown versions of documentation pages are available by appending `.md` to page URLs; this page is available as [Markdown](https://dsg-3.gitbook.io/dsg-docs/agi-simulation/formal-properties.md).

# Formal Properties

This document records the proof targets for `rust-core`.

## P1 Totality

```
process_transition(current, proposed, policy) always returns TransitionResult
```

The public transition API uses fail-closed evaluation. Invalid inputs do not panic or promote.

## P2 Fail-Closed

```
invalid_state       => Block
invalid_policy      => Block
arithmetic_overflow => Block
```

## P3 Forbidden Dominance

```
proposed.name_id in policy.forbidden_state_ids => Decision::Block
```

Forbidden state check runs before drift/stability evaluation.

## P4 Stabilize Rule

```
valid inputs
AND proposed is not forbidden
AND SCALE < threshold_scaled * (1 + drift)
=> Decision::Stabilize
```

## P5 Allow Rule

```
valid inputs
AND proposed is not forbidden
AND SCALE >= threshold_scaled * (1 + drift)
=> Decision::Allow
```

## P6 Drift Symmetry

```
valid(a) AND valid(b) => drift(a, b) == drift(b, a)
```

## P7 Same-State Identity

```
valid(a) => drift(a, a) == 0
```

## P8 Metric Boundary

If `value_hash == 0`, semantic value identity is not fully represented. In that mode the drift score is structural/pseudo-metric.

If all active fields use canonical non-zero `value_hash`, same-key semantic drift is represented by hash change.

## SMT Core Relation

```smt2
(define-fun unstable ((drift Int) (threshold Int)) Bool
  (< 1000000 (* threshold (+ 1 drift))))

(define-fun decide
  ((forbidden Bool) (drift Int) (threshold Int)) Int
  (ite forbidden
       2
       (ite (unstable drift threshold)
            1
            0)))
```

Mapping:

```
0 = Allow
1 = Stabilize
2 = Block
```

## Truth Boundary

Current repository status:

```
GO: deterministic execution evidence
GO: bounded integer-only decision relation
GO: model-checking-ready shape
NO-GO: formal proof complete
```

Formal proof complete requires actual Kani/Z3 artifacts.