You signed in with another tab or window. Reload to refresh your session.You signed out in another tab or window. Reload to refresh your session.You switched accounts on another tab or window. Reload to refresh your session.Dismiss alert
A correctness contract for Monarch cast actor routing.
4
+
5
+
This note states the correctness target for Monarch cast actor routing: given an affine target tile and an availability predicate, a cast should deliver exactly once to every live actor in the target tile, never deliver outside the target tile, and never route through unavailable actors.
6
+
7
+
The companion note, `routing-foundations.md`, explains how the algebra is built. This note states the delivery contract that an implementation can be checked against.
8
+
9
+
The Haskell model, [`tile`](https://github.com/shayne-fletcher/tile.git), is small enough to support these claims with QuickCheck properties.
10
+
11
+
## Notation
12
+
13
+
Let `T` be an affine target tile.
14
+
15
+
-`R(T)` is the set of ranks in the target tile
16
+
-`root(T)` is the offset rank of the tile
17
+
18
+
Let `E` be a schedule, i.e. a finite list of directed send steps.
19
+
20
+
-`senders(E)` is the set of sources in `E`
21
+
-`receivers(E)` is the set of destinations in `E`
22
+
23
+
Let `sched(T)` be the fault-free schedule produced by block partitioning.
24
+
25
+
Let `live ⊆ R(T)` be the set of available members in the target tile. Equivalently, `live` is the complement of an occlusion predicate restricted to `R(T)`.
26
+
27
+
Let `occSched(T, live)` be the routed schedule produced under that availability set.
28
+
29
+
## Geometric Laws
30
+
31
+
The low-level affine facts are prerequisites:
32
+
33
+
- ranks and points round-trip
34
+
- rank enumeration is exact
35
+
- affine slicing produces affine subspaces
36
+
- affine slicing stays inside its parent space
37
+
- decomposition children stay inside their parent tile
38
+
39
+
These are properties of the representation, not the main routing result. They are the geometry that makes the delivery theorems meaningful.
40
+
41
+
## Theorem T1: Fault-Free Cast Coverage
42
+
43
+
Let `T` be a non-empty affine target tile, and let:
44
+
45
+
```text
46
+
n = |R(T)|
47
+
sched(T) = E
48
+
```
49
+
50
+
Then `E` is a spanning send tree over `R(T)` rooted at `root(T)`:
51
+
52
+
```text
53
+
|E| = n - 1
54
+
receivers(E) = R(T) - {root(T)}
55
+
each receiver appears exactly once
56
+
senders(E) ⊆ R(T)
57
+
receivers(E) ⊆ R(T)
58
+
```
59
+
60
+
Equivalently: every non-root target receives exactly once, the root does not receive, and no actor outside the target tile participates.
61
+
62
+
This theorem states delivery behavior, not schedule order. DFS and BFS may satisfy the same law with different edge orderings.
63
+
64
+
## Theorem T2: Occluded Cast Coverage
65
+
66
+
If `live = ∅`, then:
67
+
68
+
```text
69
+
occSched(T, live) = Nothing
70
+
```
71
+
72
+
If `live ≠ ∅`, then:
73
+
74
+
```text
75
+
occSched(T, live) = Just (ingress, E)
76
+
```
77
+
78
+
where:
79
+
80
+
```text
81
+
ingress ∈ live
82
+
receivers(E) = live - {ingress}
83
+
each receiver appears exactly once
84
+
senders(E) ⊆ live
85
+
receivers(E) ⊆ live
86
+
```
87
+
88
+
Equivalently: the ingress is live, every other live target receives exactly once, and unavailable actors neither send nor receive.
89
+
90
+
The affine geometry is unchanged. Occlusion only changes representative selection and pruning.
91
+
92
+
## Corollary C1: Jagged Regions
93
+
94
+
Let `J` be a jagged participant set inside an affine envelope `T`. Define:
95
+
96
+
```text
97
+
live = J
98
+
occluded = R(T) - J
99
+
```
100
+
101
+
Then routing the envelope under `live` delivers exactly to the jagged region:
102
+
103
+
```text
104
+
receivers(E) ∪ {ingress} = J
105
+
```
106
+
107
+
Sparse participation and node failure are the same problem at this layer.
108
+
109
+
## Corollary C2: Monarch Cast Correctness Target
110
+
111
+
For a Monarch cast implementation, the core correctness target is:
112
+
113
+
```text
114
+
Given an affine target tile and an availability predicate,
115
+
cast delivers exactly once to every live actor in the target tile,
116
+
never delivers to an actor outside the target tile,
117
+
never delivers to an unavailable actor,
118
+
and every forwarding actor is live under the representative policy.
119
+
```
120
+
121
+
Internal reshape is allowed to change the routing tree, but not the target set. A reshaped cast should deliver to the same live members of the affine target tile as the unreshaped model. This preservation law is the next piece to model explicitly.
122
+
123
+
## Supporting Properties
124
+
125
+
The Haskell model supports these claims with QuickCheck properties in [`test/Main.hs`](https://github.com/shayne-fletcher/tile/blob/main/test/Main.hs):
126
+
127
+
```text
128
+
affine rank/point roundtrip
129
+
ranks enumerate the affine space exactly once
130
+
affine slicing is closed and included in its parent
131
+
structural and communication children are included in their parent
132
+
fault-free schedules form a spanning send tree
133
+
occluded schedules deliver exactly to live members
134
+
```
135
+
136
+
The first four properties support the geometric assumptions. The last two correspond directly to T1 and T2.
0 commit comments