Building OptimalOTS.Challenge.LowerGenerality1
⚠ [2690/2690] Built OptimalOTS.Challenge.LowerGenerality1 (1.9s)
warning: OptimalOTS/Challenge/LowerGenerality1.lean:9:8: declaration uses `sorry`
Build completed successfully (2690 jobs).
Exporting #[OptimalOTS.Challenge.LowerGenerality1.candidate, 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] from OptimalOTS.Challenge.LowerGenerality1
Building Submissions.LowerGenerality1.Solution
✔ [6701/6896] Built Submissions.LowerGenerality1.Semantics (2.1s)
✔ [8799/8823] Built Submissions.LowerGenerality1.Patterns (2.3s)
✔ [8800/8823] Built Submissions.LowerGenerality1.WeakSecurity (2.2s)
✔ [8801/8823] Built Submissions.LowerGenerality1.Cache (2.5s)
⚠ [8802/8823] Built Submissions.LowerGenerality1.Encoding (2.5s)
warning: Submissions/LowerGenerality1/Encoding.lean:23:23: Used `tac1 <;> tac2` where `(tac1; tac2)` would suffice

Note: This linter can be disabled with `set_option linter.unnecessarySeqFocus false`
warning: Submissions/LowerGenerality1/Encoding.lean:51:12: This simp argument is unused:
  List.filter_cons

Hint: Omit it from the simp argument list.
  [apply] simp [h1, h2]

Note: This linter can be disabled with `set_option linter.unusedSimpArgs false`
warning: Submissions/LowerGenerality1/Encoding.lean:54:12: This simp argument is unused:
  List.filter_cons

Hint: Omit it from the simp argument list.
  [apply] simp [hav, not_lt.2 hav.le]

Note: This linter can be disabled with `set_option linter.unusedSimpArgs false`
✔ [8803/8823] Built Submissions.LowerGenerality1.CostCore (2.7s)
✔ [8804/8823] Built Submissions.LowerGenerality1.KeygenSupport (2.0s)
✔ [8805/8823] Built Submissions.LowerGenerality1.Expectation (1.9s)
✔ [8806/8823] Built Submissions.LowerGenerality1.CacheFresh (2.1s)
⚠ [8807/8823] Built Submissions.LowerGenerality1.OrderedCounting (4.0s)
warning: Submissions/LowerGenerality1/OrderedCounting.lean:14:8: automatically included section variable(s) unused in theorem `_private.Submissions.LowerGenerality1.OrderedCounting.0.OptimalOTS.DisclosureCounting.zero_left`:
  [DecidableEq ι]
  [LinearOrder α]
consider restructuring your `variable` declarations so that the variables are not in scope or explicitly omit them:
  omit [DecidableEq ι] [LinearOrder α] in theorem ...

Note: This linter can be disabled with `set_option linter.unusedSectionVars false`
warning: Submissions/LowerGenerality1/OrderedCounting.lean:32:4: Try `simp at hv` instead of `simpa using hv`

Note: This linter can be disabled with `set_option linter.unnecessarySimpa false`
warning: Submissions/LowerGenerality1/OrderedCounting.lean:22:8: automatically included section variable(s) unused in theorem `_private.Submissions.LowerGenerality1.OrderedCounting.0.OptimalOTS.DisclosureCounting.zero_right`:
  [DecidableEq ι]
consider restructuring your `variable` declarations so that the variables are not in scope or explicitly omit them:
  omit [DecidableEq ι] in theorem ...

Note: This linter can be disabled with `set_option linter.unusedSectionVars false`
warning: Submissions/LowerGenerality1/OrderedCounting.lean:109:20: Used `tac1 <;> tac2` where `(tac1; tac2)` would suffice

Note: This linter can be disabled with `set_option linter.unnecessarySeqFocus false`
✔ [8808/8823] Built Submissions.LowerGenerality1.PatternHelpers (2.3s)
⚠ [8809/8823] Built Submissions.LowerGenerality1.Conversion (2.6s)
warning: Submissions/LowerGenerality1/Conversion.lean:446:20: This simp argument is unused:
  hk

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

Note: This linter can be disabled with `set_option linter.unusedSimpArgs false`
warning: Submissions/LowerGenerality1/Conversion.lean:451:15: This simp argument is unused:
  cacheTab

Hint: Omit it from the simp argument list.
  [apply] simp only [hk, NodeKind.input, NodeKind.inLen, NodeKind.value, hv, Option.getD_some, BitVec.cast_cast,
    BitVec.cast_eq]

Note: This linter can be disabled with `set_option linter.unusedSimpArgs false`
warning: Submissions/LowerGenerality1/Conversion.lean:451:25: This simp argument is unused:
  hk

Hint: Omit it from the simp argument list.
  [apply] simp only [cacheTab, NodeKind.input, NodeKind.inLen, NodeKind.value, hv, Option.getD_some, BitVec.cast_cast,
    BitVec.cast_eq]

Note: This linter can be disabled with `set_option linter.unusedSimpArgs false`
warning: Submissions/LowerGenerality1/Conversion.lean:466:15: This simp argument is unused:
  cacheTab

Hint: Omit it from the simp argument list.
  [apply] simp only [hk, NodeKind.input, NodeKind.inLen, hv, Option.getD_some]

Note: This linter can be disabled with `set_option linter.unusedSimpArgs false`
warning: Submissions/LowerGenerality1/Conversion.lean:466:25: This simp argument is unused:
  hk

Hint: Omit it from the simp argument list.
  [apply] simp only [cacheTab, NodeKind.input, NodeKind.inLen, hv, Option.getD_some]

Note: This linter can be disabled with `set_option linter.unusedSimpArgs false`
✔ [8810/8823] Built Submissions.LowerGenerality1.Index (2.8s)
✔ [8811/8823] Built Submissions.LowerGenerality1.DisclosurePatterns (3.0s)
✔ [8812/8823] Built Submissions.LowerGenerality1.SignFresh (5.9s)
✔ [8813/8823] Built Submissions.LowerGenerality1.WholeWordOrigins (3.9s)
✔ [8814/8823] Built Submissions.LowerGenerality1.PatternGoods (4.1s)
✔ [8815/8823] Built Submissions.LowerGenerality1.AveragedSigning (4.2s)
✔ [8816/8823] Built Submissions.LowerGenerality1.PatternSearch (4.4s)
⚠ [8817/8823] Built Submissions.LowerGenerality1.PatternAttack (3.9s)
warning: Submissions/LowerGenerality1/PatternAttack.lean:146:10: This simp argument is unused:
  he

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

Note: This linter can be disabled with `set_option linter.unusedSimpArgs false`
✔ [8818/8823] Built Submissions.LowerGenerality1.AveragedSearch (4.1s)
⚠ [8819/8823] Built Submissions.LowerGenerality1.PatternAssembly (3.7s)
warning: Submissions/LowerGenerality1/PatternAssembly.lean:46:76: This simp argument is unused:
  check

Hint: Omit it from the simp argument list.
  [apply] simp only [afterSign, Option.map_some, Option.isNone_some, Bool.false_or]

Note: This linter can be disabled with `set_option linter.unusedSimpArgs false`
✔ [8820/8823] Built Submissions.LowerGenerality1.AveragedAttack (3.9s)
✔ [8821/8823] Built Submissions.LowerGenerality1.AveragedCounting (4.2s)
✔ [8822/8823] Built Submissions.LowerGenerality1.AveragedAssembly (3.0s)
✔ [8823/8823] Built Submissions.LowerGenerality1.Solution (3.6s)
Build completed successfully (8823 jobs).
Exporting #[OptimalOTS.Challenge.LowerGenerality1.candidate, 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] from Submissions.LowerGenerality1.Solution
Running Lean default kernel on solution.
Lean default kernel accepts the solution
Your solution is okay!