Closed ajewellamz closed 2 weeks ago
Description of changes:
CanonizeForEn(De)crypt moved to Canonize.ForEn(De)crypt, using mech different verification strategy.
Output ensure's for En(De)cryptPathStructure moved to lemmas, so they never need to see the final opaque ensured predicate.
By submitting this pull request, I confirm that you can use, modify, copy, and redistribute this contribution, under the terms of your choice.
Description of changes:
CanonizeForEn(De)crypt moved to Canonize.ForEn(De)crypt, using mech different verification strategy.
Output ensure's for En(De)cryptPathStructure moved to lemmas, so they never need to see the final opaque ensured predicate.
By submitting this pull request, I confirm that you can use, modify, copy, and redistribute this contribution, under the terms of your choice.