public-crc-combine.lean

Lean source with line numbers. Follow a line number to locate a statement, or an import to read its dependency.

1import ZlibF.Proof.«crc32.c»
2import ZlibF.Spec.Public.Checksums
3
4/-! Complete numeric results for the public CRC combination entries. -/
5
6namespace Zlib.Crc32.Proofs
7open C Zlib.Crc32
8
9/-- `uLong crc32_combine_gen64(z_off64_t len2)` returns zero for a negative
10length; otherwise it returns the independent bitwise polynomial operator. -/
11theorem crc32_combine_gen64_public (h : Heap) (hs : StaticsOK h) (len2 : Int64) :
12    C.run (crc32_combine_gen64 len2) h = .ok
13      ((if len2.toInt < 0 then 0 else
14        ((List.range (8 * len2.toInt.toNat)).foldl
15          (fun c _ => ZlibF.Spec.crcBit c) (0x80000000 : UInt32)).toUInt64), h) := by
16  by_cases hn : len2.toInt < 0
17  · simpa [hn, C.run, OkOn] using gen64_neg h len2 hn
18  · simpa [hn] using crc32_combine_gen64_correct h hs len2 (by omega)
19
20/-- `uLong crc32_combine_gen(z_off_t len2)` has the same LP64 result. -/
21theorem crc32_combine_gen_public (h : Heap) (hs : StaticsOK h) (len2 : Int64) :
22    C.run (crc32_combine_gen len2) h = .ok
23      ((if len2.toInt < 0 then 0 else
24        ((List.range (8 * len2.toInt.toNat)).foldl
25          (fun c _ => ZlibF.Spec.crcBit c) (0x80000000 : UInt32)).toUInt64), h) :=
26  by
27    by_cases hz : len2 = 0
28    · subst len2
29      rfl
30    · exact crc32_combine_gen64_public h hs len2
31
32/-- `uLong crc32_combine64(uLong crc1, uLong crc2, z_off64_t len2)` is total
33for all checksum arguments and signed lengths, preserving the heap. -/
34theorem crc32_combine64_public (h : Heap) (hs : StaticsOK h)
35    (first second : UInt64) (len2 : Int64) :
36    C.run (crc32_combine64 first second len2) h = .ok
37      ((if len2.toInt < 0 then 0 else
38        (((List.range (8 * len2.toInt.toNat)).foldl
39          (fun c _ => ZlibF.Spec.crcBit c) first.toUInt32) ^^^ second.toUInt32).toUInt64), h) := by
40  have hr := combine64_ok h hs first second len2
41  simpa only [C.run, OkOn, pw_foldl] using hr
42
43/-- `uLong crc32_combine(uLong crc1, uLong crc2, z_off_t len2)` has the same LP64 result. -/
44theorem crc32_combine_public (h : Heap) (hs : StaticsOK h)
45    (first second : UInt64) (len2 : Int64) :
46    C.run (crc32_combine first second len2) h = .ok
47      ((if len2.toInt < 0 then 0 else
48        (((List.range (8 * len2.toInt.toNat)).foldl
49          (fun c _ => ZlibF.Spec.crcBit c) first.toUInt32) ^^^ second.toUInt32).toUInt64), h) :=
50  crc32_combine64_public h hs first second len2
51
52/-- `uLong crc32_combine_op(uLong crc1, uLong crc2, uLong op)` returns the
53independent polynomial result when the operator is generated from any signed length. -/
54theorem crc32_combine_op_public (h : Heap) (hs : StaticsOK h)
55    (first second : UInt64) (len2 : Int64) :
56    C.run (crc32_combine_op first second
57      (if len2.toInt < 0 then 0 else
58        ((List.range (8 * len2.toInt.toNat)).foldl
59          (fun c _ => ZlibF.Spec.crcBit c) (0x80000000 : UInt32)).toUInt64)) h = .ok
60      ((if len2.toInt < 0 then 0 else
61        (((List.range (8 * len2.toInt.toNat)).foldl
62          (fun c _ => ZlibF.Spec.crcBit c) first.toUInt32) ^^^ second.toUInt32).toUInt64), h) := by
63  have hg := crc32_combine_gen64_public h hs len2
64  have hc := crc32_combine64_public h hs first second len2
65  unfold C.run at hg hc ⊢
66  unfold crc32_combine64 at hc
67  simp only [bind_app, hg] at hc
68  exact hc
69
70end Zlib.Crc32.Proofs
71
72namespace ZlibF.Spec.Public.CrcCombineProof
73
74/-- `uLong crc32_combine_gen(z_off_t len2)`; complete operator-generation contract.
75The exact public contract, including rejected negative lengths and the unchanged heap. -/
76theorem gen : Goal.crc32_combine_gen := by
77  intro h length hg
78  exact Zlib.Crc32.Proofs.crc32_combine_gen_public h hg length
79
80/-- `uLong crc32_combine_gen64(z_off64_t len2)`; complete operator-generation contract.
81The exact public contract, including rejected negative lengths and the unchanged heap. -/
82theorem gen64 : Goal.crc32_combine_gen64 := by
83  intro h length hg
84  exact Zlib.Crc32.Proofs.crc32_combine_gen64_public h hg length
85
86/-- `uLong crc32_combine_op(uLong crc1, uLong crc2, uLong op)`
87The exact operator result, including the zero-operator sentinel and the unchanged heap. -/
88theorem op : Goal.crc32_combine_op := by
89  intro h first second length hg
90  exact Zlib.Crc32.Proofs.crc32_combine_op_public h hg first second length
91
92/-- `uLong crc32_combine(uLong crc1, uLong crc2, z_off_t len2)`; full combine contract.
93The exact public contract, including rejected negative lengths and the unchanged heap. -/
94theorem combine : Goal.crc32_combine := by
95  intro h first second length hg
96  exact Zlib.Crc32.Proofs.crc32_combine_public h hg first second length
97
98/-- `uLong crc32_combine64(uLong crc1, uLong crc2, z_off64_t len2)`; full combine contract.
99The exact public contract, including rejected negative lengths and the unchanged heap. -/
100theorem combine64 : Goal.crc32_combine64 := by
101  intro h first second length hg
102  exact Zlib.Crc32.Proofs.crc32_combine64_public h hg first second length
103
104#print axioms gen
105#print axioms gen64
106#print axioms op
107#print axioms combine
108#print axioms combine64
109end ZlibF.Spec.Public.CrcCombineProof