:prove not propagating constants

[weaversa]

https://github.com/weaversa/CryptolSpecifications/tree/master/ECDSA

$ cryptol ECDSA_tests.cry 
┏━╸┏━┓╻ ╻┏━┓╺┳╸┏━┓╻  
┃  ┣┳┛┗┳┛┣━┛ ┃ ┃ ┃┃  
┗━╸╹┗╸ ╹ ╹   ╹ ┗━┛┗━╸
version 2.6.1 (5156423)

Loading module Cryptol
Loading module utils
Loading module ECDSA
Loading module p192
Loading module p224
Loading module p256
Loading module p384
Loading module p521
:Loading module ECDSA_tests
ECDSA_tests> :prove
:prove p192_G_compress
	Q.E.D.
(Total Elapsed Time: 0.006s, using Z3)
:prove p192_full_add_example
	Q.E.D.
(Total Elapsed Time: 0.006s, using Z3)
:prove p192_full_subtract_example
	Q.E.D.
(Total Elapsed Time: 0.007s, using Z3)
:prove p192_double_example
	Q.E.D.
(Total Elapsed Time: 0.008s, using Z3)
:prove p192_scalar_multiply_example
^C	Ctrl-C

p192_scalar_multiply_example has no symbolic inputs. :check quickly succeeds on the property. :prove hangs when trying to prove the property. I figure this means there is a bug in symbolic execution of the new Z type...I have not done any diagnosis.

[brianhuffman]

With :set debug=yes, please this gets stuck at Simulating..., so something is going wrong before it gets to the solver. I'll try it with profiling to see what I can find out.

[brianhuffman]

It looks like all the time is spent running svTimes from the SBV library. A potential reason could be that the concrete numbers are just getting too big.

For concrete evaluation on Z n types, we reduce modulo n after every operation. But for symbolic evaluation we represent values of type Z n as symbolic integers, and don't bother reducing them until we do something that requires it, like a comparison. For symbolic values I think this is the right choice, as having lots of extra mod operations in formulas makes life difficult for the solver. But when the values are concrete, we should probably do the reduction more eagerly.

[brianhuffman]

In revision 4db27c0, I made the symbolic-backend implementation of * on type Z n do reduction mod n when the arguments are concrete. This makes :prove p192_scalar_multiply_example finish, but it still takes a lot longer to run than :check (several seconds). I probably need to put mod in some other places too. I can try some more things on Monday.

[weaversa]

Thank you!