View source
h-correction
  • Contributors
    1. Loading...
Author Commit Message Date Builds
2 commits behind master.
Robert Sison
Disable nested branching & guard against abs H-region in I'_H_region_step. Also shuffle theory around so coupling invar can refer to noop-refinement.
Robert Sison
Design new ideal requirement for coupling invar, just need to prove it...
Robert Sison
Safety commit stub of same_intermediacy_class rework and its proof impacts
Robert Sison
Reinstate N'_if_H as clone of N'_if_L but with call to inner padding func
Robert Sison
Start getting a sense of the R_N'_preservation proof, discover some TODOs
Robert Sison
Another note FOR TOBY for a pass-thru helper proof I'm going to put aside
Robert Sison
Introduce 'same sans meta' equality & use it to fix a broken safety proof
Robert Sison
Work on difficulty proving N'_terminal_forms: See notes marked FOR TOBY. Note that the changes in N' shuffle the numbers around for readability, but don't actually make any changes to the N'_if_L mega-clause.
Robert Sison
Totally redesign Jz wellformedness conds with heavy use of Jz metadata. JzMeta is now a parameter to the locale, and the RISCCompilation locale makes heavy use of it, essentially shoving the entire of the compiled sub-programs (then/else cases of an If-branch) in there. I'm now roughly up to where I was this morning before this change, just have to deal with complications of metadata affecting "sameness" of instructions.
Robert Sison
Commit some difficulties proving extract_parts_jz correctness before pivot
Robert Sison
Improve N'_if_L usability down to a TODO for extract_parts_jz correctness
Robert Sison
Safety commit: Tom's Let mono helper, & experimental If-L/H N' case forms. The ind_let_mono helper allows us to use "let" statements inside the guards of the inductive set N', which reduces the number of annoying schematic variables to fill in when trying to use its intro rules. Tried a huge guard covering all of the internal steps of the If-cmd, so we don't have to split it into several cases like we did for R. With a bit of wrangling, seems workable. Also proved an in…
Robert Sison
Good point of progress: kick jumps out of N'_default, making proofs easier
Robert Sison
WIP starting to adapt pad_H_branches and N to metadata-indicated structure
Robert Sison
Move all H-branch padding func-related WIPs to RISCHighBranchPadding.thy
Robert Sison
Sharpen Jz metadata to carry ex label for If-L & distinguish from While-L
Robert Sison
More floundering at proof structure for H-padding as noop refinement
Robert Sison
Some naive approaches at proof nonnesting_pad_H_branches a noop refinement
Robert Sison
Adapt existing refinement safety proofs for noop refinement and stub TODOs
Robert Sison
One weird trick to prove noop refinement step-closedness lock stall cases
Robert Sison
Prove closedness under steps for noop refinement except lock stall cases
Robert Sison
Sketch out 'noop-refinement relation' & start proving nice things about it
Robert Sison
Just repair rest of refinement proofs for new H_region compile_cmd argument
Robert Sison
Fix issues found with Jz wellformed-check/splitting at expense of usability
Robert Sison
Fix compile_cmd_exit_label_oob proof, de-duplicating it significantly
Robert Sison
Reverse most of damage to proofs by no longer padding at compiler If case
Robert Sison
Note 6 more helper lemmas' If-cases broken due to new use of pad_H_branches
Robert Sison
Survey the unmaintainable trainwreck of the compile_cmd_output_label proof
Robert Sison
Safety commit of attempts at lemmas about pad_H_branches' effect on labels
Robert Sison
Give up on code equations for pad_H because a waste of time without proofs
Robert Sison
Try adding some code equations but the simple pad_H still doesn't execute
Robert Sison
Improve measure, fix bug where todo pile not depleted, find other problems
Robert Sison
Safety commit after struggle w termination/conds for nested H-padding func I'm considering stepping back to simpler H-padding that doesn't support nested branching, to see what the coupling invar proof for that will be like, until I get some advice on my approach for the nested version. Also my tree datatype isn't executable apparently due to some cryptic 'not of sort' error I don't understand. I think I need a consult.
Robert Sison
Safety commit per-step re-implementation of H-padding func & testing setup
Robert Sison
Stash more thoughts on nested branching before starting redesign of pad_H
Robert Sison
Some thoughts on how to handle nested branching support in pad_H_branches
Robert Sison
Have pad_H_branches take AugPMem & implement compile_cmd H-region support. This includes forcing branch equalisation & Lock/While bans in H-regions. The basic sanity-checks for pad_H_branches still hold. Now must refurbish the entire wr-compiler proof base for argument changes to compile_cmd...
Robert Sison
Move pad_H_branches draft up & revive expr_never_H If-L/H compiler switch
Robert Sison
Tweak I'_default to allow Jz-None (TODO: R next) to distinguish L-branches
Robert Sison
Prove Assign case of compiler-coupling with hacky lemma about compile_expr
Robert Sison
Trouble getting traction reasoning about coupling invar with compile_expr
Robert Sison
Prove trivial terminal cases of compiler-coupling proof and plan approach
Robert Sison
Delete same_structure draft & find goal anticipated by last commit message
Robert Sison
Simplify I'_H_region_step making I' sym & closed under steps for our Bs, R We've proved our nominated coupling invariant I simpler_refinement_safe for our R and for Bs with no looping nor visible effects in H regions, but I'm still expecting an obligation to show that it is a reasonable characterisation for low-eq pairs of init states for compiled programs. I expect to need to add a padding post-processing step and to prove that it yields programs whose low-eq pairs of …
Robert Sison
Prove I'_if_H case surprisingly easily & start teeing up I'_H_region_step
Robert Sison
Prove I'_default case of I'_closed_under_steps_R_H_region_conds_B lemma
Robert Sison
Use some helpful properties to simplify step-closedness goal somewhat
Robert Sison
Tee up simpler_refinement lemmas for concrete 'I' pending step-closedness
Robert Sison
With feedback & cleanup prove nice stuff about H-branch padding function. The cleanups were: Move visible_var definition to Security.thy, add an official decoration to Tau to distinguish between non-/epilogue steps, & ensure TimingSafe lemmas pertain to an arbitrary coupling invariant.
Robert Sison
Move RISC H-branching stuff to new .thy to reduce long build dependency
Robert Sison
Draft a H-branch padding function but trouble proving basic facts about it
Robert Sison
Attempt closed_under_steps, uncovering deficiencies in coupling invar draft
Robert Sison
Draft new coupling invar & prove desired reqs apart from closed_under_steps
Robert Sison
Fix no_L_assign definition so no_L_assign_in_H_region true of type system
Robert Sison
Start trying to prove the type system establishes no_L_assign_in_H_region
Robert Sison
Prove that the type system establishes no_locking/looping_in_H_region
Robert Sison
Successfully push 'visible effects in H region ban' up to WhileLang level. That is to say, prove that for our R it is sufficient to impose it at the WhileLang level (as a side-requirement on the bisimulation B) rather than trying to impose it on the coupling invariant 'I' we'll be constructing, in order to obtain that B, R, and I satisfy simpler_refinement_safe.
Robert Sison
Tweak visible effects ban only to apply when the program location differs
Robert Sison
Tweak conditions for abs_steps consistency so loop ban can be more precise
Robert Sison
Typecheck branch on a H-assigned NoRW-locked L-var in the nesting example
Robert Sison
Typecheck a number of H-branching example programs including nested If-Hs
Robert Sison
Prove R2 closed under globally consistent changes. No sorries left! Next TBD is to define and prove suitable side-conditions to replace "consistent branching" for the compiler to be able to handle the new H-branching regions, and perhaps sanity-check on an example program.
Robert Sison
Prove R2_mem_eq by extracting the common part from R1_mem_eq as a lemma
Robert Sison
Refurbish R_typed_step proof. Just R2_mem_eq/cg_consistent lemmas left!
Robert Sison
Obtain R2_weak_bisim trivially now we know its sufficient conditions hold
Robert Sison
Repair R_equiv_entailment by allowing subtyping on final env of if_H_type
Robert Sison
Re-prove R_typed_step lemma except broken R_equiv_entailment for sub case
Robert Sison
Wipe preds mentioning vars touched by H-regions so R2 closed under steps
Robert Sison
Prove R2 closed under steps pending wiping preds mentioning touched vars
Robert Sison
Improve design of H_region checks and re-prove some desired properties
Robert Sison
Start moving over to simpler checks for H-regions/R2, including step counts
Robert Sison
Revert subtyping rule relaxation attempt but keep new definitions/lemmas
Robert Sison
Draft context_subtype definitions to relax subtyping rule, but hit trouble
Robert Sison
Draft rephrase of preservation to allow either has_(H_)type as destination. Also note TobyM suggestion to generalise sub rule to allow safe overapprox.
Robert Sison
Messy attempt to inflate touched var types to H, but preservation violated
Robert Sison
Notes on various options for R2 guard relating mems, and their problems
Robert Sison
A bit of work towards R2 tyenv_eq preservation but unsure how far off I am
Robert Sison
Adapt preservation lemma to H_type system, towards R2_closed_under_steps
Robert Sison
Move up nice proofs & check closed_under_steps sufficient for 'weak_bisim'
Robert Sison
Prove some desired properties of has_H_type and R2 plus some While helpers
Robert Sison
Prove R2 case of R3_weak_bisim but note that it leans on a sorried lemma
Robert Sison
Kludge stops_consistently in if_H_type to make R_typed_step lemma provable
Robert Sison
Make R2's guards line up a bit better to compose sequentially with R1's
Robert Sison
Kludge stops_consistently to see proof impact. Also remove offer of evB_eq
Robert Sison
Finish proving if_H case of R_typed_step, take stock of what's broken by R2
Robert Sison
Start reinstating H-branch sub-relation R2, prove/stub some relevant facts
Robert Sison
Tweak assign cases for inner H type system so it implies outer typecheck
Robert Sison
Start drafting new case and an inner type system for If-H and its branches
Robert Sison
Impose conditions for abs_steps consistency. Proof difficulty to be seen
Robert Sison
Survey gap between these reqs & simpler_refinement_safe: namely abs_steps
Robert Sison
Analogous no_visible_effects definition & lemmas for RISCLang bisim rels
Robert Sison
Rename old 'same_timing' draft to 'same_structure' to prep for new attempt
Robert Sison
Tweak draft WL bisim side-condition informed by lemma in previous commit
Robert Sison
Determine reqs to impose on subset of bisim so also a strong_low_bisim_mm
Robert Sison
Commit fixes to RISCCompiledWhileCmd forgotten from Jz metadata commit
Robert Sison
Small proof that states remain low-eq after a step with no visible effects
Robert Sison
Add a no-locking condition too, try defining a closed-under-eval condition
Robert Sison
Bar-napkin-sketch bisim condition that applies naive one to If-'H'-branch?
Robert Sison
Naive no-L-assign condition on bisim that covers too much of the program
Robert Sison
Add always-on metadata to wr-compiler for If-cond Jz & gauge proof impact
Robert Sison
Tiny tweaks to statement to be refurbished for timing consistency
Robert Sison
Fill out experiment a bit more with tentative coupling invar. definition
Robert Sison
Note an idea on retaining knowledge of program structure from WhileLang
Robert Sison
Notes to experiment with non-PC-secure coupling invariant for H-branching