use proptest::collection;
use proptest::prelude::*;

use arenavec::rc::{Arena, SliceVec};
use arenavec::ArenaBacking;

const DEFAULT_CAPACITY: usize = 4096 << 16;

#[derive(Clone, Debug)]
enum SliceVecOp {
    Push(usize),
    Resize(usize, usize),
    Reserve(usize),
}

prop_compose! {
    fn arb_op() (id in 0..3, size in 0..100, val in 0..std::usize::MAX) -> SliceVecOp {
        match id {
             0 => SliceVecOp::Push(val),
             1 => SliceVecOp::Resize(size as usize, val),
             2 => SliceVecOp::Reserve(size as usize),
             _ => unreachable!(),
        }
    }
}

prop_compose! {
    fn arb_op_seq(num_vecs: usize, len: usize)
        (ids in collection::vec(0..num_vecs, len),
         ops in collection::vec(arb_op(), len))
    -> Vec<(usize, SliceVecOp)> {
        let mut res = Vec::with_capacity(len);

        for i in 0..len {
            res.push((ids[i], ops[i].clone()));
        }

        res
    }
}

const NUM_VECS: usize = 8;

fn rand_op_seq_inner(mut seq: Vec<(usize, SliceVecOp)>, filter: Option<&[usize]>) {
    let arena = Arena::init_capacity(ArenaBacking::SystemAllocation, DEFAULT_CAPACITY).unwrap();
    let mut vecs = Vec::with_capacity(NUM_VECS);
    let mut slice_vecs = Vec::with_capacity(NUM_VECS);

    for _ in 0..NUM_VECS {
        vecs.push(Vec::new());
    }

    for _ in 0..NUM_VECS {
        slice_vecs.push(SliceVec::new(arena.inner()));
    }

    for (v, op) in seq.drain(..) {
        if let Some(s) = filter {
            if !s.contains(&v) {
                continue;
            }
        }

        match op {
            SliceVecOp::Push(e) => {
                vecs[v].push(e);
                slice_vecs[v].push(e);
            }
            SliceVecOp::Resize(l, e) => {
                vecs[v].resize(l, e);
                slice_vecs[v].resize(l, e);
            }
            SliceVecOp::Reserve(l) => {
                vecs[v].reserve(l);
                slice_vecs[v].reserve(l);
            }
        }

        for i in 0..NUM_VECS {
            assert_eq!(&*vecs[i], &*slice_vecs[i]);
        }
    }
}

#[cfg(not(miri))]
mod prop {
    use super::*;
    const NUM_OPS: usize = 400;

    proptest! {
        #[test]
        fn rand_op_seq(seq in arb_op_seq(NUM_VECS, NUM_OPS)) {
            use std::fs::OpenOptions;
            use std::io::Write;

            let mut file =
                OpenOptions::new().create(true).append(true).open("static").unwrap();
            writeln!(file, "{:?}", seq).unwrap();
            rand_op_seq_inner(seq, None);
        }
    }
}

#[test]
fn pre_rand_op_seq1() {
    use SliceVecOp::*;

    let seq = vec![
        (5, Reserve(18)),
        (5, Resize(96, 7434532511546272613)),
        (6, Resize(55, 11836171166212578863)),
        (1, Reserve(73)),
        (4, Push(14991789319801324260)),
        (7, Resize(28, 12717166742316467252)),
        (3, Push(16592071023974211167)),
        (0, Resize(86, 16429603189613580378)),
        (2, Resize(88, 7793320186926176013)),
        (0, Reserve(34)),
        (4, Resize(56, 15179050872186518862)),
        (6, Reserve(67)),
        (1, Reserve(99)),
        (7, Reserve(44)),
        (1, Reserve(86)),
        (3, Resize(28, 14535255266552044782)),
        (6, Resize(48, 14105599279454668572)),
        (4, Resize(27, 9527322489505289215)),
        (1, Reserve(55)),
        (4, Resize(54, 13779177552654293536)),
        (4, Push(814320020935280048)),
        (2, Push(13321971741513898712)),
        (1, Resize(24, 18291098732177080589)),
        (6, Resize(78, 9148270455281011662)),
        (6, Push(8833158480580114405)),
        (5, Resize(27, 1274906245410706342)),
        (3, Reserve(56)),
        (5, Push(12869799416869990094)),
        (6, Push(915054377613569407)),
        (0, Reserve(12)),
        (1, Reserve(67)),
        (7, Resize(16, 3789659809604807811)),
        (3, Reserve(20)),
        (1, Reserve(40)),
        (7, Push(6922281658351195093)),
        (2, Resize(82, 13539788957650865408)),
        (6, Reserve(82)),
        (0, Resize(36, 882642177597567028)),
        (1, Reserve(42)),
        (7, Resize(78, 826798127694797277)),
        (1, Push(10990333923729152933)),
        (7, Resize(34, 3500577806690379107)),
        (4, Reserve(72)),
        (1, Resize(68, 11748951353819237183)),
        (0, Reserve(43)),
        (6, Reserve(85)),
        (7, Reserve(8)),
        (7, Resize(52, 11073697234124871737)),
        (6, Reserve(15)),
        (3, Reserve(61)),
        (4, Push(1554299979281996185)),
        (3, Resize(94, 3486907836119369331)),
        (7, Reserve(81)),
        (4, Reserve(36)),
        (7, Push(13734558101552238331)),
        (2, Reserve(30)),
        (4, Push(14469684486135786576)),
        (4, Resize(42, 12992470109552634917)),
        (7, Reserve(20)),
        (0, Push(7866590370907767796)),
        (3, Resize(18, 6584163843175693599)),
        (5, Push(7688937448577411386)),
        (0, Reserve(38)),
        (3, Resize(2, 2367775010005837822)),
        (5, Resize(23, 11821434197020047061)),
        (0, Reserve(5)),
        (1, Push(8097179394331876406)),
        (1, Reserve(46)),
        (7, Push(3029851440503049484)),
        (2, Resize(18, 11548509876046543326)),
        (4, Reserve(12)),
        (7, Push(1593774132763176699)),
        (4, Push(12399826378467105353)),
        (5, Resize(53, 9546063174298787707)),
        (0, Push(13985504485696120884)),
        (3, Resize(65, 12870527496588722859)),
        (7, Reserve(18)),
        (6, Resize(15, 2369818071208968029)),
        (1, Reserve(22)),
        (6, Reserve(2)),
        (7, Reserve(35)),
        (2, Reserve(59)),
        (6, Reserve(6)),
        (3, Reserve(77)),
        (3, Resize(55, 14399546376740999461)),
        (6, Resize(90, 805929507655167903)),
        (7, Resize(23, 987129242317969159)),
        (0, Reserve(27)),
        (3, Resize(93, 17995679049300670256)),
        (4, Resize(25, 9652416451722358081)),
        (3, Resize(42, 1117105597129765631)),
        (3, Push(17071450624198860125)),
        (5, Push(15556953558815298799)),
        (1, Push(6777489812646189744)),
        (0, Push(3420467694587346486)),
        (5, Reserve(1)),
        (7, Resize(7, 4784347693029963215)),
        (5, Push(17581632846449609163)),
        (6, Reserve(15)),
        (1, Push(16548635869386875967)),
        (4, Push(8985473428401699581)),
        (2, Reserve(28)),
        (5, Resize(66, 13546264137598621127)),
        (6, Resize(40, 17253870872849269820)),
        (5, Push(10279553803484858365)),
        (6, Reserve(78)),
        (3, Push(8887485158247156070)),
        (7, Push(5419091861778966634)),
        (1, Reserve(36)),
        (5, Resize(8, 8096136916066598173)),
        (5, Reserve(24)),
        (5, Push(627254974063755064)),
        (5, Push(9035846514407681585)),
        (3, Push(8194052711830070641)),
        (6, Resize(82, 7651231518029554847)),
        (3, Push(15836795116344246968)),
        (5, Push(17618535346168238634)),
        (4, Reserve(33)),
        (1, Reserve(93)),
        (2, Resize(60, 13372644315447413471)),
        (3, Resize(44, 9430698778940913120)),
        (4, Push(1891902720743089149)),
        (6, Push(18403865303966597389)),
        (4, Reserve(49)),
        (5, Reserve(23)),
        (3, Resize(52, 789580560073913388)),
        (6, Resize(19, 17261691963387684276)),
        (2, Reserve(32)),
        (3, Resize(68, 3238836699368529878)),
        (2, Push(16543570418418538438)),
        (2, Resize(34, 4814923162354884313)),
        (0, Push(13325533280353813112)),
        (4, Push(13864360737784853712)),
        (6, Resize(24, 1592605390302100212)),
        (6, Reserve(52)),
        (5, Reserve(30)),
        (7, Resize(47, 1425498795419035517)),
        (1, Push(3848451596760165612)),
        (3, Push(15089234937428320911)),
        (2, Reserve(39)),
        (2, Push(5713960296948700510)),
        (6, Resize(45, 12100875500011920742)),
        (7, Push(12062076374931716414)),
        (2, Reserve(45)),
        (1, Reserve(38)),
        (0, Push(9138762390727573675)),
        (3, Resize(12, 7617883756884930449)),
        (7, Resize(90, 14512857894682084132)),
        (4, Resize(26, 9702020285439726243)),
        (1, Resize(20, 17354431448132454830)),
        (4, Push(15600115716981553405)),
        (3, Resize(82, 4332456343976075177)),
        (1, Push(17579533218773998033)),
        (7, Push(3861319371437802116)),
        (1, Push(4238676302210114556)),
        (3, Resize(20, 14728372563112249573)),
        (2, Reserve(31)),
        (0, Reserve(94)),
        (7, Resize(61, 13622545542577143562)),
        (3, Reserve(3)),
        (3, Resize(71, 10729988071305226681)),
        (7, Resize(6, 7426108624556647785)),
        (4, Reserve(50)),
        (4, Resize(39, 10224587222459554962)),
        (4, Resize(44, 570548645906481521)),
        (7, Push(9420687631161847908)),
        (3, Resize(29, 489925511289468281)),
        (2, Resize(37, 1858657781982553873)),
        (6, Push(13891528011355657627)),
        (4, Reserve(91)),
        (7, Resize(66, 6661376383413711898)),
        (4, Push(1916598647339775945)),
        (6, Reserve(15)),
        (5, Push(6956938135864214783)),
        (0, Reserve(45)),
        (3, Push(11684865107781406689)),
        (4, Resize(79, 15196479610394063796)),
        (1, Resize(76, 8510470983404048639)),
        (2, Resize(18, 8540564175138020844)),
        (7, Reserve(36)),
        (7, Reserve(7)),
        (7, Resize(82, 10369146083588901681)),
        (3, Reserve(78)),
        (2, Reserve(30)),
        (2, Reserve(86)),
        (6, Reserve(53)),
        (0, Resize(62, 4081661520403283412)),
        (1, Push(1732056619466402251)),
        (7, Reserve(29)),
        (4, Push(6468446417235325484)),
        (7, Push(1300512593664612238)),
        (5, Push(13803896047621899962)),
        (6, Push(10168224645268992510)),
        (2, Reserve(2)),
        (1, Resize(56, 18381331589099637809)),
        (5, Reserve(70)),
        (7, Reserve(59)),
        (7, Push(8327431407684993266)),
        (5, Push(5553637212980114752)),
        (6, Push(13729085403743721172)),
        (5, Resize(40, 9472983903595113633)),
        (6, Push(17533714037682523667)),
        (4, Reserve(25)),
        (4, Push(13367231127912003528)),
        (5, Push(3805442765486049018)),
        (6, Reserve(8)),
        (4, Reserve(87)),
        (0, Reserve(21)),
        (5, Resize(89, 10732247370426436277)),
        (3, Resize(5, 2020562476612454987)),
        (0, Reserve(20)),
        (2, Reserve(81)),
        (1, Reserve(42)),
        (0, Reserve(27)),
        (6, Reserve(46)),
        (5, Resize(65, 17501060746955555737)),
        (3, Push(8477000901703784552)),
        (7, Reserve(24)),
        (2, Resize(41, 10863320204162507024)),
        (6, Push(4776005791173790931)),
        (2, Push(12549462382137704871)),
        (2, Resize(39, 17561928801683131965)),
        (7, Reserve(98)),
        (4, Reserve(52)),
        (2, Resize(99, 16491524746282208841)),
        (7, Push(11466547191694976267)),
        (1, Resize(23, 2248955733084774259)),
        (2, Push(13976748479160618391)),
        (0, Push(9829509661504466993)),
        (5, Reserve(65)),
        (4, Reserve(88)),
        (1, Push(12464862572709632597)),
        (7, Push(7958578588217181700)),
        (3, Reserve(51)),
        (6, Reserve(93)),
        (6, Reserve(92)),
        (7, Push(13736681831895922008)),
        (5, Reserve(56)),
        (6, Push(1650707862179895666)),
        (1, Push(15449995469481788571)),
        (7, Resize(36, 9805349881339365818)),
        (5, Push(6404087729724611804)),
        (2, Push(15196452833475501888)),
        (6, Push(2730470788408704076)),
        (2, Reserve(24)),
        (1, Resize(5, 3595298397402076354)),
        (3, Push(15290799440347688)),
        (4, Push(14006473401008893296)),
        (5, Resize(3, 10451862953297807063)),
        (1, Resize(74, 265309732783932296)),
        (0, Reserve(55)),
        (0, Reserve(54)),
        (2, Reserve(2)),
        (1, Reserve(54)),
        (2, Reserve(91)),
        (7, Resize(99, 15245773801816280978)),
        (6, Push(2953136686063730661)),
        (2, Resize(43, 6243229630648977189)),
        (3, Reserve(75)),
        (1, Push(3212425695570232032)),
        (6, Reserve(85)),
        (0, Push(17717453381519020148)),
        (0, Push(12937359446267210119)),
        (3, Reserve(3)),
        (5, Reserve(36)),
        (1, Reserve(75)),
        (2, Resize(53, 2845317859068894618)),
        (2, Reserve(52)),
        (1, Push(15491795612141018262)),
        (6, Resize(64, 10251876321685121580)),
        (2, Reserve(18)),
        (4, Reserve(9)),
        (1, Resize(62, 12415563551632339417)),
        (7, Resize(72, 2993443444742592288)),
        (1, Reserve(27)),
        (4, Reserve(54)),
        (6, Push(7908828014430241492)),
        (5, Reserve(12)),
        (7, Push(6852433628287986625)),
        (6, Push(9794161938746646723)),
        (1, Push(451632942197011340)),
        (1, Push(2281780498448241994)),
        (2, Resize(12, 17302563519604653656)),
        (1, Resize(50, 16079140408200486745)),
        (0, Push(3563922921970803189)),
        (6, Reserve(95)),
        (0, Resize(95, 6328196690094006589)),
        (5, Resize(51, 16535457293684301111)),
        (3, Resize(72, 18294727691595166965)),
        (5, Reserve(67)),
        (4, Push(10750347787304408774)),
        (7, Resize(13, 4812695112627343575)),
        (4, Resize(71, 8873528311297012767)),
        (0, Push(17150718072159411663)),
        (5, Reserve(0)),
        (3, Push(14005157157345397976)),
        (3, Push(10236229771925961686)),
        (0, Reserve(65)),
        (4, Resize(4, 3810045160007715666)),
        (1, Reserve(96)),
        (6, Reserve(23)),
        (7, Resize(87, 5642488162026501146)),
        (5, Push(6221691914213430142)),
        (1, Reserve(15)),
        (4, Reserve(35)),
        (0, Resize(90, 6625694300628371279)),
        (4, Push(13633972252472168822)),
        (0, Push(5913651452064016401)),
        (4, Reserve(28)),
        (3, Resize(52, 16132288721990023755)),
        (7, Push(10951066952073463152)),
        (2, Push(17012835433406106620)),
        (3, Reserve(49)),
        (5, Resize(0, 10757036212954212254)),
        (5, Push(17558520471082390717)),
        (2, Push(6030951989897128161)),
        (5, Push(6192812795771748990)),
        (1, Resize(21, 8182847900438242280)),
        (2, Reserve(4)),
        (4, Push(1912563234267631336)),
        (4, Reserve(35)),
        (2, Reserve(61)),
        (2, Push(4417126518861866896)),
        (7, Resize(27, 16586350593895250795)),
        (6, Reserve(69)),
        (7, Resize(74, 12442472354864680048)),
        (1, Reserve(90)),
        (5, Reserve(33)),
        (1, Reserve(40)),
        (7, Reserve(19)),
        (5, Resize(16, 15448378381288877643)),
        (6, Push(2384921129845462378)),
        (4, Push(1013321282484744767)),
        (4, Push(13271344473838945078)),
        (0, Push(2190931531631436621)),
        (0, Resize(75, 1215803094246020623)),
        (2, Push(12642696422898771728)),
        (4, Resize(16, 9159112165581493102)),
        (2, Push(13066839194534133079)),
        (3, Resize(72, 3782309607529202990)),
        (7, Reserve(0)),
        (0, Push(14444802699059598249)),
        (4, Resize(52, 3472629142902738772)),
        (1, Resize(4, 10850167234350445461)),
        (4, Resize(71, 898855096635968587)),
        (7, Resize(95, 13200366182641147137)),
        (5, Reserve(53)),
        (5, Push(11239406290682213077)),
        (7, Resize(96, 11271031291738299086)),
        (7, Push(13446965229295377341)),
        (4, Resize(48, 11716682760119559957)),
        (6, Push(9603590962195566523)),
        (7, Resize(38, 6235453618755557023)),
        (1, Resize(83, 2198020767332768068)),
        (6, Reserve(52)),
        (7, Resize(74, 5043395211010898773)),
        (5, Reserve(83)),
        (1, Reserve(47)),
        (1, Push(14703457258365147126)),
        (3, Reserve(91)),
        (5, Resize(30, 15590066610425715599)),
        (0, Resize(55, 8853521250954134046)),
        (6, Push(16195402152382416595)),
        (2, Push(9422096042476496900)),
        (2, Reserve(7)),
        (5, Push(17805686037271418567)),
        (2, Push(5147554562838977248)),
        (7, Push(17974847039109331148)),
        (3, Reserve(34)),
        (7, Resize(76, 18089078196912612808)),
        (2, Resize(46, 12459793132713846679)),
        (0, Resize(79, 14480165576712101013)),
        (5, Resize(21, 15071476447610373821)),
        (7, Push(4992448698263760096)),
        (1, Push(10020600278138913520)),
        (4, Reserve(72)),
        (0, Reserve(61)),
        (6, Resize(7, 15064964772413805485)),
        (0, Reserve(97)),
        (4, Resize(34, 7202041726188883415)),
        (5, Resize(5, 4750971916391312718)),
        (5, Reserve(51)),
        (0, Reserve(87)),
        (4, Resize(73, 14451155451840320170)),
        (1, Resize(58, 4201312026579324206)),
        (1, Push(7087037479030288788)),
        (3, Reserve(35)),
        (7, Reserve(34)),
        (1, Push(973573467986414015)),
        (3, Resize(33, 17073760823659202543)),
        (4, Resize(90, 7002136876418133005)),
        (1, Resize(99, 8243106874128009760)),
        (4, Reserve(96)),
        (5, Push(18139700090506776254)),
        (0, Push(17838226851675992773)),
        (2, Reserve(40)),
        (1, Resize(79, 7324287648850370154)),
        (7, Push(2988546105184828028)),
        (2, Resize(49, 6555181995891599849)),
        (6, Reserve(19)),
    ];
    rand_op_seq_inner(seq, None);
}

#[test]
fn pre_rand_op_seq2() {
    use SliceVecOp::*;

    let seq = vec![
        (6, Push(8571704643031140639)),
        (0, Resize(98, 17598300304473862305)),
        (2, Push(10673108108330974792)),
        (2, Reserve(0)),
        (3, Reserve(25)),
        (2, Reserve(76)),
        (7, Resize(85, 8147346080438701674)),
        (2, Resize(83, 964644805778128179)),
        (7, Reserve(94)),
        (2, Reserve(30)),
        (4, Resize(19, 15160805831113754163)),
        (4, Resize(44, 1502254100891562158)),
        (5, Reserve(80)),
        (1, Resize(35, 11531738861786119800)),
        (0, Push(3664415400661013128)),
        (4, Push(16911168056797407744)),
        (3, Resize(62, 15284348711435874451)),
        (3, Reserve(55)),
        (0, Reserve(58)),
        (3, Reserve(72)),
        (7, Reserve(0)),
        (3, Resize(80, 13364769953759628791)),
        (1, Reserve(19)),
        (4, Resize(70, 9857562065498559959)),
        (5, Reserve(34)),
        (4, Resize(27, 10211445460498058801)),
        (5, Push(15094763455739304238)),
        (6, Reserve(47)),
        (2, Push(10442044456551944993)),
        (0, Resize(34, 1812854062588894737)),
        (7, Resize(79, 17565298827834421763)),
        (6, Resize(42, 13521913155721089079)),
        (0, Resize(13, 701208137330599767)),
        (4, Reserve(54)),
        (6, Resize(91, 10311663382213544238)),
        (4, Resize(65, 8473632458421022773)),
        (3, Push(6448923683892002613)),
        (0, Push(4985722735428100225)),
        (2, Reserve(30)),
        (1, Reserve(34)),
        (4, Reserve(23)),
        (4, Push(6604452905770361145)),
        (4, Reserve(31)),
        (3, Push(3665268368356514533)),
        (1, Push(13491316185381568805)),
        (0, Resize(77, 14985355469545938484)),
        (1, Resize(76, 9794777480629469760)),
        (6, Push(8486083127508768000)),
        (5, Push(3579000517743526593)),
        (2, Resize(65, 5097567639574804681)),
        (4, Reserve(50)),
        (7, Push(9076403318192407882)),
        (4, Push(228001952269633685)),
        (4, Reserve(93)),
        (4, Resize(73, 6117577782634335007)),
        (1, Reserve(49)),
        (3, Resize(42, 1274811717647677032)),
        (4, Resize(29, 5794915859890527824)),
        (2, Reserve(55)),
        (1, Resize(71, 227201394442576538)),
        (6, Reserve(72)),
        (3, Resize(0, 6289667211629638856)),
        (1, Reserve(18)),
        (3, Push(13834230432887299611)),
        (0, Push(9820546493818449427)),
        (0, Push(13211181115898970904)),
        (0, Push(10966940377309801532)),
        (7, Resize(20, 16290344738375090040)),
        (6, Push(8376557472076204755)),
        (5, Push(7075107822081082475)),
        (4, Push(13688906561890343957)),
        (6, Push(18397397298154655122)),
        (1, Push(12241272500589537243)),
        (3, Push(12647322535621493448)),
        (4, Reserve(52)),
        (6, Push(16708086432963643365)),
        (0, Resize(59, 11616400252456090558)),
        (0, Push(11933557546634591469)),
        (2, Push(4465138436592395375)),
        (1, Reserve(91)),
        (0, Resize(99, 6582327297630873598)),
        (0, Push(2917645691347360867)),
        (2, Push(13540072504010523105)),
        (3, Reserve(17)),
        (2, Reserve(16)),
        (0, Reserve(2)),
        (3, Push(752321737674337719)),
        (7, Reserve(32)),
        (0, Reserve(71)),
        (2, Push(9081992076940592004)),
        (1, Resize(43, 7684511904390755849)),
        (5, Push(17569856771915805365)),
        (4, Push(5548408350015950457)),
        (1, Resize(75, 4915642915733658997)),
        (0, Push(987102234284290876)),
        (6, Reserve(82)),
        (6, Push(10293356557352555457)),
        (1, Push(1300257579199677867)),
        (4, Push(12889788053091681020)),
        (3, Push(822814087742694605)),
        (7, Reserve(25)),
        (1, Reserve(79)),
        (6, Resize(89, 2257550051579926048)),
        (6, Reserve(16)),
        (2, Resize(9, 13488887023827776204)),
        (2, Resize(69, 12839521478462225630)),
        (6, Push(9205953369572398835)),
        (1, Push(9243504304607826725)),
        (7, Push(429236702686864935)),
        (4, Resize(41, 15488999146079567718)),
        (0, Push(14851820478376629590)),
        (4, Push(15896539374520472181)),
        (3, Resize(27, 5692976620089907557)),
        (6, Resize(52, 14377327576084841497)),
        (5, Push(3306479383112047596)),
        (6, Push(441983513269468745)),
        (0, Reserve(43)),
        (1, Resize(57, 5487696609942702356)),
        (2, Push(344299554771332129)),
        (7, Reserve(49)),
        (5, Reserve(5)),
        (4, Reserve(67)),
        (1, Resize(96, 6398700515314304433)),
        (2, Resize(19, 16068163172971061627)),
        (3, Reserve(59)),
        (6, Resize(46, 7556766827689372214)),
        (0, Resize(69, 13270043707243941141)),
        (3, Resize(80, 15435745910835209784)),
        (0, Resize(23, 17678716989182847050)),
        (7, Reserve(57)),
        (6, Push(18232981473844706499)),
        (3, Resize(7, 5774591707393533770)),
        (1, Push(12046682489383942907)),
        (3, Resize(41, 5224387578766817303)),
        (5, Reserve(97)),
        (3, Resize(78, 2679295251457757521)),
        (7, Reserve(1)),
        (6, Reserve(45)),
        (3, Push(16509358460557708371)),
        (4, Reserve(31)),
        (7, Reserve(94)),
        (0, Push(3937217562061589671)),
        (1, Push(5906037351812797474)),
        (3, Reserve(36)),
        (1, Push(15178821695834095251)),
        (7, Resize(91, 9794502638203248100)),
        (6, Resize(42, 9613929237883037624)),
        (1, Push(4599326753355542128)),
        (1, Reserve(24)),
        (2, Reserve(3)),
        (6, Push(17488390456372991652)),
        (1, Resize(35, 10413538906329710191)),
        (3, Resize(63, 7089861612598655412)),
        (7, Resize(73, 2503708897832437533)),
        (5, Push(4640814851723099506)),
        (0, Push(6996082249668953711)),
        (6, Resize(86, 15227194503105842076)),
        (3, Reserve(63)),
        (6, Push(3196056850873317527)),
        (4, Push(399836781972870995)),
        (5, Resize(43, 14825103139336093147)),
        (5, Reserve(6)),
        (1, Resize(76, 4892475064355782827)),
        (6, Push(12390075741166097247)),
        (4, Resize(90, 18436285272951707514)),
        (1, Resize(21, 2918140766224845648)),
        (5, Reserve(88)),
        (5, Push(3335204913117583534)),
        (0, Push(15743747858747785255)),
        (5, Resize(31, 10267170282093158614)),
        (3, Resize(49, 14231167602682777350)),
        (3, Reserve(84)),
        (7, Reserve(85)),
        (0, Push(5019514301157935629)),
        (5, Resize(17, 5883624102454575456)),
        (3, Reserve(94)),
        (5, Reserve(51)),
        (6, Push(9217450148175425243)),
        (7, Resize(59, 9633693270724072726)),
        (7, Reserve(10)),
        (1, Reserve(5)),
        (2, Resize(81, 4649551299926023161)),
        (3, Push(7611674631818278927)),
        (7, Reserve(71)),
        (1, Reserve(1)),
        (1, Reserve(38)),
        (4, Resize(81, 15783501365382499737)),
        (5, Reserve(73)),
        (1, Push(3337285622280602938)),
        (1, Resize(32, 561682769353209217)),
        (2, Push(7477863033752468939)),
        (1, Resize(18, 15076461858634126137)),
        (2, Resize(26, 6756497160158165109)),
        (3, Push(14531825449056867231)),
        (2, Reserve(42)),
        (0, Reserve(59)),
        (6, Reserve(99)),
        (3, Push(16582187338810011513)),
        (0, Reserve(7)),
        (7, Reserve(49)),
        (7, Reserve(83)),
        (7, Push(16440204891268282632)),
        (4, Resize(82, 16570023916659548634)),
        (4, Push(12683962471258754451)),
        (5, Push(5791973939458236569)),
        (6, Push(13213510239406200528)),
        (3, Reserve(79)),
        (6, Push(15151307855246737024)),
        (5, Push(18110379106169373794)),
        (6, Resize(70, 16265517345271633039)),
        (3, Reserve(24)),
        (7, Reserve(88)),
        (5, Resize(25, 941960336346673535)),
        (1, Resize(63, 10216767809765890372)),
        (3, Push(13304940051244382601)),
        (2, Push(14882904976297793409)),
        (2, Push(11569588926909486508)),
        (3, Push(5528621615841482224)),
        (1, Reserve(59)),
        (0, Push(12857827069239766853)),
        (5, Resize(13, 15867530733364759125)),
        (5, Resize(79, 7083622966161660992)),
        (6, Resize(73, 17745503955733160843)),
        (5, Reserve(17)),
        (1, Reserve(15)),
        (2, Push(16159478224118658921)),
        (2, Resize(83, 6143385470724018223)),
        (2, Push(2861412736163086968)),
        (5, Reserve(9)),
        (2, Resize(49, 2597859128867577171)),
        (7, Resize(8, 8691095441763065170)),
        (3, Resize(85, 14749237194408553888)),
        (1, Push(12613456404160136228)),
        (6, Reserve(62)),
        (0, Resize(9, 13445206803119276873)),
        (1, Reserve(99)),
        (7, Reserve(29)),
        (2, Resize(59, 14780250818751707961)),
        (4, Push(18230048853166366343)),
        (1, Reserve(82)),
        (2, Push(18262091739584071212)),
        (6, Push(12340500320916417079)),
        (0, Push(16718706910633256492)),
        (5, Push(10022904588350819343)),
        (1, Push(14513473731490793527)),
        (1, Push(13321333111082934834)),
        (3, Resize(57, 16035774627986749941)),
        (2, Resize(79, 7516080677271412287)),
        (0, Resize(84, 3275081912479550278)),
        (1, Push(9335943052069771717)),
        (3, Resize(90, 741665365317424548)),
        (7, Push(4784516684947081405)),
        (7, Resize(33, 11931793047609001431)),
        (2, Resize(4, 18270819633106215317)),
        (2, Push(1800214047186378173)),
        (4, Resize(86, 2500544818230093706)),
        (7, Resize(29, 4676717314521769775)),
        (3, Push(1032059459069719847)),
        (3, Resize(9, 10330166000581011355)),
        (3, Resize(8, 2751967310522721445)),
        (7, Push(4781601218464691600)),
        (0, Resize(34, 4678438393402615100)),
        (3, Resize(19, 15674867404793608550)),
        (1, Push(6137232626642763037)),
        (0, Push(18439788688585119739)),
        (3, Resize(79, 10186791813373670715)),
        (0, Resize(9, 4381079811306291212)),
        (6, Reserve(58)),
        (3, Push(2590056937737970261)),
        (5, Reserve(95)),
        (7, Reserve(80)),
        (4, Reserve(64)),
        (1, Push(10783417499695203044)),
        (3, Resize(9, 14468736489993925518)),
        (7, Resize(5, 16128883050309857162)),
        (0, Reserve(2)),
        (5, Push(12785926325014837615)),
        (2, Resize(99, 15878487414784161903)),
        (4, Resize(32, 11436782439796538255)),
        (0, Resize(72, 1570104243660315982)),
        (0, Push(13714353127567045290)),
        (7, Reserve(35)),
        (7, Reserve(36)),
        (1, Resize(20, 4254330562542153936)),
        (4, Reserve(21)),
        (6, Reserve(1)),
        (6, Push(15723119482315723397)),
        (6, Reserve(68)),
        (1, Reserve(39)),
        (3, Push(13925026279088168711)),
        (1, Push(12512371844331225703)),
        (3, Push(17491843885563059621)),
        (5, Push(15640843850412469565)),
        (4, Resize(6, 5495866525514215352)),
        (0, Resize(78, 376812290890297982)),
        (4, Push(3119804732190693274)),
        (0, Push(10649693029762344711)),
        (4, Resize(0, 2805787139708530871)),
        (1, Push(5799739932524152048)),
        (2, Reserve(74)),
        (3, Resize(20, 3819612525069790771)),
        (2, Resize(41, 10102602867279941121)),
        (7, Resize(85, 17495981587299947726)),
        (7, Push(17110771282840114449)),
        (1, Reserve(85)),
        (5, Reserve(21)),
        (3, Reserve(6)),
        (7, Push(8335952026385400474)),
        (6, Push(11596903061863365962)),
        (4, Push(964814673025398563)),
        (7, Reserve(82)),
        (0, Reserve(33)),
        (6, Reserve(46)),
        (6, Reserve(60)),
        (4, Reserve(22)),
        (7, Resize(71, 9806261207981417408)),
        (4, Push(5819104801120654773)),
        (7, Push(16107863213855999050)),
        (7, Push(2702720670289344196)),
        (7, Push(16049741483323875487)),
        (5, Reserve(5)),
        (0, Resize(67, 3016723081177068981)),
        (0, Resize(87, 6290252406291272204)),
        (4, Resize(63, 1509437710969278911)),
        (0, Reserve(46)),
        (2, Resize(35, 12695478531576903684)),
        (1, Push(1919515398301307586)),
        (6, Reserve(15)),
        (0, Resize(49, 9334302579832564788)),
        (1, Reserve(95)),
        (6, Push(3205104346745568223)),
        (7, Reserve(21)),
        (5, Push(13994165259637534467)),
        (6, Reserve(33)),
        (3, Resize(78, 568884156863163741)),
        (1, Resize(4, 1578751576855810311)),
        (3, Push(612827329542074034)),
        (6, Reserve(65)),
        (5, Resize(91, 11597552787912730251)),
        (6, Resize(70, 16794745016355576351)),
        (6, Resize(22, 8010685806294072765)),
        (5, Resize(50, 16501264971956211474)),
        (5, Reserve(19)),
        (4, Reserve(16)),
        (0, Resize(88, 9056857703603157841)),
        (6, Push(10387213449934502296)),
        (4, Resize(81, 11181275113404847846)),
        (3, Push(18293768560649599640)),
        (1, Resize(39, 7325648604548967540)),
        (0, Push(3204513896835787907)),
        (5, Push(4785596010931471935)),
        (2, Resize(28, 1915217858803857846)),
        (7, Push(14013567789228732649)),
        (3, Push(8717620574923877051)),
        (0, Push(6180107370417069911)),
        (4, Reserve(99)),
        (7, Push(4937820000918431608)),
        (0, Resize(17, 11028864438573721116)),
        (4, Push(14526351704074105667)),
        (3, Push(14698974792005445501)),
        (4, Push(13473872864183283796)),
        (4, Reserve(97)),
        (2, Push(11565790739491550656)),
        (6, Push(12867301537842065675)),
        (3, Resize(57, 18395334540803284173)),
        (7, Push(10669324893310290347)),
        (2, Reserve(93)),
        (4, Push(7302556619043146732)),
        (4, Push(16059879797872393380)),
        (1, Resize(80, 15707822832450654573)),
        (4, Resize(67, 17322616832252248336)),
        (3, Resize(89, 15664268963544292746)),
        (6, Push(10224960836742423014)),
        (7, Resize(46, 1535430416666820101)),
        (2, Reserve(19)),
        (4, Reserve(23)),
        (3, Push(16165956669883332935)),
        (1, Reserve(46)),
        (3, Reserve(91)),
        (4, Reserve(86)),
        (6, Reserve(33)),
        (0, Push(8383723510733348605)),
        (2, Resize(62, 5050263965764670933)),
        (2, Resize(60, 13414652522662030188)),
        (0, Push(2163545114686344084)),
        (0, Push(8159566120606897744)),
        (2, Reserve(81)),
        (2, Push(65198384152091738)),
        (6, Push(13063063387541250953)),
        (6, Push(8263764888341946834)),
        (3, Resize(81, 11361146613014776609)),
        (7, Push(6777904842678076726)),
        (4, Resize(28, 16747455473350839104)),
        (1, Push(1022572818789219642)),
        (4, Resize(65, 10438872822855775470)),
        (3, Resize(82, 3728010992530822830)),
        (1, Reserve(46)),
        (1, Resize(6, 3074843612257847349)),
        (5, Resize(73, 8276561271062403640)),
        (3, Reserve(10)),
    ];
    rand_op_seq_inner(seq, None);
}