import%20marimo%0A%0A__generated_with%20%3D%20%220.25.2%22%0Aapp%20%3D%20marimo.App(width%3D%22medium%22)%0A%0A%0A%40app.cell(hide_code%3DTrue)%0Adef%20_()%3A%0A%20%20%20%20import%20statistics%0A%20%20%20%20import%20sys%0A%20%20%20%20import%20time%0A%20%20%20%20from%20pathlib%20import%20Path%0A%0A%20%20%20%20import%20marimo%20as%20mo%0A%20%20%20%20import%20numpy%20as%20np%0A%0A%20%20%20%20start%20%3D%20Path(__file__).resolve().parent%20if%20%22__file__%22%20in%20globals()%20else%20Path.cwd().resolve()%0A%20%20%20%20for%20candidate%20in%20(start%2C%20*start.parents)%3A%0A%20%20%20%20%20%20%20%20if%20(candidate%20%2F%20%22fomtools%22).is_dir()%3A%0A%20%20%20%20%20%20%20%20%20%20%20%20repo_root%20%3D%20candidate%0A%20%20%20%20%20%20%20%20%20%20%20%20break%0A%20%20%20%20else%3A%0A%20%20%20%20%20%20%20%20repo_root%20%3D%20start%0A%0A%20%20%20%20if%20str(repo_root)%20not%20in%20sys.path%3A%0A%20%20%20%20%20%20%20%20sys.path.insert(0%2C%20str(repo_root))%0A%0A%20%20%20%20examples_dir%20%3D%20repo_root%20%2F%20%22examples%22%0A%0A%20%20%20%20from%20docs.tutorials.helper_functions.lasso%20import%20(%0A%20%20%20%20%20%20%20%20ista_step%2C%0A%20%20%20%20%20%20%20%20make_lasso_data%2C%0A%20%20%20%20%20%20%20%20solve_ista_numpy%2C%0A%20%20%20%20)%0A%20%20%20%20from%20docs.tutorials.helper_functions.codegen_benchmarks%20import%20(%0A%20%20%20%20%20%20%20%20run_lasso_codegen_benchmark%2C%0A%20%20%20%20)%0A%20%20%20%20from%20fomtools.codegen%20import%20CodegenConfig%2C%20TerminationSpec%0A%20%20%20%20import%20fomtools%20as%20ft%0A%0A%20%20%20%20timing_file%20%3D%20start%20%2F%20%22_recorded_timings.json%22%0A%0A%20%20%20%20np.set_printoptions(precision%3D5)%0A%20%20%20%20np.set_printoptions(suppress%3DTrue)%0A%20%20%20%20return%20(%0A%20%20%20%20%20%20%20%20CodegenConfig%2C%0A%20%20%20%20%20%20%20%20TerminationSpec%2C%0A%20%20%20%20%20%20%20%20examples_dir%2C%0A%20%20%20%20%20%20%20%20ft%2C%0A%20%20%20%20%20%20%20%20ista_step%2C%0A%20%20%20%20%20%20%20%20make_lasso_data%2C%0A%20%20%20%20%20%20%20%20mo%2C%0A%20%20%20%20%20%20%20%20np%2C%0A%20%20%20%20%20%20%20%20run_lasso_codegen_benchmark%2C%0A%20%20%20%20%20%20%20%20solve_ista_numpy%2C%0A%20%20%20%20%20%20%20%20statistics%2C%0A%20%20%20%20%20%20%20%20time%2C%0A%20%20%20%20%20%20%20%20timing_file%2C%0A%20%20%20%20)%0A%0A%0A%40app.cell(hide_code%3DTrue)%0Adef%20_(mo)%3A%0A%20%20%20%20mo.md(r%22%22%22%0A%20%20%20%20%23%20Lasso%3A%20Python%20vs%20Codegen%0A%0A%20%20%20%20%5BBack%20to%20the%20code%20generation%20tutorials%5D(.%2F)%0A%0A%20%20%20%20In%20this%20tutorial%20we%20benchmark%20iterative%20soft-thresholding%20for%20the%20Lasso%20problem%3A%0A%0A%20%20%20%20%5Cbegin%7Barray%7D%7Bll%7D%0A%20%20%20%20%20%20%20%20%5Ctext%7Bminimize%7D%20%26%20(1%2F2)%5C%7CDz%20-%20x%5C%7C_2%5E2%20%2B%20%5Clambda%20%5C%7Cz%5C%7C_1%2C%0A%20%20%20%20%5Cend%7Barray%7D%0A%0A%20%20%20%20where%20%24D%20%5Cin%20%5Cmathbf%7BR%7D%5E%7Bp%20%5Ctimes%20n%7D%24%2C%20%24z%20%5Cin%20%5Cmathbf%7BR%7D%5En%24%20is%20the%20decision%20variable%2C%20and%20%24x%20%5Cin%20%5Cmathbf%7BR%7D%5Ep%24%20is%20the%20parameter.%0A%20%20%20%20The%20method%20is%0A%0A%20%20%20%20%24%24%0A%20%20%20%20z%5E%7Bk%2B1%7D%20%3D%0A%20%20%20%20%5Cmathbf%7Bsoft%7D_%7B%5Clambda%5Ceta%7D%5Cleft(z%5Ek%20-%20%5Ceta%20D%5ET(Dz%5Ek%20-%20x)%5Cright)%2C%0A%20%20%20%20%24%24%0A%0A%20%20%20%20where%20%24%5Cmathbf%7Bsoft%7D_%5Ckappa(v)_i%20%3D%20%5Cmathbf%7Bsign%7D(v_i)%5Cmax%5C%7B%7Cv_i%7C%20-%20%5Ckappa%2C%200%5C%7D%24%20is%20the%20soft-thresholding%20operator%2C%20applied%20element-wise.%0A%0A%20%20%20%20We%20compare%20a%20direct%20NumPy%20implementation%20with%20the%20verified%20generated%20C%20solver.%0A%20%20%20%20The%20problem%20construction%2C%20ISTA%20step%2C%20and%20NumPy%20reference%20solver%20are%20shared%20with%20the%20%5BLasso%20verification%20tutorial%5D(..%2Fverification%2Flasso.html).%0A%20%20%20%20The%20generated%20C%20is%20timed%20after%20code%20generation%2C%20then%20timed%20again%20after%20the%20C-editing%20optimization%20pass.%0A%20%20%20%20%22%22%22)%0A%20%20%20%20return%0A%0A%0A%40app.cell(hide_code%3DTrue)%0Adef%20_(mo)%3A%0A%20%20%20%20mo.md(r%22%22%22%0A%20%20%20%20We%20generate%20a%20small%20sparse%20dictionary%20%24D%24%2C%20sample%20sparse%20signals%2C%20and%20use%20those%20samples%20to%20define%20the%20range%20of%20possible%20inputs%20%24x%24.%0A%20%20%20%20Both%20implementations%20run%20the%20same%20update%20rule%20for%20the%20same%20number%20of%20iterations.%0A%20%20%20%20%22%22%22)%0A%20%20%20%20return%0A%0A%0A%40app.cell%0Adef%20_(examples_dir%2C%20make_lasso_data%2C%20np)%3A%0A%20%20%20%20p%2C%20n%2C%20lambd%20%3D%203%2C%204%2C%201e-1%0A%20%20%20%20num_star%20%3D%20200%0A%20%20%20%20D%2C%20x_lb%2C%20x_ub%2C%20_%2C%20eta%2C%20lambd%20%3D%20make_lasso_data(%0A%20%20%20%20%20%20%20%20p%3Dp%2C%20n%3Dn%2C%20lambd%3Dlambd%2C%20num_signals%3Dnum_star%2C%20seed%3D0%0A%20%20%20%20)%0A%20%20%20%20x_mid%20%3D%200.5%20*%20(x_lb%20%2B%20x_ub)%0A%0A%20%20%20%20K%20%3D%20200%0A%20%20%20%20s0%20%3D%20np.zeros(n)%0A%0A%20%20%20%20out_dir%20%3D%20examples_dir%20%2F%20%22_codegen_speedups%22%20%2F%20%22lasso_codegen_speedup%22%0A%20%20%20%20return%20D%2C%20K%2C%20eta%2C%20lambd%2C%20n%2C%20out_dir%2C%20p%2C%20s0%2C%20x_lb%2C%20x_mid%2C%20x_ub%0A%0A%0A%40app.cell%0Adef%20_(%0A%20%20%20%20CodegenConfig%2C%0A%20%20%20%20D%2C%0A%20%20%20%20K%2C%0A%20%20%20%20TerminationSpec%2C%0A%20%20%20%20eta%2C%0A%20%20%20%20ft%2C%0A%20%20%20%20ista_step%2C%0A%20%20%20%20lambd%2C%0A%20%20%20%20n%2C%0A%20%20%20%20p%2C%0A%20%20%20%20s0%2C%0A%20%20%20%20x_lb%2C%0A%20%20%20%20x_ub%2C%0A)%3A%0A%20%20%20%20verifier%20%3D%20ft.Verifier(%0A%20%20%20%20%20%20%20%20method%3D%22mip%22%2C%0A%20%20%20%20%20%20%20%20solver%3D%22highs%22%2C%0A%20%20%20%20%20%20%20%20obbt_solver%3DNone%2C%0A%20%20%20%20)%0A%0A%20%20%20%20x_param%20%3D%20verifier.parameter(p%2C%20lb%3Dx_lb%2C%20ub%3Dx_ub)%0A%20%20%20%20s%20%3D%20verifier.iterate(n%2C%20lb%3Ds0%2C%20ub%3Ds0)%0A%20%20%20%20next_s%2C%20_%2C%20_%2C%20_%20%3D%20ista_step(%0A%20%20%20%20%20%20%20%20verifier%2C%20D%2C%20eta%2C%20lambd%2C%20s%2C%20s%2C%20x_param%2C%201.0%2C%20k%3D1%2C%20momentum%3DFalse%0A%20%20%20%20)%0A%0A%20%20%20%20config%20%3D%20CodegenConfig(%0A%20%20%20%20%20%20%20%20termination%3DTerminationSpec(max_iters%3DK)%2C%0A%20%20%20%20%20%20%20%20num_verify_samples%3D4%2C%0A%20%20%20%20)%0A%20%20%20%20return%20config%2C%20next_s%2C%20s%2C%20verifier%2C%20x_param%0A%0A%0A%40app.cell(hide_code%3DTrue)%0Adef%20_(D%2C%20K%2C%20eta%2C%20lambd%2C%20s0%2C%20solve_ista_numpy%2C%20statistics%2C%20time%2C%20x_mid)%3A%0A%20%20%20%20def%20python_lasso_solve()%3A%0A%20%20%20%20%20%20%20%20return%20solve_ista_numpy(D%2C%20eta%2C%20lambd%2C%20s0%2C%20x_mid%2C%20max_iters%3DK)%0A%0A%20%20%20%20for%20_%20in%20range(3)%3A%0A%20%20%20%20%20%20%20%20python_lasso_solve()%0A%0A%20%20%20%20python_times%20%3D%20%5B%5D%0A%20%20%20%20for%20_%20in%20range(40)%3A%0A%20%20%20%20%20%20%20%20t0%20%3D%20time.perf_counter()%0A%20%20%20%20%20%20%20%20python_lasso_solve()%0A%20%20%20%20%20%20%20%20python_times.append((time.perf_counter()%20-%20t0)%20*%201.0e6)%0A%0A%20%20%20%20python_us%20%3D%20statistics.median(python_times)%0A%20%20%20%20return%20(python_us%2C)%0A%0A%0A%40app.cell(hide_code%3DTrue)%0Adef%20_(%0A%20%20%20%20config%2C%0A%20%20%20%20next_s%2C%0A%20%20%20%20out_dir%2C%0A%20%20%20%20python_us%2C%0A%20%20%20%20run_lasso_codegen_benchmark%2C%0A%20%20%20%20s%2C%0A%20%20%20%20timing_file%2C%0A%20%20%20%20verifier%2C%0A%20%20%20%20x_param%2C%0A)%3A%0A%20%20%20%20timings%20%3D%20run_lasso_codegen_benchmark(%0A%20%20%20%20%20%20%20%20config%3Dconfig%2C%0A%20%20%20%20%20%20%20%20next_state%3Dnext_s%2C%0A%20%20%20%20%20%20%20%20out_dir%3Dout_dir%2C%0A%20%20%20%20%20%20%20%20python_us%3Dpython_us%2C%0A%20%20%20%20%20%20%20%20state%3Ds%2C%0A%20%20%20%20%20%20%20%20timing_file%3Dtiming_file%2C%0A%20%20%20%20%20%20%20%20verifier%3Dverifier%2C%0A%20%20%20%20%20%20%20%20x_param%3Dx_param%2C%0A%20%20%20%20)%0A%20%20%20%20return%20(timings%2C)%0A%0A%0A%40app.cell(hide_code%3DTrue)%0Adef%20_(K%2C%20mo%2C%20out_dir%2C%20timings)%3A%0A%20%20%20%20if%20timings%5B%22live%22%5D%3A%0A%20%20%20%20%20%20%20%20_footer%20%3D%20f%22%22%22%0A%20%20%20%20Generated%20solver%20directory%3A%20%60%7Bout_dir%7D%60%0A%0A%20%20%20%20Generated%20solver%20source%3A%20%60%7Btimings%5B%22solver_path%22%5D%7D%60%0A%20%20%20%20%22%22%22%0A%20%20%20%20else%3A%0A%20%20%20%20%20%20%20%20_footer%20%3D%20%22%22%0A%20%20%20%20summary%20%3D%20mo.md(f%22%22%22%0A%20%20%20%20%23%23%20Timing%20summary%0A%0A%20%20%20%20One%20complete%20solve%20runs%20%60%7BK%7D%60%20iterations.%0A%0A%20%20%20%20%7C%20implementation%20%7C%20median%20%2F%20mean%20per%20solve%20%7C%0A%20%20%20%20%7C---%7C---%3A%7C%0A%20%20%20%20%7C%20direct%20NumPy%20Python%20%7C%20%60%7Btimings%5B%22python_us%22%5D%3A.3f%7D%20%C2%B5s%60%20%7C%0A%20%20%20%20%7C%20generated%20C%20after%20code%20generation%20%7C%20%60%7Btimings%5B%22codegen_us%22%5D%3A.3f%7D%20%C2%B5s%60%20%7C%0A%20%20%20%20%7C%20generated%20C%20after%20optimization%20iteration%20%7C%20%60%7Btimings%5B%22iteration_us%22%5D%3A.3f%7D%20%C2%B5s%60%20%7C%0A%0A%20%20%20%20The%20speedup%20from%20code%20generation%20is%20%60%7Btimings%5B%22codegen_speedup%22%5D%3A.1f%7Dx%60%2C%20while%20the%20speedup%20from%20the%20optimization%20iteration%20is%20%60%7Btimings%5B%22iteration_speedup%22%5D%3A.2f%7Dx%60%2C%20totaling%20a%20speedup%20of%20%60%7Btimings%5B%22total_speedup%22%5D%3A.1f%7Dx%60.%0A%0A%20%20%20%20%7B_footer%7D%22%22%22%0A%20%20%20%20)%0A%20%20%20%20summary%0A%20%20%20%20return%0A%0A%0Aif%20__name__%20%3D%3D%20%22__main__%22%3A%0A%20%20%20%20app.run()%0A
63766239ea05f8185a1f07176d9e7255