Skip to content

Commit 5f29f35

Browse files
Define initial state for Phase C5 formal model
1 parent 28987a5 commit 5f29f35

File tree

1 file changed

+52
-0
lines changed

1 file changed

+52
-0
lines changed

formal/INIT-STATE.md

Lines changed: 52 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,52 @@
1+
# XSTRP Phase C5 — Initial State Definition
2+
3+
## Purpose
4+
5+
This document defines the initial conditions for the Phase C5
6+
formal verification model of XSTRP.
7+
8+
The initial state represents the moment immediately after an intent
9+
is created, before any authorization, proof submission, or expiry.
10+
11+
---
12+
13+
## Initial Conditions
14+
15+
At model start, the following conditions hold:
16+
17+
- intent_state = Created
18+
- authorization_valid = FALSE
19+
- proof_present = FALSE
20+
- is_expired = FALSE
21+
22+
No other state is permitted as an initial condition.
23+
24+
---
25+
26+
## Rationale
27+
28+
The Created state is the only valid protocol entry point.
29+
30+
At creation time:
31+
- No authorization has yet been satisfied
32+
- No proof artifacts exist
33+
- The intent has not expired
34+
35+
All other states must be reached through explicit transitions
36+
defined in the protocol.
37+
38+
---
39+
40+
## Exclusions
41+
42+
- No transition is assumed at initialization
43+
- No implicit authorization exists
44+
- No implicit expiry exists
45+
- No terminal state is reachable at initialization
46+
47+
---
48+
49+
## Status
50+
51+
Initial state defined.
52+
No transitions specified yet.

0 commit comments

Comments
 (0)