Importing cryptol file twice results in separate versions of constants

[brianhuffman]

Since the fix for #568, we now add a unique-id to all abstract constants defined with scConstant. However, that has revealed another bug: When we have multiple import statements that import the same cryptol module (possibly via chasing module dependencies) we now get duplicate copies of the constants in the reloaded module. This breaks some of the s2n proof scripts. For example, if we create a file A.cry containing a function foo : [8] -> [8] and import it twice, we get a different foo the second time:

import "A.cry";
let foo1 = {{ foo }};
import "A.cry";
let foo2 = {{ foo }};
prove (offline_unint_smtlib2 ["foo"] "foo") {{ \x -> foo1 x == foo2 x }};

The generated foo.prove0.smt2 now contains:

; --- uninterpreted constants ---
(declare-fun |foo#145| ((_ BitVec 8)) (_ BitVec 8))
(declare-fun |foo#96| ((_ BitVec 8)) (_ BitVec 8))
; --- user given axioms ---
; --- formula ---
(assert (forall ((s0 (_ BitVec 8)))
            (let ((s1 (|foo#96| s0)))
            (let ((s2 (|foo#145| s0)))
            (let ((s3 (= s1 s2)))
            (not s3))))))
(check-sat)

The goal is not provable by reflexivity as it should be. The same thing happens if instead of importing A.cry a second time, we import another module that transitively imports A.cry.

To fix the problem, we need to avoid re-translating previously-loaded cryptol modules to saw-core when we import a new one. References to functions in previously-loaded modules should use the saw-core constants that were defined when the earlier module was loaded.

[brianhuffman]

There's already a TODO in the source code for this issue: https://github.com/GaloisInc/cryptol-verifier/blob/2c74471f3ee2bfce86af0d6164fdd600032b354d/src/Verifier/SAW/CryptolEnv.hs#L364