Building OptimalOTS.Challenge.UpperCompressions
⚠ [2689/2689] Built OptimalOTS.Challenge.UpperCompressions (1.9s)
warning: OptimalOTS/Challenge/UpperCompressions.lean:8:18: declaration uses `sorry`
warning: OptimalOTS/Challenge/UpperCompressions.lean:12:8: declaration uses `sorry`
warning: OptimalOTS/Challenge/UpperCompressions.lean:15:8: declaration uses `sorry`
warning: OptimalOTS/Challenge/UpperCompressions.lean:18:8: declaration uses `sorry`
Build completed successfully (2689 jobs).
Exporting #[OptimalOTS.Challenge.UpperCompressions.admissible, OptimalOTS.Challenge.UpperCompressions.secure, OptimalOTS.Challenge.UpperCompressions.cost, propext, Quot.sound, Classical.choice, Nat.add, Nat.sub, Nat.mul, Nat.pow, Nat.gcd, Nat.div, Nat.mod, Nat.beq, Nat.ble, Nat.land, Nat.lor, Nat.xor, Nat.shiftLeft, Nat.shiftRight, String.ofList, Char.ofNat, List, eagerReduce, OptimalOTS.Challenge.UpperCompressions.scheme] from OptimalOTS.Challenge.UpperCompressions
Building Submissions.UpperCompressions.Solution
✔ [8797/8833] Built Submissions.UpperCompressions.TypedScheme (2.4s)
✔ [8798/8833] Built Submissions.UpperCompressions.Semantics (2.5s)
✔ [8800/8833] Built Submissions.UpperCompressions.Cache (2.3s)
✔ [8801/8833] Built Submissions.UpperCompressions.Adapter (2.5s)
✔ [8802/8833] Built Submissions.UpperCompressions.KeygenSupport (3.7s)
✔ [8803/8833] Built Submissions.UpperCompressions.IUB (3.9s)
✔ [8804/8833] Built Submissions.UpperCompressions.Count (6.1s)
✔ [8805/8833] Built Submissions.UpperCompressions.Deterministic (3.7s)
✔ [8806/8833] Built Submissions.UpperCompressions.AlgorithmCosts (3.0s)
✔ [8807/8833] Built Submissions.UpperCompressions.Master (2.6s)
✔ [8808/8833] Built Submissions.UpperCompressions.WireAdapter (2.3s)
✔ [8809/8833] Built Submissions.UpperCompressions.Resources (2.7s)
✔ [8810/8833] Built Submissions.UpperCompressions.Keygen (3.5s)
✔ [8811/8833] Built Submissions.UpperCompressions.SignIdx (3.7s)
✔ [8812/8833] Built Submissions.UpperCompressions.Reconstruct (3.7s)
✔ [8813/8833] Built Submissions.UpperCompressions.Names (12s)
✔ [8814/8833] Built Submissions.UpperCompressions.Correctness (2.1s)
✔ [8815/8833] Built Submissions.UpperCompressions.EncCharges (2.3s)
⚠ [8816/8833] Built Submissions.UpperCompressions.RowIneq (14s)
warning: Submissions/UpperCompressions/RowIneq.lean:47:5: Variable name `hr0` is not explicitly referenced.

Hint: The binding can be removed (if unused) or named `_` (if used implicitly). Alternatively, prefix the name with `_` to silence this warning:
  [apply] _hr0

Note: This linter can be disabled with `set_option linter.unusedVariables false`
warning: Submissions/UpperCompressions/RowIneq.lean:47:19: Variable name `hr1` is not explicitly referenced.

Hint: The binding can be removed (if unused) or named `_` (if used implicitly). Alternatively, prefix the name with `_` to silence this warning:
  [apply] _hr1

Note: This linter can be disabled with `set_option linter.unusedVariables false`
⚠ [8817/8833] Built Submissions.UpperCompressions.Tree (2.8s)
warning: Submissions/UpperCompressions/Tree.lean:370:54: Variable name `hA` is not explicitly referenced.

Hint: The binding can be removed (if unused) or named `_` (if used implicitly). Alternatively, prefix the name with `_` to silence this warning:
  [apply] _hA

Note: This linter can be disabled with `set_option linter.unusedVariables false`
✔ [8818/8833] Built Submissions.UpperCompressions.Values (3.2s)
⚠ [8819/8833] Built Submissions.UpperCompressions.SignRho (4.8s)
warning: Submissions/UpperCompressions/SignRho.lean:316:27: This simp argument is unused:
  mul_add

Hint: Omit it from the simp argument list.
  [apply] simp only [Finset.mul_sum]

Note: This linter can be disabled with `set_option linter.unusedSimpArgs false`
⚠ [8820/8833] Built Submissions.UpperCompressions.Resample (3.2s)
warning: Submissions/UpperCompressions/Resample.lean:35:18: Variable name `ξ` is not explicitly referenced.

Hint: The binding can be removed (if unused) or named `_` (if used implicitly). Alternatively, prefix the name with `_` to silence this warning:
  [apply] _ξ

Note: This linter can be disabled with `set_option linter.unusedVariables false`
warning: Submissions/UpperCompressions/Resample.lean:86:49: Variable name `hs` is not explicitly referenced.

Hint: The binding can be removed (if unused) or named `_` (if used implicitly). Alternatively, prefix the name with `_` to silence this warning:
  [apply] _hs

Note: This linter can be disabled with `set_option linter.unusedVariables false`
warning: Submissions/UpperCompressions/Resample.lean:161:52: Variable name `ξ` is not explicitly referenced.

Hint: The binding can be removed (if unused) or named `_` (if used implicitly). Alternatively, prefix the name with `_` to silence this warning:
  [apply] _ξ

Note: This linter can be disabled with `set_option linter.unusedVariables false`
warning: Submissions/UpperCompressions/Resample.lean:493:64: Variable name `ξ` is not explicitly referenced.

Hint: The binding can be removed (if unused) or named `_` (if used implicitly). Alternatively, prefix the name with `_` to silence this warning:
  [apply] _ξ

Note: This linter can be disabled with `set_option linter.unusedVariables false`
warning: Submissions/UpperCompressions/Resample.lean:526:12: Variable name `ξ` is not explicitly referenced.

Hint: The binding can be removed (if unused) or named `_` (if used implicitly). Alternatively, prefix the name with `_` to silence this warning:
  [apply] _ξ

Note: This linter can be disabled with `set_option linter.unusedVariables false`
✔ [8821/8833] Built Submissions.UpperCompressions.Events (3.7s)
⚠ [8822/8833] Built Submissions.UpperCompressions.Rows (2.8s)
warning: Submissions/UpperCompressions/Rows.lean:51:10: This simp argument is unused:
  BitVec.getLsbD_setWidth

Hint: Omit it from the simp argument list.
  [apply] simp [h]

Note: This linter can be disabled with `set_option linter.unusedSimpArgs false`
⚠ [8823/8833] Built Submissions.UpperCompressions.RowPotential (8.8s)
warning: Submissions/UpperCompressions/RowPotential.lean:176:0: automatically included section variable(s) unused in theorem `OptimalOTS.Row.sum_u_le`:
  hP
consider restructuring your `variable` declarations so that the variables are not in scope or explicitly omit them:
  omit hP in theorem ...

Note: This linter can be disabled with `set_option linter.unusedSectionVars false`
warning: Submissions/UpperCompressions/RowPotential.lean:190:0: automatically included section variable(s) unused in theorem `OptimalOTS.Row.N_le`:
  hc
consider restructuring your `variable` declarations so that the variables are not in scope or explicitly omit them:
  omit hc in theorem ...

Note: This linter can be disabled with `set_option linter.unusedSectionVars false`
warning: Submissions/UpperCompressions/RowPotential.lean:305:59: Used `tac1 <;> tac2` where `(tac1; tac2)` would suffice

Note: This linter can be disabled with `set_option linter.unnecessarySeqFocus false`
warning: Submissions/UpperCompressions/RowPotential.lean:350:59: Used `tac1 <;> tac2` where `(tac1; tac2)` would suffice

Note: This linter can be disabled with `set_option linter.unnecessarySeqFocus false`
warning: Submissions/UpperCompressions/RowPotential.lean:521:0: automatically included section variable(s) unused in theorem `OptimalOTS.sum_idxOf`:
  hc
consider restructuring your `variable` declarations so that the variables are not in scope or explicitly omit them:
  omit hc in theorem ...

Note: This linter can be disabled with `set_option linter.unusedSectionVars false`
✔ [8824/8833] Built Submissions.UpperCompressions.Cuts (57s)
✔ [8825/8833] Built Submissions.UpperCompressions.Scheme (3.6s)
⚠ [8826/8833] Built Submissions.UpperCompressions.Potentials (4.4s)
warning: Submissions/UpperCompressions/Potentials.lean:119:38: Variable name `ξ` is not explicitly referenced.

Hint: The binding can be removed (if unused) or named `_` (if used implicitly). Alternatively, prefix the name with `_` to silence this warning:
  [apply] _ξ

Note: This linter can be disabled with `set_option linter.unusedVariables false`
✔ [8827/8833] Built Submissions.UpperCompressions.StageB (4.0s)
✔ [8828/8833] Built Submissions.UpperCompressions.Assembly (4.2s)
✔ [8829/8833] Built Submissions.UpperCompressions.Main (3.8s)
✔ [8830/8833] Built Submissions.UpperCompressions.Availability (4.3s)
✔ [8831/8833] Built Submissions.UpperCompressions.ForestAlgorithm (3.7s)
✔ [8832/8833] Built Submissions.UpperCompressions.Wire (3.8s)
✔ [8833/8833] Built Submissions.UpperCompressions.Solution (3.6s)
Build completed successfully (8833 jobs).
Exporting #[OptimalOTS.Challenge.UpperCompressions.admissible, OptimalOTS.Challenge.UpperCompressions.secure, OptimalOTS.Challenge.UpperCompressions.cost, propext, Quot.sound, Classical.choice, Nat.add, Nat.sub, Nat.mul, Nat.pow, Nat.gcd, Nat.div, Nat.mod, Nat.beq, Nat.ble, Nat.land, Nat.lor, Nat.xor, Nat.shiftLeft, Nat.shiftRight, String.ofList, Char.ofNat, List, eagerReduce, OptimalOTS.Challenge.UpperCompressions.scheme] from Submissions.UpperCompressions.Solution
Running Lean default kernel on solution.
Lean default kernel accepts the solution
Your solution is okay!