fact: Definition maybe_params_of_size (n : nat) : option params := match n with | 1%nat => Some {| n := 1; s := 2305843009213693952; c := [(1, 1)]; idxs := [0%nat; 0%nat; 1%nat]; machine_wordsize := 64 |} | 2%nat => Some {| n := 2; s := 162259276829213363391578010288128; c := [(1, 1)]; idxs := [0%nat; 1%nat; 0%nat; 1%nat]; machine_wordsize := 64 |} | 3%nat => Some {| n := 3; s := 170141183460469231731687303715884105728; c := [(1, 1)]; idxs := [0%nat; 1%nat; 2%nat; 0%nat; 1%nat]; machine_wordsize := 64 |} | 4%nat => Some {| n := 4; s := 1569275433846670190958947355801916604025588861116008628224; c := [(1, 11)]; idxs := [0%nat; 1%nat; 2%nat; 3%nat; 0%nat; 1%nat]; machine_wordsize := 64 |} | 5%nat => Some {| n := 5; s := 57896044618658097711785492504343953926634992332820282019728792003956564819968; c := [(1, 19)]; idxs := [0%nat; 1%nat; 2%nat; 3%nat; 4%nat; 0%nat; 1%nat]; machine_wordsize := 64 |} | 6%nat => Some {| n := 6; s := 4271974071841820164790043412339104229205409044713305539894083215644439451561281100045924173873152; c := [(1, 9)]; idxs := [0%nat; 1%nat; 2%nat; 3%nat; 4%nat; 5%nat; 0%nat; 1%nat]; machine_wordsize := 64 |} | 7%nat => Some {| n := 7; s := 1260864198284623334792929283204595641762551656654894293374345388935863096687910739565256520156317300505812095689818112; c := [(1, 21)]; idxs := [0%nat; 1%nat; 2%nat; 3%nat; 4%nat; 5%nat; 6%nat; 0%nat; 1%nat]; machine_wordsize := 64 |} | 8%nat => Some {| n := 8; s := 11629419588729710248789180926208072549658261770997088964503843186890228609814366773219056811420217048972200345700258846936553626057834496; c := [(1, 3)]; idxs := [0%nat; 1%nat; 2%nat; 3%nat; 4%nat; 5%nat; 6%nat; 7%nat; 0%nat; 1%nat]; machine_wordsize := 64 |} | 9%nat => Some {| n := 9; s := 6864797660130609714981900799081393217269435300143305409394463459185543183397656052122559640661454554977296311391480858037121987999716643812574028291115057152; c := [(1, 1)]; idxs := [0%nat; 1%nat; 2%nat; 3%nat; 4%nat; 5%nat; 6%nat; 7%nat; 8%nat; 0%nat; 1%nat]; machine_wordsize := 64 |} | 10%nat => Some {| n := 10; s := 57896044618658097711785492504343953926634992332820282019728792003956564819968; c := [(1, 19)]; idxs := [0%nat; 1%nat; 2%nat; 3%nat; 4%nat; 5%nat; 6%nat; 7%nat; 8%nat; 9%nat; 0%nat; 1%nat]; machine_wordsize := 32 |} | 11%nat => Some {| n := 11; s := 62165404551223330269422781018352605012557018849668464680057997111644937126566671941632; c := [(1, 9)]; idxs := [0%nat; 1%nat; 2%nat; 3%nat; 4%nat; 5%nat; 6%nat; 7%nat; 8%nat; 9%nat; 10%nat; 0%nat; 1%nat]; machine_wordsize := 32 |} | 12%nat => Some {| n := 12; s := 3978585891278293137243057985174566720803649206378781739523711815145275976100267004264448; c := [(1, 19)]; idxs := [0%nat; 1%nat; 2%nat; 3%nat; 4%nat; 5%nat; 6%nat; 7%nat; 8%nat; 9%nat; 10%nat; 11%nat; 0%nat; 1%nat]; machine_wordsize := 32 |} | 13%nat => Some {| n := 13; s := 4271974071841820164790043412339104229205409044713305539894083215644439451561281100045924173873152; c := [(1, 9)]; idxs := [0%nat; 1%nat; 2%nat; 3%nat; 4%nat; 5%nat; 6%nat; 7%nat; 8%nat; 9%nat; 10%nat; 11%nat; 12%nat; 0%nat; 1%nat]; machine_wordsize := 32 |} | 15%nat => Some {| n := 15; s := 1202453802380202612679414065556140558016349465041059773802132977424491020858679523053413887173001575952350707712; c := [(1, 25)]; idxs := [0%nat; 1%nat; 2%nat; 3%nat; 4%nat; 5%nat; 6%nat; 7%nat; 8%nat; 9%nat; 10%nat; 11%nat; 12%nat; 13%nat; 14%nat; 0%nat; 1%nat]; machine_wordsize := 32 |} | nlimbs => None end.
imports: Coq.ZArith.ZArith Coq.Lists.List Coq.Setoids.Setoid Coq.Classes.Morphisms Coq.QArith.QArith_base Coq.QArith.Qreduction Coq.QArith.Qround