Add support for variable length shifts (wordLang + below)#1341
Merged
tanyongkiam merged 65 commits intomasterfrom Feb 25, 2026
Merged
Add support for variable length shifts (wordLang + below)#1341tanyongkiam merged 65 commits intomasterfrom
tanyongkiam merged 65 commits intomasterfrom
Conversation
Progress on #1213
Something for #1036 to relax
- Adjusted shift_rwt - Added shift_imm_rwt (also added to arm7_encode_rwts)
One in ssa_cc_trans_correct, and the other two have something to do with the conventions, presumably (inst_arg_convention (Arith (Shift _ _ _ (Reg r))) ⇔ r = 8) ∧ from wordConvs.
In theorem inst_select_exp_thm
- 3 cheats in comp_correct - Broken starting init_code_thm
This reverts commit 89ce8a9.
derive_corr_thm fails for some theorems.
Co-authored-by: Yong Kiam <tanyongkiam@gmail.com>
Verified fixes: - stackPropsScript: reg_bound_exp/reg_bound_inst handle both Shift subexps - word_to_stackScript: wInst handles reg_imm Shift argument - word_copyScript: copy_prop_inst handles Shift reg_imm - word_to_stackProofScript: map_var/evaluate_wInst for new Shift - word_allocProofScript: nlive_store/every_inst proofs for Shift - stack_removeProofScript: state_rel_inst/comp_correct for Shift - stack_allocProofScript: inst_select_exp for Shift reg_imm - wordConvsProofScript: copy_prop for new Shift - data_to_wordScript: ShiftN overload for assign/assign_var - data_to_word_bignumProofScript: AnyHeader_thm ShiftVar cases - stack_to_labProofScript: add simp[w2n_lt] for Shift assert in inst_correct Not yet fixed: - lab_to_targetProofScript: arith_upd_lemma needs new Shift >- block (WIP) Co-Authored-By: Claude Opus 4.6 <noreply@anthropic.com>
Co-authored-by: Magnus Myreen <myreen@chalmers.se>
Co-Authored-By: Claude Opus 4.6 <noreply@anthropic.com>
Co-Authored-By: Claude Opus 4.6 <noreply@anthropic.com>
…imps Co-Authored-By: Claude Opus 4.6 <noreply@anthropic.com>
…refByte Co-Authored-By: Claude Opus 4.6 <noreply@anthropic.com>
Once cheats are removed, this file should be done (hopefully)
Split Shift d1 definitions into Imm/Reg variants for arm7, arm8, mips, riscv. Split shift theorem processing to handle reg_imm for arm8, mips, riscv. Add Store16/Store32/Load16/Load32 d1 entries for mips, riscv, ag32. Co-Authored-By: Claude Opus 4.6 <noreply@anthropic.com>
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
3 participants
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.
Closes #1213