Building OptimalOTS.Challenge.UpperRiscv ⚠ [2703/2703] Built OptimalOTS.Challenge.UpperRiscv (1.8s) 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 ✔ [7193/7405] Built Submissions.UpperRiscv.TypedScheme (2.1s) ✔ [8813/8880] Built Submissions.UpperRiscv.MachineCost (2.6s) ✔ [8814/8880] Built Submissions.UpperRiscv.Semantics (2.0s) ✔ [8815/8880] Built Submissions.UpperRiscv.Cache (3.2s) ✔ [8816/8880] Built Submissions.UpperRiscv.IUB (2.9s) ✔ [8817/8880] Built Submissions.UpperRiscv.Digits (6.3s) ✔ [8818/8880] Built Submissions.UpperRiscv.Count (6.5s) ✔ [8819/8880] Built Submissions.UpperRiscv.BlockExecution (4.0s) ✔ [8820/8880] Built Submissions.UpperRiscv.Master (2.5s) ⚠ [8821/8880] Built Submissions.UpperRiscv.Names (8.3s) warning: Submissions/UpperRiscv/Names.lean:107: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:110: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:110: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:119: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` ⚠ [8822/8880] Built Submissions.UpperRiscv.RowIneq (13s) 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` ⚠ [8823/8880] Built Submissions.UpperRiscv.Tree (2.6s) warning: Submissions/UpperRiscv/Tree.lean:385: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` ✔ [8824/8880] Built Submissions.UpperRiscv.Cuts (4.0s) ✔ [8825/8880] Built Submissions.UpperRiscv.Valid (211s) ✔ [8826/8880] Built Submissions.UpperRiscv.FixedChoice (4.2s) ✔ [8827/8880] Built Submissions.UpperRiscv.PackFiber (4.3s) ⚠ [8828/8880] Built Submissions.UpperRiscv.GScheme (4.4s) warning: Submissions/UpperRiscv/GScheme.lean:50: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:65: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:109: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` ✔ [8829/8880] Built Submissions.UpperRiscv.KeygenSupport (4.4s) ✔ [8830/8880] Built Submissions.UpperRiscv.PackCount (5.2s) ✔ [8831/8880] Built Submissions.UpperRiscv.Scheme (5.3s) ⚠ [8832/8880] Built Submissions.UpperRiscv.Adapter (5.6s) 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/8880] Built Submissions.UpperRiscv.Reconstruct (6.2s) ✔ [8834/8880] Built Submissions.UpperRiscv.Program (10s) ✔ [8835/8880] Built Submissions.UpperRiscv.Keygen (7.2s) ✔ [8836/8880] Built Submissions.UpperRiscv.Deterministic (4.6s) ✔ [8837/8880] Built Submissions.UpperRiscv.AlgorithmCosts (5.5s) ✔ [8838/8880] Built Submissions.UpperRiscv.SignIdx (6.4s) ✔ [8839/8880] Built Submissions.UpperRiscv.AssemblyMacros (6.1s) ✔ [8840/8880] Built Submissions.UpperRiscv.Lanes (11s) ✔ [8841/8880] Built Submissions.UpperRiscv.WireAdapter (7.1s) ✔ [8842/8880] Built Submissions.UpperRiscv.Resources (7.3s) ✔ [8843/8880] Built Submissions.UpperRiscv.Correctness (7.3s) ✔ [8844/8880] Built Submissions.UpperRiscv.Refines (6.8s) ⚠ [8845/8880] Built Submissions.UpperRiscv.Values (9.6s) 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:114: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:437: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:609: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:609: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:609: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:609:77: Try `simp at hs` instead of `simpa using hs` Note: This linter can be disabled with `set_option linter.unnecessarySimpa false` ✔ [8846/8880] Built Submissions.UpperRiscv.EncCharges (12s) ✔ [8847/8880] Built Submissions.UpperRiscv.Events (4.8s) ⚠ [8848/8880] Built Submissions.UpperRiscv.Resample (5.5s) 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:195: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:227: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:374: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:384: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:539: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:589: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:601: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` ✔ [8849/8880] Built Submissions.UpperRiscv.MachineMemory (21s) ⚠ [8850/8880] Built Submissions.UpperRiscv.SignRho (7.3s) 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` ⚠ [8851/8880] Built Submissions.UpperRiscv.GoodRec (4.5s) 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:100: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:239: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` ✔ [8852/8880] Built Submissions.UpperRiscv.LoaderProof (5.3s) ⚠ [8853/8880] Built Submissions.UpperRiscv.Rows (4.8s) 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` ✔ [8854/8880] Built Submissions.UpperRiscv.HashOutput (4.1s) ✔ [8855/8880] Built Submissions.UpperRiscv.CopyProof (4.1s) ⚠ [8856/8880] Built Submissions.UpperRiscv.MachineFacts (4.4s) 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` ⚠ [8857/8880] 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` ⚠ [8858/8880] Built Submissions.UpperRiscv.Potentials (4.4s) 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` ✔ [8859/8880] Built Submissions.UpperRiscv.StageB (4.0s) ✔ [8860/8880] Built Submissions.UpperRiscv.Assembly (4.3s) ✔ [8861/8880] Built Submissions.UpperRiscv.Main (4.0s) ⚠ [8862/8880] 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` ✔ [8863/8880] Built Submissions.UpperRiscv.ForestAlgorithm (3.7s) ✔ [8864/8880] Built Submissions.UpperRiscv.Wire (3.8s) ✔ [8865/8880] Built Submissions.UpperRiscv.Layout (3.7s) ✔ [8866/8880] Built Submissions.UpperRiscv.ForestVerifier (4.8s) ✔ [8867/8880] Built Submissions.UpperRiscv.ForestVerifierProof (3.9s) ✔ [8868/8880] Built Submissions.UpperRiscv.Reader (3.8s) ✔ [8869/8880] Built Submissions.UpperRiscv.ChainContext (4.1s) ⚠ [8870/8880] Built Submissions.UpperRiscv.ChainPrologue (4.9s) warning: Submissions/UpperRiscv/ChainPrologue.lean:96: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.x10 = Reg.x28) by decide, show ¬(Reg.x10 = Reg.x12) by decide, step0] Note: This linter can be disabled with `set_option linter.unusedSimpArgs false` warning: Submissions/UpperRiscv/ChainPrologue.lean:96: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.x10 = Reg.x28) by decide, show ¬(Reg.x10 = Reg.x12) by decide, step0] Note: This linter can be disabled with `set_option linter.unusedSimpArgs false` warning: Submissions/UpperRiscv/ChainPrologue.lean:100: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.x28) by decide, show ¬(Reg.x12 = Reg.x10) by decide, step0, s8] Note: This linter can be disabled with `set_option linter.unusedSimpArgs false` warning: Submissions/UpperRiscv/ChainPrologue.lean:100: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.x28) by decide, show ¬(Reg.x12 = Reg.x10) by decide, step0, s8] Note: This linter can be disabled with `set_option linter.unusedSimpArgs false` warning: Submissions/UpperRiscv/ChainPrologue.lean:103:74: This simp argument is unused: MachineState.getMem_setPC Hint: Omit it from the simp argument list. [apply] simp only [execInstrBr, MachineState.getReg_setPC, getReg_setReg_ite, MachineState.getMem_setReg] Note: This linter can be disabled with `set_option linter.unusedSimpArgs false` warning: Submissions/UpperRiscv/ChainPrologue.lean:104:6: This simp argument is unused: MachineState.getMem_setReg Hint: Omit it from the simp argument list. [apply] simp only [execInstrBr, MachineState.getReg_setPC, getReg_setReg_ite, MachineState.getMem_setPC] Note: This linter can be disabled with `set_option linter.unusedSimpArgs false` warning: Submissions/UpperRiscv/ChainPrologue.lean:105: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.x10) by decide, step0, s8, lane] Note: This linter can be disabled with `set_option linter.unusedSimpArgs false` warning: Submissions/UpperRiscv/ChainPrologue.lean:105: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.x10) by decide, step0, s8, lane] Note: This linter can be disabled with `set_option linter.unusedSimpArgs false` warning: Submissions/UpperRiscv/ChainPrologue.lean:127:13: 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.x10) by decide, step0, s8, lane_offset k hk] Note: This linter can be disabled with `set_option linter.unusedSimpArgs false` warning: Submissions/UpperRiscv/ChainPrologue.lean:127:82: 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.x10) by decide, step0, s8, lane_offset k hk] Note: This linter can be disabled with `set_option linter.unusedSimpArgs false` ⚠ [8871/8880] Built Submissions.UpperRiscv.IndexLanes (7.2s) warning: Submissions/UpperRiscv/IndexLanes.lean:76:4: Unused tactic linter: `(try constructor)` does nothing Note: This linter can be disabled with `set_option linter.unusedTactic false` ✔ [8872/8880] Built Submissions.UpperRiscv.ChainSteps (4.6s) ✖ [8873/8880] Building Submissions.UpperRiscv.IndexArith (4.7s) trace: .> LEAN_PATH=/srv/ots-work/b94a12f44f31b4342a1b1c5b20c6de33/project/formal/.lake/packages/Cli/.lake/build/lib/lean:/srv/ots-work/b94a12f44f31b4342a1b1c5b20c6de33/project/formal/.lake/packages/cslib/.lake/build/lib/lean:/srv/ots-work/b94a12f44f31b4342a1b1c5b20c6de33/project/formal/.lake/packages/batteries/.lake/build/lib/lean:/srv/ots-work/b94a12f44f31b4342a1b1c5b20c6de33/project/formal/.lake/packages/Qq/.lake/build/lib/lean:/srv/ots-work/b94a12f44f31b4342a1b1c5b20c6de33/project/formal/.lake/packages/aesop/.lake/build/lib/lean:/srv/ots-work/b94a12f44f31b4342a1b1c5b20c6de33/project/formal/.lake/packages/proofwidgets/.lake/build/lib/lean:/srv/ots-work/b94a12f44f31b4342a1b1c5b20c6de33/project/formal/.lake/packages/importGraph/.lake/build/lib/lean:/srv/ots-work/b94a12f44f31b4342a1b1c5b20c6de33/project/formal/.lake/packages/LeanSearchClient/.lake/build/lib/lean:/srv/ots-work/b94a12f44f31b4342a1b1c5b20c6de33/project/formal/.lake/packages/plausible/.lake/build/lib/lean:/srv/ots-work/b94a12f44f31b4342a1b1c5b20c6de33/project/formal/.lake/packages/loom2/.lake/build/lib/lean:/srv/ots-work/b94a12f44f31b4342a1b1c5b20c6de33/project/formal/.lake/packages/PolyFun/.lake/build/lib/lean:/srv/ots-work/b94a12f44f31b4342a1b1c5b20c6de33/project/formal/.lake/packages/mathlib/.lake/build/lib/lean:/srv/ots-work/b94a12f44f31b4342a1b1c5b20c6de33/project/formal/.lake/packages/Sail/.lake/build/lib/lean:/srv/ots-work/b94a12f44f31b4342a1b1c5b20c6de33/project/formal/.lake/packages/VCVio/.lake/build/lib/lean:/srv/ots-work/b94a12f44f31b4342a1b1c5b20c6de33/project/formal/.lake/packages/riscv-zkvm/.lake/build/lib/lean:/srv/ots-work/b94a12f44f31b4342a1b1c5b20c6de33/project/formal/.lake/build/lib/lean /srv/ots/.elan/toolchains/leanprover--lean4---v4.33.1/bin/lean /srv/ots-work/b94a12f44f31b4342a1b1c5b20c6de33/project/formal/Submissions/UpperRiscv/IndexArith.lean -o /srv/ots-work/b94a12f44f31b4342a1b1c5b20c6de33/project/formal/.lake/build/lib/lean/Submissions/UpperRiscv/IndexArith.olean -i /srv/ots-work/b94a12f44f31b4342a1b1c5b20c6de33/project/formal/.lake/build/lib/lean/Submissions/UpperRiscv/IndexArith.ilean -c /srv/ots-work/b94a12f44f31b4342a1b1c5b20c6de33/project/formal/.lake/build/ir/Submissions/UpperRiscv/IndexArith.c --setup /srv/ots-work/b94a12f44f31b4342a1b1c5b20c6de33/project/formal/.lake/build/ir/Submissions/UpperRiscv/IndexArith.setup.json --json error: Submissions/UpperRiscv/IndexArith.lean:32:46: unsolved goals u p : ℕ ⊢ u / 2 ^ p % 1 = 0 warning: Submissions/UpperRiscv/IndexArith.lean:153:53: Variable name `hk` 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] _hk Note: This linter can be disabled with `set_option linter.unusedVariables false` error: Lean exited with code 1 ⚠ [8875/8880] Built Submissions.UpperRiscv.ChainBlock (6.7s) 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:165:29: This simp argument is unused: lowCat Hint: Omit it from the simp argument list. [apply] simp only [Nat.sub_self] at next ⊢ Note: This linter can be disabled with `set_option linter.unusedSimpArgs false` warning: Submissions/UpperRiscv/ChainBlock.lean:417:9: Unused tactic linter: `unfold slotAddr` does nothing Note: This linter can be disabled with `set_option linter.unusedTactic false` warning: Submissions/UpperRiscv/ChainBlock.lean:417:26: Unused tactic linter: `omega` does nothing Note: This linter can be disabled with `set_option linter.unusedTactic false` warning: Submissions/UpperRiscv/ChainBlock.lean:417:26: this tactic is never executed Note: This linter can be disabled with `set_option linter.unreachableTactic false` ✔ [8876/8880] Built Submissions.UpperRiscv.ChainPhase (5.5s) Some required targets logged failures: - Submissions.UpperRiscv.IndexArith error: build failed uncaught exception: Child exited with 1