WWN Termination Proofs
Table of Contents
Two-Hop Termination Theorem
Claim: For any input w, the redirect chain terminates in at most 2 redirects.
String ──────> Integer ──────> Canonical
step1 step2 (done)
Proof
- String → Integer: charCode sum always produces finite integer
- Integer → Wrapped:
wrapW(w)always produces value in[-8191, 8191] - Canonical: Values in range are terminal (no redirect)
Verified Properties
| Theorem | Statement |
|---|---|
WrapProducesCanonical |
∀w. wrapW(w) ∈ [-8191, 8191] |
CanonicalIsFixedPoint |
∀w. isCanonical(w) ⟹ wrapW(w) = w |
WrapIdempotent |
∀w. wrapW(wrapW(w)) = wrapW(w) |
Test Cases
| Input | Result | Redirects |
|---|---|---|
w=0 |
0 | 0 (canonical) |
w=8192 |
-8191 | 1 (wrap) |
w=🔥 (111970) |
-2711 | 2 (string→int→wrap) |
w=999999999 |
-1938 | 1 (wrap) |
Alloy Specifications
torus-termination.als
Core wrap function and termination theorems.
-- Constants
let W_MAX = 8191
let MODULUS = 16383 -- 2 * W_MAX + 1
-- The wrap function: maps any integer to [-W_MAX, W_MAX]
fun wrapW[w: Int]: Int {
let normalized = rem[add[w, W_MAX], MODULUS] |
sub[normalized, W_MAX]
}
-- Predicate: value is canonical (in valid range)
pred isCanonical[w: Int] {
w >= negate[W_MAX] and w <= W_MAX
}
-- THEOREM: wrapW always produces canonical output
assert WrapProducesCanonical {
all w: Int | isCanonical[wrapW[w]]
}
-- THEOREM: Wrap is idempotent
assert WrapIdempotent {
all w: Int | wrapW[wrapW[w]] = wrapW[w]
}
check WrapProducesCanonical for 5 Int
check WrapIdempotent for 5 Int
redirect-chain.als
State machine model proving maximum 2 redirects.
-- State machine for redirect chain
-- PARSE → STRING_TO_INT → WRAP → CANONICAL
abstract sig InputType {}
one sig StringInput, IntegerInput extends InputType {}
sig Step {
w: Int,
inputType: InputType,
needsRedirect: Bool
}
-- THEOREM: Chain length is at most 3 steps (input → convert → wrap)
-- Which means at most 2 redirects
assert MaxTwoRedirects {
#Step <= 3
}
check MaxTwoRedirects for 5 Step, 6 Int
Constants
| Name | Value | Description |
|---|---|---|
| WMAX | 8191 | 213 - 1 (Mersenne prime) |
| MODULUS | 16383 | 2 × WMAX + 1 |
| Range | ±8191 | Canonical w values |
Running the Proofs
# Install Alloy Analyzer # https://alloytools.org alloy torus-termination.als alloy redirect-chain.als