AES256GCM.aes_bytes_valid_cons_proof: def of qasim-bend-kit@0.1.0.2
Import: import qasim-bend-kit@0.1.0.2/libs/AES256GCM.bend as AES256GCM
Lines 333-346 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=333&end_line=346

import Base

def aes_bytes_valid_cons_proof(x: U32, tail: List<&2, U32>,
    head_proof: Maybe<&0, {U32.is_lt(x, 256) == True{} : Bool}>,
    tail_proof: Maybe<&0, {bytes_valid(tail) == True{} : Bool}>) ->
    Maybe<&0, {bytes_valid(x <> tail) == True{} : Bool}>:
    match head_proof tail_proof:
        case None{} _: None{}
        case _ None{}: None{}
        case Some{hp} Some{tp}:
            Some{Equal.trans(Bool, Bool.and(U32.is_lt(x, 256), bytes_valid(tail)),
                Bool.and(True{}, bytes_valid(tail)), True{},
                Equal.cong(Bool, Bool, b => Bool.and(b, bytes_valid(tail)),
                    U32.is_lt(x, 256), True{}, hp),
                Equal.trans(Bool, Bool.and(True{}, bytes_valid(tail)),
                    bytes_valid(tail), True{}, {==}, tp))}

Uses (9):
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Bool
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Bool.and
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Equal.cong
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Equal.trans
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=List
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Maybe
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=U32
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=U32.is_lt
  https://jend.leeeet.dev/definition.txt?path=qasim-bend-kit@0.1.0.2/libs/AES256GCM.bend&name=bytes_valid