chore: workaround for missing ByteArray literals

LeanSAT/Tactics/BVTrace.lean

@@ -34,16 +34,28 @@ def evalBvTrace : Tactic := fun stx =>
   match stx with
   | `(tactic| bv_decide?%$tk) => do
     let lratFile : System.FilePath ← getLratFileName
-    let cfg ← BVCheck.mkContext lratFile
+    let cfg := { (← BVCheck.mkContext lratFile) with trimProofs := false }
     let g ← getMainGoal
     let trace ← g.withContext do
       g.bvDecide cfg
+    /-
+    Ideally trace.lratCert would be the `ByteArray` version of the proof already and we just write
+    it. This isn't yet possible so instead we do the following:
+    1. Produce the proof in the tactic.
+    2. Skip trimming it in the tactic.
+    3. Run trimming on the LRAT file that was produced by the SAT solver directly, emitting the
+       correct binary format according to `sat.binaryProofs`.
+    TODO: Fix this hack:
+    1. Introduce `ByteArray` literals to the kernel.
+    2. Just return the fully trimmed proof in the format desired by the configuration from `bvDecide`.
+    3. Write it to the file driectly.
+    -/
     match trace.lratCert with
     | none =>
       let normalizeStx ← `(tactic| bv_normalize)
       TryThis.addSuggestion tk normalizeStx (origSpan? := ← getRef)
     | some .. =>
-      if cfg.trimProofs then
+      if sat.trimProofs.get (← getOptions) then
         let lratPath := (← BVCheck.getSrcDir) / lratFile
         LRAT.trimFile lratPath lratPath cfg.binaryProofs
       let bvCheckStx ← `(tactic| bv_check $(quote lratFile.toString))