Restructure venom/ into defs/proofs/props, simplify equiv API#168
Merged
charles-cooper merged 14 commits intomainfrom Mar 4, 2026
Merged
Restructure venom/ into defs/proofs/props, simplify equiv API#168charles-cooper merged 14 commits intomainfrom
charles-cooper merged 14 commits intomainfrom
Conversation
Directory structure:
defs/ - venomState, venomInst, venomWf(new), venomEffects,
venomExecSemantics(was venomSem), stateEquiv(defs only)
proofs/ - stateEquivProofs, venomProofs, execEquivProofs
props/ - stateEquivProps, venomProps, execEquivProps (ACCEPT_TAC API)
Theory renames:
venomSem -> venomExecSemantics
venomSemProps -> venomProofs/venomProps
execEquiv -> execEquivProofs/execEquivProps
Other changes:
- venomWf extracted from venomInst (well-formedness predicates)
- stateEquiv split: definitions in defs/, 74 theorems in proofs/
- lookup_block/lookup_function refactored to use FIND (stdlib)
- exec_binop/unop/modop -> exec_pure2/pure1/pure3
- Downstream Ancestors updated in passes/ (phi_elimination, revert_to_assert)
- Internal proof helpers marked Triviality
Known issues (to fix in follow-up):
- venomProofs: lookup_block_MEM etc need FIND-based reproof
- execEquivProofs: step_inst_{state,result}_equiv cheated
Consistent naming chain: defs: venomExecSemantics proofs: venomExecProofs props: venomExecProps
stateEquivProps: 74 -> 33 (40 demoted to [local] in proofs)
execEquivProps: 6 -> 2 (4 step-level demoted, keep run_block only)
venomExecProps: 15 -> 13 (4 dead removed)
result_equiv_{ok,halt,revert,error,error_any,mismatch} kept as
exported [simp] rules since execEquivProofs depends on them.
- state_equiv_except vars s1 s2 -> state_equiv vars s1 s2
- execution_equiv_except -> execution_equiv
- result_equiv_except -> result_equiv
- Delete old binary state_equiv, result_equiv, var_equiv
- state_equiv {} s1 s2 replaces old state_equiv s1 s2
…ith vars
stateEquivProps:
- All predicates now parameterized by vars (no {} specializations)
- Drop _except suffix from all theorem names
- Delete crossing theorems (halt/revert_state_from_state_except)
- Delete state_equiv_implies_except (identity after rename)
execEquivProps:
- Add step_inst_result_equiv (general, with operand precondition)
- Generalize run_block_{state,result}_equiv with vars + operand precondition
- 2 -> 3 exported theorems
stateEquivProofs:
- All theorems use state_equiv/execution_equiv (no _except suffix)
- Drop var_equiv references, use execution_equiv_def directly
- Merge {} specializations into general versions
- Delete crossing theorems, observable_equiv extras
- 74 -> ~45 theorems (many internals consolidated)
execEquivProofs:
- Generalize step_inst_result_equiv with vars + operand precondition
- Absorb RTA pattern: per-opcode dispatch with category helpers
- step_inst_result_equiv now canonical (was duplicated in RTA)
- run_block_{state,result}_equiv cheated pending induction proof
venomExecProofs:
- Fix 3 FIND-based lookup cheats via FIND_MEM/FIND_P/FIND_NONE
- Simplify lookup_block_MEM proof
- execEquivProofs: prove step_inst_result_equiv, run_block_{state,result}_equiv
with operand condition (vars parameter)
- venomExecProofs: update for new exec helpers (exec_read0/1, exec_write2)
- revert_to_assert: migrate binary->ternary equiv (state_equiv {}, result_equiv {})
- phiTransform: add stateEquiv ancestor for result_equiv_def access
All 0 cheats. All theories build clean.
- phiBlock: state_equiv/result_equiv {} for all theorem statements and proofs
- Add stateEquiv ancestor for def access
- Add exec_read0/1, exec_write2 to step_inst_preserves_prev_bb
- Fix Halt/Revert cases: execution_equiv_refl instead of state_equiv_refl
- Remove dead trailing tactics
- phiFunction: same binary->ternary migration
- Fix run_function_state_equiv halted case with state_equiv_def unfolding
- Fix result_equiv symmetry with execution_equiv_def
All 0 cheats. All theories build clean.
…t comments - Add result_equiv_trans to stateEquivProofs/Props (used by phi+rta) - Remove duplicate result_equiv_trans from phiBlock and rtaProofHelpers - Remove dead resolve_phi_MEM from rtaProofHelpers (was unused) - Add placement comment for step_inst_preserves_inst_idx in defs file - Mark FIND lemmas as stdlib-gap candidates
…oofs lookup_function_mem, lookup_function_not_mem, lookup_function_MEM were either local or in venomExecProofs, invisible to analysis consumers. Move to venomInstScript.sml where lookup_function is defined. Fix liveness proofs that assumed pattern-matching lookup_block_def (now FIND-based): add FIND_thm to induction proofs.
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.
co-authored by claude opus 4.6
Restructure
venom/intodefs/proofs/propspattern and simplify the equivalence API. All theories build clean with 0 cheats.Changes
Directory restructure
venom/split intovenom/defs/,venom/proofs/,venom/props/with proper HolmakefilesvenomSem→venomExecSemantics,venomProofs→venomExecProofs,venomProps→venomExecPropsstateEquivsplit into defs (indefs/) + proofs (inproofs/) + props API (inprops/)ACCEPT_TACwrappers — clean public APIstep_inst refactoring
step_inst_definto category helpers:exec_pure{1,2,3},exec_read{0,1},exec_write2step_inst_result_equivproven via MEM bridge dispatch (no cheats)Equivalence API simplification
state_equiv_except vars→state_equiv vars,execution_equiv_except→execution_equiv,result_equiv_except→result_equivvar_equivand old binary versionsstate_equiv {}for full equivalence)Downstream passes updated
revert_to_assert: all 4 theories build cleanphi_elimination: all 3 theories build clean (phiTransform, phiBlock, phiFunction)lookup_block/lookup_functionmigrated from custom recursion toFINDStats