1	import Base
2	import ./change_tick.bend as Tick
3	import lifecycle.bend as L
4	
5	# Owned scalar arrays; exceptional authority is disjoint (id0 or id>131072).
6	# Raw constructor consistency is trusted provisioning, not a universal refinement.
7	type Metadata is Type:
8	  Metadata{added:Array<Maybe<&2,Tick.Tick>>,changed:Array<Maybe<&2,Tick.Tick>>,capacity:U32,depth:Nat,exceptional:List<&2,L.Entry>}
9	def empty() -> Metadata:
10	  Metadata{ALeaf{None{}},ALeaf{None{}},1,0n,[]}
11	def normal(+id:U32) -> Bool:
12	  U32.is_gt(id,0) && U32.is_le(id,131072)
13	def got_changed(added:Array<Maybe<&2,Tick.Tick>>,+capacity:U32,+depth:Nat,exceptional:List<&2,L.Entry>,first:Maybe<&2,Tick.Tick>,observed:Array<Maybe<&2,Tick.Tick>> & Maybe<&2,Tick.Tick>) -> Metadata & L.Stamp:
14	  match observed:
15	    case (changed,last): (Metadata{added,changed,capacity,depth,exceptional},L.Stamp{first,last})
16	def got_added(+id:U32,changed:Array<Maybe<&2,Tick.Tick>>,capacity:U32,depth:Nat,exceptional:List<&2,L.Entry>,observed:Array<Maybe<&2,Tick.Tick>> & Maybe<&2,Tick.Tick>) -> Metadata & L.Stamp:
17	  match observed:
18	    case (added,first): got_changed(added,capacity,depth,exceptional,first,Array.get(Maybe<&2,Tick.Tick>,changed,U32.sub(id,1)))
19	def get_checked(+id:U32,added:Array<Maybe<&2,Tick.Tick>>,changed:Array<Maybe<&2,Tick.Tick>>,capacity:U32,depth:Nat,+exceptional:List<&2,L.Entry>,isnormal:Bool,fits:Bool) -> Metadata & L.Stamp:
20	  match isnormal fits:
21	    case False{} _: (Metadata{added,changed,capacity,depth,exceptional},L.get(exceptional,id))
22	    case True{} False{}: (Metadata{added,changed,capacity,depth,exceptional},L.Stamp{None{},None{}})
23	    case True{} True{}: got_added(id,changed,capacity,depth,exceptional,Array.get(Maybe<&2,Tick.Tick>,added,U32.sub(id,1)))
24	def get(metadata:Metadata,+id:U32) -> Metadata & L.Stamp:
25	  match metadata:
26	    case Metadata{added,changed,+capacity,depth,exceptional}: get_checked(id,added,changed,capacity,depth,exceptional,normal(id),U32.is_le(id,capacity))
27	def write_ready(+id:U32,added:Array<Maybe<&2,Tick.Tick>>,changed:Array<Maybe<&2,Tick.Tick>>,capacity:U32,depth:Nat,exceptional:List<&2,L.Entry>,stamp:L.Stamp) -> Metadata:
28	  match stamp:
29	    case L.Stamp{first,last}: Metadata{Array.set(Maybe<&2,Tick.Tick>,added,U32.sub(id,1),first),Array.set(Maybe<&2,Tick.Tick>,changed,U32.sub(id,1),last),capacity,depth,exceptional}
30	# Factory-produced metadata starts at1 and normal targets require at most17 grows.
31	def write_grow(fuel:Nat,+id:U32,stamp:L.Stamp,added:Array<Maybe<&2,Tick.Tick>>,changed:Array<Maybe<&2,Tick.Tick>>,+capacity:U32,+depth:Nat,exceptional:List<&2,L.Entry>,fits:Bool) -> Metadata:
32	  match fuel fits:
33	    case _ True{}: write_ready(id,added,changed,capacity,depth,exceptional,stamp)
34	    case 0n False{}: Metadata{added,changed,capacity,depth,exceptional}
35	    case 1n+rest False{}:
36	      +next = U32.shl(capacity)
37	      write_grow(rest,id,stamp,ANode{added,Array.new(Maybe<&2,Tick.Tick>,depth,None{})},ANode{changed,Array.new(Maybe<&2,Tick.Tick>,depth,None{})},next,1n+depth,exceptional,U32.is_le(id,next))
38	def set_checked(+id:U32,+stamp:L.Stamp,added:Array<Maybe<&2,Tick.Tick>>,changed:Array<Maybe<&2,Tick.Tick>>,+capacity:U32,depth:Nat,exceptional:List<&2,L.Entry>,isnormal:Bool) -> Metadata:
39	  match isnormal:
40	    case False{}: Metadata{added,changed,capacity,depth,L.set(exceptional,id,stamp)}
41	    case True{}: write_grow(17n,id,stamp,added,changed,capacity,depth,exceptional,U32.is_le(id,capacity))
42	def set(metadata:Metadata,+id:U32,stamp:L.Stamp) -> Metadata:
43	  match metadata:
44	    case Metadata{added,changed,capacity,depth,exceptional}: set_checked(id,stamp,added,changed,capacity,depth,exceptional,normal(id))
45	def clear_checked(+id:U32,added:Array<Maybe<&2,Tick.Tick>>,changed:Array<Maybe<&2,Tick.Tick>>,capacity:U32,depth:Nat,exceptional:List<&2,L.Entry>,isnormal:Bool,fits:Bool) -> Metadata:
46	  match isnormal fits:
47	    case False{} _: Metadata{added,changed,capacity,depth,L.clear(exceptional,id)}
48	    case True{} False{}: Metadata{added,changed,capacity,depth,exceptional}
49	    case True{} True{}: write_ready(id,added,changed,capacity,depth,exceptional,L.Stamp{None{},None{}})
50	def clear(metadata:Metadata,+id:U32) -> Metadata:
51	  match metadata:
52	    case Metadata{added,changed,+capacity,depth,exceptional}: clear_checked(id,added,changed,capacity,depth,exceptional,normal(id),U32.is_le(id,capacity))