Rolling Dice 1a - Peaceful Shores

(Or, Theorem Proving 101 - First Week)

In this series, we’re going to explore dice expressions in tabletop games, what they mean, how to roll them, and hopefully get a grip on evaluating them in a secure context.

Setting Expectations

Today, we’re going to lay out our goals, the tools we’re going to use to reach our goals, and maybe get a taste of what lies ahead.

First, the meat of our code this time around is going to be written in Idris 2. This will likely prove to be a hindrance in many respects- I won’t lie, I have tried and failed to write non-trivial things in Idris 2 multiple times before. It won’t be easy but, if we play our cards right, what we end up with might turn out to be more robust than if we had done it any other way.

Second, this is going to involve references to many traditionally tabletop role-playing games, including D&D, Shadowrun, Masks - The New Generation, and Fate. If that’s not your cup of tea, I do urge you to try and bear with us. Maybe you’ll discover an interest you’d assumed wasn’t there, but this should turn out useful even for those who won’t be making a dice rolling Discord bot any time soon.

Third, we’re going to be writing our code with the mindset of a backend developer for a service whose users aren’t vetted in any particular way, who wants to make mathematically certain that those users cannot cause the service to do anything unintended or interfere with its use by other users. We may to need to refine our intentions a bit further later on, but this should be good enough for now.

Laying The Groundwork

Installing Idris 2

I’m going to be expanding this section according to feedback I get- if you have trouble installing Idris 2, please let me know. I’ll try and help, and extract what I can from your struggles to put here and perhaps help others in the future.

For now, though, I’ll just tell you to go to the download page, and install what it tells you to: https://www.idris-lang.org/pages/download.html

You want the things in the Idris 2 section. I recommend you clone the source repository, https://github.com/idris-lang/Idris2, as the release tarball, 0.6.0 as of this writing, is from a year ago and missing a fix for a bug in the totality checker I tripped over while learning enough about Idris 2 to write this series.

After that, there’s an INSTALL.md file in the Idris 2 repository. This is your in-depth guide to installing Idris 2, and it will almost definitely be more helpful installing whatever version of the language toolchain you got than this blog could be. This is because it is maintained together with the toolchain, and so has the lowest risk of becoming out of sync.

Getting Some Rule Books

While you won’t need the rule books for the games we’ll be covering, you might consider purchasing some of them if you find an interest in playing.

Below are product pages for each game we’ll cover. If I add a new one later in the series, I will come back here and add it to the list.

• Dungeons & Dragons
• Shadowrun
• Masks - The New Generation
• Fate

Making Our Project Directory

To really start on our project, we’ll want to create a directory on our filesystem in which to save everything for it.

So we open our shell, navigate somewhere nice, create a directory (I’m calling it theorem_proving), and then run this command: idris2 --init.

Package name: 

Aw jeez. We have to think of a package name? Let’s just call it demo.

It asks a few more questions, which I’ve answered as follows:

Package name: demo 
Package authors: Monadic Cat
Package options: 
Source directory: src

Now we have a file named demo.ipkg. Its contents don’t matter quite yet. Let’s create our source code first.

mkdir src

Then, let’s create a file inside src, named Main.idr. We’ll write this inside it:

module Main

main : IO ()
main = putStrLn "Hello, world."

Next, let’s edit demo.ipkg. Below is a list of commented lines, -- <something> =, which you will find in the file, and lines with which to replace those commented lines.

-- modules =
modules = Main

-- main =
main = Main

-- executable =
executable = demo

Unlike in Rust, where the main.rs or lib.rs file is implicitly the root of a crate, you must specify which file to start with in an Idris 2 package description. Similarly, the name of a compiled executable must be specified.

Anyway, to verify that we now have a working project directory, we run:

idris2 --build demo.ipkg
./build/exec/demo

Which outputs:

Hello, world.

Cool.

Gathering Test Cases

Now, let’s list out some commonly used dice expressions for each of the above games:

In D&D, d20 + <modifier> is frequently used for skill checks. Damage rolls can use any combination of the standard set of dice, which includes four, six, eight, and twelve sided dice, as well as the aforementioned twenty sided die. For example, 3d4 + 3 is the damage you’d roll when targeting a single creature with all of the darts from a first level cast of Magic Missile.

In Shadowrun, you use a lot of six sided dice. So many that it’s common to purchase boxes of a bazillion smaller-than-usual d6s to make it easier to roll tons of them at once. Hopefully Chessex, whom I bought this box off of at GenCon in 2019, won’t mind me sharing this photo:

Inflation is a thing, it’s been several years since then, and that “Off-Color” labeling has me suspecting I got these on sale, so I don’t expect you’ll be able to find this exact price for this product, but you see what I mean. Lots of dice. And, in Shadowrun, this frequently involves what some people call “exploding dice” and others call “bouncing dice”. In particular, you roll a collection of six sided dice, then roll an extra die for each one that came up six, repeating until no more sixes come up. We will be writing this operation like this: 10d6!.

In Masks, almost every dice roll is that of two six sided dice, plus some modifier depending on a character’s stats and various bonuses and penalties that can come into effect throughout play. This looks like 2d6 + 3.

In Fate, you do things completely different. There are special dice, called “Fudge dice”, which are six sided, but which are labeled with plus and minus signs instead of numbers. In effect, a “Fudge die” simulates having a three sided die, with sides negative 1, blank for zero, and positive 1. The common notation for this is dF, and the most common roll is 4dF. If I owned any of these myself, I’d show you a photo, but I don’t. Have a link to Wikipedia instead.

Getting Some Players

Now, our desire to evaluate dice expressions presupposes the idea that we have people who want us to do that. In my case, I maintain a Discord bot which rolls dice expressions for people who play TTRPGs online. Your mileage may vary, but I recommend finding a gaming group to use as a source of real-world usage scenarios, if you go down the path of making such a thing yourself.

There is an unlimited amount of complexity here, just as unlimited as the number of possible game systems people can make. It is helpful to keep your work grounded in reality, where you know that a feature you’re adding actually has players who would benefit from having it for a particular game.

It’s also nice to have real players around to inform you when you’ve missed a real use case with an implicit assumption you had about how a feature would be used.

Your First Proof

With all that said, the meat of this series is going to be about writing code which is automatically verified to finish executing (it is “total”), ideally with as many other useful properties as possible automatically checked as well.

To get a taste of how that’s going to play out, let’s write a total program which counts from 0 to a user input natural number:

module Main
import Data.String
%default total


main : IO ()
main = do
  putStr "Enter a positive whole number: "
  line <- getLine
  let top = parsePositive line
  case top of
    Just n => countUp 0 n
    Nothing => putStrLn "Entered invalid number."
  where
    countUp : Nat -> Nat -> IO ()
    countUp _ 0 = pure ()
    countUp i (S n) = do
      putStrLn (show i)
      countUp (S i) n

Try running this! (Copy it into the src/Main.idr file from earlier, then run that.)

Now, it probably looks a little weird to you, but this is structured to make the termination property of the program obvious to the compiler. We do this by having one parameter, n, which always decreases toward a base case. We’ll get into the specifics next time, but the fact that it compiles and runs successfully with %default total at the top indicates that the compiler can indeed see that this program always finishes.

Don’t worry about the syntax of Idris 2, we’ll cover it later. It probably looks decently familiar to people who’ve used Haskell, but you won’t need that prior experience to learn from this series.

Next Time

Next time, we’re going to dive into the syntax of Idris 2 with a bunch of examples. It might take us a while to get back to rolling dice, but we will get there.

If you want to get a head start on learning about Idris 2 before we continue, the Crash Course in Idris 2 book is an essentially canonical learning resource. It isn’t complete, but it’s still useful. You might also consider joining the Idris Discord Server, or one of the other communities listed on the Idris website.

Till then!

Addendum: Hardware Vulnerabilities

There are limits to how much of an assurance you can get with respect to software operation, due to unavoidable realities of how the computer hardware we have available works. Hardware vulnerabilities like Meltdown, Spectre, etc., are things which can often be mitigated as they are discovered, both by hardware improvements and low level compiler workarounds, but we may not get to that in this series.

I’d like to, though. I might research this and include a note about it in a future post’s appendix. We’ll see.

By the way, I was motivated to write this for the Writing Gaggle. You should check that out for more interesting written works. (And the occasional other creative work, for which written planning is a major component.)

You can find more stuff by me at my blog.