I was looking at the padder proofs and realized that in #926 I had a typo and accidentally pushed the wrong branch (sha-padder-proofs4 instead of sha-padder-proofs5, that's what I get for non-descriptive branch names). The version that got merged was the first draft of the full proofs with still a number of padder-specific admits; this updated version has the admits factored into the small set discussed in #926. Sorry for the mixup!
I was looking at the padder proofs and realized that in #926 I had a typo and accidentally pushed the wrong branch (
sha-padder-proofs4instead ofsha-padder-proofs5, that's what I get for non-descriptive branch names). The version that got merged was the first draft of the full proofs with still a number of padder-specific admits; this updated version has the admits factored into the small set discussed in #926. Sorry for the mixup!