I noticed that the theorem bytes_invariant_vk was stating properties on pk instead of vk. This means that we couldn't prove honest uses of vk, the malicious uses of vk were correctly captured by vk_preserves_publishability and the attacker theorem in DY.Core.Attacker.Knowledge, so this typo did not impact the soundness of DY*.
I also noticed a redundant hypothesis in bytes_invariant_sign so I removed it.
I noticed that the theorem
bytes_invariant_vkwas stating properties onpkinstead ofvk. This means that we couldn't prove honest uses ofvk, the malicious uses ofvkwere correctly captured byvk_preserves_publishabilityand the attacker theorem in DY.Core.Attacker.Knowledge, so this typo did not impact the soundness of DY*.I also noticed a redundant hypothesis in
bytes_invariant_signso I removed it.