Currently, prime constraints do not participate with SMT solving during typechecking. Among other things, this means that Cryptol will typecheck something like this:
foo : {n} (prime n, n == 4) => [n]
Even though the context (prime n, n == 4) is unsatisfiable, so one can never actually call foo. The immediate reason that this happens is because prime constraints do not have special treatment in this part of the code that deals with "numeric" constraints:
To start, we would need to add prime to both of these parts of the code. This means that we would need to figure out how prime should work at the SMTLIB level. We may want to treat prime as an uninterpreted function and add assertions about its behavior, similarly to how exponentiation is handled (here).
Currently,
primeconstraints do not participate with SMT solving during typechecking. Among other things, this means that Cryptol will typecheck something like this:Even though the context
(prime n, n == 4)is unsatisfiable, so one can never actually callfoo. The immediate reason that this happens is becauseprimeconstraints do not have special treatment in this part of the code that deals with "numeric" constraints:https://github.com/GaloisInc/cryptol/blob/be32aaae7c0bc6ef6b0e2a93027882ce926ce53c/src/Cryptol/TypeCheck/Solver/SMT.hs#L348-L352
Nor does
primehave a corresponding SMTLIB definition here:https://github.com/GaloisInc/cryptol/blob/be32aaae7c0bc6ef6b0e2a93027882ce926ce53c/src/Cryptol/TypeCheck/Solver/SMT.hs#L363-L393
To start, we would need to add
primeto both of these parts of the code. This means that we would need to figure out howprimeshould work at the SMTLIB level. We may want to treatprimeas an uninterpreted function and add assertions about its behavior, similarly to how exponentiation is handled (here).