Mr Solver support for monadic Cryptol specs#1609

Merged

m-yac merged 16 commits intomasterfrom cryptol-abstract-types

Mar 11, 2022

+327-49

Commits on Mar 9, 2022

added the cryptol_add_prim_type SAW command to set the translation of Cryptol abstract types
Eddy Westbrook
committed
whoops, marked cryptol_add_prim_type as experimental
Eddy Westbrook
committed

Commits on Mar 10, 2022

added cryptol_add_prim; also fixed a bug in translating abstract types, where the translation of the types were not getting applied
Eddy Westbrook
committed
added a macro for monadifying the either eliminator
Eddy Westbrook
committed
changed cryptol monadification to translate any global of semi-pure type to itself
Eddy Westbrook
committed
added a case to computation normalization in Mr Solver to handle beta redexes
Eddy Westbrook
committed
changed mrApplyAll to use the new scApplyAllBeta combinator rather than beta normalizing the entire output term
Eddy Westbrook
committed
trying to prove is_elem refines a cryptol spec for its behavior
Eddy Westbrook
committed
reimplemented assertFiniteM to use the maybe eliminator
Eddy Westbrook
committed
added support to Mr Solver for maybe eliminators over isFinite proofs
Eddy Westbrook
committed
added support for CompM types during normalization with normSMTProp
Eddy Westbrook
committed
changed the handling for normalizing multiFixM so that the function being called is not unfolded during normalization; also added a special case for normalizing multiArgFixM
Eddy Westbrook
committed
renamed normSMTProp to mrNormTerm, and added a mrNormOpenTerm function that can normalize open terms
Eddy Westbrook
committed
updated the linked_list_mr_solver.saw test case to prove that is_elem refines a cryptol version of its specification
Eddy Westbrook
committed

Commits on Mar 11, 2022

whoops, fixed some typos
Eddy Westbrook
committed
Merge branch 'master' into cryptol-abstract-types
Eddy Westbrook
authored