lean-zip/ZipTest/NativeCompressBench.lean at master · kim-em/lean-zip · 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
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
import ZipTest.Helpers
import ZipTest.BenchHelpers
import Zip.Native.Inflate
import Zip.Native.Gzip

/-! Compression throughput and ratio benchmarks: native Lean compressor vs FFI (zlib).
    Covers raw deflate, gzip, and zlib formats at levels 0, 1, and 6
    across sizes from 1KB to 256KB. Includes all-level (0–9) compression
    ratio comparison at 64KB and MB/s throughput metrics. -/

namespace ZipTest.NativeCompressBench

def tests : IO Unit := do
  IO.println "  NativeCompressBench tests..."
  let pats := #[("constant", mkConstantData), ("cyclic", mkCyclicData), ("prng", mkPrngData),
                 ("text", mkTextData)]
  let sizes := #[1024, 4096, 16384, 32768, 65536, 131072, 262144]
  let allLevels : Array UInt8 := #[0, 1, 6]

  -- Raw deflate
  IO.println "    --- raw deflate compression (native vs FFI) ---"
  for size in sizes do
    for (pname, pgen) in pats do
      let data := pgen size
      for level in allLevels do
        let s1 ← IO.monoNanosNow
        let nc ← forceEval (Zip.Native.Deflate.deflateRaw data level)
        let e1 ← IO.monoNanosNow
        let s2 ← IO.monoNanosNow
        let _fc ← RawDeflate.compress data level
        let e2 ← IO.monoNanosNow
        match Zip.Native.Inflate.inflate nc with
        | .ok r => unless r == data do
            throw (IO.userError s!"deflate roundtrip: {sizeName size} {pname} lvl={level}")
        | .error e => throw (IO.userError e)
        let nElapsed := e1 - s1
        let fElapsed := e2 - s2
        IO.println s!"      {pad (sizeName size) 6} {pad pname 9} lvl={level}  native={pad (fmtMs nElapsed ++ "ms") 10} ({fmtMBps size nElapsed} MB/s)  ffi={pad (fmtMs fElapsed ++ "ms") 10} ({fmtMBps size fElapsed} MB/s)"

  -- Gzip
  IO.println "    --- gzip compression (native vs FFI) ---"
  for size in sizes do
    for (pname, pgen) in pats do
      let data := pgen size
      for level in allLevels do
        let s1 ← IO.monoNanosNow
        let nc ← forceEval (Zip.Native.GzipEncode.compress data level)
        let e1 ← IO.monoNanosNow
        let s2 ← IO.monoNanosNow
        let _fc ← Gzip.compress data level
        let e2 ← IO.monoNanosNow
        match Zip.Native.GzipDecode.decompress nc with
        | .ok r => unless r == data do
            throw (IO.userError s!"gzip roundtrip: {sizeName size} {pname} lvl={level}")
        | .error e => throw (IO.userError e)
        let nElapsed := e1 - s1
        let fElapsed := e2 - s2
        IO.println s!"      {pad (sizeName size) 6} {pad pname 9} lvl={level}  native={pad (fmtMs nElapsed ++ "ms") 10} ({fmtMBps size nElapsed} MB/s)  ffi={pad (fmtMs fElapsed ++ "ms") 10} ({fmtMBps size fElapsed} MB/s)"

  -- Zlib
  IO.println "    --- zlib compression (native vs FFI) ---"
  for size in sizes do
    for (pname, pgen) in pats do
      let data := pgen size
      for level in allLevels do
        let s1 ← IO.monoNanosNow
        let nc ← forceEval (Zip.Native.ZlibEncode.compress data level)
        let e1 ← IO.monoNanosNow
        let s2 ← IO.monoNanosNow
        let _fc ← Zlib.compress data level
        let e2 ← IO.monoNanosNow
        match Zip.Native.ZlibDecode.decompress nc with
        | .ok r => unless r == data do
            throw (IO.userError s!"zlib roundtrip: {sizeName size} {pname} lvl={level}")
        | .error e => throw (IO.userError e)
        let nElapsed := e1 - s1
        let fElapsed := e2 - s2
        IO.println s!"      {pad (sizeName size) 6} {pad pname 9} lvl={level}  native={pad (fmtMs nElapsed ++ "ms") 10} ({fmtMBps size nElapsed} MB/s)  ffi={pad (fmtMs fElapsed ++ "ms") 10} ({fmtMBps size fElapsed} MB/s)"

  -- Compression ratio
  IO.println "    --- compression ratio (native/FFI) ---"
  IO.println s!"      {pad "Size" 6} {pad "Format" 8} {pad "Pattern" 9} {pad "Level" 6} {pad "Native" 10} {pad "FFI" 10} Ratio"
  for ratioSize in sizes do
   for (pname, pgen) in pats do
    let data := pgen ratioSize
    for level in allLevels do
      let ncR ← forceEval (Zip.Native.Deflate.deflateRaw data level)
      let fcR ← RawDeflate.compress data level
      let rR := if fcR.size == 0 then 0.0 else ncR.size.toFloat / fcR.size.toFloat
      let sR := let s := s!"{rR}"; if s.length > 6 then s.take 6 else s
      IO.println s!"      {pad (sizeName ratioSize) 6} {pad "raw" 8} {pad pname 9} {pad s!"lvl={level}" 6} {pad (toString ncR.size) 10} {pad (toString fcR.size) 10} {sR}"
      let ncG ← forceEval (Zip.Native.GzipEncode.compress data level)
      let fcG ← Gzip.compress data level
      let rG := if fcG.size == 0 then 0.0 else ncG.size.toFloat / fcG.size.toFloat
      let sG := let s := s!"{rG}"; if s.length > 6 then s.take 6 else s
      IO.println s!"      {pad (sizeName ratioSize) 6} {pad "gzip" 8} {pad pname 9} {pad s!"lvl={level}" 6} {pad (toString ncG.size) 10} {pad (toString fcG.size) 10} {sG}"
      let ncZ ← forceEval (Zip.Native.ZlibEncode.compress data level)
      let fcZ ← Zlib.compress data level
      let rZ := if fcZ.size == 0 then 0.0 else ncZ.size.toFloat / fcZ.size.toFloat
      let sZ := let s := s!"{rZ}"; if s.length > 6 then s.take 6 else s
      IO.println s!"      {pad (sizeName ratioSize) 6} {pad "zlib" 8} {pad pname 9} {pad s!"lvl={level}" 6} {pad (toString ncZ.size) 10} {pad (toString fcZ.size) 10} {sZ}"

  -- All-level compression ratio at 64KB (raw deflate only)
  IO.println "    --- all-level compression ratio at 64KB (raw deflate, native vs FFI) ---"
  IO.println s!"      {pad "Pattern" 9} {pad "Level" 6} {pad "Native" 10} {pad "FFI" 10} Ratio"
  let ratioFixedSize := 65536
  for (pname, pgen) in pats do
    let data := pgen ratioFixedSize
    for level in #[(0 : UInt8), 1, 2, 3, 4, 5, 6, 7, 8, 9] do
      let nc ← forceEval (Zip.Native.Deflate.deflateRaw data level)
      let fc ← RawDeflate.compress data level
      let r := if fc.size == 0 then 0.0 else nc.size.toFloat / fc.size.toFloat
      let sr := let s := s!"{r}"; if s.length > 6 then s.take 6 else s
      IO.println s!"      {pad pname 9} {pad s!"lvl={level}" 6} {pad (toString nc.size) 10} {pad (toString fc.size) 10} {sr}"

  -- Decompression benchmarks: compress with FFI, then time native vs FFI decompress
  IO.println "    --- raw deflate decompression (native vs FFI) ---"
  for size in sizes do
    for (pname, pgen) in pats do
      let data := pgen size
      for level in allLevels do
        let compressed ← RawDeflate.compress data level
        let s1 ← IO.monoNanosNow
        let nd ← forceEval (match Zip.Native.Inflate.inflate compressed with
          | .ok r => r | .error _ => ByteArray.empty)
        let e1 ← IO.monoNanosNow
        let s2 ← IO.monoNanosNow
        let fd ← RawDeflate.decompress compressed
        let e2 ← IO.monoNanosNow
        unless nd == data do
          throw (IO.userError s!"inflate raw roundtrip: {sizeName size} {pname} lvl={level}")
        unless fd == data do
          throw (IO.userError s!"ffi raw decomp roundtrip: {sizeName size} {pname} lvl={level}")
        let nElapsed := e1 - s1
        let fElapsed := e2 - s2
        IO.println s!"      {pad (sizeName size) 6} {pad pname 9} lvl={level}  native={pad (fmtMs nElapsed ++ "ms") 10} ({fmtMBps size nElapsed} MB/s)  ffi={pad (fmtMs fElapsed ++ "ms") 10} ({fmtMBps size fElapsed} MB/s)"

  IO.println "    --- gzip decompression (native vs FFI) ---"
  for size in sizes do
    for (pname, pgen) in pats do
      let data := pgen size
      for level in allLevels do
        let compressed ← Gzip.compress data level
        let s1 ← IO.monoNanosNow
        let nd ← forceEval (match Zip.Native.GzipDecode.decompress compressed with
          | .ok r => r | .error _ => ByteArray.empty)
        let e1 ← IO.monoNanosNow
        let s2 ← IO.monoNanosNow
        let fd ← Gzip.decompress compressed
        let e2 ← IO.monoNanosNow
        unless nd == data do
          throw (IO.userError s!"inflate gzip roundtrip: {sizeName size} {pname} lvl={level}")
        unless fd == data do
          throw (IO.userError s!"ffi gzip decomp roundtrip: {sizeName size} {pname} lvl={level}")
        let nElapsed := e1 - s1
        let fElapsed := e2 - s2
        IO.println s!"      {pad (sizeName size) 6} {pad pname 9} lvl={level}  native={pad (fmtMs nElapsed ++ "ms") 10} ({fmtMBps size nElapsed} MB/s)  ffi={pad (fmtMs fElapsed ++ "ms") 10} ({fmtMBps size fElapsed} MB/s)"

  IO.println "    --- zlib decompression (native vs FFI) ---"
  for size in sizes do
    for (pname, pgen) in pats do
      let data := pgen size
      for level in allLevels do
        let compressed ← Zlib.compress data level
        let s1 ← IO.monoNanosNow
        let nd ← forceEval (match Zip.Native.ZlibDecode.decompress compressed with
          | .ok r => r | .error _ => ByteArray.empty)
        let e1 ← IO.monoNanosNow
        let s2 ← IO.monoNanosNow
        let fd ← Zlib.decompress compressed
        let e2 ← IO.monoNanosNow
        unless nd == data do
          throw (IO.userError s!"inflate zlib roundtrip: {sizeName size} {pname} lvl={level}")
        unless fd == data do
          throw (IO.userError s!"ffi zlib decomp roundtrip: {sizeName size} {pname} lvl={level}")
        let nElapsed := e1 - s1
        let fElapsed := e2 - s2
        IO.println s!"      {pad (sizeName size) 6} {pad pname 9} lvl={level}  native={pad (fmtMs nElapsed ++ "ms") 10} ({fmtMBps size nElapsed} MB/s)  ffi={pad (fmtMs fElapsed ++ "ms") 10} ({fmtMBps size fElapsed} MB/s)"

  IO.println "  NativeCompressBench tests passed."

end ZipTest.NativeCompressBench