eyeprolog

Reproducible UUIDs

Can a random identifier be reproducible?

A version 4 UUID is a 128-bit identifier made mostly of random bits. This example generates one from an explicit random seed, so the same seed always gives the same UUID, and then checks that the result has the shape the UUID standard requires.

Run it in the playground · Source

The question

Does uuid/3, seeded with 20260807, produce a well-formed version 4 UUID?

A UUID is written as 36 characters: 32 hexadecimal digits in groups of 8, 4, 4, 4, and 12, separated by hyphens. In version 4, the first digit of the third group is 4, and the first digit of the fourth group is 8, 9, a, or b.

The program

uuid_example(true) :-
  uuid(20260807, UUID, _),
  atom(UUID),
  atom_length(UUID, 36),
  sub_atom(UUID, 8, 1, 27, '-'),
  sub_atom(UUID, 13, 1, 22, '-'),
  sub_atom(UUID, 14, 1, 21, '4'),
  sub_atom(UUID, 18, 1, 17, '-'),
  sub_atom(UUID, 19, 1, 16, Variant),
  member(Variant, ['8', '9', a, b]),
  sub_atom(UUID, 23, 1, 12, '-').

uuid/3 takes a seed and returns a UUID and the next seed, so randomness is threaded explicitly instead of hidden in global state. sub_atom/5 checks one character at a time: the hyphens, the version digit, and the variant digit.

The answer

eyeprolog examples/uuid.pl

uuid_example(true).

Every structural check passed.

The reason

step(uuid(20260807, '08b72882-8bb9-484f-addc-f8c1a3867f4d', 1745479741), builtin, [], []).
step(sub_atom('08b72882-8bb9-484f-addc-f8c1a3867f4d', 14, 1, 21, '4'), builtin, [], []).

The proof shows the actual UUID, 08b72882-8bb9-484f-addc-f8c1a3867f4d, and the next seed, 1745479741. Position 14 holds the version digit 4, and position 19 holds the variant digit a.

The check

condition('C1', resolution, ok, 1).
condition('C5', re_decision, ok, 10).
recomputed(10).
verdict(checked).

The checker recomputes all 10 built-in steps, including uuid/3 itself. Because the generator is seeded, it gets the same UUID again, so even the “random” step is checked.

Try it

Pass the returned seed 1745479741 into a second uuid/3 call and check that the second UUID differs from the first.
Change the seed and confirm that the shape checks still pass.
Write a relation that generates five UUIDs from one seed and checks that they are all distinct.

Learn more in The Art of EyeProlog, Chapter 35.

This site is open source. Improve this page.