def ok_append

bend-collections-laws-crypto@1.0.0.0 · proofs/crypto/argon2/password.bend:134

import Base
import bend-collections-laws-crypto@1.0.0.0/proofs/lib/logic.bend as L
import bend-collections-laws-crypto@1.0.0.0/proofs/crypto/argon2/phc.bend as PP

134def ok_append(+a: List<&2, U32>, +b: List<&2, U32>, +ha: {PP.ok(a) == True{} : Bool}, +hb: {PP.ok(b) == True{} : Bool}) -> {PP.ok(List.append(&2, U32, a, b)) == True{} : Bool}:
135  match a:
136    case Nil{}:
137      hb
138    case +x <> +r:
139      L.and_intro(Nat.is_lt(U32.to_nat(x), 256n), PP.ok(List.append(&2, U32, r, b)), PP.ok_head(x, r, ha), ok_append(r, b, PP.ok_tail(x, r, ha), hb))