(Summary of discussion consensus in Bristol. - I hope this is faithful. @bgregoir @mbbarbosa @bacelar @strub @lyonel2017)
The current extraction generates non-trivial code around array indexing and sub-arrays.
This code is annoying in easycrypt proofs, since there is no easy way to write generic lemmas about it. Further, it is not easy to verify the correctness of the extraction code in the compiler.
A first step for improving this situation is to define new operators in Array and WArray that correspond to the code generated by the extraction, and use these operators in the extraction.
This breaks existing proofs, but this breakage can be managed by:
in the long term: adapt the proofs (should not be too difficult, essentially hint simplify the operators)
in the short term: add a (off-by-default) option to keep current behavior
Further changes we proposed but there was no consensus:
using only WArray (would simplify the extracted code, but might be less convenient for proving code that doesn't do any typecast, and would break proofs)
using variable-length arrays to get rid of theory cloning, with length checks in operators (would break proofs, and is not compatible with a future "circuit" proof technique)
(Summary of discussion consensus in Bristol. - I hope this is faithful. @bgregoir @mbbarbosa @bacelar @strub @lyonel2017)
The current extraction generates non-trivial code around array indexing and sub-arrays.
This code is annoying in easycrypt proofs, since there is no easy way to write generic lemmas about it. Further, it is not easy to verify the correctness of the extraction code in the compiler.
A first step for improving this situation is to define new operators in Array and WArray that correspond to the code generated by the extraction, and use these operators in the extraction.
This breaks existing proofs, but this breakage can be managed by:
hint simplifythe operators)Further changes we proposed but there was no consensus: