-
Notifications
You must be signed in to change notification settings - Fork 16
Symbolically Terminating
Frank edited this page Jul 8, 2020
·
1 revision
Symbolically terminating functions in Cryptol are those whose translation into a form suitable for consumption by reasoning tools completes.
For some functions, particularly those with recursion in terms of the values of arguments, the symbolic simulator can't determine that the function will ever terminate. It attempts to build an infinite expression and so the :prove command hangs.
Add Neil's fac function and Jared's reworked one as examples.