Add expModInteger to specification

[bezirg]

Pre-submit checklist:

• Branch
  • Tests are provided (if possible)
  • Commit sequence broadly makes sense
  • Key commits have useful messages
  • Changelog fragments have been written (if appropriate)
  • Relevant tickets are mentioned in commit messages
  • Formatting, PNG optimization, etc. are updated
• PR
  • (For external contributions) Corresponding issue exists and is linked in the description
  • Targeting master unless this is a cherry-pick backport
  • Self-reviewed the diff
  • Useful pull request description
  • Reviewer requested

[zliu41]

Can you remind me how I can build this locally?

[bezirg]

plutus-core-specification.pdf

Can you remind me how I can build this locally?

make under doc/plutus-core-spec

[zliu41]

make under doc/plutus-core-spec

Ok, this seems to require a separate installation of pdflatex, as it's not provided by nix develop.

[zliu41]

This table will need to be reworked or discarded. Since we can now add (new or existing) builtins to existing Plutus versions, the table may no longer make sense. This particular builtin will likely be introduced into V1, V2 and V3 at the same time, at Protocol version 11.0.

[kwxm]

This table will need to be reworked or discarded. Since we can now add (new or existing) builtins to existing Plutus versions, the table may no longer make sense. This particular builtin will likely be introduced into V1, V2 and V3 at the same time, at Protocol version 11.0.

@ZLiu21 There's an issue to fix the explanation of versions here. We should probably do what you mention above as part of that as well.

[kwxm]

@bezirg I'll look at this more closely next week, but note that the PR to add the bitwise operations to the specification is still unmerged and this will probably have to be rebased on it.

[kwxm]

This looks fine, although it could be a bit more precise about what the denotation of the builtin actually is. You should wait for #6426 to be merged first (which I hope will happen soon) since that contains a lot of stuff that goes just before this.

[kwxm]

I was going to suggest making this a bit more precise by making the denotation something like

$ (a,e,m) \mapsto 
  \begin{cases}
     \modfn(a^e,m) & \text{if $m > 0$ and $e \geq 0$}\\
     \min\{r \in \N: ra^{-e} \equiv 1 \pmod{m}\}\  \text{if $m > 0, e < 0$ and $\mathrm{gcd}(a,m) = 1$ }\\
     \errorX & \text{otherwise}
  \end{cases})$ 

but I don't know if that'll fit into the box (and it's pretty much what you say later on). Also, what I wrote has two different things denoted by mod, which might be confusing: the first one's the function defined on pages 32 and 33 and the second one's the usual thing in the congruence relation ≡. Maybe you could add a function like itobs in pages 36-37. The point is that we want to precisely define the denotation as a mathematical function and it should say explicitly what the conditions are that lead to the big X error value, and that's maybe not obvious here unless you already know what's going on.

[kwxm]

It might be helpful to have a reference to the fact that if e<0 then a^e only exists mod m if gcd(a,m)=1 (and include that condition in the definition). Thats' a standard number-theoretic fact which can be found in eg Proposition I.3.1 of

@book{Koblitz,
      author = "Koblitz, Neal"
      title = "{A Course in Number Theory and Cryptography}",
      publisher = "Springer-Verlag",
      series = "Graduate Texts in Mathematics",
      volume = 114,
      edition = 2,
      year = "1994"
}

[kwxm]

I've tidied up a couple of things and merged the updates for the bitwise builtins into this branch. I think we can merge this now.