1	import Base
2	import entity_key.bend as Key
3	import ./decode_utf16.bend as Utf16
4	# Raw is a typed Data description. Arbitrary affine payload ownership is a
5	# separate explicit receipt; this validator never invents an inverse Raw -> C.
6	type Raw is Data:
7	  Missing{}
8	  Null{}
9	  Number{value:U32}
10	  SignedInteger{negative:Bool,magnitude:Nat}
11	  Float{value:F32}
12	  Binary64{high:U32,low:U32}
13	  Text{value:String}
14	  Utf16Text{units:List<&2,U32>}
15	  Boolean{value:Bool}
16	  Handle{namespace:U32,key:Key.Key}
17	  Array{items:List<&2,Raw>}
18	  Object{fields:List<&2,Field>}
19	type Field is Data:
20	  Field{name:String,value:Raw}
21	type Codec is Data:
22	  FiniteNumber{}
23	  Integer{}
24	  StringValue{}
25	  BoolValue{}
26	  Literal{value:Raw}
27	  LiteralValues{values:List<&2,Raw>}
28	  LiteralRendered{values:List<&2,Raw>,expected:String}
29	  Nullable{inner:Codec}
30	  ArrayValue{inner:Codec}
31	  Struct{fields:List<&2,NamedCodec>}
32	  HandleValue{namespace:U32}
33	type NamedCodec is Data:
34	  NamedCodec{name:String,codec:Codec}
35	type Error is Data:
36	  Invalid{path:String,expected:String,actual:Raw}
37	  FuelExhausted{path:String}
38	type Checked is Data:
39	  Accepted{value:Raw}
40	  Rejected{error:Error}
41	type Owned<Owner:Type> is Type:
42	  Owned{owner:Owner,description:Raw}
43	type Receipt<Owner:Type> is Type:
44	  Receipt{owner:Owner,checked:Checked}
45	def field_choose(equal:Bool,value:Raw,next:Unit -> Raw) -> Raw:
46	  match equal:
47	    case True{}: value
48	    case False{}: next(Unit{})
49	def field(+name:String,fields:List<&2,Field>) -> Raw:
50	  match fields:
51	    case []: Missing{}
52	    case Field{key,value} <> rest: field_choose(String.eq(name,key),value,_ => field(name,rest))
53	type Work is Data:
54	  Work{codec:Codec,raw:Raw,path:String}
55	type Step is Data:
56	  Continue{work:List<&2,Work>}
57	  Stop{error:Error}
58	# Exact SameValueZero numeric equality uses a 53-bit mantissa pair, avoiding
59	# impossible runtime Nat immediates above Bend's 2^48-1 emitter limit.
60	type Numeric is Data:
61	  Finite{negative:Bool,high:U32,low:U32,exponent:U32}
62	  Infinity{negative:Bool}
63	  NotNumber{}
64	  NaN{}
65	def normalize_checked(fuel:Nat,+negative:Bool,+high:U32,+low:U32,+exponent:U32,zero:Bool,even:Bool) -> Numeric:
66	  match fuel zero even:
67	    case _ True{} _: Finite{False{},0,0,0}
68	    case _ False{} False{}: Finite{negative,high,low,exponent}
69	    case 0n False{} True{}: Finite{negative,high,low,exponent}
70	    case 1n+more False{} True{}: normalize_checked(more,negative,U32.div(high,2),U32.add(U32.div(low,2),U32.mul(U32.mod(high,2),2147483648)),U32.add(exponent,1),False{},U32.is_eq(U32.mod(U32.div(low,2),2),0))
71	def normalize(fuel:Nat,+negative:Bool,+high:U32,+low:U32,+exponent:U32) -> Numeric:
72	  normalize_checked(fuel,negative,high,low,exponent,U32.is_eq(high,0) && U32.is_eq(low,0),U32.is_eq(U32.mod(low,2),0))
73	def numeric_special(negative:Bool,infinite:Bool) -> Numeric:
74	  match infinite:
75	    case True{}: Infinity{negative}
76	    case False{}: NaN{}
77	def float_parts(+bits:U32,+exponent:U32,+fraction:U32,special:Bool,zero:Bool) -> Numeric:
78	  match special zero:
79	    case True{} _: numeric_special(U32.is_ge(bits,2147483648),U32.is_eq(fraction,0))
80	    case False{} True{}: normalize(64n,U32.is_ge(bits,2147483648),0,fraction,925)
81	    case False{} False{}: normalize(64n,U32.is_ge(bits,2147483648),0,U32.add(fraction,8388608),U32.add(exponent,924))
82	def float_numeric(+bits:U32) -> Numeric:
83	  float_parts(bits,U32.mod(U32.div(bits,8388608),256),U32.mod(bits,8388608),U32.is_eq(U32.mod(U32.div(bits,8388608),256),255),U32.is_eq(U32.mod(U32.div(bits,8388608),256),0))
84	def binary_parts(+negative:Bool,+exponent:U32,+high:U32,+low:U32,special:Bool,zero:Bool) -> Numeric:
85	  match special zero:
86	    case True{} _: numeric_special(negative,U32.is_eq(high,0) && U32.is_eq(low,0))
87	    case False{} True{}: normalize(64n,negative,high,low,0)
88	    case False{} False{}: normalize(64n,negative,U32.add(high,1048576),low,U32.sub(exponent,1))
89	def binary_numeric(+high:U32,+low:U32) -> Numeric:
90	  binary_parts(U32.is_ge(high,2147483648),U32.mod(U32.div(high,1048576),2048),U32.mod(high,1048576),low,U32.is_eq(U32.mod(U32.div(high,1048576),2048),2047),U32.is_eq(U32.mod(U32.div(high,1048576),2048),0))
91	def numeric(raw:Raw) -> Numeric:
92	  match raw:
93	    case Number{value}: normalize(64n,False{},0,value,1074)
94	    case SignedInteger{negative,+value}: normalize(64n,negative,U32.from_nat(Nat.div(value,Nat.mul(65536n,65536n))),U32.from_nat(Nat.mod(value,Nat.mul(65536n,65536n))),1074)
95	    case Float{value}: float_numeric(F32.bits(value))
96	    case Binary64{high,low}: binary_numeric(high,low)
97	    case _: NotNumber{}
98	def same_bool(a:Bool,b:Bool) -> Bool:
99	  match a b:
100	    case True{} True{}: True{}
101	    case False{} False{}: True{}
102	    case _ _: False{}
103	def same_numeric(a:Numeric,b:Numeric) -> Bool:
104	  match a b:
105	    case Finite{an,ah,al,ae} Finite{bn,bh,bl,be}: same_bool(an,bn) && U32.is_eq(ah,bh) && U32.is_eq(al,bl) && U32.is_eq(ae,be)
106	    case Infinity{a} Infinity{b}: same_bool(a,b)
107	    case NaN{} NaN{}: True{}
108	    case _ _: False{}
109	def equal(+a:Raw,+b:Raw) -> Bool:
110	  match a b:
111	    case Null{} Null{}: True{}
112	    case Text{a} Text{b}: String.eq(a,b)
113	    case Utf16Text{a} Utf16Text{b}: Utf16.checked(a,b)
114	    case Utf16Text{a} Text{b}: Utf16.checked(a,Utf16.text(b))
115	    case Text{a} Utf16Text{b}: Utf16.checked(Utf16.text(a),b)
116	    case Boolean{a} Boolean{b}: same_bool(a,b)
117	    case _ _: same_numeric(numeric(a),numeric(b))
118	def alternatives(values:List<&2,Raw>,+raw:Raw) -> Bool:
119	  match values:
120	    case []: False{}
121	    case value <> tail: equal(value,raw) || alternatives(tail,raw)
122	def choose_checked(valid:Bool,+path:String,+expected:String,raw:Raw,rest:List<&2,Work>) -> Step:
123	  match valid:
124	    case True{}: Continue{rest}
125	    case False{}: Stop{Invalid{path,expected,raw}}
126	def array_work(+codec:Codec,items:List<&2,Raw>,+path:String,+index:U32,rest:List<&2,Work>) -> List<&2,Work>:
127	  match items:
128	    case []: rest
129	    case value <> tail: Work{codec,value,path ++ "[" ++ U32.show(index) ++ "]"} <> array_work(codec,tail,path,U32.add(index,1),rest)
130	def struct_work(fields:List<&2,NamedCodec>,+values:List<&2,Field>,+path:String,rest:List<&2,Work>) -> List<&2,Work>:
131	  match fields:
132	    case []: rest
133	    case NamedCodec{+name,codec} <> tail: Work{codec,field(name,values),path ++ "." ++ name} <> struct_work(tail,values,path,rest)
134	def binary64_exponent(high:U32) -> U32:
135	  U32.mod(U32.div(high,1048576),2048)
136	def binary_integer_normal(result:Numeric) -> Bool:
137	  match result:
138	    case Finite{_,high,low,+exponent}: (U32.is_eq(high,0) && U32.is_eq(low,0)) || (U32.is_ge(exponent,1074) && U32.is_le(exponent,1126))
139	    case _: False{}
140	def binary_integer_checked(result:Numeric,small:Bool) -> Bool:
141	  small && binary_integer_normal(result)
142	def binary_integer(+high:U32,+low:U32) -> Bool:
143	  binary_integer_checked(binary_numeric(high,low),U32.is_lt(binary64_exponent(high),1076))
144	def expand(codec:Codec,+raw:Raw,+path:String,rest:List<&2,Work>) -> Step:
145	  match codec raw:
146	    case Integer{} Number{_}: Continue{rest}
147	    case Integer{} SignedInteger{_,magnitude}: choose_checked(Nat.is_lt(Nat.div(magnitude,Nat.mul(65536n,65536n)),2097152n),path,"integer",raw,rest)
148	    case Integer{} Float{+value}: choose_checked(F32.is_eq(F32.floor(value),value) && F32.is_lt(F32.abs(value),9007199254740992.0),path,"integer",raw,rest)
149	    case Integer{} Binary64{high,low}: choose_checked(binary_integer(high,low),path,"integer",raw,rest)
150	    case FiniteNumber{} Number{_}: Continue{rest}
151	    case FiniteNumber{} SignedInteger{_,_}: Continue{rest}
152	    case FiniteNumber{} Float{value}: choose_checked(F32.is_le(F32.abs(value),3.4028234e38),path,"finite number",raw,rest)
153	    case FiniteNumber{} Binary64{high,_}: choose_checked(U32.is_lt(binary64_exponent(high),2047),path,"finite number",raw,rest)
154	    case StringValue{} Text{_}: Continue{rest}
155	    case StringValue{} Utf16Text{units}: choose_checked(Utf16.valid(units),path,"string",raw,rest)
156	    case BoolValue{} Boolean{_}: Continue{rest}
157	    case Literal{value} _: choose_checked(equal(value,raw),path,"literal",raw,rest)
158	    case LiteralValues{values} _: choose_checked(alternatives(values,raw),path,"literal",raw,rest)
159	    case LiteralRendered{values,expected} _: choose_checked(alternatives(values,raw),path,expected,raw,rest)
160	    case Nullable{_} Null{}: Continue{rest}
161	    case Nullable{inner} _: Continue{Work{inner,raw,path} <> rest}
162	    case ArrayValue{inner} Array{items}: Continue{array_work(inner,items,path,0,rest)}
163	    case Struct{fields} Object{values}: Continue{struct_work(fields,values,path,rest)}
164	    case HandleValue{ns} Handle{actual,id}: choose_checked(U32.is_eq(ns,actual) && U32.is_gt(Key.index(id),0),path,"same-world handle",raw,rest)
165	    case Integer{} _: Stop{Invalid{path,"integer",raw}}
166	    case FiniteNumber{} _: Stop{Invalid{path,"finite number",raw}}
167	    case StringValue{} _: Stop{Invalid{path,"string",raw}}
168	    case BoolValue{} _: Stop{Invalid{path,"boolean",raw}}
169	    case ArrayValue{_} _: Stop{Invalid{path,"array",raw}}
170	    case Struct{_} _: Stop{Invalid{path,"object",raw}}
171	    case HandleValue{_} _: Stop{Invalid{path,"same-world handle",raw}}
172	def validate(fuel:Nat,step:Step,+original:Raw) -> Checked:
173	  match fuel step:
174	    case _ Stop{error}: Rejected{error}
175	    case _ Continue{[]}: Accepted{original}
176	    case 0n Continue{Work{_,_,path} <> _}: Rejected{FuelExhausted{path}}
177	    case 1n+more Continue{Work{codec,raw,path} <> rest}: validate(more,expand(codec,raw,path,rest),original)
178	def owned(~Owner:Type,fuel:Nat,codec:Codec,input:Owned<Owner>) -> Receipt<Owner>:
179	  match input:
180	    case Owned{owner,+description}: Receipt{owner,validate(fuel,Continue{[Work{codec,description,"$"}]},description)}
181	
182	def associated(~Owner:Type,fuel:Nat,codec:Codec,observed:Owner & Raw) -> Receipt<Owner>:
183	  match observed:
184	    case (owner,description): owned(~Owner,fuel,codec,Owned{owner,description})
185	# The closed schema projection must inspect the actual owner. It returns that
186	# owner rather than caller-supplied unrelated metadata. Its semantics are trusted.
187	def validate_owner(~Owner:Type,~project:Owner -> Owner & Raw,fuel:Nat,codec:Codec,owner:Owner) -> Receipt<Owner>:
188	  associated(~Owner,fuel,codec,project(owner))
189	
190	def canonical_array_join(head:Raw,tail:Raw) -> Raw:
191	  match tail:
192	    case Array{values}: Array{head <> values}
193	    case other: other
194	def canonical_struct_join(name:String,head:Raw,tail:Raw) -> Raw:
195	  match tail:
196	    case Object{fields}: Object{Field{name,head} <> fields}
197	    case other: other
198	def canonical(fuel:Nat,codec:Codec,raw:Raw) -> Raw:
199	  match fuel codec raw:
200	    case 0n _ raw: raw
201	    case 1n+more Nullable{inner} Null{}: Null{}
202	    case 1n+more Nullable{inner} raw: canonical(more,inner,raw)
203	    case 1n+more ArrayValue{_} Array{[]}: Array{[]}
204	    case 1n++more ArrayValue{+inner} Array{head <> tail}: canonical_array_join(canonical(more,inner,head),canonical(more,ArrayValue{inner},Array{tail}))
205	    case 1n+more Struct{[]} Object{_}: Object{[]}
206	    case 1n++more Struct{NamedCodec{+name,codec} <> rest} Object{+values}: canonical_struct_join(name,canonical(more,codec,field(name,values)),canonical(more,Struct{rest},Object{values}))
207	    case _ _ raw: raw
208	def normalized(~Owner:Type,+fuel:Nat,+codec:Codec,result:Receipt<Owner>) -> Receipt<Owner>:
209	  match result:
210	    case Receipt{owner,Accepted{value}}: Receipt{owner,Accepted{canonical(fuel,codec,value)}}
211	    case Receipt{owner,Rejected{error}}: Receipt{owner,Rejected{error}}
212	def decode_owner(~Owner:Type,~project:Owner -> Owner & Raw,+fuel:Nat,+codec:Codec,owner:Owner) -> Receipt<Owner>:
213	  normalized(~Owner,fuel,codec,validate_owner(~Owner,~project,fuel,codec,owner))