hcorrection

 Loading...
Author  Commit  Message  Date  Builds  

2 commits behind master.  
Disable nested branching & guard against abs Hregion in I'_H_region_step.
Also shuffle theory around so coupling invar can refer to nooprefinement.



Design new ideal requirement for coupling invar, just need to prove it...



Safety commit stub of same_intermediacy_class rework and its proof impacts



Reinstate N'_if_H as clone of N'_if_L but with call to inner padding func



Start getting a sense of the R_N'_preservation proof, discover some TODOs



Another note FOR TOBY for a passthru helper proof I'm going to put aside



Introduce 'same sans meta' equality & use it to fix a broken safety proof



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 megaclause.



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
subprograms (then/else cases of an Ifbranch) 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.



Commit some difficulties proving extract_parts_jz correctness before pivot



Improve N'_if_L usability down to a TODO for extract_parts_jz correctness



Safety commit: Tom's Let mono helper, & experimental IfL/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 Ifcmd,
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â€¦



Good point of progress: kick jumps out of N'_default, making proofs easier



WIP starting to adapt pad_H_branches and N to metadataindicated structure



Move all Hbranch padding funcrelated WIPs to RISCHighBranchPadding.thy



Sharpen Jz metadata to carry ex label for IfL & distinguish from WhileL



More floundering at proof structure for Hpadding as noop refinement



Some naive approaches at proof nonnesting_pad_H_branches a noop refinement



Adapt existing refinement safety proofs for noop refinement and stub TODOs



One weird trick to prove noop refinement stepclosedness lock stall cases



Prove closedness under steps for noop refinement except lock stall cases



Sketch out 'nooprefinement relation' & start proving nice things about it



Just repair rest of refinement proofs for new H_region compile_cmd argument



Fix issues found with Jz wellformedcheck/splitting at expense of usability



Fix compile_cmd_exit_label_oob proof, deduplicating it significantly



Reverse most of damage to proofs by no longer padding at compiler If case



Note 6 more helper lemmas' Ifcases broken due to new use of pad_H_branches



Survey the unmaintainable trainwreck of the compile_cmd_output_label proof



Safety commit of attempts at lemmas about pad_H_branches' effect on labels



Give up on code equations for pad_H because a waste of time without proofs



Try adding some code equations but the simple pad_H still doesn't execute



Improve measure, fix bug where todo pile not depleted, find other problems



Safety commit after struggle w termination/conds for nested Hpadding func
I'm considering stepping back to simpler Hpadding 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.



Safety commit perstep reimplementation of Hpadding func & testing setup



Stash more thoughts on nested branching before starting redesign of pad_H



Some thoughts on how to handle nested branching support in pad_H_branches



Have pad_H_branches take AugPMem & implement compile_cmd Hregion support.
This includes forcing branch equalisation & Lock/While bans in Hregions.
The basic sanitychecks for pad_H_branches still hold. Now must refurbish
the entire wrcompiler proof base for argument changes to compile_cmd...



Move pad_H_branches draft up & revive expr_never_H IfL/H compiler switch



Tweak I'_default to allow JzNone (TODO: R next) to distinguish Lbranches



Prove Assign case of compilercoupling with hacky lemma about compile_expr



Trouble getting traction reasoning about coupling invar with compile_expr



Prove trivial terminal cases of compilercoupling proof and plan approach



Delete same_structure draft & find goal anticipated by last commit message



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 loweq pairs of init states for compiled programs.
I expect to need to add a padding postprocessing step and to prove that
it yields programs whose loweq pairs of â€¦



Prove I'_if_H case surprisingly easily & start teeing up I'_H_region_step



Prove I'_default case of I'_closed_under_steps_R_H_region_conds_B lemma



Use some helpful properties to simplify stepclosedness goal somewhat



Tee up simpler_refinement lemmas for concrete 'I' pending stepclosedness



With feedback & cleanup prove nice stuff about Hbranch 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.



Move RISC Hbranching stuff to new .thy to reduce long build dependency



Draft a Hbranch padding function but trouble proving basic facts about it



Attempt closed_under_steps, uncovering deficiencies in coupling invar draft



Draft new coupling invar & prove desired reqs apart from closed_under_steps



Fix no_L_assign definition so no_L_assign_in_H_region true of type system



Start trying to prove the type system establishes no_L_assign_in_H_region



Prove that the type system establishes no_locking/looping_in_H_region



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 siderequirement 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.



Tweak visible effects ban only to apply when the program location differs



Tweak conditions for abs_steps consistency so loop ban can be more precise



Typecheck branch on a Hassigned NoRWlocked Lvar in the nesting example



Typecheck a number of Hbranching example programs including nested IfHs



Prove R2 closed under globally consistent changes. No sorries left!
Next TBD is to define and prove suitable sideconditions to replace
"consistent branching" for the compiler to be able to handle the new
Hbranching regions, and perhaps sanitycheck on an example program.



Prove R2_mem_eq by extracting the common part from R1_mem_eq as a lemma



Refurbish R_typed_step proof. Just R2_mem_eq/cg_consistent lemmas left!



Obtain R2_weak_bisim trivially now we know its sufficient conditions hold



Repair R_equiv_entailment by allowing subtyping on final env of if_H_type



Reprove R_typed_step lemma except broken R_equiv_entailment for sub case



Wipe preds mentioning vars touched by Hregions so R2 closed under steps



Prove R2 closed under steps pending wiping preds mentioning touched vars



Improve design of H_region checks and reprove some desired properties



Start moving over to simpler checks for Hregions/R2, including step counts



Revert subtyping rule relaxation attempt but keep new definitions/lemmas



Draft context_subtype definitions to relax subtyping rule, but hit trouble



Draft rephrase of preservation to allow either has_(H_)type as destination.
Also note TobyM suggestion to generalise sub rule to allow safe overapprox.



Messy attempt to inflate touched var types to H, but preservation violated



Notes on various options for R2 guard relating mems, and their problems



A bit of work towards R2 tyenv_eq preservation but unsure how far off I am



Adapt preservation lemma to H_type system, towards R2_closed_under_steps



Move up nice proofs & check closed_under_steps sufficient for 'weak_bisim'



Prove some desired properties of has_H_type and R2 plus some While helpers



Prove R2 case of R3_weak_bisim but note that it leans on a sorried lemma



Kludge stops_consistently in if_H_type to make R_typed_step lemma provable



Make R2's guards line up a bit better to compose sequentially with R1's



Kludge stops_consistently to see proof impact. Also remove offer of evB_eq



Finish proving if_H case of R_typed_step, take stock of what's broken by R2



Start reinstating Hbranch subrelation R2, prove/stub some relevant facts



Tweak assign cases for inner H type system so it implies outer typecheck



Start drafting new case and an inner type system for IfH and its branches



Impose conditions for abs_steps consistency. Proof difficulty to be seen



Survey gap between these reqs & simpler_refinement_safe: namely abs_steps



Analogous no_visible_effects definition & lemmas for RISCLang bisim rels



Rename old 'same_timing' draft to 'same_structure' to prep for new attempt



Tweak draft WL bisim sidecondition informed by lemma in previous commit



Determine reqs to impose on subset of bisim so also a strong_low_bisim_mm



Commit fixes to RISCCompiledWhileCmd forgotten from Jz metadata commit



Small proof that states remain loweq after a step with no visible effects



Add a nolocking condition too, try defining a closedundereval condition



Barnapkinsketch bisim condition that applies naive one to If'H'branch?



Naive noLassign condition on bisim that covers too much of the program



Add alwayson metadata to wrcompiler for Ifcond Jz & gauge proof impact



Tiny tweaks to statement to be refurbished for timing consistency



Fill out experiment a bit more with tentative coupling invar. definition



Note an idea on retaining knowledge of program structure from WhileLang



Notes to experiment with nonPCsecure coupling invariant for Hbranching

