Attempted to register the following name twice: cryptol:

[weaversa]

@yav

I have a Cryptol file that uses parameterized modules. When I load it w/ Cryptol 2.13 and 3.0.0 I get no errors with either version. When I load it with SAW 1.0 I get the message "Attempted to register the following name twice: cryptol:" and then the path and name of a function.

Sorry I don't have an example to share atm.

[yav]

Thanks for reporting this. The issue is very likely to do with importName/crytpolURI in Verifier.SAW.Cryptol. Will investigate further.

[eddywestbrook]

@weaversa We have tried a bit and haven't been able to reproduce this bug yet. Is there any way you can point us in the right direction for finding it?

[RyanGlScott]

I believe I've figured out a minimal example. Given this Cryptol file:

// bug.cry
interface submodule A where
  a : [8]

submodule F where
  import interface submodule A as X
  import interface submodule A as Y

  f : [8]
  f = X::a + Y::a

submodule I where
  a : [8]
  a = 1

submodule J where
  a : [8]
  a = 2

submodule M = submodule F { X = submodule I, Y = submodule J }

import submodule M as M

And this SAWScript file:

// bug.saw
import "bug.cry";

Then you can load bug.cry into Cryptol 3.0.0 without issue:

$ ~/Software/cryptol-3.0.0/bin/cryptol -c "M::f" bug.cry 
Loading module Cryptol
Loading module Main
0x03

But loading bug.saw into SAW 1.0 will fail:

$ ~/Software/saw-1.0/bin/saw bug.saw



[19:46:46.064] Loading file "/home/rscott/Documents/Hacking/SAW/bug.saw"
[19:46:46.096] Attempted to register the following name twice: cryptol:/Main/F/a

[qsctr]

This might be related to GaloisInc/cryptol#1556 (or might not be, haven't really looked into it from the SAW side)

[qsctr]

Actually, it appears that the bug is still present when running with the cryptol fix in GaloisInc/cryptol#1559, so my guess is that the bug is in how SAW is handling Cryptol names and not in Cryptol itself.