AESLengthLimitProof.bytes_length_limit_same: def of qasim-bend-kit@0.1.0.2
Import: import qasim-bend-kit@0.1.0.2/proof/AES_LengthLimitProof.bend as AESLengthLimitProof
Lines 71-78 of qasim-bend-kit@0.1.0.2/proof/AES_LengthLimitProof.bend: https://jend.leeeet.dev/read.txt?path=qasim-bend-kit@0.1.0.2/proof/AES_LengthLimitProof.bend&start_line=71&end_line=78

import Base
import qasim-bend-kit@0.1.0.2/libs/AES256GCM.bend as AES

def bytes_length_limit_same(+a: List<&2, U32>, +b: List<&2, U32>,
    +max_low: U32, +max_high: U32,
    same_length: {List.length(&2, U32, a) ==
        List.length(&2, U32, b) : Nat}) ->
    {AES.bytes_length_limit(a, max_low, max_high) ==
     AES.bytes_length_limit(b, max_low, max_high) : Bool}:
    length_limit_go_same(a, b, 0, 0, max_low, max_high, True{},
        same_length)

Uses (7):
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Bool
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=List
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=List.length
  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=qasim-bend-kit@0.1.0.2/libs/AES256GCM.bend&name=bytes_length_limit
  https://jend.leeeet.dev/definition.txt?path=qasim-bend-kit@0.1.0.2/proof/AES_LengthLimitProof.bend&name=length_limit_go_same