Allow users to customize random seed

[ngernest]

The problem

The suite gets its inputs from the random number generator of the operating system.
If a property fails, you cannot get the same inputs a second time. You cannot look at
the failure again. A defect that only 1 input in 300 makes visible has no reliable test.

What this change adds

There are 2 new controls: a flag for the full suite, and an attribute argument for one
property.

--seed=N

Give this flag to test or to test-plain:

lake test -- --seed=7 --only="mypass:"

Each property then makes its inputs from the seed N and from its own name. If you give
the same command 2 times, the suite makes the same inputs. A property that fails shows its
seed in the report:

  × FAIL expr: progress (closed)
-------------------
    seed: 7 — replay with `--seed=7`, or keep this draw with `@[strata_property (seed := 7)]`

The seed also goes to the random number generator of the process. Because of this, the
self-driving IO properties, the diagnostics and the Tyche panels also give the same
output again.

Each property gets N itself. hspec and tasty-quickcheck do the same. Because of
this, 2 properties of 1 input type get the same inputs, and a suite with a seed covers
less than a suite without one. Use the flag to get a failure again, not to gate a merge.

A bad value stops the suite with an error. --seed=abc does not make a suite without a seed
that the header shows as a suite with one.

A seed in the declaration

@[strata_property (seed := 8021)]
def liftFreshSnapshotNames : TestDecl :=
  knownFailure "strata-org/Strata#123: a minted snapshot name can collide" <| …

The property then makes the same inputs each time, and it ignores --seed=.
@[strata_properties (seed := N)] does the same for each member of a list. withSeed N
is the term form.

This is the reason for the feature. A defect on a rare input now fails each time, so
knownFailure can watch it. Before this change, such a property could not have a mark.

The seed in the declaration has a higher precedence than the flag. The seed makes the
failure reliable. If the flag replaced the seed, the property becomes unreliable again.
Its knownFailure mark then fails the suite on each input that does not show the defect.

The cost is clear: a property with a seed in its declaration stops the search for new
defects, because it makes the same inputs each time. Give a seed to 1 property, and remove
the seed with the knownFailure mark that it helps.

Why 1 attribute with an argument

Lean reads @[strata_property, seed = 42] as 2 independent attributes. A seed attribute
is then a global name that other packages cannot use. It also does nothing if
strata_property is not there, which is a silent fault. This change puts the argument in
the attribute, as Lean core does for @[deprecated (since := "…")].

Checks

• 2 tests with --quick --seed=7 on all 147 properties give the same output, byte for
  byte. The Tyche JSONL file is also the same, except for its clock field.
• Both drivers give the same result with a seed.
• A property with a seed in its declaration gave the same counterexample with no --seed=
  flag. The seed came from the report of an earlier --seed=7 test.
• Without a seed, 2 tests give different results. This was true before this change.
• The set of failures is the same as the set from the driver of the base branch.
• Tyche panels ignore a seed in a declaration. 1000 samples of 1 input are not a
  distribution.

Notes for the reviewer

• This branch has 2 commits on top of main. The second commit removes a seed mixer from
  the first one. The suite gave each property a mix of N and the name of the property.
  1 seed for each property is enough for basic use, and the report then shows the number
  that the reader gave.
• There is no new property in the suite. The repo has no self-test for the harness.
• docs/writing-properties.md has the new section Reproducing a draw, with the
  precedence rules and the costs.