Archived entries from file /home/kirang/Documents/research/suslik-ocaml-writeup/ocaml/todo.org
Extract forall sequence to a sequence of args + properties + body Calculate parameters to instantiate by dropping implicit arguments First parameters are arguments. If body is pure, last argument is function, evars for all intermediate arguments. Print expressions in Coq format Look at pattern of let-exp - if complex (tuple), then emit destruct w.names, update sanitiser with annotations for patterns if annotations w. patterns, then rewrite sepsplittuple if pattern was tuple if match, emit a case on match argument if value [| |] then xvalemptyarr Write function to pretty print VC
Write function to extract vc from coq ctxt
Write function to convert VC to a Z3-checkable VC Refactor proof reduction plugin to be customisable Update plugin to setup proof reduction Build binding of program variables to concrete values Update dynamic tracer to return bindings Fix proof generator state to update program point tracking correctly Map proof variables to program variables to concrete values Store Observation id at start of lambda in function Update context to track mapping of Coq variables to program variables Print out thte concrete values at the current lambda state generate evars for arguments call print reduced tactic on argument to retrieve reduced proof term perform analysis on proof term Implement generator function for higher order functions
Extract proof arguments, determine no. invariants
calculate type of instantiated invariant with explicit parameters collect full explicit parameters for spec using evars for invariant & properties fold over type tracking parameters split params into invariants and evars (tuple) gen fresh var using proof context Generate concrete values for the current point generate concrete values at current program point iterate through concrete values loop through parameters to specification Bind concrete values to proof variables Convert concrete values to Coq terms Create concrete proof term from concrete args Pretty print application as Coq string Pose proof to add it to context
Extract from last element in context then revert, just like typeof function
Perform data flow analysis over reduced proof term Check type of properties evar applied to concrete arguments
extract arguments to evar
Fix bug in translating programs Add unit test for translating programs Add regression test for proof parser Work out why proofs are failing Fix failing program parser configure code to only take branch for symexec higher order pure function when the spec itself is appropriate Debug proof reduction to work out why it isn’t expanding Update cmdliner to take in logical bindings Update tests to pass in logical bindings Work out way to fix for pure programs Fix issues with Z3 encoding construction Implement support for make_rev_list Create branch for array of rev list Rewrite array of rev list in terms of for loop combinator Prove correctness of for loop combinator Prove correctness of rev list using loop combinator Get benchmark running on array of rev list Fix issues with program structure of array of rev list Handle proof parsing of array of rev list Get to Proof term analysis or better w.r.t array of rev list Run tests to ensure current proofs still go through Refactor code to force reduce if normal reduction fails Fix printing of proof terms to make reading manageable Update env to track local_fun_vars Update reduction to handle var apps correctly Analyze proof term to work out how to handle it
Identify what causes the name clashes when extracting
Solve name clash error with extraction
Work out cause of error in specification generator update code to handle empty pure conditions Check that old behaviour is preserved try reversing the candidates Try proving the new proof yourself Add extra column for ifs/matches Print out the full query to z3 for preservation and send to z3 manually Print out check preserved query and debug in Z3 Refactor code with appropriate logging (logs) Update code to take in multiple coq-libs Conditionally send things to z3 if env SIS_Z3 is set Read through SLING To work out why it outputs such poor invariants Setup benchmark test for array find mapi Add support for if then else Setup unit tests for array find mapi Setup code to generate function arguments Get array find map compiling on current code Work out appropriate tactic for xif Update symexec to handle if then else and if then constructs Add handling for ref allocations Update Dune file to work more nicely across projects Add support for xif lemma in proof analysis Add support for simple cases on Bool
Add support for extracting xif lemmas
Update proof env to track poly variables Update proof env to track gamma update symexec higher order pure fun update symexec higher order fun Update generate candidate invariants to use gamma to determine type of holes Update proof env to track updated names of results of let bindings Update mut var checking to use proof vars Fix bug in working out the type of find_mapi Instantiate lemmas with all polymorphic variables Update code to check if intros is needed Add nil constant when lists Make fuzzed functions dependent on ints Fix binding of fp for constants to generator? Bind logical variables (l) extend observation with logical variables If we keep a variable concrete, keep it available in the context Add negb and is_some to context For while and for loops, don’t constrain i Add parsing unit tests for array_exists Add parsing unit tests for array_findi Add parsing unit tests for array_foldi Add parsing unit tests for array_is_sorted Add parsing unit tests for array_map2 Add parsing unit tests for array_of_rev_list Add parsing unit tests for hashtbl_invert Add parsing unit tests for seq_to_array Add parsing unit tests for set_to_list Add parsing unit tests for sll_of_array Add parsing unit tests for sll_partition Add parsing unit tests for stack_filter Add parsing unit tests for stack_reverse Add parsing unit tests for vec_filter Update code to use combinator Update code to properly instantiate until and fold combinators Update build testing function to instantiate arguments properly again Update proof term to have casing on ADTs Add support for casing on ADTs fix xapp arguments to take a type
fix extracted type of combinator for until upto to remove option
Update extraction to work with case ADT
Collect arguments to inv ty that are not ints and are fully instantiated Take as input parameter to ty the concrete variables you need When given functions with one polymorphic variable, instantiate with input parameter Test whether array iter works with list as parameter after invariant Update examples to use new interface to array iter Add function to PCFML to test if a function returns hprop Add parsing unit tests for array_partition Once we’ve instantiated the function with concrete arguments, when instantiating subsequent parameters, check if the variables are constrained.
from extract inv ty, return a list of concrete params + logical params ahtt follow the invariant
Run seq to array with dump output Add folder for generation tests Ensure that generator can find the invariant for TRUE invariant for seq to array Add test for make rev list Add test for array exists Add test for array find mapi Add test for array of rev list Check observation used in list partition and see if l is defined Check source code to work out if observation is printed before or after normalisation work out why l isn’t defined Test if true candidate is accepted by generated test fun Leave out heaplets that are consumed by the higher order combinator iterate through functions, find the naem At Xapp, seed generator with expressions from pre-heap If gamma contains Option pair then add option_value_snd and option_value_fst to generation context Seed polymorphic functions with arguments to inv Fix end of higher order function to only intros when needed iterate through functions, find the naem Leave out heaplets that are consumed by the higher order combinator Test if true candidate is accepted by generated test fun