Fill.keep_c: def of bend-collections-laws-crypto@1.0.0.0
Import: import bend-collections-laws-crypto@1.0.0.0/proofs/crypto/argon2/fill.bend as Fill
Lines 306-307 of bend-collections-laws-crypto@1.0.0.0/proofs/crypto/argon2/fill.bend: https://jend.leeeet.dev/read.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/crypto/argon2/fill.bend&start_line=306&end_line=307

import Base
import bend-collections-laws-crypto@1.0.0.0/spec/lib/common.bend as SC
import bend-collections-laws-crypto@1.0.0.0/proofs/lib/logic.bend as L
import bend-collections-laws-crypto@1.0.0.0/src/crypto/argon2/types.bend as A

def keep_c(+d: Nat, +m1: List<&2, A.Block>, +m2: List<&2, A.Block>, +e: {SC.length(A.Block, m2) == SC.length(A.Block, m1) : Nat}, +hc: {Nat.is_le(Nat.mul(SC.length(A.Block, m1), 256n), SC.pow2(d)) == True{} : Bool}) -> {Nat.is_le(Nat.mul(SC.length(A.Block, m2), 256n), SC.pow2(d)) == True{} : Bool}:
  L.subst(Nat, z => {Nat.is_le(Nat.mul(z, 256n), SC.pow2(d)) == True{} : Bool}, SC.length(A.Block, m1), SC.length(A.Block, m2), Equal.sym(Nat, SC.length(A.Block, m2), SC.length(A.Block, m1), e), hc)

Uses (10):
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Bool
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Equal.sym
  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=Nat.is_le
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Nat.mul
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/lib/logic.bend&name=subst
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/spec/lib/common.bend&name=length
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/spec/lib/common.bend&name=pow2
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/src/crypto/argon2/types.bend&name=Block