AES256GCM.bytes_length_limit.go: def of qasim-bend-kit@0.1.0.2
Import: import qasim-bend-kit@0.1.0.2/libs/AES256GCM.bend as AES256GCM
Lines 40-53 of qasim-bend-kit@0.1.0.2/libs/AES256GCM.bend: https://jend.leeeet.dev/read.txt?path=qasim-bend-kit@0.1.0.2/libs/AES256GCM.bend&start_line=40&end_line=53

import Base

def bytes_length_limit.go(fuel: Nat, bytes: List<&2, U32>,
                          low: U32, +high: U32, +max_low: U32, +max_high: U32,
                          within: Bool) -> Bool:
    match fuel bytes within:
        case 0n Nil{} _: within
        case 0n _ <> _ _: False{}
        case 1n+p Nil{} _: False{}
        case 1n+p _ <> _ False{}: False{}
        case 1n+p _ <> tail True{}:
            +next_low = U32.add(low, 1)
            +next_high = Bool.pick(U32, U32.is_eq(next_low, 0), U32.add(high, 1), high)
            bytes_length_limit.go(p, tail, next_low, next_high,
                max_low, max_high,
                length_pair_within(next_low, next_high, max_low, max_high))

Uses (8):
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Bool
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Bool.pick
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=List
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Nat
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=U32
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=U32.add
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=U32.is_eq
  https://jend.leeeet.dev/definition.txt?path=qasim-bend-kit@0.1.0.2/libs/AES256GCM.bend&name=length_pair_within