Typing error with square brackets

Stream: new members

[Ashley Blacquiere]

The following is not type checking, and it's telling me that the type I have is ?m_1[g ^ m.val * h ^ d.val] ℕ : Type ?. I don't quite understand the syntax in the error: Why is g ^ m.val * h ^ d.val inside square brackets? Is that term being treated as a type class in some way?

import data.zmod.basic
import probability.probability_mass_function.monad

variables (G : Type) [fintype G] [group G] [decidable_eq G]
          (g : G)
          (q : ℕ)

def verify (h : G) (c : G) (d : zmod q) (m : zmod q) : Prop :=
do
  let c' := g^m.val * h^d.val,
  pure (if c' = c then 1 else 0)

[Ruben Van de Velde]

I think it means "a metavariable that depends on the bit between the square brackets"

[Ashley Blacquiere]

Is there some way to coerce the c' term to be an element of G then?

[Alex J. Best]

What are you trying to do really? The code confuses me a bit, I'm not sure if Prop is a monad, so I don't know how the do notation will work, and what are 1 and 0?

[Ashley Blacquiere]

I've forked a Lean project that proves security properties for ElGamal encryption and I'm attempting to extend it to Pedersen and ElGamal commitments as part of an MSc project. The original project was part of an MSc thesis too, and the author used the pmf monad extensively as sort of a proxy for a shallow embedding for his game-based security proofs.

As for what specifically I'm trying to do, the MWE above is a verification function intended to 'accept' or 'reject' (i.e. boolean 1 or 0) a given commit (c : G) given the public parameter (h:G) and the message and opening value (m:zmod q and d:zmod q) . But I could be approaching this completely the wrong way...

[Alex J. Best]

If you're writing a pure function you don't really need the do notaiton, then it sounds like you want something like

import data.zmod.basic
import probability.probability_mass_function.monad

variables (G : Type) [fintype G] [group G] [decidable_eq G]
          (g : G)
          (q : ℕ)

def verify (h : G) (c : G) (d : zmod q) (m : zmod q) : bool :=
  let c' := g^m.val * h^d.val in if c' = c then tt else ff

does that fit with your application?

[Ashley Blacquiere]

It type checks, so that's good. I'll have to think about whether it'll fit with the rest. There are many lines of code that I am trying to conceptually untangle, so the 'right' approach isn't quite clear to me yet. This has been helpful though. Thanks!