How to deal with fromIntMod?

[msaaltink]

I was experimenting again with the use of modular types. Now goal_eval_unint does not crash, so that's an improvement. I get back a term containing things like

x@52 = toIntMod 17 (intMod (fromIntMod 17 (f x)) (natToInt 17))

and now I need some rewrites to eliminate those coercions (so that other rewrites I want to use will match). These functions do not appear in the Cryptol prelude but rather in Prelude.sawcore so I need to refer to them somehow using parse_core. This happens when I try.

sawscript> parse_core "fromIntMod"

You have encountered a bug in cryptol-saw-core's implementation.
*** Please create an issue at https://github.com/GaloisInc/saw-script/issues

%< --------------------------------------------------- 
  Revision:  2e4fc0603da85bb1b188d4739a3386e25eea50ab
  Branch:    master (uncommited files present)
  Location:  scCryptolType
  Message:   scCryptolType: unsupported type (n : Prelude.Nat)
-> Prelude.IntMod n
-> Prelude.Integer
CallStack (from HasCallStack):
  panic, called at src/Verifier/SAW/Cryptol/Panic.hs:13:9 in cryptol-saw-core-0.1-inplace:Verifier.SAW.Cryptol.Panic
  panic, called at src/Verifier/SAW/Cryptol.hs:1615:13 in cryptol-saw-core-0.1-inplace:Verifier.SAW.Cryptol
%< --------------------------------------------------- 

I have previously had a problem like this, that SAWCore terms involving type Nat cannot easily be manipulated.

Is there any way to define rewrites for these functions so that they can be eliminated where they are redundant?

[brianhuffman]

The problem here is not with parsing saw-core terms using fromIntMod, but rather that parse_core can't handle terms with polymorphic types. Things work out fine if you use parse_core or prove_core as long as fromIntMod is applied to a fixed numeric argument:

sawscript> let t = parse_core "fromIntMod 17"
sawscript> t
[17:12:46.888] Prelude.fromIntMod 17
sawscript> type t
[17:12:49.328] Z 17 -> Integer
sawscript> rule <- prove_core z3 "(x : IntMod 17) -> EqTrue (intEq (intMod (fromIntMod 17 x) (natToInt 17)) (fromIntMod 17 x))"
sawscript> rule
[17:13:08.383] Theorem (let { x@1 = Prelude.Nat
      -> sort 0
    }
 in (x : Prelude.IntMod 17)
-> let { x@2 = Prelude.fromIntMod 17 x
    }
 in Prelude.EqTrue
      (Prelude.intEq (Prelude.intMod x@2 (Prelude.natToInt 17)) x@2))

You can also state rewrite rules about fromIntMod in cryptol syntax, as Cryptol's fromZ primitive is defined in terms of fromIntMod.

sawscript> rule2 <- prove_print z3 (rewrite (cryptol_ss()) {{ \(x : Z 17) -> fromZ x % 17 == fromZ x }})
sawscript> rule2
[17:14:54.611] Theorem (let { x@1 = Prelude.Nat
      -> sort 0
    }
 in (x : Prelude.IntMod 17)
-> let { x@2 = Prelude.fromIntMod 17 x
    }
 in Prelude.EqTrue
      (Cryptol.ecEq Prelude.Integer Cryptol.PEqInteger
         (Prelude.intMod x@2 (Prelude.natToInt 17))
         x@2))

[msaaltink]

That's pretty helpful (and hopeful) but I still have a problem:

sawscript> addsimp rule basic_ss;

Stack trace:
"addsimp" (<stdin>:1:1-1:8):
addsimp: theorem not an equation

Should some other equality relation be used?

[brianhuffman]

Ah, that "theorem not an equation" error message is definitely a bug; it's related to #1261. (Basically we have an ad hoc collection of equality relations that are used currently to recognize rewrite rules, and intEq is probably missing.)

EDIT: See #1297 for a fix to this error message.

[sauclovian-g]

It appears to me that with #1297 this is now a duplicate of #1261. Also nowadays:

sawscript> parse_core "fromIntMod"
[22:05:45.683] fromIntMod
sawscript> 

Ok to close?

[RyanGlScott]

Yes, let's close this in favor of #1261.