easyuc / EasyUC

Experiments with Universal Composability in EasyCrypt
30 stars 1 forks source link

assertion syntax & error messages #27

Closed alleystoughton closed 11 months ago

alleystoughton commented 11 months ago

I think the expression of error messages could be improved. E.g.,

assert of EffectMsgOut failed. The Env has control
              , asserted control was Adv
;

This could be made more grammatical, without the weird line break. Also, our commands don't generally use CamelCase, and yet we are writing

assert MsgOut
((func, 1))@SMC2.SMC2Dir.Pt1.smc_rsp(text)@(([], 1))
CtrlEnv.
alleystoughton commented 11 months ago

And the debugging output of formula deconstruction should be cleaned up, eventually.


trying to deconstruct formula:

epdp_port_port_key_univ.`dec (epdp_port_port_key_univ.`enc
((func ++ [1], 1), (func ++ [1], 2), g ^ rand))

deconstruction by simplification failed.

         Trying to simplify by evaluating get_as_Constr

deconstruction failed
alleystoughton commented 11 months ago

Fixed the CamelCase issue, but not the error message formatting.