1	import Base
2	
3	# Logical change timestamp. low wraps modulo 2^32; epoch preserves the history
4	# needed to age dormant components/readers across low wraps within runtime limits.
5	# Raw constructors are trusted: execution must not supply future stamps/cursors.
6	type Tick is Data:
7	  Tick{epoch:Nat,low:U32}
8	
9	# Pinned Bevy ad678262 change_detection/mod.rs MAX_CHANGE_AGE.
10	# Exact epochs replace periodic storage sweeps, not this observable age bound.
11	def max_change_age() -> U32:3258167296
12	
13	# Initial administrative timestamp. Zero is valid, not component absence or a
14	# fabricated first-run cursor; first-run reader policy is supplied separately.
15	def zero() -> Tick:Tick{0n,0}
16	
17	def incremented(wrapped:Bool,epoch:Nat,low:U32) -> Tick:
18	  match wrapped:
19	    case False{}:Tick{epoch,U32.add(low,1)}
20	    case True{}:Tick{1n+epoch,0}
21	
22	# Advance one logical execution boundary, carrying the epoch on low-word wrap.
23	def next(tick:Tick) -> Tick:
24	  match tick:
25	    case Tick{epoch,+low}:incremented(U32.is_eq(low,4294967295),epoch,low)
26	
27	# Diagnostic low word only; never use this projection as an independent cursor.
28	def low(tick:Tick) -> U32:
29	  match tick:
30	    case Tick{_,value}:value
31	
32	# Monotone logical ordinal for existing Nat-based observation/runtime domains.
33	# Backend Nat representation limits still apply to consumers of this projection.
34	def total(tick:Tick) -> Nat:
35	  match tick:
36	    case Tick{epoch,value}:Nat.add(Nat.mul(epoch,1n+4294967295n),U32.to_nat(value))
37	
38	def ordered_epochs(equal:Bool,earlier:Bool,stamp:U32,this:U32) -> Bool:
39	  match equal:
40	    case True{}:U32.is_le(stamp,this)
41	    case False{}:earlier
42	
43	# Explicit validity of a timestamp relative to this execution. Future values
44	# are not made recent by saturating Nat subtraction.
45	def not_future(stamp:Tick,this:Tick) -> Bool:
46	  match stamp this:
47	    case Tick{+se,sl} Tick{+te,tl}:ordered_epochs(Nat.is_eq(se,te),Nat.is_lt(se,te),sl,tl)
48	
49	def crossing_age(lowWrapped:Bool,stamp:U32,this:U32) -> U32:
50	  match lowWrapped:
51	    case False{}:max_change_age()
52	    case True{}:U32.min(U32.sub(this,stamp),max_change_age())
53	
54	def distance(same:Bool,adjacent:Bool,+stamp:U32,+this:U32) -> U32:
55	  match same adjacent:
56	    case True{} _:U32.min(U32.sub(this,stamp),max_change_age())
57	    case False{} True{}:crossing_age(U32.is_lt(this,stamp),stamp,this)
58	    case False{} False{}:max_change_age()
59	
60	def valid_age(valid:Bool,stamp:Tick,this:Tick) -> U32:
61	  match valid stamp this:
62	    case False{} _ _:max_change_age()
63	    case True{} Tick{+se,sl} Tick{+te,tl}:distance(Nat.is_eq(se,te),Nat.is_eq(1n+se,te),sl,tl)
64	
65	# True elapsed age capped at Bevy's MAX_CHANGE_AGE, including multiple wraps.
66	# Invalid future stamps return MAX; use not_future when distinguishing invalid
67	# inputs from legitimately old data. No global storage maintenance is required.
68	def age(+stamp:Tick,+this:Tick) -> U32:
69	  valid_age(not_future(stamp,this),stamp,this)
70	
71	def valid_newer(valid:Bool,stamp:Tick,last:Tick,+this:Tick) -> Bool:
72	  match valid:
73	    case False{}:False{}
74	    case True{}:U32.is_gt(age(last,this),age(stamp,this))
75	
76	# Compare component age with independent reader age. Equality and two maximally
77	# old timestamps are not new. A future stamp OR reader cursor rejects as False;
78	# callers separately establish component presence and first-run reader policy.
79	def newer(+stamp:Tick,+last:Tick,+this:Tick) -> Bool:
80	  valid_newer(Bool.and(not_future(stamp,this),not_future(last,this)),stamp,last,this)
81	
82	# Detached full-timestamp diagnostic; the epoch is never discarded.
83	def show(tick:Tick) -> String:
84	  match tick:
85	    case Tick{epoch,low}:Nat.show(epoch) ++ ":" ++ U32.show(low)
86	# Distinguish an uninitialized lifecycle cursor from the legitimate zero tick.
87	def cursor_show(cursor:Maybe<&2,Tick>) -> String:
88	  match cursor:
89	    case None{}:"never"
90	    case Some{tick}:show(tick)