def aes_bytes_valid_cons_proof

qasim-bend-kit@0.1.0.2 · libs/AES256GCM.bend:333

import Base

333def aes_bytes_valid_cons_proof(x: U32, tail: List<&2, U32>,
334    head_proof: Maybe<&0, {U32.is_lt(x, 256) == True{} : Bool}>,
335    tail_proof: Maybe<&0, {bytes_valid(tail) == True{} : Bool}>) ->
336    Maybe<&0, {bytes_valid(x <> tail) == True{} : Bool}>:
337    match head_proof tail_proof:
338        case None{} _: None{}
339        case _ None{}: None{}
340        case Some{hp} Some{tp}:
341            Some{Equal.trans(Bool, Bool.and(U32.is_lt(x, 256), bytes_valid(tail)),
342                Bool.and(True{}, bytes_valid(tail)), True{},
343                Equal.cong(Bool, Bool, b => Bool.and(b, bytes_valid(tail)),
344                    U32.is_lt(x, 256), True{}, hp),
345                Equal.trans(Bool, Bool.and(True{}, bytes_valid(tail)),
346                    bytes_valid(tail), True{}, {==}, tp))}