Not so random

Stream: general

[Yaël Dillies]

If you run this file from the command line

import control.random

open io list nat

def rand_nat' (lo hi : ℕ) : rand ℕ :=
⟨λ seed, (rand_nat seed.down lo hi).map id ulift.up⟩

/-- Runs the program. -/
def main : io unit := do
  l ← mmap (λ _, io.run_rand (rand_nat' 0 10)) (range 10),
  print_ln l

you always get the same result. This looks like Lean gets the same seed from the system over and over again.

[Kyle Miller]

If you don't do docs#io.set_rand_gen, it uses C++'s std::rand, I guess seeded automatically by std::srand(1) (the vm never calls std::srand itself).

You can use docs#mk_std_gen to create seeded random number generators, but then it will use a pseudorandom number generator written in Lean.

It's pretty common for languages to have pseudorandom number generators that are seeded with a constant unless you seed it yourself. (Long ago I remember typing randomize timer in QBasic, to use the current time as a seed.)

[Heather Macbeth]

Kyle Miller said:

(Long ago I remember typing randomize timer in QBasic, to use the current time as a seed.)

Ha, me too!

[Heather Macbeth]

00's kids ...

[Yaël Dillies]

I know about mk_std_gen, and running it from the command line was my attempt to not get the same seed over and over again.

[Yaël Dillies]

Is there really no way to get nondeterminism?

[Kyle Miller]

There's nothing in the vm that calls std::srand, so not using the C++ generator.

[Bhavik Mehta]

Kyle Miller said:

If you don't do docs#io.set_rand_gen, it uses C++'s std::rand, I guess seeded automatically by std::srand(1) (the vm never calls std::srand itself).

You can use docs#mk_std_gen to create seeded random number generators, but then it will use a pseudorandom number generator written in Lean.

It's pretty common for languages to have pseudorandom number generators that are seeded with a constant unless you seed it yourself. (Long ago I remember typing randomize timer in QBasic, to use the current time as a seed.)

Is this true? io.run_rand uses mk_generator which says it seeds a random number generator, and the seed is generated using the instance of monad_io_random

[Bhavik Mehta]

And that instance is implemented in C++, with the rand part of it depending on std::rand()

[Kyle Miller]

io.run_rand does do mk_std_gen for you, using whatever the current random generator is for a seed. If you didn't do io.set_rand_gen, it's the unseeded std::rand.

[Kyle Miller]

At least, this is all how I've understood the code. The key part for the behavior of set_rand_gen is https://github.com/leanprover-community/lean/blob/master/src/library/vm/vm_io.cpp#L904

[Kyle Miller]

(is_simple checks that the object is not a pointer.)

[Bhavik Mehta]

Ah I see, I was also looking at the same bit of code, but I didn't know about the behaviour of std::rand before seeding occurred. I agree with you!

[Kyle Miller]

I guess there's no way to get the current time in Lean?

@Yaël Dillies I don't see a good cross-platform way to seed the random number generator and get nondeterminism. It looks like you can (1) run a program that reports the time and then capture the standard output, (2) docs#io.net.connect to some random host for HTTP and rely on the headers containing a timestamp, so you can hash the response to get a seed(!), (3) have a file containing a seed that Lean reads, and by alternative means you update it each time you run lean, or (4) patch lean to have a function that gives the current time.

[Yaël Dillies]

I was expecting such a timer function to already exist.

[Kyle Miller]

It looks like in Lean 4 you can look forward to io.get_random_bytes, which uses /dev/urandom on Linux and BCryptGenRandom on Windows.

[Bhavik Mehta]

I wonder if we can use io.read to get bytes from /dev/urandom already in Lean 3?

[Kyle Miller]

@Bhavik Mehta Yeah, certainly, it's just not cross-platform

import control.random

open io list nat

def rand_bytes (n : ℕ) : io (buffer ℕ) := do
  h ← mk_file_handle "/dev/urandom" mode.read tt,
  chrs ← io.fs.read h n,
  when (chrs.size < n) $ io.fail "did not read enough bytes of randomness",
  pure $ chrs.map char.val

def rand_seed : io unit := do
  bytes ← rand_bytes 8,
  let seed : ℕ := bytes.foldl 0 (λ a b, a * 256 + b),
  set_rand_gen $ mk_std_gen seed

def rand_nat' (lo hi : ℕ) : rand ℕ :=
⟨λ seed, (rand_nat seed.down lo hi).map id ulift.up⟩

/-- Runs the program. -/
def main : io unit := do
  rand_seed,
  l ← mmap (λ _, io.run_rand (rand_nat' 0 10)) (range 10),
  print_ln l

[Kyle Miller]

@Yaël Dillies Since you mentioned that running from the command line was an attempted workaround, then for one of the many things it might be a workaround for I thought I'd mention that #eval runs IO actions.

#eval set_rand_gen $ mk_std_gen 37

#eval io.rand 0 5 >>= print_ln
#eval io.rand 0 5 >>= print_ln
#eval io.rand 0 5 >>= print_ln

[Yaël Dillies]

Oh, very cool! And it's also much faster than running it from the command line.