1	import Base
2	import ./decode_data.bend as D
3	
4	def codec_size(codec:D.Codec) -> Nat:
5	  match codec:
6	    case D.Nullable{inner}: Nat.add(1n,codec_size(inner))
7	    case D.ArrayValue{inner}: Nat.add(1n,codec_size(inner))
8	    case D.Struct{[]}: 1n
9	    case D.Struct{D.NamedCodec{_,child} <> rest}: Nat.add(1n,Nat.add(codec_size(child),codec_size(D.Struct{rest})))
10	    case _: 1n
11	
12	def raw_size(raw:D.Raw) -> Nat:
13	  match raw:
14	    case D.Array{[]}: 1n
15	    case D.Array{head <> rest}: Nat.add(raw_size(head),raw_size(D.Array{rest}))
16	    case D.Object{[]}: 1n
17	    case D.Object{D.Field{_,child} <> rest}: Nat.add(raw_size(child),raw_size(D.Object{rest}))
18	    case _: 1n
19	
20	def budget(codec:D.Codec,raw:D.Raw) -> Nat:
21	  Nat.mul(4n,Nat.mul(codec_size(codec),Nat.add(raw_size(raw),1n)))