Building OptimalOTS.Challenge.UpperCompressions
⚠ [2689/2689] Built OptimalOTS.Challenge.UpperCompressions (2.1s)
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
✔ [8798/8840] Built Submissions.UpperCompressions.TypedScheme (3.1s)
✔ [8799/8840] Built Submissions.UpperCompressions.Semantics (3.2s)
✔ [8800/8840] Built Submissions.UpperCompressions.Cache (3.4s)
ℹ [8801/8840] Built Submissions.UpperCompressions.ShallowAvailability (3.8s)
info: Submissions/UpperCompressions/ShallowAvailability.lean:63:0: 'AvailabilityCubic.block_bound' depends on axioms: [propext, Classical.choice, Quot.sound]
info: Submissions/UpperCompressions/ShallowAvailability.lean:64:0: 'AvailabilityCubic.signing_failure_bound' depends on axioms: [propext, Classical.choice, Quot.sound]
ℹ [8802/8840] Built Submissions.UpperCompressions.ShallowNames (7.0s)
info: Submissions/UpperCompressions/ShallowNames.lean:493:0: 'OptimalOTS.ShallowForest.graph_keygenCost' depends on axioms: [propext, Classical.choice, Quot.sound]
✔ [8803/8840] Built Submissions.UpperCompressions.Adapter (2.6s)
✔ [8804/8840] Built Submissions.UpperCompressions.KeygenSupport (2.3s)
✔ [8805/8840] Built Submissions.UpperCompressions.IUB (2.6s)
ℹ [8806/8840] Built Submissions.UpperCompressions.ShallowTree (4.0s)
info: Submissions/UpperCompressions/ShallowTree.lean:444:0: 'OptimalOTS.ShallowForest.exists_mem_evaluated_of_ne' depends on axioms: [propext, Classical.choice, Quot.sound]
info: Submissions/UpperCompressions/ShallowTree.lean:445:0: 'OptimalOTS.ShallowForest.reconstructCost_eq' depends on axioms: [propext, Classical.choice, Quot.sound]
✔ [8807/8840] Built Submissions.UpperCompressions.Deterministic (3.2s)
✔ [8808/8840] Built Submissions.UpperCompressions.IndexedScheme (3.5s)
✔ [8809/8840] Built Submissions.UpperCompressions.AlgorithmCosts (3.6s)
✔ [8810/8840] Built Submissions.UpperCompressions.Master (3.4s)
✔ [8811/8840] Built Submissions.UpperCompressions.WireAdapter (3.1s)
✔ [8812/8840] Built Submissions.UpperCompressions.Resources (3.3s)
✔ [8813/8840] Built Submissions.UpperCompressions.Reconstruct (4.4s)
✔ [8814/8840] Built Submissions.UpperCompressions.Keygen (4.9s)
ℹ [8815/8840] Built Submissions.UpperCompressions.IndexedSampling (5.0s)
info: Submissions/UpperCompressions/IndexedSampling.lean:614:0: 'OptimalOTS.IndexedAnalysis.sign_eq_map' depends on axioms: [propext, Classical.choice, Quot.sound]
info: Submissions/UpperCompressions/IndexedSampling.lean:615:0: 'OptimalOTS.IndexedAnalysis.signIdx_support' depends on axioms: [propext, Classical.choice, Quot.sound]
✔ [8816/8840] Built Submissions.UpperCompressions.SignIdx (5.2s)
✔ [8817/8840] Built Submissions.UpperCompressions.IndexedResources (3.4s)
ℹ [8818/8840] Built Submissions.UpperCompressions.IndexedReconstruct (2.8s)
info: Submissions/UpperCompressions/IndexedReconstruct.lean:52:0: 'OptimalOTS.IndexedAnalysis.verify_support' depends on axioms: [propext, Classical.choice, Quot.sound]
⚠ [8819/8840] Built Submissions.UpperCompressions.RowIneq (16s)
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`
✔ [8820/8840] Built Submissions.UpperCompressions.IndexedCharges (2.0s)
✔ [8821/8840] Built Submissions.UpperCompressions.Correctness (3.1s)
ℹ [8822/8840] Built Submissions.UpperCompressions.IndexedAvailability (3.7s)
info: Submissions/UpperCompressions/IndexedAvailability.lean:166:0: 'OptimalOTS.IndexedAnalysis.Availability.loop_failure' depends on axioms: [propext, Classical.choice, Quot.sound]
info: Submissions/UpperCompressions/IndexedAvailability.lean:167:0: 'OptimalOTS.IndexedAnalysis.Availability.sign_failure_le' depends on axioms: [propext, Classical.choice, Quot.sound]
✔ [8823/8840] Built Submissions.UpperCompressions.ShallowValues (4.4s)
ℹ [8824/8840] Built Submissions.UpperCompressions.IndexedCorrectness (2.6s)
info: Submissions/UpperCompressions/IndexedCorrectness.lean:117:0: 'OptimalOTS.IndexedAnalysis.Correctness.correct' depends on axioms: [propext, Classical.choice, Quot.sound]
✔ [8825/8840] Built Submissions.UpperCompressions.IndexedFreshness (2.9s)
ℹ [8826/8840] Built Submissions.UpperCompressions.ShallowEvents (3.3s)
info: Submissions/UpperCompressions/ShallowEvents.lean:495:0: 'OptimalOTS.ShallowForest.events_none' depends on axioms: [propext, Classical.choice, Quot.sound]
info: Submissions/UpperCompressions/ShallowEvents.lean:496:0: 'OptimalOTS.ShallowForest.events_ne' depends on axioms: [propext, Classical.choice, Quot.sound]
info: Submissions/UpperCompressions/ShallowEvents.lean:497:0: 'OptimalOTS.ShallowForest.events_same' depends on axioms: [propext, Classical.choice, Quot.sound]
ℹ [8827/8840] Built Submissions.UpperCompressions.ShallowResample (3.6s)
info: Submissions/UpperCompressions/ShallowResample.lean:544:0: 'OptimalOTS.ShallowForest.hits_charge_A' depends on axioms: [propext, Classical.choice, Quot.sound]
info: Submissions/UpperCompressions/ShallowResample.lean:545:0: 'OptimalOTS.ShallowForest.hits_charge_B' depends on axioms: [propext, Classical.choice, Quot.sound]
⚠ [8828/8840] Built Submissions.UpperCompressions.IndexedRho (5.4s)
warning: Submissions/UpperCompressions/IndexedRho.lean:317: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`
info: Submissions/UpperCompressions/IndexedRho.lean:451:0: 'OptimalOTS.IndexedAnalysis.signRho_bound' depends on axioms: [propext, Classical.choice, Quot.sound]
⚠ [8829/8840] Built Submissions.UpperCompressions.IndexedRows (2.4s)
warning: Submissions/UpperCompressions/IndexedRows.lean:52: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`
⚠ [8830/8840] Built Submissions.UpperCompressions.IndexedPotential (8.8s)
warning: Submissions/UpperCompressions/IndexedPotential.lean:177:0: automatically included section variable(s) unused in theorem `OptimalOTS.IndexedAnalysis.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/IndexedPotential.lean:191:0: automatically included section variable(s) unused in theorem `OptimalOTS.IndexedAnalysis.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/IndexedPotential.lean:306:59: Used `tac1 <;> tac2` where `(tac1; tac2)` would suffice

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

Note: This linter can be disabled with `set_option linter.unnecessarySeqFocus false`
warning: Submissions/UpperCompressions/IndexedPotential.lean:522:0: automatically included section variable(s) unused in theorem `OptimalOTS.IndexedAnalysis.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`
info: Submissions/UpperCompressions/IndexedPotential.lean:685:0: 'OptimalOTS.IndexedAnalysis.candidateRowHyp' depends on axioms: [propext, Classical.choice, Quot.sound]
info: Submissions/UpperCompressions/IndexedPotential.lean:686:0: 'OptimalOTS.IndexedAnalysis.psi_charge' depends on axioms: [propext, Classical.choice, Quot.sound]
info: Submissions/UpperCompressions/IndexedPotential.lean:687:0: 'OptimalOTS.IndexedAnalysis.psi_dom' depends on axioms: [propext, Classical.choice, Quot.sound]
ℹ [8831/8840] Built Submissions.UpperCompressions.ShallowCount (51s)
info: Submissions/UpperCompressions/ShallowCount.lean:119:0: 'OptimalOTS.ShallowResearch.single_shape_ge' depends on axioms: [propext, Classical.choice, Quot.sound]
info: Submissions/UpperCompressions/ShallowCount.lean:120:0: 'OptimalOTS.ShallowResearch.single_shape_102_ge' depends on axioms: [propext, Classical.choice, Quot.sound]
ℹ [8832/8840] Built Submissions.UpperCompressions.ShallowCuts (4.5s)
info: Submissions/UpperCompressions/ShallowCuts.lean:499:0: 'OptimalOTS.ShallowForest.card_family' depends on axioms: [propext, Classical.choice, Quot.sound]
info: Submissions/UpperCompressions/ShallowCuts.lean:500:0: 'OptimalOTS.ShallowForest.isCut_of_mem_family' depends on axioms: [propext, Classical.choice, Quot.sound]
info: Submissions/UpperCompressions/ShallowCuts.lean:501:0: 'OptimalOTS.ShallowForest.card_of_mem_family' depends on axioms: [propext, Classical.choice, Quot.sound]
info: Submissions/UpperCompressions/ShallowCuts.lean:502:0: 'OptimalOTS.ShallowForest.cost_of_mem_family' depends on axioms: [propext, Classical.choice, Quot.sound]
info: Submissions/UpperCompressions/ShallowCuts.lean:503:0: 'OptimalOTS.ShallowForest.reconstructCost_cutOf' depends on axioms: [propext, Classical.choice, Quot.sound]
info: Submissions/UpperCompressions/ShallowCuts.lean:504:0: 'OptimalOTS.ShallowForest.revealBits_cutOf' depends on axioms: [propext, Classical.choice, Quot.sound]
✔ [8833/8840] Built Submissions.UpperCompressions.ShallowScheme (3.8s)
✔ [8834/8840] Built Submissions.UpperCompressions.ShallowResources (3.8s)
⚠ [8835/8840] Built Submissions.UpperCompressions.ShallowPotentials (4.7s)
warning: Submissions/UpperCompressions/ShallowPotentials.lean:122: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`
info: Submissions/UpperCompressions/ShallowPotentials.lean:434:0: 'OptimalOTS.ShallowForest.ΦA_charge' depends on axioms: [propext, Classical.choice, Quot.sound]
info: Submissions/UpperCompressions/ShallowPotentials.lean:435:0: 'OptimalOTS.ShallowForest.ΦB_charge_some' depends on axioms: [propext, Classical.choice, Quot.sound]
info: Submissions/UpperCompressions/ShallowPotentials.lean:436:0: 'OptimalOTS.ShallowForest.ΦB_charge_none' depends on axioms: [propext, Classical.choice, Quot.sound]
✔ [8836/8840] Built Submissions.UpperCompressions.ShallowStageB (5.2s)
✔ [8837/8840] Built Submissions.UpperCompressions.ShallowAssembly (4.3s)
✔ [8838/8840] Built Submissions.UpperCompressions.ShallowMain (3.9s)
ℹ [8839/8840] Built Submissions.UpperCompressions.ShallowWire (3.8s)
info: Submissions/UpperCompressions/ShallowWire.lean:78:0: 'OptimalOTS.ShallowUpperForest.Wire.secure' depends on axioms: [propext, Classical.choice, Quot.sound]
info: Submissions/UpperCompressions/ShallowWire.lean:79:0: 'OptimalOTS.ShallowUpperForest.Wire.admissible' depends on axioms: [propext, Classical.choice, Quot.sound]
info: Submissions/UpperCompressions/ShallowWire.lean:80:0: 'OptimalOTS.ShallowUpperForest.Wire.cost' depends on axioms: [propext, Classical.choice, Quot.sound]
✔ [8840/8840] Built Submissions.UpperCompressions.Solution (3.6s)
Build completed successfully (8840 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!