DecodeSize.budget: def of bendvy-ecs-core@0.1.0.3
Import: import bendvy-ecs-core@0.1.0.3/decode_size.bend as DecodeSize
Lines 20-21 of bendvy-ecs-core@0.1.0.3/decode_size.bend: https://jend.leeeet.dev/read.txt?path=bendvy-ecs-core@0.1.0.3/decode_size.bend&start_line=20&end_line=21

import Base
import bendvy-ecs-core@0.1.0.3/decode_data.bend as D

def budget(codec:D.Codec,raw:D.Raw) -> Nat:
  Nat.mul(4n,Nat.mul(codec_size(codec),Nat.add(raw_size(raw),1n)))

Uses (7):
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Nat
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Nat.add
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Nat.mul
  https://jend.leeeet.dev/definition.txt?path=bendvy-ecs-core@0.1.0.3/decode_data.bend&name=Codec
  https://jend.leeeet.dev/definition.txt?path=bendvy-ecs-core@0.1.0.3/decode_data.bend&name=Raw
  https://jend.leeeet.dev/definition.txt?path=bendvy-ecs-core@0.1.0.3/decode_size.bend&name=codec_size
  https://jend.leeeet.dev/definition.txt?path=bendvy-ecs-core@0.1.0.3/decode_size.bend&name=raw_size