Fill W1_zero_eq sorry in X_exp_equiv#40
Closed
eliasjudin wants to merge 1 commit intoruntimeverification:masterfrom
Closed
Fill W1_zero_eq sorry in X_exp_equiv#40eliasjudin wants to merge 1 commit intoruntimeverification:masterfrom
W1_zero_eq sorry in X_exp_equiv#40eliasjudin wants to merge 1 commit intoruntimeverification:masterfrom
Conversation
Replaces the `sorry` in the local helper `W1_zero_eq` inside `X_exp_equiv` with a proof using BEq-to-equality conversion, `intMap_toNat`, and `Int.toNat_eq_zero`. Aristotle solved the decomposed micro-theorem `int_eq_zero_of_nonneg_toNat_zero` (project 00c420ff-9399-41cc-9401-8e44071a3fcd, solved_target: true), which directly guided this recomposition. Co-authored-by: Aristotle (Harmonic) <aristotle-harmonic@harmonic.fun>
Author
|
Superseded by a stacked split where this commit is included in a broader base PR with summary precondition normalization. |
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
1 participant
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
This PR fills the
sorryfor the local helperW1_zero_eqinsideX_exp_equivinEvmEquivalence/Equivalence/Operations/ExpEquivalence.lean. The proof converts theBEqhypothesis to equality, usesintMap_toNatto reduce to atoNatstatement, and closes withInt.toNat_eq_zero.sorrys inX_exp_equiv(gas +gt0/eq0branches) are still blocked onTODO.exp_representation.lake build EvmEquivalence.Equivalence.Operations.ExpEquivalencelake buildPart of #25.
cc @Aristotle-Harmonic