leanexe/Library/Random/Lcg/Verified.lean at main · jsmorph/leanexe · GitHub

1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
import Verified.Reflect.Command
import Library.Random.Lcg.Jump

/-! The thirty-second program of the verified compiler: the linear congruential generator of
`Library/Random/Lcg/Program.lean`, compiled unchanged.  None of its functions allocates, so the compiler's
theorem states that the module computes each of them without a trap.  `lcg_advance` adds the
theorem of `Library/Random/Lcg/Period.lean` that from every word each word occurs at exactly one count,
and `lcg_jump` the theorem of `Library/Random/Lcg/Jump.lean` that `jump` computes `advance`. -/

namespace Library.Random.Lcg

open _root_.Library.Random.Lcg

verified_compile compiled := [affine, step, advance, jumpPass, jump]

/-- The module's bytes decode to the module, whose function 4 computes `advance` without a trap,
and for all words `x` and `y` exactly one count `n` gives `advance n x = y`. -/
theorem lcg_advance : ∃ bytes, Wasm.Encoding.encode compiled.module = .ok bytes ∧
    Wasm.Encoding.decode bytes = .ok compiled.module ∧
    LeanExe.Pipeline.ImplementsA false compiled.module 4
      (fun x : UInt64 × UInt64 => advance x.1 x.2) (fun _ _ _ => True) (fun _ _ _ _ _ => True) ∧
    ∀ x y : UInt64, ∃! n : UInt64, advance n x = y := by
  obtain ⟨bytes, success, decoded, _⟩ := compiled.bytes
  exact ⟨bytes, success, decoded, compiled.advance.implements, advance_existsUnique⟩

/-- The module's bytes decode to the module, whose function 6, `jump`, computes `advance` without a
trap by one squaring of the affine map per bit of the count. -/
theorem lcg_jump : ∃ bytes, Wasm.Encoding.encode compiled.module = .ok bytes ∧
    Wasm.Encoding.decode bytes = .ok compiled.module ∧
    LeanExe.Pipeline.ImplementsA false compiled.module 6
      (fun x : UInt64 × UInt64 => advance x.1 x.2) (fun _ _ _ => True)
      (fun _ _ _ _ _ => True) := by
  obtain ⟨bytes, success, decoded, _⟩ := compiled.bytes
  have h := compiled.jump.implements
  rw [show (fun x : UInt64 × UInt64 => jump x.1 x.2) = fun x => advance x.1 x.2 from
    funext fun x => jump_eq x.1 x.2] at h
  exact ⟨bytes, success, decoded, h⟩

#print axioms minimalPeriod_affine_iff
#print axioms step_minimalPeriod
#print axioms step_bijective
#print axioms advance_existsUnique
#print axioms advance_ne_self
#print axioms periodic_testBit_iff
#print axioms step_periodic_testBit_iff

end Library.Random.Lcg