Building OptimalOTS.Challenge.UpperRiscv
⚠ [2703/2703] Built OptimalOTS.Challenge.UpperRiscv (2.4s)
warning: OptimalOTS/Challenge/UpperRiscv.lean:9:18: declaration uses `sorry`
warning: OptimalOTS/Challenge/UpperRiscv.lean:13:8: declaration uses `sorry`
warning: OptimalOTS/Challenge/UpperRiscv.lean:16:8: declaration uses `sorry`
Build completed successfully (2703 jobs).
Exporting #[OptimalOTS.Challenge.UpperRiscv.certificate, OptimalOTS.Challenge.UpperRiscv.image_size, 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.UpperRiscv.submission] from OptimalOTS.Challenge.UpperRiscv
Building Submissions.UpperRiscv.Solution
✔ [5775/5897] Built Submissions.UpperRiscv.TypedScheme (2.2s)
✔ [5776/5897] Built Submissions.UpperRiscv.Parameters (2.1s)
✔ [8814/8900] Built Submissions.UpperRiscv.Semantics (3.1s)
✔ [8815/8900] Built Submissions.UpperRiscv.MachineCost (3.3s)
✔ [8816/8900] Built Submissions.UpperRiscv.Cache (3.4s)
✔ [8817/8900] Built Submissions.UpperRiscv.Program (6.3s)
✔ [8818/8900] Built Submissions.UpperRiscv.IUB (3.5s)
✔ [8819/8900] Built Submissions.UpperRiscv.BlockExecution (4.6s)
✔ [8820/8900] Built Submissions.UpperRiscv.Count (9.3s)
✔ [8821/8900] Built Submissions.UpperRiscv.Digits (9.3s)
✔ [8822/8900] Built Submissions.UpperRiscv.Payload (9.3s)
✔ [8823/8900] Built Submissions.UpperRiscv.Master (3.9s)
✔ [8824/8900] Built Submissions.UpperRiscv.AssemblyMacros (3.2s)
✔ [8825/8900] Built Submissions.UpperRiscv.Refines (2.1s)
⚠ [8826/8900] Built Submissions.UpperRiscv.Names (10s)
warning: Submissions/UpperRiscv/Names.lean:110:37: This simp argument is unused:
  Finset.mem_insert

Hint: Omit it from the simp argument list.
  [apply] simp only [parents, child, prev, Finset.mem_singleton, Finset.mem_image, Finset.mem_univ, true_and,
    Finset.notMem_empty, Option.some.injEq, reduceCtorEq, Name.ci.injEq, Name.ch.injEq, Name.cv.injEq, Fin.ext_iff,
    Fin.val_zero, iff_true, iff_false, false_iff, or_false, exists_false]

Note: This linter can be disabled with `set_option linter.unusedSimpArgs false`
warning: Submissions/UpperRiscv/Names.lean:113:20: This simp argument is unused:
  iff_true

Hint: Omit it from the simp argument list.
  [apply] simp only [parents, child, prev, Finset.mem_insert, Finset.mem_singleton, Finset.mem_image, Finset.mem_univ,
    true_and, Finset.notMem_empty, Option.some.injEq, reduceCtorEq, Name.ci.injEq, Name.ch.injEq, Name.cv.injEq,
    Fin.ext_iff, Fin.val_zero, iff_false, false_iff, or_false, exists_false]

Note: This linter can be disabled with `set_option linter.unusedSimpArgs false`
warning: Submissions/UpperRiscv/Names.lean:113:52: This simp argument is unused:
  or_false

Hint: Omit it from the simp argument list.
  [apply] simp only [parents, child, prev, Finset.mem_insert, Finset.mem_singleton, Finset.mem_image, Finset.mem_univ,
    true_and, Finset.notMem_empty, Option.some.injEq, reduceCtorEq, Name.ci.injEq, Name.ch.injEq, Name.cv.injEq,
    Fin.ext_iff, Fin.val_zero, iff_true, iff_false, false_iff, exists_false]

Note: This linter can be disabled with `set_option linter.unusedSimpArgs false`
warning: Submissions/UpperRiscv/Names.lean:122:64: This simp argument is unused:
  reduceCtorEq

Hint: Omit it from the simp argument list.
  [apply] simp only [Option.some.injEq] at h

Note: This linter can be disabled with `set_option linter.unusedSimpArgs false`
⚠ [8827/8900] Built Submissions.UpperRiscv.Tree (3.0s)
warning: Submissions/UpperRiscv/Tree.lean:376: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`
⚠ [8828/8900] Built Submissions.UpperRiscv.RowIneq (16s)
warning: Submissions/UpperRiscv/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/UpperRiscv/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`
✔ [8829/8900] Built Submissions.UpperRiscv.Cuts (4.2s)
✔ [8830/8900] Built Submissions.UpperRiscv.MixedProgram (16s)
✔ [8831/8900] Built Submissions.UpperRiscv.Valid (105s)
✔ [8832/8900] Built Submissions.UpperRiscv.FixedChoice (4.4s)
✔ [8833/8900] Built Submissions.UpperRiscv.PackFiber (4.5s)
⚠ [8834/8900] Built Submissions.UpperRiscv.GScheme (4.7s)
warning: Submissions/UpperRiscv/GScheme.lean:49:8: This simp argument is unused:
  BitVec.getLsbD_setWidth

Hint: Omit it from the simp argument list.
  [apply] simp [BitVec.getLsbD_append, hi]

Note: This linter can be disabled with `set_option linter.unusedSimpArgs false`
warning: Submissions/UpperRiscv/GScheme.lean:64: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`
warning: Submissions/UpperRiscv/GScheme.lean:108:10: This simp argument is unused:
  BitVec.getLsbD_setWidth

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

Note: This linter can be disabled with `set_option linter.unusedSimpArgs false`
✔ [8835/8900] Built Submissions.UpperRiscv.Scheme (5.8s)
✔ [8836/8900] Built Submissions.UpperRiscv.PackCount (6.0s)
⚠ [8837/8900] Built Submissions.UpperRiscv.Adapter (5.9s)
warning: Submissions/UpperRiscv/Adapter.lean:77:37: This simp argument is unused:
  experiment

Hint: Omit it from the simp argument list.
  [apply] simp only [TypedScheme.experiment, GScheme.toAlgorithm, toDAGAdversary]

Note: This linter can be disabled with `set_option linter.unusedSimpArgs false`
warning: Submissions/UpperRiscv/Adapter.lean:93:37: This simp argument is unused:
  experiment

Hint: Omit it from the simp argument list.
  [apply] simp only [TypedScheme.experiment, GScheme.toAlgorithm, fromDAGAdversary]

Note: This linter can be disabled with `set_option linter.unusedSimpArgs false`
✔ [8838/8900] Built Submissions.UpperRiscv.KeygenSupport (6.0s)
✔ [8839/8900] Built Submissions.UpperRiscv.Reconstruct (6.6s)
✔ [8840/8900] Built Submissions.UpperRiscv.Keygen (6.7s)
✔ [8841/8900] Built Submissions.UpperRiscv.Deterministic (4.3s)
✔ [8842/8900] Built Submissions.UpperRiscv.AlgorithmCosts (5.9s)
✔ [8843/8900] Built Submissions.UpperRiscv.SignIdx (6.1s)
✔ [8844/8900] Built Submissions.UpperRiscv.Lanes (19s)
✔ [8845/8900] Built Submissions.UpperRiscv.Resources (6.1s)
✔ [8846/8900] Built Submissions.UpperRiscv.WireAdapter (6.3s)
✔ [8847/8900] Built Submissions.UpperRiscv.Correctness (6.7s)
⚠ [8848/8900] Built Submissions.UpperRiscv.Values (8.8s)
warning: Submissions/UpperRiscv/Values.lean:53:15: This simp argument is unused:
  BitVec.getLsbD_extractLsb'

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

Note: This linter can be disabled with `set_option linter.unusedSimpArgs false`
warning: Submissions/UpperRiscv/Values.lean:116:48: This simp argument is unused:
  BitVec.toNat_cast

Hint: Omit it from the simp argument list.
  [apply] simp only [kindOf, NodeKind.value, detVal_cv]

Note: This linter can be disabled with `set_option linter.unusedSimpArgs false`
warning: Submissions/UpperRiscv/Values.lean:445:14: Used `tac1 <;> tac2` where `(tac1; tac2)` would suffice

Note: This linter can be disabled with `set_option linter.unnecessarySeqFocus false`
warning: Submissions/UpperRiscv/Values.lean:620:10: This simp argument is unused:
  BitVec.getLsbD_setWidth

Hint: Omit it from the simp argument list.
  [apply] simp [BitVec.getLsbD_extractLsb', hi, hi']

Note: This linter can be disabled with `set_option linter.unusedSimpArgs false`
warning: Submissions/UpperRiscv/Values.lean:620:35: This simp argument is unused:
  BitVec.getLsbD_extractLsb'

Hint: Omit it from the simp argument list.
  [apply] simp [BitVec.getLsbD_setWidth, hi, hi']

Note: This linter can be disabled with `set_option linter.unusedSimpArgs false`
warning: Submissions/UpperRiscv/Values.lean:631:77: Try `simp at hs` instead of `simpa using hs`

Note: This linter can be disabled with `set_option linter.unnecessarySimpa false`
warning: Submissions/UpperRiscv/Values.lean:631:77: Try `simp at hs` instead of `simpa using hs`

Note: This linter can be disabled with `set_option linter.unnecessarySimpa false`
warning: Submissions/UpperRiscv/Values.lean:631:77: Try `simp at hs` instead of `simpa using hs`

Note: This linter can be disabled with `set_option linter.unnecessarySimpa false`
warning: Submissions/UpperRiscv/Values.lean:631:77: Try `simp at hs` instead of `simpa using hs`

Note: This linter can be disabled with `set_option linter.unnecessarySimpa false`
⚠ [8849/8900] Built Submissions.UpperRiscv.MixedLanes (6.6s)
warning: Submissions/UpperRiscv/MixedLanes.lean:57:15: This simp argument is unused:
  and_pair _ 5 3 (by omega)

Hint: Omit it from the simp argument list.
  [apply] simp only [and_pair _ 4 4 (by omega)]

Note: This linter can be disabled with `set_option linter.unusedSimpArgs false`
warning: Submissions/UpperRiscv/MixedLanes.lean:59:15: This simp argument is unused:
  mod_f5

Hint: Omit it from the simp argument list.
  [apply] simp only [mod_f4, mod_c3, mod_c4, Nat.div_div_eq_div_mul]

Note: This linter can be disabled with `set_option linter.unusedSimpArgs false`
warning: Submissions/UpperRiscv/MixedLanes.lean:59:31: This simp argument is unused:
  mod_c3

Hint: Omit it from the simp argument list.
  [apply] simp only [mod_f5, mod_f4, mod_c4, Nat.div_div_eq_div_mul]

Note: This linter can be disabled with `set_option linter.unusedSimpArgs false`
✔ [8850/8900] Built Submissions.UpperRiscv.EncCharges (12s)
✔ [8851/8900] Built Submissions.UpperRiscv.Events (5.1s)
⚠ [8852/8900] Built Submissions.UpperRiscv.Resample (5.7s)
warning: Submissions/UpperRiscv/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/UpperRiscv/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/UpperRiscv/Resample.lean:200:53: 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/UpperRiscv/Resample.lean:234: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/UpperRiscv/Resample.lean:381:44: 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`
warning: Submissions/UpperRiscv/Resample.lean:391:43: 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`
warning: Submissions/UpperRiscv/Resample.lean:546: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`
warning: Submissions/UpperRiscv/Resample.lean:596: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/UpperRiscv/Resample.lean:608: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`
✔ [8853/8900] Built Submissions.UpperRiscv.MachineMemory (20s)
⚠ [8854/8900] Built Submissions.UpperRiscv.GoodRec (4.8s)
warning: Submissions/UpperRiscv/GoodRec.lean:33:45: 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/UpperRiscv/GoodRec.lean:49:45: 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/UpperRiscv/GoodRec.lean:102:17: This simp argument is unused:
  Fin.val_mk

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

Note: This linter can be disabled with `set_option linter.unusedSimpArgs false`
warning: Submissions/UpperRiscv/GoodRec.lean:241:44: Variable name `hp` 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] _hp

Note: This linter can be disabled with `set_option linter.unusedVariables false`
⚠ [8855/8900] Built Submissions.UpperRiscv.SignRho (7.4s)
warning: Submissions/UpperRiscv/SignRho.lean:92:46: Variable name `hM` 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] _hM

Note: This linter can be disabled with `set_option linter.unusedVariables false`
warning: Submissions/UpperRiscv/SignRho.lean:313: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`
✔ [8856/8900] Built Submissions.UpperRiscv.LoaderProof (5.7s)
✔ [8857/8900] Built Submissions.UpperRiscv.CopyProof (4.2s)
✔ [8858/8900] Built Submissions.UpperRiscv.HashOutput (4.2s)
⚠ [8859/8900] Built Submissions.UpperRiscv.Rows (4.0s)
warning: Submissions/UpperRiscv/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`
⚠ [8860/8900] Built Submissions.UpperRiscv.MachineFacts (4.5s)
warning: Submissions/UpperRiscv/MachineFacts.lean:81:4: This simp argument is unused:
  decide_true

Hint: Omit it from the simp argument list.
  [apply] simp only [show (8 : Word) = W 8 from rfl, show (16 : Word) = W 16 from rfl, show (24 : Word) = W 24 from rfl,
    W_add, dword_ok a h1 (by omega) h3, dword_ok (a + 8) (by omega) (by omega) (by omega),
    dword_ok (a + 16) (by omega) (by omega) (by omega), dword_ok (a + 24) (by omega) (by omega) (by omega),
    Bool.and_self]

Note: This linter can be disabled with `set_option linter.unusedSimpArgs false`
⚠ [8861/8900] Built Submissions.UpperRiscv.RowPotential (8.8s)
warning: Submissions/UpperRiscv/RowPotential.lean:177: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/UpperRiscv/RowPotential.lean:191: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/UpperRiscv/RowPotential.lean:270:59: Used `tac1 <;> tac2` where `(tac1; tac2)` would suffice

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

Note: This linter can be disabled with `set_option linter.unnecessarySeqFocus false`
warning: Submissions/UpperRiscv/RowPotential.lean:524: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`
✔ [8862/8900] Built Submissions.UpperRiscv.MixedIndexLanes (5.7s)
⚠ [8863/8900] Built Submissions.UpperRiscv.Potentials (4.9s)
warning: Submissions/UpperRiscv/Potentials.lean:124: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`
✔ [8864/8900] Built Submissions.UpperRiscv.MixedIndexArith (4.5s)
✔ [8865/8900] Built Submissions.UpperRiscv.StageB (5.2s)
✔ [8866/8900] Built Submissions.UpperRiscv.MixedDispatchArith (4.8s)
✔ [8867/8900] Built Submissions.UpperRiscv.Assembly (4.5s)
✔ [8868/8900] Built Submissions.UpperRiscv.Main (4.2s)
⚠ [8869/8900] Built Submissions.UpperRiscv.Availability (4.7s)
warning: Submissions/UpperRiscv/Availability.lean:58:5: Variable name `hM` 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] _hM

Note: This linter can be disabled with `set_option linter.unusedVariables false`
✔ [8870/8900] Built Submissions.UpperRiscv.ForestAlgorithm (3.8s)
✔ [8871/8900] Built Submissions.UpperRiscv.Wire (3.9s)
✔ [8872/8900] Built Submissions.UpperRiscv.Layout (3.9s)
✔ [8873/8900] Built Submissions.UpperRiscv.ForestVerifier (5.1s)
✔ [8874/8900] Built Submissions.UpperRiscv.ForestVerifierProof (4.1s)
✔ [8875/8900] Built Submissions.UpperRiscv.Reader (4.0s)
✔ [8876/8900] Built Submissions.UpperRiscv.MixedContext (3.9s)
✔ [8877/8900] Built Submissions.UpperRiscv.MixedJump (4.4s)
✔ [8878/8900] Built Submissions.UpperRiscv.MixedLayout (5.1s)
⚠ [8879/8900] Built Submissions.UpperRiscv.MixedMemory (4.3s)
warning: Submissions/UpperRiscv/MixedMemory.lean:87:89: Unused tactic linter: `decide` does nothing

Note: This linter can be disabled with `set_option linter.unusedTactic false`
warning: Submissions/UpperRiscv/MixedMemory.lean:87:89: this tactic is never executed

Note: This linter can be disabled with `set_option linter.unreachableTactic false`
✔ [8880/8900] Built Submissions.UpperRiscv.MixedIndexPhase (12s)
✔ [8881/8900] Built Submissions.UpperRiscv.MixedChainSemantics (4.4s)
✔ [8882/8900] Built Submissions.UpperRiscv.MixedEntry (4.7s)
✔ [8883/8900] Built Submissions.UpperRiscv.MixedPayload (4.2s)
✔ [8884/8900] Built Submissions.UpperRiscv.MixedHashStep (4.1s)
✔ [8885/8900] Built Submissions.UpperRiscv.MixedChainSteps (4.8s)
✔ [8886/8900] Built Submissions.UpperRiscv.MixedChainStart (4.1s)
⚠ [8887/8900] Built Submissions.UpperRiscv.MixedRoot (20s)
warning: Submissions/UpperRiscv/MixedRoot.lean:102:78: This simp argument is unused:
  execInstrBr

Hint: Omit it from the simp argument list.
  [apply] simp only [Riscv.LinearReady, Riscv.linearInstruction, Riscv.memoryReady, MachineState.getReg_setPC,
    getReg_setReg_ite, true_and, and_true]

Note: This linter can be disabled with `set_option linter.unusedSimpArgs false`
warning: Submissions/UpperRiscv/MixedRoot.lean:103:6: This simp argument is unused:
  MachineState.getReg_setPC

Hint: Omit it from the simp argument list.
  [apply] simp only [Riscv.LinearReady, Riscv.linearInstruction, Riscv.memoryReady, execInstrBr, getReg_setReg_ite,
    true_and, and_true]

Note: This linter can be disabled with `set_option linter.unusedSimpArgs false`
warning: Submissions/UpperRiscv/MixedRoot.lean:103:33: This simp argument is unused:
  getReg_setReg_ite

Hint: Omit it from the simp argument list.
  [apply] simp only [Riscv.LinearReady, Riscv.linearInstruction, Riscv.memoryReady, execInstrBr,
    MachineState.getReg_setPC, true_and, and_true]

Note: This linter can be disabled with `set_option linter.unusedSimpArgs false`
warning: Submissions/UpperRiscv/MixedRoot.lean:112:14: This simp argument is unused:
  Ne.symm hr

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

Note: This linter can be disabled with `set_option linter.unusedSimpArgs false`
warning: Submissions/UpperRiscv/MixedRoot.lean:117:15: This simp argument is unused:
  true_and

Hint: Omit it from the simp argument list.
  [apply] simp only [ne_eq, reduceCtorEq, not_false_eq_true, if_true, and_true, false_and, if_false,
    show ¬(Reg.x12 = Reg.x26) by decide, x12, l0, BitVec.add_zero]

Note: This linter can be disabled with `set_option linter.unusedSimpArgs false`
warning: Submissions/UpperRiscv/MixedRoot.lean:117:84: This simp argument is unused:
  false_and

Hint: Omit it from the simp argument list.
  [apply] simp only [true_and, ne_eq, reduceCtorEq, not_false_eq_true, if_true, and_true, if_false,
    show ¬(Reg.x12 = Reg.x26) by decide, x12, l0, BitVec.add_zero]

Note: This linter can be disabled with `set_option linter.unusedSimpArgs false`
warning: Submissions/UpperRiscv/MixedRoot.lean:117:95: This simp argument is unused:
  if_false

Hint: Omit it from the simp argument list.
  [apply] simp only [true_and, ne_eq, reduceCtorEq, not_false_eq_true, if_true, and_true, false_and,
    show ¬(Reg.x12 = Reg.x26) by decide, x12, l0, BitVec.add_zero]

Note: This linter can be disabled with `set_option linter.unusedSimpArgs false`
warning: Submissions/UpperRiscv/MixedRoot.lean:118:6: This simp argument is unused:
  show ¬(Reg.x12 = Reg.x26) by decide

Hint: Omit it from the simp argument list.
  [apply] simp only [true_and, ne_eq, reduceCtorEq, not_false_eq_true, if_true, and_true, false_and, if_false, x12, l0,
    BitVec.add_zero]

Note: This linter can be disabled with `set_option linter.unusedSimpArgs false`
warning: Submissions/UpperRiscv/MixedRoot.lean:154:80: This simp argument is unused:
  execInstrBr

Hint: Omit it from the simp argument list.
  [apply] simp only [Riscv.LinearReady, Riscv.linearInstruction, Riscv.memoryReady, MachineState.getReg_setPC,
    getReg_setReg_ite, true_and, and_true]

Note: This linter can be disabled with `set_option linter.unusedSimpArgs false`
warning: Submissions/UpperRiscv/MixedRoot.lean:155:8: This simp argument is unused:
  MachineState.getReg_setPC

Hint: Omit it from the simp argument list.
  [apply] simp only [Riscv.LinearReady, Riscv.linearInstruction, Riscv.memoryReady, execInstrBr, getReg_setReg_ite,
    true_and, and_true]

Note: This linter can be disabled with `set_option linter.unusedSimpArgs false`
warning: Submissions/UpperRiscv/MixedRoot.lean:155:35: This simp argument is unused:
  getReg_setReg_ite

Hint: Omit it from the simp argument list.
  [apply] simp only [Riscv.LinearReady, Riscv.linearInstruction, Riscv.memoryReady, execInstrBr,
    MachineState.getReg_setPC, true_and, and_true]

Note: This linter can be disabled with `set_option linter.unusedSimpArgs false`
warning: Submissions/UpperRiscv/MixedRoot.lean:164:16: This simp argument is unused:
  Ne.symm hr

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

Note: This linter can be disabled with `set_option linter.unusedSimpArgs false`
warning: Submissions/UpperRiscv/MixedRoot.lean:169:17: This simp argument is unused:
  true_and

Hint: Omit it from the simp argument list.
  [apply] simp only [ne_eq, reduceCtorEq, not_false_eq_true, if_true, and_true, false_and, if_false,
    show ¬(Reg.x12 = Reg.x28) by decide]

Note: This linter can be disabled with `set_option linter.unusedSimpArgs false`
warning: Submissions/UpperRiscv/MixedRoot.lean:169:86: This simp argument is unused:
  false_and

Hint: Omit it from the simp argument list.
  [apply] simp only [true_and, ne_eq, reduceCtorEq, not_false_eq_true, if_true, and_true, if_false,
    show ¬(Reg.x12 = Reg.x28) by decide]

Note: This linter can be disabled with `set_option linter.unusedSimpArgs false`
warning: Submissions/UpperRiscv/MixedRoot.lean:169:97: This simp argument is unused:
  if_false

Hint: Omit it from the simp argument list.
  [apply] simp only [true_and, ne_eq, reduceCtorEq, not_false_eq_true, if_true, and_true, false_and,
    show ¬(Reg.x12 = Reg.x28) by decide]

Note: This linter can be disabled with `set_option linter.unusedSimpArgs false`
warning: Submissions/UpperRiscv/MixedRoot.lean:170:8: This simp argument is unused:
  show ¬(Reg.x12 = Reg.x28) by decide

Hint: Omit it from the simp argument list.
  [apply] simp only [true_and, ne_eq, reduceCtorEq, not_false_eq_true, if_true, and_true, false_and, if_false]

Note: This linter can be disabled with `set_option linter.unusedSimpArgs false`
warning: Submissions/UpperRiscv/MixedRoot.lean:296:10: This simp argument is unused:
  Ne.symm h10

Hint: Omit it from the simp argument list.
  [apply] simp [Ne.symm h11, h10, h11]

Note: This linter can be disabled with `set_option linter.unusedSimpArgs false`
warning: Submissions/UpperRiscv/MixedRoot.lean:296:23: This simp argument is unused:
  Ne.symm h11

Hint: Omit it from the simp argument list.
  [apply] simp [Ne.symm h10, h10, h11]

Note: This linter can be disabled with `set_option linter.unusedSimpArgs false`
warning: Submissions/UpperRiscv/MixedRoot.lean:312:44: This simp argument is unused:
  show ¬(Reg.x11 = Reg.x12) by decide

Hint: Omit it from the simp argument list.
  [apply] simp only [true_and, ne_eq, reduceCtorEq, not_false_eq_true, if_true, false_and, if_false,
    show ¬(Reg.x13 = Reg.x10) by decide, show ¬(Reg.x13 = Reg.x12) by decide, show ¬(Reg.x13 = Reg.x11) by decide]

Note: This linter can be disabled with `set_option linter.unusedSimpArgs false`
warning: Submissions/UpperRiscv/MixedRoot.lean:313:6: This simp argument is unused:
  show ¬(Reg.x13 = Reg.x12) by decide

Hint: Omit it from the simp argument list.
  [apply] simp only [true_and, ne_eq, reduceCtorEq, not_false_eq_true, if_true, false_and, if_false,
    show ¬(Reg.x13 = Reg.x10) by decide, show ¬(Reg.x11 = Reg.x12) by decide, show ¬(Reg.x13 = Reg.x11) by decide]

Note: This linter can be disabled with `set_option linter.unusedSimpArgs false`
warning: Submissions/UpperRiscv/MixedRoot.lean:313:44: This simp argument is unused:
  show ¬(Reg.x13 = Reg.x11) by decide

Hint: Omit it from the simp argument list.
  [apply] simp only [true_and, ne_eq, reduceCtorEq, not_false_eq_true, if_true, false_and, if_false,
    show ¬(Reg.x13 = Reg.x10) by decide, show ¬(Reg.x11 = Reg.x12) by decide, show ¬(Reg.x13 = Reg.x12) by decide]

Note: This linter can be disabled with `set_option linter.unusedSimpArgs false`
⚠ [8888/8900] Built Submissions.UpperRiscv.MixedRootMemory (4.1s)
warning: Submissions/UpperRiscv/MixedRootMemory.lean:60:22: Used `tac1 <;> tac2` where `(tac1; tac2)` would suffice

Note: This linter can be disabled with `set_option linter.unnecessarySeqFocus false`
warning: Submissions/UpperRiscv/MixedRootMemory.lean:60:34: Used `tac1 <;> tac2` where `(tac1; tac2)` would suffice

Note: This linter can be disabled with `set_option linter.unnecessarySeqFocus false`
✔ [8889/8900] Built Submissions.UpperRiscv.MixedChainFrame (3.9s)
✔ [8890/8900] Built Submissions.UpperRiscv.MixedCode (35s)
✔ [8891/8900] Built Submissions.UpperRiscv.MixedPrepare (4.2s)
✔ [8892/8900] Built Submissions.UpperRiscv.MixedCost (4.2s)
✔ [8893/8900] Built Submissions.UpperRiscv.MixedDispatch (4.6s)
⚠ [8894/8900] Built Submissions.UpperRiscv.MixedChain (5.1s)
warning: Submissions/UpperRiscv/MixedChain.lean:50:15: This simp argument is unused:
  Bool.false_eq_true

Hint: Omit it from the simp argument list.
  [apply] simp only [↓reduceIte, entryNodes, hn, if_true, earlyHash, Nat.mul_one] at bound ⊢

Note: This linter can be disabled with `set_option linter.unusedSimpArgs false`
warning: Submissions/UpperRiscv/MixedChain.lean:50:63: This simp argument is unused:
  if_true

Hint: Omit it from the simp argument list.
  [apply] simp only [Bool.false_eq_true, ↓reduceIte, entryNodes, hn, earlyHash, Nat.mul_one] at bound ⊢

Note: This linter can be disabled with `set_option linter.unusedSimpArgs false`
warning: Submissions/UpperRiscv/MixedChain.lean:67:63: This simp argument is unused:
  if_false

Hint: Omit it from the simp argument list.
  [apply] simp only [Bool.false_eq_true, ↓reduceIte, entryNodes, hn, runNodes', pure_bind, earlyHash, Nat.mul_zero,
    Nat.add_zero] at bound ⊢

Note: This linter can be disabled with `set_option linter.unusedSimpArgs false`
warning: Submissions/UpperRiscv/MixedChain.lean:71:97: This simp argument is unused:
  if_false

Hint: Omit it from the simp argument list.
  [apply] simp only [Bool.false_eq_true, ↓reduceIte, wireSlot, hn]

Note: This linter can be disabled with `set_option linter.unusedSimpArgs false`
warning: Submissions/UpperRiscv/MixedChain.lean:101:17: This simp argument is unused:
  Bool.false_eq_true

Hint: Omit it from the simp argument list.
  [apply] simp only [↓reduceIte, remaining, earlyHash, hn, if_true]

Note: This linter can be disabled with `set_option linter.unusedSimpArgs false`
warning: Submissions/UpperRiscv/MixedChain.lean:101:75: This simp argument is unused:
  if_true

Hint: Omit it from the simp argument list.
  [apply] simp only [Bool.false_eq_true, ↓reduceIte, remaining, earlyHash, hn]

Note: This linter can be disabled with `set_option linter.unusedSimpArgs false`
warning: Submissions/UpperRiscv/MixedChain.lean:104:15: This simp argument is unused:
  Bool.false_eq_true

Hint: Omit it from the simp argument list.
  [apply] simp only [↓reduceIte, tableNodes, entryCursor, hn, if_true, suffixNodes]

Note: This linter can be disabled with `set_option linter.unusedSimpArgs false`
warning: Submissions/UpperRiscv/MixedChain.lean:104:76: This simp argument is unused:
  if_true

Hint: Omit it from the simp argument list.
  [apply] simp only [Bool.false_eq_true, ↓reduceIte, tableNodes, entryCursor, hn, suffixNodes]

Note: This linter can be disabled with `set_option linter.unusedSimpArgs false`
warning: Submissions/UpperRiscv/MixedChain.lean:109:114: This simp argument is unused:
  if_false

Hint: Omit it from the simp argument list.
  [apply] simp only [Bool.false_eq_true, ↓reduceIte, remaining, earlyHash, hn, Nat.sub_zero]

Note: This linter can be disabled with `set_option linter.unusedSimpArgs false`
warning: Submissions/UpperRiscv/MixedChain.lean:110:97: This simp argument is unused:
  if_false

Hint: Omit it from the simp argument list.
  [apply] simp only [Bool.false_eq_true, ↓reduceIte, wireSlot, hn]

Note: This linter can be disabled with `set_option linter.unusedSimpArgs false`
warning: Submissions/UpperRiscv/MixedChain.lean:112:76: This simp argument is unused:
  if_false

Hint: Omit it from the simp argument list.
  [apply] simp only [Bool.false_eq_true, ↓reduceIte, tableNodes, entryCursor, hn, Nat.add_zero]

Note: This linter can be disabled with `set_option linter.unusedSimpArgs false`
✔ [8895/8900] Built Submissions.UpperRiscv.MixedLanding (4.1s)
✔ [8896/8900] Built Submissions.UpperRiscv.MixedPair (5.8s)
✔ [8897/8900] Built Submissions.UpperRiscv.MixedPhase (5.5s)
✔ [8898/8900] Built Submissions.UpperRiscv.MixedVerifier (4.0s)
✔ [8899/8900] Built Submissions.UpperRiscv.Candidate (3.8s)
✔ [8900/8900] Built Submissions.UpperRiscv.Solution (3.8s)
Build completed successfully (8900 jobs).
Exporting #[OptimalOTS.Challenge.UpperRiscv.certificate, OptimalOTS.Challenge.UpperRiscv.image_size, 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.UpperRiscv.submission] from Submissions.UpperRiscv.Solution
Running Lean default kernel on solution.
Lean default kernel accepts the solution
Your solution is okay!