Building OptimalOTS.Challenge.UpperRiscv
⚠ [2703/2703] Built OptimalOTS.Challenge.UpperRiscv (2.3s)
warning: OptimalOTS/Challenge/UpperRiscv.lean:9:18: declaration uses `sorry`
warning: OptimalOTS/Challenge/UpperRiscv.lean:13:8: declaration uses `sorry`
Build completed successfully (2703 jobs).
Exporting #[OptimalOTS.Challenge.UpperRiscv.certificate, 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
✔ [8811/8877] Built Submissions.UpperRiscv.TypedScheme (2.9s)
✔ [8813/8877] Built Submissions.UpperRiscv.Semantics (2.9s)
✔ [8814/8877] Built Submissions.UpperRiscv.Cache (2.9s)
✔ [8815/8877] Built Submissions.UpperRiscv.MachineCost (2.8s)
✔ [8816/8877] Built Submissions.UpperRiscv.IUB (2.2s)
✔ [8817/8877] Built Submissions.UpperRiscv.BlockExecution (3.1s)
✔ [8818/8877] Built Submissions.UpperRiscv.Master (2.5s)
✔ [8819/8877] Built Submissions.UpperRiscv.Count (8.3s)
✔ [8820/8877] Built Submissions.UpperRiscv.Constants (8.5s)
⚠ [8821/8877] Built Submissions.UpperRiscv.RowIneq (14s)
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`
⚠ [8822/8877] Built Submissions.UpperRiscv.Names (7.2s)
warning: Submissions/UpperRiscv/Names.lean:114: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:117: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:117: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:126: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`
✔ [8823/8877] Built Submissions.UpperRiscv.Program (10s)
⚠ [8824/8877] Built Submissions.UpperRiscv.Tree (4.6s)
warning: Submissions/UpperRiscv/Tree.lean:317:72: Used `tac1 <;> tac2` where `(tac1; tac2)` would suffice

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

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

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

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

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

Note: This linter can be disabled with `set_option linter.unnecessarySeqFocus false`
warning: Submissions/UpperRiscv/Tree.lean:341: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`
✔ [8825/8877] Built Submissions.UpperRiscv.AssemblyMacros (4.1s)
⚠ [8826/8877] Built Submissions.UpperRiscv.Cuts (4.2s)
warning: Submissions/UpperRiscv/Cuts.lean:74:67: This simp argument is unused:
  reduceCtorEq

Hint: Omit it from the simp argument list.
  [apply] simp only [Name.src.injEq, Name.cv.injEq] at equal

Note: This linter can be disabled with `set_option linter.unusedSimpArgs false`
✔ [8827/8877] Built Submissions.UpperRiscv.Refines (3.0s)
✔ [8828/8877] Built Submissions.UpperRiscv.Valid (52s)
✔ [8829/8877] Built Submissions.UpperRiscv.FixedChoice (3.8s)
✔ [8830/8877] Built Submissions.UpperRiscv.GScheme (3.0s)
⚠ [8831/8877] Built Submissions.UpperRiscv.Lanes (5.5s)
warning: Submissions/UpperRiscv/Lanes.lean:35:28: Variable name `hx` 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] _hx

Note: This linter can be disabled with `set_option linter.unusedVariables false`
⚠ [8832/8877] Built Submissions.UpperRiscv.Adapter (4.9s)
warning: Submissions/UpperRiscv/Adapter.lean:76: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:92: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`
✔ [8833/8877] Built Submissions.UpperRiscv.Scheme (5.4s)
✔ [8834/8877] Built Submissions.UpperRiscv.KeygenSupport (5.0s)
✔ [8835/8877] Built Submissions.UpperRiscv.Reconstruct (6.6s)
✔ [8836/8877] Built Submissions.UpperRiscv.SignIdx (6.9s)
✔ [8837/8877] Built Submissions.UpperRiscv.Keygen (7.2s)
✔ [8838/8877] Built Submissions.UpperRiscv.AlgorithmCosts (5.1s)
✔ [8839/8877] Built Submissions.UpperRiscv.Deterministic (5.5s)
✔ [8840/8877] Built Submissions.UpperRiscv.Correctness (5.7s)
✔ [8841/8877] Built Submissions.UpperRiscv.EncCharges (5.0s)
✔ [8842/8877] Built Submissions.UpperRiscv.Values (7.1s)
✔ [8843/8877] Built Submissions.UpperRiscv.Resources (5.5s)
✔ [8844/8877] Built Submissions.UpperRiscv.WireAdapter (6.2s)
⚠ [8845/8877] Built Submissions.UpperRiscv.Events (5.4s)
warning: Submissions/UpperRiscv/Events.lean:113:72: Used `tac1 <;> tac2` where `(tac1; tac2)` would suffice

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

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

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

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

Note: This linter can be disabled with `set_option linter.unnecessarySeqFocus false`
⚠ [8846/8877] Built Submissions.UpperRiscv.Resample (5.8s)
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: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/UpperRiscv/Resample.lean:467: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:500: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`
⚠ [8847/8877] Built Submissions.UpperRiscv.SignRho (7.0s)
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`
⚠ [8848/8877] Built Submissions.UpperRiscv.Rows (4.5s)
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`
✔ [8849/8877] Built Submissions.UpperRiscv.MachineMemory (20s)
✔ [8850/8877] Built Submissions.UpperRiscv.LoaderProof (5.7s)
⚠ [8851/8877] Built Submissions.UpperRiscv.RowPotential (8.0s)
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`
✔ [8852/8877] Built Submissions.UpperRiscv.CopyProof (4.0s)
✔ [8853/8877] Built Submissions.UpperRiscv.HashOutput (4.0s)
⚠ [8854/8877] Built Submissions.UpperRiscv.Potentials (4.7s)
warning: Submissions/UpperRiscv/Potentials.lean:121: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`
⚠ [8855/8877] Built Submissions.UpperRiscv.MachineFacts (4.5s)
warning: Submissions/UpperRiscv/MachineFacts.lean:75: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`
✔ [8856/8877] Built Submissions.UpperRiscv.StageB (5.1s)
✔ [8857/8877] Built Submissions.UpperRiscv.Assembly (4.2s)
✔ [8858/8877] Built Submissions.UpperRiscv.Main (4.0s)
⚠ [8859/8877] Built Submissions.UpperRiscv.Availability (4.5s)
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`
✔ [8860/8877] Built Submissions.UpperRiscv.ForestAlgorithm (3.8s)
✔ [8861/8877] Built Submissions.UpperRiscv.Wire (3.7s)
✔ [8862/8877] Built Submissions.UpperRiscv.Layout (3.8s)
✔ [8863/8877] Built Submissions.UpperRiscv.ForestVerifier (4.6s)
✔ [8864/8877] Built Submissions.UpperRiscv.ForestVerifierProof (3.9s)
✔ [8865/8877] Built Submissions.UpperRiscv.Reader (3.0s)
✔ [8866/8877] Built Submissions.UpperRiscv.ChainContext (4.0s)
✔ [8867/8877] Built Submissions.UpperRiscv.ChainPrologue (5.9s)
⚠ [8868/8877] Built Submissions.UpperRiscv.IndexLanes (7.1s)
warning: Submissions/UpperRiscv/IndexLanes.lean:61:4: Unused tactic linter: `(try constructor)` does nothing

Note: This linter can be disabled with `set_option linter.unusedTactic false`
⚠ [8869/8877] Built Submissions.UpperRiscv.ChainSteps (5.3s)
warning: Submissions/UpperRiscv/ChainSteps.lean:67:48: Unused tactic linter: `omega` does nothing

Note: This linter can be disabled with `set_option linter.unusedTactic false`
warning: Submissions/UpperRiscv/ChainSteps.lean:67:48: this tactic is never executed

Note: This linter can be disabled with `set_option linter.unreachableTactic false`
✔ [8870/8877] Built Submissions.UpperRiscv.IndexArith (5.1s)
⚠ [8871/8877] Built Submissions.UpperRiscv.ChainBlock (6.8s)
warning: Submissions/UpperRiscv/ChainBlock.lean:30:25: This simp argument is unused:
  tripleN

Hint: Omit it from the simp argument list.
  [apply] simp only [chainNodes, List.finRange, List.range]

Note: This linter can be disabled with `set_option linter.unusedSimpArgs false`
warning: Submissions/UpperRiscv/ChainBlock.lean:306: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, show ¬(Reg.x12 = Reg.x10) by decide,
    if_false, inv.slot, signExtend12_nat _ (show (if k.val = 0 then 136 else 24) < 2048 by split_ifs <;> norm_num),
    W_add, prevSlot_step k k.isLt]

Note: This linter can be disabled with `set_option linter.unusedSimpArgs false`
✔ [8872/8877] Built Submissions.UpperRiscv.ChainPhase (5.7s)
⚠ [8873/8877] Built Submissions.UpperRiscv.IndexPhase (11s)
warning: Submissions/UpperRiscv/IndexPhase.lean:113:53: This simp argument is unused:
  l16

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

Note: This linter can be disabled with `set_option linter.unusedSimpArgs false`
warning: Submissions/UpperRiscv/IndexPhase.lean:115:53: This simp argument is unused:
  l0

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

Note: This linter can be disabled with `set_option linter.unusedSimpArgs false`
warning: Submissions/UpperRiscv/IndexPhase.lean:117:53: This simp argument is unused:
  l8

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

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

Hint: Omit it from the simp argument list.
  [apply] simp [lenBlock, execInstrBr, getReg_setReg_ite, hr, S2_regs]

Note: This linter can be disabled with `set_option linter.unusedSimpArgs false`
⚠ [8874/8877] Built Submissions.UpperRiscv.RootPhase (4.0s)
warning: Submissions/UpperRiscv/RootPhase.lean:80:53: This simp argument is unused:
  show ¬(Reg.x12 = Reg.x28) by decide

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

Note: This linter can be disabled with `set_option linter.unusedSimpArgs false`
warning: Submissions/UpperRiscv/RootPhase.lean:92: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, show ¬(Reg.x10 = Reg.x26) by decide,
    show ¬(Reg.x10 = Reg.x28) by decide, show ¬(Reg.x26 = Reg.x28) by decide, show ¬(Reg.x28 = Reg.x26) by decide,
    show ¬(Reg.x30 = Reg.x26) by decide, show ¬(Reg.x31 = Reg.x28) by decide, show ¬(Reg.x31 = Reg.x26) by decide,
    show ¬(Reg.x12 = Reg.x26) by decide, show ¬(Reg.x12 = Reg.x28) by decide, false_and, if_false, x12, l0, l8,
    BitVec.add_zero, W_add, pk0, pk1]

Note: This linter can be disabled with `set_option linter.unusedSimpArgs false`
warning: Submissions/UpperRiscv/RootPhase.lean:97:6: 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,
    show ¬(Reg.x10 = Reg.x26) by decide, show ¬(Reg.x10 = Reg.x28) by decide, show ¬(Reg.x26 = Reg.x28) by decide,
    show ¬(Reg.x28 = Reg.x26) by decide, show ¬(Reg.x30 = Reg.x26) by decide, show ¬(Reg.x31 = Reg.x28) by decide,
    show ¬(Reg.x31 = Reg.x26) by decide, show ¬(Reg.x12 = Reg.x26) by decide, false_and, if_false, x12, l0, l8,
    BitVec.add_zero, W_add, pk0, pk1]

Note: This linter can be disabled with `set_option linter.unusedSimpArgs false`
warning: Submissions/UpperRiscv/RootPhase.lean:97:44: 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,
    show ¬(Reg.x10 = Reg.x26) by decide, show ¬(Reg.x10 = Reg.x28) by decide, show ¬(Reg.x26 = Reg.x28) by decide,
    show ¬(Reg.x28 = Reg.x26) by decide, show ¬(Reg.x30 = Reg.x26) by decide, show ¬(Reg.x31 = Reg.x28) by decide,
    show ¬(Reg.x31 = Reg.x26) by decide, show ¬(Reg.x12 = Reg.x26) by decide, show ¬(Reg.x12 = Reg.x28) by decide,
    if_false, x12, l0, l8, BitVec.add_zero, W_add, pk0, pk1]

Note: This linter can be disabled with `set_option linter.unusedSimpArgs false`
warning: Submissions/UpperRiscv/RootPhase.lean:155: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/RootPhase.lean:155: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`
✔ [8875/8877] Built Submissions.UpperRiscv.Verifier (4.3s)
✔ [8876/8877] Built Submissions.UpperRiscv.Candidate (3.6s)
✔ [8877/8877] Built Submissions.UpperRiscv.Solution (3.7s)
Build completed successfully (8877 jobs).
Exporting #[OptimalOTS.Challenge.UpperRiscv.certificate, 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!