GarageDoor does not fit within Coq CI memory limit #1427

JasonGross · 2022-10-12T23:59:30Z

COQC src/Bedrock/End2End/X25519/GarageDoor.v
Finished transaction in 46.551 secs (7.101u,0.757s) (successful)
Finished transaction in 17.874 secs (6.964u,0.165s) (successful)
Finished transaction in 10.409 secs (7.577u,0.452s) (successful)
Command terminated by signal 9
src/Bedrock/End2End/X25519/GarageDoor.vo (real: 1194.29, user: 633.57, sys: 22.09, mem: 3800484 ko)

GarageDoor uses too much RAM for Coq's CI. Either we should provide a target that excludes only GarageDoor and it's reverse dependencies, or we should perfomance-optimize GarageDoor.

https://github.com/coq/coq/runs/8838127340
coq/coq#16638 (comment)

cc @andres-erbsen

The text was updated successfully, but these errors were encountered:

andres-erbsen · 2022-10-13T00:31:55Z

I blindly created #1428, does our CI show enough info to see how much that helps?

JasonGross · 2022-10-13T04:20:47Z

Yes, the CI should show a table of time and memory usage at the bottom of each step

andres-erbsen · 2022-10-13T13:47:42Z

4252172 ko after #1429

JasonGross · 2022-10-13T13:48:25Z

This is better (thanks!), but I think we need to be under 3.5GB for Coq's CI

andres-erbsen · 2022-10-13T13:57:11Z

I created #1431 but I don't think it'll do it either. But wait, Coq CI got almost to the end of the file previously, to the large lemma that is now replaced with something hopefully very small?

JasonGross · 2022-10-13T16:50:52Z

I bumped coq-scripts to have the newly written script etc/coq-scripts/timing/exec-insert-mem-and-timings.sh. Running etc/coq-scripts/timing/exec-insert-mem-and-timings.sh "coqc" -time -q '-w' '+implicit-core-hint-db,+implicits-in-term,+non-reversible-notation,+deprecated-intros-until-0,+deprecated-focus,+unused-intro-pattern,+variable-collision,+unexpected-implicit-declaration,+omega-is-deprecated,+deprecated-instantiate-syntax,+non-recursive,+undeclared-scope,+deprecated-hint-rewrite-without-locality,+deprecated-hint-without-locality,+deprecated-instance-without-locality,+deprecated-typeclasses-transparency-without-locality,unsupported-attributes' -w -notation-overridden,-deprecated-hint-constr,-fragile-hint-constr,-native-compiler-disabled,-ambiguous-paths,-masking-absolute-name "-w" "-deprecated-native-compiler-option" "-native-compiler" "ondemand" -I /home/jgross/fiat-crypto/rewriter/src/Rewriter/Util/plugins -Q /home/jgross/fiat-crypto/coqprime/src/Coqprime Coqprime -Q /home/jgross/fiat-crypto/rupicola/bedrock2/deps/coqutil/src/coqutil coqutil -Q /home/jgross/fiat-crypto/rupicola/src/Rupicola Rupicola -Q /home/jgross/fiat-crypto/rupicola/bedrock2/bedrock2/src/bedrock2 bedrock2 -Q /home/jgross/fiat-crypto/rupicola/bedrock2/bedrock2/src/bedrock2Examples bedrock2Examples -Q /home/jgross/fiat-crypto/rupicola/bedrock2/compiler/src/compiler compiler -Q /home/jgross/fiat-crypto/rupicola/bedrock2/deps/riscv-coq/src/riscv riscv -Q /home/jgross/fiat-crypto/rewriter/src/Rewriter Rewriter -R src Crypto src/Bedrock/End2End/X25519/GarageDoor.v gives

Timing and memory diffs on each line (be wary that some are out of order)

.206445801s +188040kb: Chars 0 - 34 [Require~Import~Coq.Strings.Str...] 0.123 secs (0.081u,0.042s)
.008670042s +11088kb: Chars 35 - 65 [Require~Import~Coq.Lists.List.] 0.001 secs (0.u,0.s)
.064876508s +60828kb: Chars 66 - 99 [Require~Import~Coq.ZArith.ZArith.] 0.072 secs (0.051u,0.02s)
.068535884s +71544kb: Chars 100 - 138 [Require~Import~Crypto.Spec.Cur...] 0.068 secs (0.058u,0.009s)
.014529535s +14784kb: Chars 139 - 178 [Require~Import~bedrock2.Map.Se...] 0.014 secs (0.006u,0.008s)
.006953434s +7656kb: Chars 179 - 210 [Require~Import~bedrock2.Syntax.] 0. secs (0.u,0.s)
.177013846s +62300kb: Chars 211 - 244 [Require~Import~compiler.Pipeline.] 0.182 secs (0.161u,0.021s)
.007967122s +3960kb: Chars 245 - 277 [Require~Import~compiler.Symbols.] 0.001 secs (0.001u,0.s)
.006466729s +6336kb: Chars 278 - 307 [Require~Import~compiler.MMIO.] 0.005 secs (0.005u,0.s)
.006491718s +5544kb: Chars 308 - 347 [Require~Import~coqutil.Word.Bi...] 0. secs (0.u,0.s)
.050271057s +9624kb: Chars 348 - 400 [Require~Import~Crypto.Arithmet...] 0.063 secs (0.063u,0.s)
.422204029s +192716kb: Chars 401 - 460 [Require~Import~Crypto.Bedrock....] 0.421 secs (0.35u,0.07s)
1.635113554s +412264kb: Chars 461 - 530 [Require~Import~Crypto.Bedrock....] 1.634 secs (1.514u,0.119s)
.009340697s +3432kb: Chars 531 - 582 [Require~Import~Crypto.Bedrock....] 0.005 secs (0.005u,0.s)
.006790675s +8448kb: Chars 583 - 641 [Require~Import~Crypto.Bedrock....] 0.001 secs (0.001u,0.s)
.007055212s +3168kb: Chars 642 - 695 [Require~Import~Crypto.Bedrock....] 0.004 secs (0.004u,0.s)
.006687343s -2476kb: Chars 696 - 760 [Require~Import~Crypto.Bedrock....] 0.001 secs (0.001u,0.s)
.007111411s +8448kb: Chars 761 - 817 [Require~Import~Crypto.Bedrock....] 0.008 secs (0.008u,0.s)
.006825143s +1848kb: Chars 818 - 880 [Require~Import~Crypto.Bedrock....] 0.003 secs (0.u,0.003s)
.006096115s +264kb: Chars 881 - 921 [Require~Import~bedrock2Example...] 0.007 secs (0.u,0.006s)
.006468811s +852kb: Chars 922 - 964 [Require~Import~bedrock2Example...] 0.01 secs (0.u,0.01s)
.006507137s +2904kb: Chars 965 - 1006 [Require~Import~bedrock2Example...] 0. secs (0.u,0.s)
.007488790s +3432kb: Chars 1007 - 1048 [Require~Import~bedrock2Example...] 0. secs (0.u,0.s)
.006680794s +3168kb: Chars 1049 - 1089 [Require~Import~bedrock2Example...] 0. secs (0.u,0.s)
.006511101s +3696kb: Chars 1090 - 1131 [Require~Import~bedrock2Example...] 0. secs (0.u,0.s)
.006517960s +3696kb: Chars 1132 - 1191 [Require~Import~Rupicola.Exampl...] 0.002 secs (0.002u,0.s)
.006910466s +3432kb: Chars 1193 - 1223 [#[local]Open~Scope~string_scope.] 0. secs (0.u,0.s)
.006832663s +2904kb: Chars 1224 - 1276 [Import~Syntax~Syntax.Coercions...] 0.001 secs (0.001u,0.s)
.006341944s +3696kb: Chars 1277 - 1298 [Import~ListNotations.] 0. secs (0.u,0.s)
.006888052s +3432kb: Chars 1299 - 1320 [Import~Coq.Init.Byte.] 0. secs (0.u,0.s)
.006243347s +2904kb: Chars 1322 - 1523 [Definition~garageowner~:~list~...] 0. secs (0.u,0.s)
.006875835s +3696kb: Chars 1525 - 1557 [#[local]Notation~ST~:=~0x80000...] 0. secs (0.u,0.s)
.007224366s +528kb: Chars 1558 - 1590 [#[local]Notation~PK~:=~0x80000...] 0. secs (0.u,0.s)
.006925715s +0kb: Chars 1591 - 1623 [#[local]Notation~BUF~:=~0x8000...] 0. secs (0.u,0.s)
.006346601s +0kb: Chars 1625 - 1971 [Definition~initfn~:~func~:=~~~...] 0.086 secs (0.086u,0.s)
.247306608s +1056kb: Chars 1973 - 3731 [Definition~loopfn~:~func~:=~~~...] 0.257 secs (0.257u,0.s)
.006927664s +0kb: Chars 3733 - 3798 [Import~TracePredicate~TracePre...] 0. secs (0.u,0.s)
.006670698s +0kb: Chars 3799 - 3836 [Notation~OP~:=~(lightbulb_spec...] 0. secs (0.u,0.s)
.006674810s +0kb: Chars 3837 - 4111 [Definition~iocfg~:~list~OP~->~...] 0.002 secs (0.002u,0.s)
.007229409s +0kb: Chars 4112 - 4270 [Definition~BootSeq~:~list~OP~-...] 0. secs (0.u,0.s)
.010270878s +0kb: Chars 4272 - 4328 [Import~WeakestPrecondition~Pro...] 0.033 secs (0.033u,0.s)
.006927103s +0kb: Chars 4329 - 4412 [#[local]Notation~"m~=*~P"~:=~(...] 0. secs (0.u,0.s)
.006841735s +0kb: Chars 4413 - 4512 [#[local]~Notation~"xs~$@~a"~:=...] 0. secs (0.u,0.s)
.045717206s +0kb: Chars 4513 - 4841 [#[global]~Instance~spec_of_ini...] 0.058 secs (0.058u,0.s)
.006563031s +0kb: Chars 4843 - 4998 [Ltac~~fwd~:=~~~repeat~~~~match...] 0. secs (0.u,0.s)
.006879896s +0kb: Chars 4999 - 5126 [Ltac~~slv~:=~~~try~(solve~~~~[...] 0. secs (0.u,0.s)
.007122176s +0kb: Chars 5128 - 5224 [#[local]~Instance~spec_of_memc...] 0.001 secs (0.001u,0.s)
.006726138s +0kb: Chars 5225 - 5312 [#[local]~Instance~WHY_spec_of_...] 0. secs (0.u,0.s)
.006783374s +0kb: Chars 5313 - 5371 [Lemma~initfn_ok~:~program_logi...] 0.002 secs (0.002u,0.s)
.006527508s +0kb: Chars 5372 - 5378 [Proof.] 0. secs (0.u,0.s)
.006992945s +0kb: Chars 5381 - 5401 [(repeat~straightline).] 0.036 secs (0.036u,0.s)
.235521453s +5076kb: Chars 5404 - 5422 [straightline_call.] 0.237 secs (0.237u,0.s)
.007685929s +0kb: Chars 5425 - 5426 [{] 0. secs (0.u,0.s)
.007456594s +0kb: Chars 5427 - 5434 [ssplit.] 0. secs (0.u,0.s)
.007040563s +0kb: Chars 5435 - 5447 [eassumption.] 0. secs (0.u,0.s)
.007091876s +0kb: Chars 5448 - 5459 [(rewrite~H2).] 0. secs (0.u,0.s)
.007078149s +0kb: Chars 5460 - 5486 [all:~(vm_compute;~trivial).] 0.003 secs (0.003u,0.s)
.007387833s +0kb: Chars 5487 - 5488 [}] 0. secs (0.u,0.s)
.006781229s +0kb: Chars 5491 - 5511 [(repeat~straightline).] 0.037 secs (0.037u,0.s)
.011847607s +0kb: Chars 5514 - 5587 [(eapply~WeakestPreconditionPro...] 0.019 secs (0.019u,0.s)
.139029949s +0kb: Chars 5590 - 5608 [(eexists;~fwd;~slv).] 0.138 secs (0.138u,0.s)
.006947728s +0kb: Chars 5611 - 5612 [{] 0. secs (0.u,0.s)
.006512388s +0kb: Chars 5613 - 5624 [(vm_compute).] 0. secs (0.u,0.s)
.006819804s +0kb: Chars 5625 - 5646 [intuition~congruence.] 0.014 secs (0.014u,0.s)
.006701987s +0kb: Chars 5647 - 5648 [}] 0. secs (0.u,0.s)
.012798563s +0kb: Chars 5651 - 5724 [(eapply~WeakestPreconditionPro...] 0.024 secs (0.024u,0.s)
.418720807s +0kb: Chars 5727 - 5745 [(eexists;~fwd;~slv).] 0.417 secs (0.417u,0.s)
.008127349s +0kb: Chars 5748 - 5749 [{] 0. secs (0.u,0.s)
.006968646s +0kb: Chars 5750 - 5761 [(vm_compute).] 0. secs (0.u,0.s)
.006421758s +0kb: Chars 5762 - 5783 [intuition~congruence.] 0.014 secs (0.014u,0.s)
.006349887s +0kb: Chars 5784 - 5785 [}] 0. secs (0.u,0.s)
.008709904s +0kb: Chars 5788 - 5861 [(eapply~WeakestPreconditionPro...] 0.022 secs (0.022u,0.s)
.353172589s +0kb: Chars 5864 - 5882 [(eexists;~fwd;~slv).] 0.352 secs (0.351u,0.s)
.009055276s +0kb: Chars 5885 - 5886 [{] 0. secs (0.u,0.s)
.006729171s +0kb: Chars 5887 - 5898 [(vm_compute).] 0. secs (0.u,0.s)
.009111166s +0kb: Chars 5899 - 5920 [intuition~congruence.] 0.024 secs (0.024u,0.s)
.006959043s +0kb: Chars 5921 - 5922 [}] 0. secs (0.u,0.s)
.410001633s +0kb: Chars 5925 - 5969 [(straightline_call;~repeat~str...] 0.416 secs (0.415u,0.s)
.008203620s +0kb: Chars 5972 - 5973 [{] 0. secs (0.u,0.s)
.007396735s +0kb: Chars 5974 - 6070 [(repeat~~~eapply~align_trace_c...] 0.014 secs (0.014u,0.s)
.006493281s +0kb: Chars 6071 - 6072 [}] 0. secs (0.u,0.s)
.006728109s +0kb: Chars 6075 - 6076 [{] 0. secs (0.u,0.s)
.074669918s +0kb: Chars 6077 - 6173 [(repeat~~~(eapply~List.Forall2...] 0.088 secs (0.088u,0.s)
.634429301s +0kb: Chars 6174 - 6223 [all:~(cbv[mmio_event_abstracti...] 0.633 secs (0.633u,0.s)
.007571043s +0kb: Chars 6224 - 6225 [}] 0. secs (0.u,0.s)
.006940086s +0kb: Chars 6228 - 6243 [(cbv[BootSeq]).] 0. secs (0.u,0.s)
.006823396s +0kb: Chars 6246 - 6279 [(eapply~TracePredicate.concat_...] 0. secs (0.u,0.s)
.026445606s +0kb: Chars 6282 - 6322 [2:~(solve~[~cbv[choice];~intui...] 0.046 secs (0.046u,0.s)
.006793365s +0kb: Chars 6325 - 6337 [(cbv[iocfg]).] 0. secs (0.u,0.s)
.006792687s +0kb: Chars 6340 - 6412 [(eapply~(TracePredicate.concat...] 0.004 secs (0.004u,0.s)
.006900584s +0kb: Chars 6415 - 6482 [(eapply~(TracePredicate.concat...] 0.006 secs (0.006u,0.s)
.901681875s +264kb: Chars 6483 - 6487 [Qed.] 0.864 secs (0.864u,0.s)
.009334068s +0kb: Chars 6489 - 6517 [#[local]Open~Scope~list_scope.] 0. secs (0.u,0.s)
.006894956s +0kb: Chars 6518 - 6569 [Require~Crypto.Bedrock.End2End...] 0. secs (0.u,0.s)
.006991903s +0kb: Chars 6570 - 6600 [Import~Tuple~LittleEndianList.] 0. secs (0.u,0.s)
.006922923s +0kb: Chars 6601 - 6646 [#[local]Definition~be2~z~:=~re...] 0. secs (0.u,0.s)
.006806881s +0kb: Chars 6647 - 6687 [#[local]Coercion~to_list~:~tup...] 0. secs (0.u,0.s)
.006575843s +0kb: Chars 6688 - 6722 [#[local]Coercion~Z.b2z~:~bool~...] 0. secs (0.u,0.s)
.007000896s +264kb: Chars 6724 - 6773 [Definition~state~:~Type~:=~lis...] 0. secs (0.u,0.s)
.006983187s +0kb: Chars 6806 - 9751 [Definition~garagedoor_iteratio...] 0.017 secs (0.017u,0.s)
.007040561s +0kb: Chars 9753 - 9838 [#[local]~Instance~spec_of_recv...] 0. secs (0.u,0.s)
.006772806s +0kb: Chars 9839 - 9918 [#[local]~Instance~spec_of_lan9...] 0. secs (0.u,0.s)
.007444007s +0kb: Chars 9919 - 9989 [#[local]Instance~spec_of_memsw...] 0. secs (0.u,0.s)
.006640798s +0kb: Chars 9990 - 10063 [#[local]Instance~spec_of_memeq...] 0. secs (0.u,0.s)
.006982731s +0kb: Chars 10065 - 10568 [#[local]~Instance~spec_of_chac...] 0.015 secs (0.015u,0.s)
.006606744s +0kb: Chars 10570 - 10897 [Definition~memrep~bs~R~:~~~sta...] 0.012 secs (0.012u,0.s)
.007153908s +0kb: Chars 10899 - 11245 [#[global]~Instance~spec_of_loo...] 0.005 secs (0.005u,0.s)
.006895887s +0kb: Chars 11247 - 11262 [Import~ZnWords.] 0. secs (0.u,0.s)
.007066663s +0kb: Chars 11263 - 11298 [Import~coqutil.Tactics.autofor...] 0. secs (0.u,0.s)
.006726035s +0kb: Chars 11300 - 11334 [Import~Crypto.Util.FixCoqMista...] 0. secs (0.u,0.s)
.006841383s +0kb: Chars 11336 - 11394 [Lemma~loopfn_ok~:~program_logi...] 0.004 secs (0.004u,0.s)
.006586893s +0kb: Chars 11395 - 11401 [Proof.] 0. secs (0.u,0.s)
.006534460s +0kb: Chars 11404 - 11417 [straightline.] 0.013 secs (0.013u,0.s)
.007015156s +0kb: Chars 11420 - 11459 [(cbv[memrep~garagedoor_iterati...] 0.001 secs (0.001u,0.s)
.436496670s +0kb: Chars 11462 - 11482 [(repeat~straightline).] 0.506 secs (0.505u,0.s)
.007744314s +0kb: Chars 11485 - 11507 [rename~H11~into~Lseed.] 0. secs (0.u,0.s)
.006596059s +0kb: Chars 11508 - 11528 [rename~H12~into~Lsk.] 0. secs (0.u,0.s)
.006486032s +0kb: Chars 11529 - 11549 [rename~H13~into~H11.] 0. secs (0.u,0.s)
1.020756782s +17688kb: Chars 11552 - 11624 [(straightline_call;~try~ecance...] 1.04 secs (1.039u,0.s)
.975610330s +22704kb: Chars 11627 - 11763 [(intuition~idtac;~repeat~strai...] 0.975 secs (0.964u,0.009s)
.940940147s +15312kb: Chars 11766 - 11778 [2:~(fwd;~slv).] 0.94 secs (0.939u,0.s)
.009905388s +0kb: Chars 11782 - 11805 [(pose~proof~H12~as~Hbuf).] 0. secs (0.u,0.s)
.100128577s +1056kb: Chars 11808 - 11850 [(seprewrite_in~@bytearray_inde...] 0.11 secs (0.109u,0.s)
.007326080s +0kb: Chars 11851 - 11852 [{] 0. secs (0.u,0.s)
.288857612s +2376kb: Chars 11853 - 11861 [ZnWords.] 0.295 secs (0.284u,0.01s)
.008547449s +1176kb: Chars 11862 - 11863 [}] 0. secs (0.u,0.s)
.353233508s +8976kb: Chars 11867 - 11903 [(eexists;~split;~repeat~straig...] 0.361 secs (0.361u,0.s)
2.331045788s +43032kb: Chars 11906 - 12121 [(rewrite~word.unsigned_ltu,~?w...] 2.33 secs (2.309u,0.019s)
.009448263s +1848kb: Chars 12124 - 12128 [2:~{] 0. secs (0.u,0.s)
1.585248802s +29832kb: Chars 12129 - 12138 [(fwd;~slv).] 1.594 secs (1.592u,0.s)
.009315820s +0kb: Chars 12139 - 12145 [right.] 0.002 secs (0.002u,0.s)
.006684667s +0kb: Chars 12146 - 12151 [left.] 0.002 secs (0.002u,0.s)
1.465359863s +7392kb: Chars 12152 - 12184 [(fwd;~slv;~intuition~try~ZnWor...] 1.475 secs (1.474u,0.s)
.009286033s +0kb: Chars 12185 - 12186 [}] 0. secs (0.u,0.s)
.382217842s +7128kb: Chars 12190 - 12210 [(repeat~straightline).] 0.391 secs (0.39u,0.s)
.010460033s +264kb: Chars 12213 - 12261 [(eapply~WeakestPreconditionPro...] 0.01 secs (0.01u,0.s)
.300749157s +5544kb: Chars 12264 - 12300 [(eexists;~split;~repeat~straig...] 0.3 secs (0.299u,0.s)
.418681506s +3168kb: Chars 12304 - 12374 [(destruct~(SepAutoArray.list_e...] 0.417 secs (0.417u,0.s)
.145719073s +528kb: Chars 12377 - 12411 [forget~(List.firstn~12~x3)~as~...] 0.146 secs (0.145u,0.s)
.146152815s +0kb: Chars 12414 - 12467 [forget~(nth~12~x3~Inhabited.de...] 0.145 secs (0.145u,0.s)
.139177906s +264kb: Chars 12470 - 12502 [forget~(List.skipn~13~x3)~as~pp.] 0.139 secs (0.139u,0.s)
.023208204s +0kb: Chars 12505 - 12514 [subst~x3.] 0.022 secs (0.022u,0.s)
.281324586s +3168kb: Chars 12517 - 12592 [(repeat~seprewrite_in~@Array.b...] 0.28 secs (0.28u,0.s)
.536190399s +792kb: Chars 12595 - 12658 [(rewrite~?app_length~in~*;~cbn...] 0.536 secs (0.535u,0.s)
.008565751s +0kb: Chars 12661 - 12695 [(change~(Z.of_nat~12)~with~12~...] 0.008 secs (0.008u,0.s)
.683358541s +10560kb: Chars 12699 - 12719 [(repeat~straightline).] 0.682 secs (0.672u,0.009s)
.043887951s +1584kb: Chars 12723 - 12792 [(destruct~pp~as~[|~ethertype_l...] 0.043 secs (0.043u,0.s)
.006510580s +0kb: Chars 12795 - 12796 [{] 0. secs (0.u,0.s)
.267323962s +3960kb: Chars 12797 - 12814 [(exfalso;~ZnWords).] 0.273 secs (0.273u,0.s)
.009354832s +0kb: Chars 12815 - 12816 [}] 0. secs (0.u,0.s)
.007671507s +0kb: Chars 12819 - 12886 [Import~SetEvars~coqutil.Tactic...] 0. secs (0.u,0.s)
.267351569s +1056kb: Chars 12889 - 12983 [eplace~(word.add~(word.add~buf...] 0.282 secs (0.282u,0.s)
.231890619s +4224kb: Chars 12986 - 13006 [(repeat~straightline).] 0.232 secs (0.231u,0.s)
.154617818s +0kb: Chars 13010 - 13247 [(let~v~:=~constr:((word.or~(wo...] 0.154 secs (0.154u,0.s)
.007410879s +0kb: Chars 13250 - 13251 [{] 0. secs (0.u,0.s)
.006792208s +0kb: Chars 13252 - 13296 [(pose~proof~(byte.unsigned_ran...] 0. secs (0.u,0.s)
.007045819s +0kb: Chars 13301 - 13345 [(pose~proof~(byte.unsigned_ran...] 0. secs (0.u,0.s)
.007618596s +264kb: Chars 13350 - 13374 [subst~v0~v1~v2~v3~v4~v5.] 0. secs (0.u,0.s)
.006290638s +0kb: Chars 13379 - 13431 [(cbn[le_combine];~rewrite~?Z.s...] 0.004 secs (0.004u,0.s)
11.407465406s +8976kb: Chars 13436 - 13555 [rewrite_strat~bottomup~(terms~...] 11.435 secs (11.415u,0.009s)
.422199408s +8712kb: Chars 13560 - 13571 [2:~ZnWords.] 0.421 secs (0.411u,0.01s)
.043480236s +0kb: Chars 13576 - 13653 [(change~(word.wrap~255)~with~(...] 0.043 secs (0.043u,0.s)
2.015548028s +29304kb: Chars 13658 - 13744 [(cbv[word.wrap];~rewrite_strat...] 2.014 secs (2.013u,0.s)
.009737662s +1320kb: Chars 13749 - 13750 [{] 0. secs (0.u,0.s)
.007275817s +0kb: Chars 13751 - 13783 [(rewrite~Z.lor_comm;~reflexivi...] 0. secs (0.u,0.s)
.006881760s +0kb: Chars 13784 - 13785 [}] 0. secs (0.u,0.s)
.007154807s +0kb: Chars 13786 - 13787 [}] 0. secs (0.u,0.s)
.489338696s +2904kb: Chars 13791 - 13827 [(eexists;~split;~repeat~straig...] 0.519 secs (0.519u,0.s)
2.545997135s +52800kb: Chars 13830 - 14046 [(rewrite~word.unsigned_ltu,~?w...] 2.545 secs (2.524u,0.019s)
.009323731s +0kb: Chars 14049 - 14053 [2:~{] 0. secs (0.u,0.s)
3.240464190s +30360kb: Chars 14058 - 14071 [(fwd;~slv;~[~~]).] 3.249 secs (3.246u,0.s)
.009611353s +0kb: Chars 14076 - 14082 [right.] 0.004 secs (0.004u,0.s)
.006766837s +0kb: Chars 14083 - 14088 [left.] 0.002 secs (0.002u,0.s)
.007159553s +0kb: Chars 14089 - 14097 [eexists.] 0. secs (0.u,0.s)
.006908277s +0kb: Chars 14098 - 14122 [(ssplit;~try~eassumption).] 0.003 secs (0.003u,0.s)
.006540892s +0kb: Chars 14123 - 14128 [left.] 0. secs (0.u,0.s)
.273794596s +1056kb: Chars 14133 - 14192 [(rewrite~skipn_app,~skipn_all2...] 0.298 secs (0.298u,0.s)
.008099126s +0kb: Chars 14197 - 14252 [(cbn[List.skipn~minus~firstn~L...] 0. secs (0.u,0.s)
.290448604s +1320kb: Chars 14253 - 14261 [ZnWords.] 0.298 secs (0.297u,0.s)
.009107446s +0kb: Chars 14262 - 14263 [}] 0. secs (0.u,0.s)
.485165489s +4752kb: Chars 14267 - 14338 [(destruct~(SepAutoArray.list_e...] 0.493 secs (0.493u,0.s)
.144669047s +528kb: Chars 14341 - 14375 [forget~(List.firstn~9~pp)~as~i...] 0.144 secs (0.144u,0.s)
.147738730s +0kb: Chars 14378 - 14425 [forget~(nth~9~pp~Inhabited.def...] 0.147 secs (0.147u,0.s)
.143604708s +264kb: Chars 14428 - 14461 [forget~(List.skipn~10~pp)~as~ppp.] 0.143 secs (0.143u,0.s)
.023364128s +0kb: Chars 14464 - 14473 [subst~pp.] 0.022 secs (0.022u,0.s)
.365085704s +3696kb: Chars 14476 - 14551 [(repeat~seprewrite_in~@Array.b...] 0.364 secs (0.354u,0.009s)
.575967780s +1848kb: Chars 14554 - 14618 [(rewrite~?app_length~in~*;~cbn...] 0.575 secs (0.575u,0.s)
.009588018s +0kb: Chars 14621 - 14653 [(change~(Z.of_nat~9)~with~9~in...] 0.008 secs (0.008u,0.s)
.007072097s +0kb: Chars 14656 - 14688 [(change~(Z.of_nat~1)~with~1~in...] 0.008 secs (0.008u,0.s)
1.001451098s +5016kb: Chars 14692 - 14793 [(repeat~eplace~(word.add~(word...] 1. secs (0.989u,0.009s)
.294054625s +3960kb: Chars 14797 - 14817 [(repeat~straightline).] 0.293 secs (0.293u,0.s)
.639787372s +3696kb: Chars 14820 - 14856 [(eexists;~split;~repeat~straig...] 0.639 secs (0.639u,0.s)
.008495001s +0kb: Chars 14859 - 14874 [subst~protocol.] 0. secs (0.u,0.s)
.006880787s +528kb: Chars 14877 - 14916 [(pose~proof~(byte.unsigned_ran...] 0. secs (0.u,0.s)
1.496412590s +20856kb: Chars 14919 - 15019 [(rewrite~word.unsigned_eqb,~?w...] 1.51 secs (1.509u,0.s)
.759113233s +11616kb: Chars 15022 - 15096 [(change~(255)~with~(Z.ones~8);...] 0.758 secs (0.748u,0.009s)
2.071407786s +59400kb: Chars 15099 - 15237 [(destr~Z.eqb;~rewrite~?word.un...] 2.071 secs (2.059u,0.01s)
.009655607s +0kb: Chars 15240 - 15244 [2:~{] 0. secs (0.u,0.s)
3.744094760s +38016kb: Chars 15249 - 15262 [(fwd;~slv;~[~~]).] 3.753 secs (3.74u,0.009s)
.009144291s +0kb: Chars 15267 - 15273 [right.] 0.002 secs (0.002u,0.s)
.006252785s +0kb: Chars 15274 - 15279 [left.] 0.002 secs (0.002u,0.s)
.007100802s +1320kb: Chars 15280 - 15288 [eexists.] 0. secs (0.u,0.s)
.006916173s +0kb: Chars 15289 - 15313 [(ssplit;~try~eassumption).] 0.004 secs (0.004u,0.s)
.007517358s +0kb: Chars 15314 - 15320 [right.] 0. secs (0.u,0.s)
.007056073s +0kb: Chars 15321 - 15326 [left.] 0. secs (0.u,0.s)
.279578474s +528kb: Chars 15331 - 15359 [(rewrite~app_nth2~by~ZnWords).] 0.311 secs (0.311u,0.s)
.008796002s +0kb: Chars 15364 - 15386 [(rewrite~app_comm_cons).] 0. secs (0.u,0.s)
.304857246s +1584kb: Chars 15391 - 15436 [(rewrite~app_nth2~by~SepAutoAr...] 0.312 secs (0.312u,0.s)
.317118374s +1584kb: Chars 15441 - 15486 [(rewrite~app_nth2~by~SepAutoAr...] 0.316 secs (0.316u,0.s)
.317494075s +1848kb: Chars 15491 - 15536 [(rewrite~app_nth1~by~SepAutoAr...] 0.317 secs (0.317u,0.s)
.321623807s +1584kb: Chars 15541 - 15628 [(match~goal~with~~|~|-~context...] 0.321 secs (0.32u,0.s)
.008525080s +792kb: Chars 15633 - 15637 [(cbn).] 0. secs (0.u,0.s)
.006348396s +0kb: Chars 15638 - 15644 [intro.] 0. secs (0.u,0.s)
.006306193s +0kb: Chars 15645 - 15651 [subst.] 0.009 secs (0.009u,0.s)
.006813169s +0kb: Chars 15652 - 15661 [(apply~E1).] 0. secs (0.u,0.s)
.007091306s +0kb: Chars 15662 - 15674 [reflexivity.] 0. secs (0.u,0.s)
.006798158s +0kb: Chars 15675 - 15676 [}] 0. secs (0.u,0.s)
.006700522s +0kb: Chars 15680 - 15700 [(repeat~straightline).] 0.016 secs (0.016u,0.s)
.614689973s +3432kb: Chars 15703 - 15739 [(eexists;~split;~repeat~straig...] 0.635 secs (0.635u,0.s)
.569027402s +6600kb: Chars 15742 - 15815 [(rewrite~word.unsigned_eqb,~?w...] 0.568 secs (0.568u,0.s)
2.029573282s +39336kb: Chars 15818 - 15956 [(destr~Z.eqb;~rewrite~?word.un...] 2.029 secs (2.017u,0.009s)
.009232128s +0kb: Chars 15960 - 15964 [2:~{] 0. secs (0.u,0.s)
.049490044s +0kb: Chars 15969 - 15989 [(repeat~straightline).] 0.059 secs (0.058u,0.s)
.547422841s +4224kb: Chars 15994 - 16030 [(eexists;~split;~repeat~straig...] 0.546 secs (0.546u,0.s)
.556977438s +5280kb: Chars 16035 - 16108 [(rewrite~word.unsigned_eqb,~?w...] 0.556 secs (0.556u,0.s)
2.078699421s +50424kb: Chars 16113 - 16251 [(destr~Z.eqb;~rewrite~?word.un...] 2.078 secs (2.067u,0.01s)
.009843366s +0kb: Chars 16256 - 16260 [2:~{] 0. secs (0.u,0.s)
3.803063797s +28248kb: Chars 16267 - 16276 [(fwd;~slv).] 3.812 secs (3.799u,0.009s)
.009277306s +528kb: Chars 16283 - 16289 [right.] 0.002 secs (0.002u,0.s)
.006803346s +0kb: Chars 16290 - 16295 [left.] 0.002 secs (0.002u,0.s)
.007086526s +0kb: Chars 16296 - 16304 [eexists.] 0.001 secs (0.001u,0.s)
.006801994s +0kb: Chars 16305 - 16329 [(ssplit;~try~eassumption).] 0.004 secs (0.004u,0.s)
.007703391s +0kb: Chars 16330 - 16336 [right.] 0. secs (0.u,0.s)
.007171465s +0kb: Chars 16337 - 16343 [right.] 0. secs (0.u,0.s)
.305093037s +2112kb: Chars 16344 - 16369 [SepAutoArray.listZnWords.] 0.337 secs (0.337u,0.s)
.009966274s +0kb: Chars 16370 - 16371 [}] 0. secs (0.u,0.s)
1.311841187s +4224kb: Chars 16376 - 16396 [(repeat~straightline).] 1.321 secs (1.32u,0.s)
1.213396614s +11880kb: Chars 16401 - 16477 [(straightline_call;~ssplit;~tr...] 1.213 secs (1.201u,0.009s)
.008269198s +0kb: Chars 16482 - 16483 [{] 0. secs (0.u,0.s)
.006721912s +0kb: Chars 16484 - 16488 [(compute).] 0. secs (0.u,0.s)
.006855307s +0kb: Chars 16489 - 16501 [(inversion~1).] 0. secs (0.u,0.s)
.006252886s +0kb: Chars 16502 - 16503 [}] 0. secs (0.u,0.s)
.356938502s +4752kb: Chars 16509 - 16585 [(rename~Lppp~into~Lihl;~assert...] 0.384 secs (0.383u,0.s)
.477193685s +8184kb: Chars 16591 - 16611 [(repeat~straightline).] 0.476 secs (0.476u,0.s)
.009477523s +0kb: Chars 16616 - 16681 [(pose~proof~(List.firstn_skipn...] 0. secs (0.u,0.s)
.396494698s +4488kb: Chars 16686 - 16762 [(pose~proof~(@firstn_length_le...] 0.404 secs (0.403u,0.s)
.053060432s +0kb: Chars 16767 - 16838 [(pose~proof~(skipn_length~(14~...] 0.053 secs (0.053u,0.s)
.158228137s +1056kb: Chars 16843 - 16899 [forget~(List.firstn~(14~+~20~+...] 0.157 secs (0.157u,0.s)
.154705007s +264kb: Chars 16904 - 16960 [forget~(List.skipn~(14~+~20~+~...] 0.154 secs (0.154u,0.s)
.008210271s +0kb: Chars 16965 - 16989 [(simpl~minus~in~H31,~H32).] 0.001 secs (0.001u,0.s)
.033765964s +528kb: Chars 16994 - 17004 [subst~ppp.] 0.039 secs (0.039u,0.s)
.399123786s +10560kb: Chars 17009 - 17069 [(repeat~rewrite~?(app_assoc~_~...] 0.398 secs (0.398u,0.s)
.270077227s +2112kb: Chars 17074 - 17149 [(do~3~(seprewrite_in~@Array.by...] 0.27 secs (0.269u,0.s)
.008972124s +0kb: Chars 17155 - 17215 [(change~(unsigned~x)~with~(@wo...] 0. secs (0.u,0.s)
.008898761s +0kb: Chars 17220 - 17240 [(repeat~straightline).] 0.017 secs (0.017u,0.s)
.006772077s +528kb: Chars 17245 - 17290 [(pose~proof~(List.firstn_skipn...] 0. secs (0.u,0.s)
.409886182s +4488kb: Chars 17295 - 17351 [(pose~proof~(@firstn_length_le...] 0.415 secs (0.414u,0.s)
.008640789s +0kb: Chars 17356 - 17388 [(pose~proof~(skipn_length~16~p...] 0. secs (0.u,0.s)
.044490899s +1056kb: Chars 17389 - 17406 [(rewrite~H32~in~*).] 0.053 secs (0.052u,0.s)
.160300897s +0kb: Chars 17411 - 17448 [forget~(List.firstn~16~pPPP)~a...] 0.159 secs (0.159u,0.s)
.156082329s +264kb: Chars 17453 - 17492 [forget~(List.skipn~16~pPPP)~as...] 0.155 secs (0.155u,0.s)
.041702051s +0kb: Chars 17497 - 17508 [subst~pPPP.] 0.041 secs (0.041u,0.s)
.116599182s +1848kb: Chars 17513 - 17589 [(seprewrite_in_by~(Array.bytea...] 0.116 secs (0.116u,0.s)
.698956588s +264kb: Chars 17595 - 17688 [(remember~~~(le_split~32~~~~~~...] 0.698 secs (0.697u,0.s)
.068024379s +1056kb: Chars 17693 - 17713 [(repeat~straightline).] 0.068 secs (0.058u,0.009s)
.007466762s +0kb: Chars 17718 - 17762 [(pose~proof~(List.firstn_skipn...] 0. secs (0.u,0.s)
.429092562s +5544kb: Chars 17767 - 17857 [(pose~proof~(@firstn_length_le...] 0.435 secs (0.434u,0.s)
.008938296s +0kb: Chars 17862 - 17892 [(pose~proof~(skipn_length~16~v...] 0. secs (0.u,0.s)
.152917137s +1056kb: Chars 17897 - 17931 [forget~(List.firstn~16~vv)~as~...] 0.161 secs (0.161u,0.s)
.158379379s +264kb: Chars 17936 - 17969 [forget~(List.skipn~16~vv)~as~vv1.] 0.158 secs (0.158u,0.s)
.006814537s +0kb: Chars 17974 - 17983 [subst~vv.] 0. secs (0.u,0.s)
.006791774s +0kb: Chars 17988 - 18009 [(rewrite~<-~Hvv~in~H33).] 0.006 secs (0.006u,0.s)
.334437521s +528kb: Chars 18014 - 18043 [(rewrite~length_le_split~in~*).] 0.339 secs (0.339u,0.s)
.170307481s +1056kb: Chars 18048 - 18123 [(seprewrite_in_by~(Array.bytea...] 0.169 secs (0.169u,0.s)
.017767205s +0kb: Chars 18129 - 18149 [(repeat~straightline).] 0.017 secs (0.017u,0.s)
.314316886s +1848kb: Chars 18154 - 18180 [(straightline_call;~ssplit).] 0.314 secs (0.313u,0.s)
.007837746s +0kb: Chars 18185 - 18186 [{] 0. secs (0.u,0.s)
.058767725s +2376kb: Chars 18187 - 18206 [ecancel_assumption.] 0.066 secs (0.056u,0.009s)
.007117129s +0kb: Chars 18207 - 18208 [}] 0. secs (0.u,0.s)
.006617566s +0kb: Chars 18213 - 18214 [{] 0. secs (0.u,0.s)
.007341459s +0kb: Chars 18215 - 18234 [use_sep_assumption.] 0.002 secs (0.002u,0.s)
.006627384s +0kb: Chars 18235 - 18242 [cancel.] 0.024 secs (0.024u,0.s)
.017410660s +0kb: Chars 18243 - 18278 [(cancel_seps_at_indices~2%nat~...] 0.017 secs (0.017u,0.s)
.007208220s +0kb: Chars 18285 - 18286 [{] 0. secs (0.u,0.s)
.735050562s +19008kb: Chars 18287 - 18305 [Morphisms.f_equiv.] 0.741 secs (0.73u,0.009s)
1.128678669s +8976kb: Chars 18306 - 18331 [SepAutoArray.listZnWords.] 1.128 secs (1.127u,0.s)
.008983667s +0kb: Chars 18332 - 18333 [}] 0. secs (0.u,0.s)
.007028602s +0kb: Chars 18340 - 18353 [ecancel_done.] 0.007 secs (0.007u,0.s)
.006926056s +0kb: Chars 18354 - 18355 [}] 0. secs (0.u,0.s)
.007375420s +0kb: Chars 18360 - 18361 [{] 0. secs (0.u,0.s)
.568995526s +6864kb: Chars 18362 - 18370 [ZnWords.] 0.591 secs (0.591u,0.s)
.009443900s +1056kb: Chars 18371 - 18372 [}] 0. secs (0.u,0.s)
.006925836s +0kb: Chars 18377 - 18378 [{] 0. secs (0.u,0.s)
.578707782s +6336kb: Chars 18379 - 18387 [ZnWords.] 0.594 secs (0.593u,0.s)
.007772188s +0kb: Chars 18388 - 18389 [}] 0. secs (0.u,0.s)
.708385492s +13200kb: Chars 18394 - 18414 [(repeat~straightline).] 0.715 secs (0.715u,0.s)
.018321654s +0kb: Chars 18420 - 18440 [(repeat~straightline).] 0.018 secs (0.018u,0.s)
.317424582s +1848kb: Chars 18445 - 18471 [(straightline_call;~ssplit).] 0.317 secs (0.316u,0.s)
.008400958s +0kb: Chars 18476 - 18477 [{] 0. secs (0.u,0.s)
.006537440s +0kb: Chars 18478 - 18497 [use_sep_assumption.] 0.002 secs (0.002u,0.s)
.012873849s +0kb: Chars 18498 - 18505 [cancel.] 0.024 secs (0.024u,0.s)
.012219168s +0kb: Chars 18506 - 18541 [(cancel_seps_at_indices~1%nat~...] 0.011 secs (0.011u,0.s)
.006879905s +1320kb: Chars 18548 - 18549 [{] 0. secs (0.u,0.s)
.795034793s +21912kb: Chars 18550 - 18568 [Morphisms.f_equiv.] 0.801 secs (0.8u,0.s)
1.111288275s +11352kb: Chars 18569 - 18594 [SepAutoArray.listZnWords.] 1.111 secs (1.11u,0.s)
.009270250s +0kb: Chars 18595 - 18596 [}] 0. secs (0.u,0.s)
.006958135s +0kb: Chars 18603 - 18616 [ecancel_done.] 0.005 secs (0.005u,0.s)
.006811149s +0kb: Chars 18617 - 18618 [}] 0. secs (0.u,0.s)
.006299747s +0kb: Chars 18623 - 18624 [{] 0. secs (0.u,0.s)
.007360311s +0kb: Chars 18625 - 18644 [use_sep_assumption.] 0.002 secs (0.002u,0.s)
.006369011s +792kb: Chars 18645 - 18652 [cancel.] 0.025 secs (0.024u,0.s)
.007083979s +0kb: Chars 18653 - 18688 [(cancel_seps_at_indices~2%nat~...] 0.015 secs (0.015u,0.s)
.006451204s +0kb: Chars 18695 - 18696 [{] 0. secs (0.u,0.s)
.772327472s +18744kb: Chars 18697 - 18715 [Morphisms.f_equiv.] 0.779 secs (0.768u,0.009s)
1.208238695s +11616kb: Chars 18716 - 18741 [SepAutoArray.listZnWords.] 1.207 secs (1.207u,0.s)
.009803840s +0kb: Chars 18742 - 18743 [}] 0. secs (0.u,0.s)
.006519779s +0kb: Chars 18750 - 18763 [ecancel_done.] 0.005 secs (0.005u,0.s)
.007075301s +0kb: Chars 18764 - 18765 [}] 0. secs (0.u,0.s)
.007559931s +1056kb: Chars 18770 - 18771 [{] 0. secs (0.u,0.s)
.638099917s +6336kb: Chars 18772 - 18780 [ZnWords.] 0.663 secs (0.662u,0.s)
.008290118s +0kb: Chars 18781 - 18782 [}] 0. secs (0.u,0.s)
.006315241s +0kb: Chars 18787 - 18788 [{] 0. secs (0.u,0.s)
.653897088s +8184kb: Chars 18789 - 18797 [ZnWords.] 0.668 secs (0.667u,0.s)
.009350679s +0kb: Chars 18798 - 18799 [}] 0. secs (0.u,0.s)
.383831763s +7656kb: Chars 18805 - 18825 [(repeat~straightline).] 0.393 secs (0.392u,0.s)
.010704667s +0kb: Chars 18830 - 18838 [eexists.] 0.01 secs (0.01u,0.s)
.010672790s +0kb: Chars 18839 - 18845 [split.] 0.01 secs (0.01u,0.s)
1.225114483s +3696kb: Chars 18846 - 18866 [(repeat~straightline).] 1.224 secs (1.223u,0.s)
.041409763s +1848kb: Chars 18871 - 18933 [(eexists~_,_;~split;~[~eapply~...] 0.041 secs (0.041u,0.s)
.166127867s +7920kb: Chars 18938 - 18963 [(eexists;~ssplit;~trivial).] 0.165 secs (0.165u,0.s)
.006611607s +0kb: Chars 18968 - 18969 [{] 0. secs (0.u,0.s)
.006892806s +0kb: Chars 18970 - 18974 [(compute).] 0.001 secs (0.001u,0.s)
.006599438s +0kb: Chars 18975 - 18981 [clear.] 0. secs (0.u,0.s)
.006318549s +0kb: Chars 18982 - 19003 [intuition~congruence.] 0.002 secs (0.002u,0.s)
.006507498s +0kb: Chars 19004 - 19005 [}] 0. secs (0.u,0.s)
.303273462s +6072kb: Chars 19011 - 19031 [(repeat~straightline).] 0.33 secs (0.33u,0.s)
.013449217s +1056kb: Chars 19036 - 19044 [eexists.] 0.013 secs (0.013u,0.s)
.012174689s +0kb: Chars 19045 - 19051 [split.] 0.011 secs (0.011u,0.s)
5.790857036s +6072kb: Chars 19052 - 19072 [(repeat~straightline).] 5.79 secs (5.787u,0.s)
.045946354s +1584kb: Chars 19077 - 19139 [(eexists~_,_;~split;~[~eapply~...] 0.045 secs (0.045u,0.s)
.037588509s +0kb: Chars 19144 - 19169 [(eexists;~ssplit;~trivial).] 0.037 secs (0.037u,0.s)
.174939410s +6336kb: Chars 19174 - 19199 [(eexists;~ssplit;~trivial).] 0.174 secs (0.173u,0.s)
.007505084s +264kb: Chars 19204 - 19205 [{] 0. secs (0.u,0.s)
.006436146s +264kb: Chars 19206 - 19210 [(compute).] 0.001 secs (0.001u,0.s)
.006546993s +0kb: Chars 19211 - 19217 [clear.] 0. secs (0.u,0.s)
.007232197s +0kb: Chars 19218 - 19239 [intuition~congruence.] 0.002 secs (0.002u,0.s)
.007079389s +0kb: Chars 19240 - 19241 [}] 0. secs (0.u,0.s)
.072811357s +264kb: Chars 19246 - 19266 [(repeat~straightline).] 0.102 secs (0.102u,0.s)
.048900554s +2112kb: Chars 19272 - 19318 [(eapply~map.split_empty_r~in~H...] 0.048 secs (0.048u,0.s)
.047672560s +0kb: Chars 19323 - 19369 [(eapply~map.split_empty_r~in~H...] 0.047 secs (0.047u,0.s)
.885992572s +12672kb: Chars 19374 - 19443 [(seprewrite_in_by~@bytearray_i...] 0.885 secs (0.884u,0.s)
1.077274355s +10824kb: Chars 19448 - 19517 [(seprewrite_in_by~@bytearray_i...] 1.076 secs (1.076u,0.s)
2.008381961s +20856kb: Chars 19522 - 19591 [(seprewrite_in_by~@bytearray_i...] 2.008 secs (1.996u,0.009s)
.887593743s +10296kb: Chars 19596 - 19665 [(seprewrite_in_by~@bytearray_i...] 0.887 secs (0.886u,0.s)
.881446616s +10032kb: Chars 19670 - 19739 [(seprewrite_in_by~@bytearray_i...] 0.881 secs (0.88u,0.s)
.576760523s +7920kb: Chars 19744 - 19810 [(assert~(length~(vv0~++~vv1)~=...] 0.576 secs (0.575u,0.s)
.008258192s +0kb: Chars 19817 - 19861 [(change~(word.of_Z~134217728)~...] 0. secs (0.u,0.s)
.013420225s +0kb: Chars 19866 - 19886 [(repeat~straightline).] 0.021 secs (0.02u,0.s)
2.570913297s +16368kb: Chars 19891 - 19928 [(eexists;~ssplit;~repeat~strai...] 2.57 secs (2.568u,0.s)
.008653399s +0kb: Chars 19933 - 19934 [{] 0. secs (0.u,0.s)
.333077882s +2112kb: Chars 20043 - 20069 [(straightline_call;~ssplit).] 0.341 secs (0.341u,0.s)
.009425767s +0kb: Chars 20076 - 20077 [{] 0. secs (0.u,0.s)
1.620854757s +13728kb: Chars 20078 - 20147 [(seprewrite_in_by~@bytearray_i...] 1.629 secs (1.628u,0.s)
.056782467s +1584kb: Chars 20156 - 20175 [ecancel_assumption.] 0.057 secs (0.057u,0.s)
.007394603s +0kb: Chars 20176 - 20177 [}] 0. secs (0.u,0.s)
.006981019s +0kb: Chars 20184 - 20185 [{] 0. secs (0.u,0.s)
.740445773s +9768kb: Chars 20186 - 20211 [SepAutoArray.listZnWords.] 0.753 secs (0.753u,0.s)
.009447869s +0kb: Chars 20212 - 20213 [}] 0. secs (0.u,0.s)
.007606607s +0kb: Chars 20220 - 20221 [{] 0. secs (0.u,0.s)
.094588103s +792kb: Chars 20222 - 20241 [ecancel_assumption.] 0.111 secs (0.111u,0.s)
.006903347s +0kb: Chars 20242 - 20243 [}] 0. secs (0.u,0.s)
.006918017s +0kb: Chars 20250 - 20251 [{] 0. secs (0.u,0.s)
.724039062s +9504kb: Chars 20252 - 20277 [SepAutoArray.listZnWords.] 0.737 secs (0.726u,0.009s)
.008960041s +0kb: Chars 20278 - 20279 [}] 0. secs (0.u,0.s)
.006483759s +0kb: Chars 20286 - 20287 [{] 0. secs (0.u,0.s)
.006627027s +0kb: Chars 20288 - 20340 [(rewrite~<-~(List.firstn_skipn...] 0.004 secs (0.004u,0.s)
.096531879s +792kb: Chars 20349 - 20449 [(seprewrite_in_by~(Array.bytea...] 0.114 secs (0.114u,0.s)
.062808196s +792kb: Chars 20458 - 20477 [ecancel_assumption.] 0.062 secs (0.062u,0.s)
.006864585s +0kb: Chars 20478 - 20479 [}] 0. secs (0.u,0.s)
.007597918s +0kb: Chars 20486 - 20487 [{] 0. secs (0.u,0.s)
.731654318s +9240kb: Chars 20488 - 20513 [SepAutoArray.listZnWords.] 0.745 secs (0.745u,0.s)
.007687969s +264kb: Chars 20514 - 20515 [}] 0. secs (0.u,0.s)
.634033719s +11880kb: Chars 20522 - 20542 [(repeat~straightline).] 0.64 secs (0.64u,0.s)
.007626599s +0kb: Chars 20550 - 20593 [(rewrite~<-~(List.firstn_skipn...] 0.003 secs (0.003u,0.s)
.093252043s +528kb: Chars 20600 - 20691 [(seprewrite_in_by~(Array.bytea...] 0.096 secs (0.096u,0.s)
1.212882274s +8712kb: Chars 20698 - 20837 [replace~(word.of_Z~(BinInt.Z.o...] 1.211 secs (1.191u,0.019s)
.055340344s +1320kb: Chars 20845 - 20861 [(ssplit;~trivial).] 0.055 secs (0.055u,0.s)
3.953769337s +43824kb: Chars 20868 - 20946 [(eexists~_,_,_;~ssplit;~try~ec...] 3.952 secs (3.9u,0.049s)
.010215238s +0kb: Chars 20952 - 20968 [(eexists;~ssplit).] 0.01 secs (0.01u,0.s)
.007265375s +0kb: Chars 20973 - 20974 [{] 0. secs (0.u,0.s)
.007006970s +0kb: Chars 20975 - 20986 [subst~a0~a.] 0.002 secs (0.002u,0.s)
.006718063s +0kb: Chars 20987 - 21023 [(change~(?x~::~?y~::~?t)~with~...] 0.004 secs (0.004u,0.s)
.007360398s +0kb: Chars 21024 - 21042 [(rewrite~app_assoc).] 0.009 secs (0.009u,0.s)
.018534373s +0kb: Chars 21043 - 21051 [trivial.] 0.028 secs (0.028u,0.s)
.007529772s +1320kb: Chars 21052 - 21053 [}] 0. secs (0.u,0.s)
.009307831s +1320kb: Chars 21058 - 21074 [(eexists;~ssplit).] 0.016 secs (0.016u,0.s)
.006683436s +0kb: Chars 21079 - 21080 [{] 0. secs (0.u,0.s)
.030245477s +0kb: Chars 21081 - 21117 [(eapply~Forall2_app;~try~eassu...] 0.036 secs (0.036u,0.s)
.006410343s +0kb: Chars 21124 - 21144 [(eapply~Forall2_cons).] 0.002 secs (0.002u,0.s)
.007249382s +0kb: Chars 21145 - 21167 [2:~(eapply~Forall2_cons).] 0.001 secs (0.001u,0.s)
.006640157s +0kb: Chars 21168 - 21189 [3:~(eapply~Forall2_nil).] 0. secs (0.u,0.s)
.112139504s +6072kb: Chars 21196 - 21245 [all:~([>left~|~right~];~eexist...] 0.126 secs (0.126u,0.s)
.007195064s +0kb: Chars 21246 - 21247 [}] 0. secs (0.u,0.s)
.006243594s +0kb: Chars 21252 - 21258 [right.] 0.005 secs (0.005u,0.s)
.006963303s +0kb: Chars 21263 - 21269 [right.] 0.004 secs (0.004u,0.s)
.090017244s +7656kb: Chars 21274 - 21326 [eexists~_,_,_,_,_,_,_,_,_,_,_,...] 0.099 secs (0.099u,0.s)
.027638691s +0kb: Chars 21327 - 21349 [(left;~ssplit;~trivial).] 0.027 secs (0.027u,0.s)
.018800830s +0kb: Chars 21354 - 21367 [eexists~_,_.] 0.018 secs (0.018u,0.s)
.006661862s +0kb: Chars 21372 - 21378 [split.] 0.003 secs (0.003u,0.s)
.006640756s +0kb: Chars 21383 - 21384 [{] 0. secs (0.u,0.s)
.006677202s +0kb: Chars 21389 - 21422 [(eapply~TracePredicate.concat_...] 0.002 secs (0.002u,0.s)
.459233173s +4224kb: Chars 21427 - 21495 [1:~(match~goal~with~~~~~|~|-~_...] 0.472 secs (0.471u,0.s)
.008928129s +0kb: Chars 21501 - 21510 [symmetry.] 0. secs (0.u,0.s)
.056922861s +528kb: Chars 21556 - 21614 [(rewrite~<-~(firstn_skipn~6~ma...] 0.065 secs (0.065u,0.s)
.026769016s +0kb: Chars 21619 - 21680 [(eapply~(f_equal2~app);~[~rewr...] 0.026 secs (0.026u,0.s)
.027277399s +0kb: Chars 21685 - 21746 [(eapply~(f_equal2~app);~[~rewr...] 0.026 secs (0.026u,0.s)
.007134253s +0kb: Chars 21751 - 21789 [(change~([?x]~++~?y~::~?z)~wit...] 0.007 secs (0.007u,0.s)
.007307168s +0kb: Chars 21794 - 21816 [(eapply~(f_equal2~app)).] 0.001 secs (0.001u,0.s)
.006940769s +0kb: Chars 21821 - 21822 [{] 0. secs (0.u,0.s)
.006734433s +0kb: Chars 21823 - 21833 [(cbv[be2]).] 0. secs (0.u,0.s)
.007124765s +0kb: Chars 21834 - 21904 [(progress~change~2%nat~with~(L...] 0. secs (0.u,0.s)
.025382636s +792kb: Chars 21911 - 21952 [(setoid_rewrite~split_le_combi...] 0.05 secs (0.05u,0.s)
.006304261s +0kb: Chars 21953 - 21954 [}] 0. secs (0.u,0.s)
.056503898s +0kb: Chars 21959 - 22018 [(rewrite~<-~(firstn_skipn~2~ih...] 0.062 secs (0.062u,0.s)
.026457487s +0kb: Chars 22023 - 22084 [(eapply~(f_equal2~app);~[~rewr...] 0.025 secs (0.025u,0.s)
.069884323s +0kb: Chars 22089 - 22179 [(rewrite~<-~(firstn_skipn~2~(L...] 0.069 secs (0.069u,0.s)
.007345926s +0kb: Chars 22184 - 22206 [(eapply~(f_equal2~app)).] 0.001 secs (0.001u,0.s)
.006394768s +0kb: Chars 22211 - 22212 [{] 0. secs (0.u,0.s)
.007171812s +0kb: Chars 22213 - 22223 [(cbv[be2]).] 0. secs (0.u,0.s)
.438109768s +1584kb: Chars 22224 - 22258 [(eplace~2%nat~with~_~at~3;~cyc...] 0.456 secs (0.455u,0.s)
.023805803s +0kb: Chars 22265 - 22315 [(rewrite~split_le_combine,~rev...] 0.023 secs (0.023u,0.s)
.007921053s +0kb: Chars 22322 - 22341 [(rewrite~rev_length).] 0. secs (0.u,0.s)
.872553955s +8712kb: Chars 22342 - 22367 [SepAutoArray.listZnWords.] 0.878 secs (0.878u,0.s)
.008635122s +0kb: Chars 22368 - 22369 [}] 0. secs (0.u,0.s)
.017173595s +0kb: Chars 22374 - 22435 [(eapply~(f_equal2~app);~[~rewr...] 0.025 secs (0.025u,0.s)
.006673807s +0kb: Chars 22440 - 22462 [(eapply~(f_equal2~app)).] 0.001 secs (0.001u,0.s)
.006659626s +0kb: Chars 22463 - 22464 [{] 0. secs (0.u,0.s)
.007269295s +0kb: Chars 22465 - 22473 [f_equal.] 0.018 secs (0.018u,0.s)
.006873517s +0kb: Chars 22474 - 22499 [(eapply~byte.unsigned_inj).] 0. secs (0.u,0.s)
.006674878s +0kb: Chars 22500 - 22511 [(rewrite~E1).] 0. secs (0.u,0.s)
.009535177s +0kb: Chars 22512 - 22520 [trivial.] 0.022 secs (0.022u,0.s)
.006313374s +0kb: Chars 22521 - 22522 [}] 0. secs (0.u,0.s)
.053350579s +0kb: Chars 22527 - 22585 [(rewrite~<-~(firstn_skipn~2~pP...] 0.059 secs (0.059u,0.s)
.006771303s +0kb: Chars 22590 - 22612 [(eapply~(f_equal2~app)).] 0.001 secs (0.001u,0.s)
.006834349s +2904kb: Chars 22617 - 22618 [{] 0. secs (0.u,0.s)
.452649552s +264kb: Chars 22619 - 22653 [(eplace~2%nat~with~_~at~2;~cyc...] 0.463 secs (0.453u,0.009s)
.022612006s +0kb: Chars 22660 - 22694 [(rewrite~split_le_combine;~tri...] 0.022 secs (0.022u,0.s)
.873549607s +8184kb: Chars 22701 - 22726 [SepAutoArray.listZnWords.] 0.872 secs (0.872u,0.s)
.010509648s +0kb: Chars 22727 - 22728 [}] 0. secs (0.u,0.s)
.065547241s +0kb: Chars 22733 - 22823 [(rewrite~<-~(firstn_skipn~4~(L...] 0.075 secs (0.075u,0.s)
.025895718s +0kb: Chars 22828 - 22889 [(eapply~(f_equal2~app);~[~rewr...] 0.025 secs (0.025u,0.s)
.073380000s +792kb: Chars 22894 - 22984 [(rewrite~<-~(firstn_skipn~4~(L...] 0.072 secs (0.072u,0.s)
.027799205s +0kb: Chars 22989 - 23050 [(eapply~(f_equal2~app);~[~rewr...] 0.027 secs (0.027u,0.s)
.064771864s +0kb: Chars 23055 - 23145 [(rewrite~<-~(firstn_skipn~2~(L...] 0.064 secs (0.064u,0.s)
.027255015s +0kb: Chars 23150 - 23211 [(eapply~(f_equal2~app);~[~rewr...] 0.026 secs (0.026u,0.s)
.064123775s +0kb: Chars 23216 - 23306 [(rewrite~<-~(firstn_skipn~2~(L...] 0.063 secs (0.063u,0.s)
.028379448s +1848kb: Chars 23311 - 23372 [(eapply~(f_equal2~app);~[~rewr...] 0.028 secs (0.027u,0.s)
.063254922s +0kb: Chars 23377 - 23467 [(rewrite~<-~(firstn_skipn~2~(L...] 0.062 secs (0.062u,0.s)
.006588955s +0kb: Chars 23472 - 23494 [(eapply~(f_equal2~app)).] 0.001 secs (0.001u,0.s)
.006601066s +0kb: Chars 23499 - 23500 [{] 0. secs (0.u,0.s)
.006895387s +0kb: Chars 23501 - 23511 [(cbv[be2]).] 0. secs (0.u,0.s)
.442650880s +1584kb: Chars 23512 - 23546 [(eplace~2%nat~with~_~at~7;~cyc...] 0.46 secs (0.46u,0.s)
.023807399s +0kb: Chars 23553 - 23603 [(rewrite~split_le_combine,~rev...] 0.023 secs (0.023u,0.s)
.007266818s +0kb: Chars 23610 - 23629 [(rewrite~rev_length).] 0. secs (0.u,0.s)
.855729668s +7392kb: Chars 23630 - 23655 [SepAutoArray.listZnWords.] 0.861 secs (0.86u,0.s)
.009998967s +0kb: Chars 23656 - 23657 [}] 0. secs (0.u,0.s)
.052381673s +1056kb: Chars 23662 - 23752 [(rewrite~<-~(firstn_skipn~2~(L...] 0.062 secs (0.062u,0.s)
.006522704s +528kb: Chars 23757 - 23779 [(eapply~(f_equal2~app)).] 0.004 secs (0.004u,0.s)
.007236344s +0kb: Chars 23784 - 23785 [{] 0. secs (0.u,0.s)
.006649515s +0kb: Chars 23786 - 23796 [(cbv[be2]).] 0. secs (0.u,0.s)
.442811644s +264kb: Chars 23797 - 23831 [(eplace~2%nat~with~_~at~8;~cyc...] 0.457 secs (0.457u,0.s)
.023691637s +0kb: Chars 23838 - 23888 [(rewrite~split_le_combine,~rev...] 0.023 secs (0.023u,0.s)
.006965942s +0kb: Chars 23895 - 23914 [(rewrite~rev_length).] 0. secs (0.u,0.s)
.872080631s +8712kb: Chars 23915 - 23940 [SepAutoArray.listZnWords.] 0.877 secs (0.876u,0.s)
.008762388s +0kb: Chars 23941 - 23942 [}] 0. secs (0.u,0.s)
.006973383s +0kb: Chars 23947 - 23969 [(eapply~(f_equal2~app)).] 0.003 secs (0.003u,0.s)
.006866838s +0kb: Chars 23970 - 23971 [{] 0. secs (0.u,0.s)
.010001446s +0kb: Chars 23972 - 24007 [(rewrite~to_list_from_list;~tr...] 0.029 secs (0.029u,0.s)
.006800185s +0kb: Chars 24008 - 24009 [}] 0. secs (0.u,0.s)
.006410403s +0kb: Chars 24014 - 24026 [reflexivity.] 0. secs (0.u,0.s)
.006880063s +0kb: Chars 24032 - 24063 [(change~[?x;~?y]~with~([x]~++~...] 0.005 secs (0.005u,0.s)
.045778338s +3432kb: Chars 24068 - 24136 [(eapply~TracePredicate.concat_...] 0.059 secs (0.059u,0.s)
.006902714s +0kb: Chars 24137 - 24138 [}] 0. secs (0.u,0.s)
.006358026s +0kb: Chars 24144 - 24158 [(rewrite~<-~Hvv).] 0.002 secs (0.002u,0.s)
1.763473971s +20328kb: Chars 24163 - 24209 [(rewrite~!ListUtil.firstn_app_...] 1.773 secs (1.771u,0.s)
.879363064s +6336kb: Chars 24214 - 24259 [(rewrite~!ListUtil.skipn_app_s...] 0.879 secs (0.878u,0.s)
.082753852s +1584kb: Chars 24264 - 24325 [(eexists~_,_;~ssplit;~try~eass...] 0.082 secs (0.082u,0.s)
.006652985s +0kb: Chars 24331 - 24347 [(intros;~exfalso).] 0. secs (0.u,0.s)
.006842635s +0kb: Chars 24348 - 24358 [(apply~H39).] 0. secs (0.u,0.s)
.006996167s +0kb: Chars 24363 - 24395 [(rewrite~word.unsigned_or_nowr...] 0.002 secs (0.002u,0.s)
.007092348s +0kb: Chars 24396 - 24423 [(apply~Z.lor_eq_0_iff;~auto).] 0.022 secs (0.022u,0.s)
.006845703s +0kb: Chars 24446 - 24447 [}] 0. secs (0.u,0.s)
.050076360s +3168kb: Chars 24453 - 24469 [(ssplit;~trivial).] 0.058 secs (0.058u,0.s)
3.392910691s +39864kb: Chars 24474 - 24552 [(eexists~_,_,_;~ssplit;~try~ec...] 3.391 secs (3.379u,0.009s)
.010389459s +0kb: Chars 24557 - 24573 [(eexists;~ssplit).] 0.01 secs (0.01u,0.s)
.006806269s +0kb: Chars 24578 - 24579 [{] 0. secs (0.u,0.s)
.006635503s +0kb: Chars 24580 - 24588 [subst~a.] 0.002 secs (0.002u,0.s)
.007597333s +0kb: Chars 24589 - 24625 [(change~(?x~::~?y~::~?t)~with~...] 0.003 secs (0.003u,0.s)
.006874643s +0kb: Chars 24626 - 24644 [(rewrite~app_assoc).] 0.009 secs (0.009u,0.s)
.016274409s +0kb: Chars 24645 - 24653 [trivial.] 0.028 secs (0.028u,0.s)
.006793283s +264kb: Chars 24654 - 24655 [}] 0. secs (0.u,0.s)
.010394717s +2640kb: Chars 24660 - 24676 [(eexists;~ssplit).] 0.016 secs (0.016u,0.s)
.006578227s +0kb: Chars 24681 - 24682 [{] 0. secs (0.u,0.s)
.027700732s +0kb: Chars 24683 - 24719 [(eapply~Forall2_app;~try~eassu...] 0.034 secs (0.034u,0.s)
.007143502s +0kb: Chars 24726 - 24746 [(eapply~Forall2_cons).] 0.002 secs (0.002u,0.s)
.006928195s +0kb: Chars 24747 - 24769 [2:~(eapply~Forall2_cons).] 0.001 secs (0.001u,0.s)
.007200358s +0kb: Chars 24770 - 24791 [3:~(eapply~Forall2_nil).] 0. secs (0.u,0.s)
.108673863s +6600kb: Chars 24798 - 24847 [all:~([>left~|~right~];~eexist...] 0.124 secs (0.124u,0.s)
.007056741s +0kb: Chars 24848 - 24849 [}] 0. secs (0.u,0.s)
.006594261s +0kb: Chars 24854 - 24860 [right.] 0.005 secs (0.005u,0.s)
.007281449s +0kb: Chars 24865 - 24871 [right.] 0.003 secs (0.003u,0.s)
.079263441s +7392kb: Chars 24876 - 24928 [eexists~_,_,_,_,_,_,_,_,_,_,_,...] 0.089 secs (0.089u,0.s)
.027151969s +0kb: Chars 24929 - 24951 [(left;~ssplit;~trivial).] 0.026 secs (0.026u,0.s)
.007087307s +0kb: Chars 24956 - 24969 [eexists~_,_.] 0.006 secs (0.006u,0.s)
.006674673s +0kb: Chars 24974 - 24980 [split.] 0.003 secs (0.003u,0.s)
.006364808s +0kb: Chars 24985 - 24986 [{] 0. secs (0.u,0.s)
.006746219s +0kb: Chars 24991 - 25024 [(eapply~TracePredicate.concat_...] 0.002 secs (0.002u,0.s)
.411669824s +3168kb: Chars 25029 - 25097 [1:~(match~goal~with~~~~~|~|-~_...] 0.424 secs (0.424u,0.s)
.008804897s +0kb: Chars 25103 - 25112 [symmetry.] 0. secs (0.u,0.s)
.051910633s +0kb: Chars 25158 - 25216 [(rewrite~<-~(firstn_skipn~6~ma...] 0.059 secs (0.059u,0.s)
.026191483s +0kb: Chars 25221 - 25282 [(eapply~(f_equal2~app);~[~rewr...] 0.025 secs (0.025u,0.s)
.027967210s +1320kb: Chars 25287 - 25348 [(eapply~(f_equal2~app);~[~rewr...] 0.027 secs (0.027u,0.s)
.007230095s +0kb: Chars 25353 - 25391 [(change~([?x]~++~?y~::~?z)~wit...] 0.006 secs (0.006u,0.s)
.006624708s +0kb: Chars 25396 - 25418 [(eapply~(f_equal2~app)).] 0.001 secs (0.001u,0.s)
.007328756s +0kb: Chars 25423 - 25424 [{] 0. secs (0.u,0.s)
.006425938s +0kb: Chars 25425 - 25435 [(cbv[be2]).] 0. secs (0.u,0.s)
.007087156s +0kb: Chars 25436 - 25506 [(progress~change~2%nat~with~(L...] 0. secs (0.u,0.s)
.022146344s +0kb: Chars 25513 - 25554 [(setoid_rewrite~split_le_combi...] 0.047 secs (0.047u,0.s)
.006617683s +0kb: Chars 25555 - 25556 [}] 0. secs (0.u,0.s)
.050646234s +0kb: Chars 25561 - 25620 [(rewrite~<-~(firstn_skipn~2~ih...] 0.056 secs (0.056u,0.s)
.025986667s +0kb: Chars 25625 - 25686 [(eapply~(f_equal2~app);~[~rewr...] 0.025 secs (0.025u,0.s)
.067889006s +2376kb: Chars 25691 - 25781 [(rewrite~<-~(firstn_skipn~2~(L...] 0.067 secs (0.067u,0.s)
.007230912s +0kb: Chars 25786 - 25808 [(eapply~(f_equal2~app)).] 0.001 secs (0.001u,0.s)
.006863619s +0kb: Chars 25813 - 25814 [{] 0. secs (0.u,0.s)
.007014887s +0kb: Chars 25815 - 25825 [(cbv[be2]).] 0. secs (0.u,0.s)
.391969206s +1056kb: Chars 25826 - 25860 [(eplace~2%nat~with~_~at~3;~cyc...] 0.41 secs (0.41u,0.s)
.023684478s +0kb: Chars 25867 - 25917 [(rewrite~split_le_combine,~rev...] 0.023 secs (0.023u,0.s)
.006703627s +0kb: Chars 25924 - 25943 [(rewrite~rev_length).] 0. secs (0.u,0.s)
.723371859s +8184kb: Chars 25944 - 25969 [SepAutoArray.listZnWords.] 0.728 secs (0.717u,0.009s)
.008647899s +0kb: Chars 25970 - 25971 [}] 0. secs (0.u,0.s)
.017101192s +0kb: Chars 25976 - 26037 [(eapply~(f_equal2~app);~[~rewr...] 0.025 secs (0.025u,0.s)
.006813713s +0kb: Chars 26042 - 26064 [(eapply~(f_equal2~app)).] 0.001 secs (0.001u,0.s)
.006317021s +264kb: Chars 26065 - 26066 [{] 0. secs (0.u,0.s)
.006994436s +0kb: Chars 26067 - 26075 [f_equal.] 0.012 secs (0.012u,0.s)
.007025246s +0kb: Chars 26076 - 26101 [(eapply~byte.unsigned_inj).] 0. secs (0.u,0.s)
.007140148s +0kb: Chars 26102 - 26113 [(rewrite~E1).] 0. secs (0.u,0.s)
.007607208s +0kb: Chars 26114 - 26122 [trivial.] 0.024 secs (0.024u,0.s)
.006598377s +0kb: Chars 26123 - 26124 [}] 0. secs (0.u,0.s)
.045864017s +0kb: Chars 26129 - 26187 [(rewrite~<-~(firstn_skipn~2~pP...] 0.054 secs (0.054u,0.s)
.006928566s +0kb: Chars 26192 - 26214 [(eapply~(f_equal2~app)).] 0.001 secs (0.001u,0.s)
.006640866s +0kb: Chars 26219 - 26220 [{] 0. secs (0.u,0.s)
.403233959s +2640kb: Chars 26221 - 26255 [(eplace~2%nat~with~_~at~2;~cyc...] 0.414 secs (0.413u,0.s)
.022551525s +0kb: Chars 26262 - 26296 [(rewrite~split_le_combine;~tri...] 0.022 secs (0.022u,0.s)
.708145340s +6864kb: Chars 26303 - 26328 [SepAutoArray.listZnWords.] 0.707 secs (0.706u,0.s)
.009008899s +0kb: Chars 26329 - 26330 [}] 0. secs (0.u,0.s)
.052659820s +0kb: Chars 26335 - 26425 [(rewrite~<-~(firstn_skipn~4~(L...] 0.061 secs (0.061u,0.s)
.026121285s +0kb: Chars 26430 - 26491 [(eapply~(f_equal2~app);~[~rewr...] 0.025 secs (0.025u,0.s)
.063602296s +1848kb: Chars 26496 - 26586 [(rewrite~<-~(firstn_skipn~4~(L...] 0.063 secs (0.053u,0.009s)
.025804182s +0kb: Chars 26591 - 26652 [(eapply~(f_equal2~app);~[~rewr...] 0.025 secs (0.025u,0.s)
.060495630s +0kb: Chars 26657 - 26747 [(rewrite~<-~(firstn_skipn~2~(L...] 0.06 secs (0.06u,0.s)
.025876588s +0kb: Chars 26752 - 26813 [(eapply~(f_equal2~app);~[~rewr...] 0.025 secs (0.025u,0.s)
.059149958s +0kb: Chars 26818 - 26908 [(rewrite~<-~(firstn_skipn~2~(L...] 0.058 secs (0.058u,0.s)
.027812007s +1056kb: Chars 26913 - 26974 [(eapply~(f_equal2~app);~[~rewr...] 0.027 secs (0.027u,0.s)
.064739586s +0kb: Chars 26979 - 27069 [(rewrite~<-~(firstn_skipn~2~(L...] 0.064 secs (0.064u,0.s)
.007302550s +0kb: Chars 27074 - 27096 [(eapply~(f_equal2~app)).] 0.001 secs (0.001u,0.s)
.006408233s +0kb: Chars 27101 - 27102 [{] 0. secs (0.u,0.s)
.006636384s +0kb: Chars 27103 - 27113 [(cbv[be2]).] 0. secs (0.u,0.s)
.392849202s +528kb: Chars 27114 - 27148 [(eplace~2%nat~with~_~at~7;~cyc...] 0.41 secs (0.41u,0.s)
.024303492s +0kb: Chars 27155 - 27205 [(rewrite~split_le_combine,~rev...] 0.024 secs (0.024u,0.s)
.007870198s +0kb: Chars 27212 - 27231 [(rewrite~rev_length).] 0. secs (0.u,0.s)
.719857602s +7656kb: Chars 27232 - 27257 [SepAutoArray.listZnWords.] 0.726 secs (0.725u,0.s)
.008825280s +0kb: Chars 27258 - 27259 [}] 0. secs (0.u,0.s)
.048574617s +0kb: Chars 27264 - 27354 [(rewrite~<-~(firstn_skipn~2~(L...] 0.057 secs (0.057u,0.s)
.007577433s +0kb: Chars 27359 - 27381 [(eapply~(f_equal2~app)).] 0.001 secs (0.001u,0.s)
.006870022s +0kb: Chars 27386 - 27387 [{] 0. secs (0.u,0.s)
.007338562s +0kb: Chars 27388 - 27398 [(cbv[be2]).] 0. secs (0.u,0.s)
.393163324s +792kb: Chars 27399 - 27433 [(eplace~2%nat~with~_~at~8;~cyc...] 0.412 secs (0.412u,0.s)
.024424175s +0kb: Chars 27440 - 27490 [(rewrite~split_le_combine,~rev...] 0.024 secs (0.024u,0.s)
.006852124s +0kb: Chars 27497 - 27516 [(rewrite~rev_length).] 0. secs (0.u,0.s)
.718878799s +7920kb: Chars 27517 - 27542 [SepAutoArray.listZnWords.] 0.724 secs (0.723u,0.s)
.008899170s +0kb: Chars 27543 - 27544 [}] 0. secs (0.u,0.s)
.006820977s +0kb: Chars 27549 - 27571 [(eapply~(f_equal2~app)).] 0.003 secs (0.003u,0.s)
.006325641s +0kb: Chars 27572 - 27573 [{] 0. secs (0.u,0.s)
.006936365s +0kb: Chars 27574 - 27609 [(rewrite~to_list_from_list;~tr...] 0.024 secs (0.024u,0.s)
.006657402s +0kb: Chars 27610 - 27611 [}] 0. secs (0.u,0.s)
.007067863s +0kb: Chars 27616 - 27628 [reflexivity.] 0. secs (0.u,0.s)
.006637342s +0kb: Chars 27634 - 27665 [(change~[?x;~?y]~with~([x]~++~...] 0.004 secs (0.004u,0.s)
.037084085s +528kb: Chars 27670 - 27738 [(eapply~TracePredicate.concat_...] 0.053 secs (0.053u,0.s)
.006516402s +2904kb: Chars 27739 - 27740 [}] 0. secs (0.u,0.s)
.007798946s +1584kb: Chars 27746 - 27760 [(rewrite~<-~Hvv).] 0.013 secs (0.013u,0.s)
1.437998624s +14256kb: Chars 27765 - 27811 [(rewrite~!ListUtil.firstn_app_...] 1.437 secs (1.426u,0.009s)
.716268051s +5808kb: Chars 27816 - 27861 [(rewrite~!ListUtil.skipn_app_s...] 0.715 secs (0.715u,0.s)
.071013287s +1848kb: Chars 27866 - 27927 [(eexists~_,_;~ssplit;~try~eass...] 0.071 secs (0.071u,0.s)
.007730502s +0kb: Chars 27930 - 27931 [}] 0. secs (0.u,0.s)
.007327221s +0kb: Chars 27935 - 27936 [{] 0. secs (0.u,0.s)
.216257151s +4488kb: Chars 27941 - 27961 [(repeat~straightline).] 0.23 secs (0.23u,0.s)
.007244253s +0kb: Chars 27966 - 28009 [(pose~proof~(List.firstn_skipn...] 0. secs (0.u,0.s)
.357638885s +5544kb: Chars 28014 - 28068 [(pose~proof~(@firstn_length_le...] 0.363 secs (0.353u,0.009s)
.083567100s +0kb: Chars 28073 - 28122 [(pose~proof~(skipn_length~6~ma...] 0.083 secs (0.083u,0.s)
.140934095s +0kb: Chars 28127 - 28167 [forget~(List.firstn~6~mac)~as~...] 0.14 secs (0.14u,0.s)
.139638708s +264kb: Chars 28172 - 28212 [forget~(List.skipn~6~mac)~as~m...] 0.139 secs (0.139u,0.s)
.024759654s +0kb: Chars 28217 - 28227 [subst~mac.] 0.024 secs (0.024u,0.s)
.282921488s +2640kb: Chars 28232 - 28307 [(repeat~seprewrite_in~@Array.b...] 0.282 secs (0.282u,0.s)
.044876140s +0kb: Chars 28312 - 28329 [(rewrite~H26~in~*).] 0.044 secs (0.044u,0.s)
.007611010s +0kb: Chars 28334 - 28366 [(change~(Z.of_nat~6)~with~6~in...] 0.007 secs (0.007u,0.s)
1.542798584s +18480kb: Chars 28372 - 28435 [(straightline_call;~ssplit;~tr...] 1.541 secs (1.54u,0.s)
.490200060s +7656kb: Chars 28441 - 28461 [(repeat~straightline).] 0.49 secs (0.479u,0.009s)
.010077917s +0kb: Chars 28467 - 28510 [(pose~proof~(List.firstn_skipn...] 0. secs (0.u,0.s)
.381076140s +5808kb: Chars 28515 - 28569 [(pose~proof~(@firstn_length_le...] 0.389 secs (0.389u,0.s)
.009823070s +0kb: Chars 28574 - 28620 [(pose~proof~(skipn_length~2~pp...] 0. secs (0.u,0.s)
.137533423s +528kb: Chars 28625 - 28667 [forget~(List.firstn~2~ppp)~as~...] 0.147 secs (0.147u,0.s)
.145927718s +0kb: Chars 28672 - 28706 [forget~(List.skipn~2~ppp)~as~p...] 0.145 secs (0.145u,0.s)
.525459252s +1848kb: Chars 28711 - 28747 [(subst~ppp;~rewrite~?app_lengt...] 0.524 secs (0.524u,0.s)
.287948672s +1848kb: Chars 28752 - 28827 [(repeat~seprewrite_in~@Array.b...] 0.288 secs (0.287u,0.s)
.095192918s +792kb: Chars 28832 - 28850 [(rewrite~?H28~in~*).] 0.094 secs (0.094u,0.s)
.008226165s +0kb: Chars 28855 - 28889 [(change~(Z.of_nat~24)~with~24~...] 0.008 secs (0.008u,0.s)
.008897355s +0kb: Chars 28894 - 28926 [(change~(Z.of_nat~2)~with~2~in...] 0.008 secs (0.008u,0.s)
.336936031s +1056kb: Chars 28931 - 29025 [eplace~(word.add~(word.add~buf...] 0.336 secs (0.336u,0.s)
.010078391s +0kb: Chars 29031 - 29075 [(pose~proof~(List.firstn_skipn...] 0. secs (0.u,0.s)
.398808432s +6600kb: Chars 29080 - 29135 [(pose~proof~(@firstn_length_le...] 0.408 secs (0.407u,0.s)
.145833816s +0kb: Chars 29140 - 29181 [forget~(List.firstn~4~pppp)~as...] 0.145 secs (0.145u,0.s)
.145665589s +0kb: Chars 29186 - 29222 [forget~(List.skipn~4~pppp)~as~...] 0.145 secs (0.145u,0.s)
.538233028s +0kb: Chars 29227 - 29264 [(subst~pppp;~rewrite~?app_leng...] 0.537 secs (0.536u,0.s)
.289149082s +0kb: Chars 29269 - 29344 [(repeat~seprewrite_in~@Array.b...] 0.289 secs (0.288u,0.s)
.096184697s +0kb: Chars 29349 - 29367 [(rewrite~?H30~in~*).] 0.096 secs (0.096u,0.s)
.008677774s +0kb: Chars 29372 - 29406 [(change~(Z.of_nat~28)~with~28~...] 0.008 secs (0.008u,0.s)
.008756664s +0kb: Chars 29411 - 29443 [(change~(Z.of_nat~4)~with~4~in...] 0.008 secs (0.008u,0.s)
.362375974s +0kb: Chars 29448 - 29542 [eplace~(word.add~(word.add~buf...] 0.361 secs (0.361u,0.s)
.008314147s +0kb: Chars 29548 - 29593 [(pose~proof~(List.firstn_skipn...] 0. secs (0.u,0.s)
.420376943s +0kb: Chars 29598 - 29654 [(pose~proof~(@firstn_length_le...] 0.427 secs (0.427u,0.s)
.148163703s +0kb: Chars 29659 - 29700 [forget~(List.firstn~4~ppppp)~a...] 0.148 secs (0.148u,0.s)
.145664584s +0kb: Chars 29705 - 29742 [forget~(List.skipn~4~ppppp)~as...] 0.145 secs (0.145u,0.s)
.573527445s +0kb: Chars 29747 - 29785 [(subst~ppppp;~rewrite~?app_len...] 0.572 secs (0.572u,0.s)
.320727691s +0kb: Chars 29790 - 29865 [(repeat~seprewrite_in~@Array.b...] 0.32 secs (0.32u,0.s)
.097065373s +0kb: Chars 29870 - 29888 [(rewrite~?H31~in~*).] 0.096 secs (0.096u,0.s)
.009101032s +0kb: Chars 29893 - 29927 [(change~(Z.of_nat~30)~with~30~...] 0.008 secs (0.008u,0.s)
.009087788s +0kb: Chars 29932 - 29964 [(change~(Z.of_nat~4)~with~4~in...] 0.008 secs (0.008u,0.s)
.364128822s +0kb: Chars 29969 - 30063 [eplace~(word.add~(word.add~buf...] 0.363 secs (0.362u,0.s)
1.752416251s +0kb: Chars 30069 - 30132 [(straightline_call;~ssplit;~tr...] 1.752 secs (1.75u,0.s)
.577520205s +0kb: Chars 30138 - 30158 [(repeat~straightline).] 0.577 secs (0.576u,0.s)
.008599853s +0kb: Chars 30164 - 30210 [(pose~proof~(List.firstn_skipn...] 0. secs (0.u,0.s)
.452187674s +0kb: Chars 30215 - 30272 [(pose~proof~(@firstn_length_le...] 0.459 secs (0.459u,0.s)
.156247863s +0kb: Chars 30277 - 30321 [forget~(List.firstn~2~pppppp)~...] 0.156 secs (0.156u,0.s)
.153606246s +0kb: Chars 30326 - 30360 [forget~(List.skipn~2~pppppp)~a...] 0.153 secs (0.153u,0.s)
.736493542s +0kb: Chars 30365 - 30404 [(subst~pppppp;~rewrite~?app_le...] 0.735 secs (0.735u,0.s)
.343248655s +0kb: Chars 30409 - 30484 [(repeat~seprewrite_in~@Array.b...] 0.342 secs (0.342u,0.s)
.104148573s +0kb: Chars 30489 - 30507 [(rewrite~?H32~in~*).] 0.104 secs (0.104u,0.s)
.009647162s +0kb: Chars 30512 - 30546 [(change~(Z.of_nat~34)~with~34~...] 0.009 secs (0.009u,0.s)
.009875034s +0kb: Chars 30551 - 30583 [(change~(Z.of_nat~4)~with~4~in...] 0.009 secs (0.009u,0.s)
.387459993s +0kb: Chars 30588 - 30682 [eplace~(word.add~(word.add~buf...] 0.386 secs (0.386u,0.s)
.007548706s +0kb: Chars 30688 - 30730 [(pose~proof~(List.firstn_skipn...] 0. secs (0.u,0.s)
.464518040s +0kb: Chars 30735 - 30788 [(pose~proof~(@firstn_length_le...] 0.471 secs (0.47u,0.s)
.152580557s +0kb: Chars 30793 - 30832 [forget~(List.firstn~2~pP)~as~u...] 0.152 secs (0.152u,0.s)
.155728042s +0kb: Chars 30837 - 30868 [forget~(List.skipn~2~pP)~as~pPP.] 0.155 secs (0.155u,0.s)
.744524183s +0kb: Chars 30873 - 30908 [(subst~pP;~rewrite~?app_length...] 0.743 secs (0.743u,0.s)
.345826819s +0kb: Chars 30913 - 30988 [(repeat~seprewrite_in~@Array.b...] 0.345 secs (0.345u,0.s)
.105832780s +0kb: Chars 30993 - 31011 [(rewrite~?H34~in~*).] 0.106 secs (0.106u,0.s)
.010137878s +0kb: Chars 31016 - 31050 [(change~(Z.of_nat~36)~with~36~...] 0.009 secs (0.009u,0.s)
.009943146s +0kb: Chars 31055 - 31087 [(change~(Z.of_nat~4)~with~4~in...] 0.009 secs (0.009u,0.s)
.409134690s +0kb: Chars 31092 - 31186 [eplace~(word.add~(word.add~buf...] 0.408 secs (0.407u,0.s)
1.926192504s +0kb: Chars 31192 - 31255 [(straightline_call;~ssplit;~tr...] 1.925 secs (1.924u,0.s)
.752889632s +0kb: Chars 31261 - 31281 [(repeat~straightline).] 0.752 secs (0.751u,0.s)
.691791094s +0kb: Chars 31287 - 31356 [(destruct~(SepAutoArray.list_e...] 0.691 secs (0.69u,0.s)
.162134228s +0kb: Chars 31361 - 31401 [forget~(List.firstn~2~ih_l)~as...] 0.162 secs (0.162u,0.s)
.167899211s +0kb: Chars 31406 - 31460 [forget~(nth~2~ih_l~Inhabited.d...] 0.167 secs (0.167u,0.s)
.165415064s +0kb: Chars 31465 - 31508 [forget~(List.skipn~3~ih_l)~as~...] 0.165 secs (0.165u,0.s)
.049988863s +0kb: Chars 31513 - 31524 [subst~ih_l.] 0.049 secs (0.049u,0.s)
.629102163s +0kb: Chars 31529 - 31604 [(repeat~seprewrite_in~@Array.b...] 0.628 secs (0.627u,0.s)
1.519278115s +0kb: Chars 31609 - 31671 [(rewrite~?app_length~in~*;~cbn...] 1.518 secs (1.517u,0.s)
.010217663s +0kb: Chars 31676 - 31708 [(change~(Z.of_nat~1)~with~1~in...] 0.01 secs (0.01u,0.s)
.011965589s +0kb: Chars 31713 - 31745 [(change~(Z.of_nat~2)~with~2~in...] 0.011 secs (0.011u,0.s)
.453038500s +0kb: Chars 31750 - 31844 [eplace~(word.add~(word.add~buf...] 0.451 secs (0.451u,0.s)
.451530413s +0kb: Chars 31849 - 31943 [eplace~(word.add~(word.add~buf...] 0.451 secs (0.45u,0.s)
.771740797s +0kb: Chars 31949 - 31969 [(repeat~straightline).] 0.771 secs (0.77u,0.s)
.093203788s +0kb: Chars 31975 - 32025 [(destruct~ip_length_lo~as~[|~i...] 0.093 secs (0.093u,0.s)
.006968480s +0kb: Chars 32030 - 32031 [{] 0. secs (0.u,0.s)
.006476573s +0kb: Chars 32032 - 32050 [(cbn[length]~in~*).] 0.006 secs (0.006u,0.s)
.079199093s +0kb: Chars 32051 - 32068 [(exfalso;~Lia.lia).] 0.085 secs (0.085u,0.s)
.007398763s +0kb: Chars 32069 - 32070 [}] 0. secs (0.u,0.s)
.006825403s +0kb: Chars 32075 - 32098 [(cbn[Array.array]~in~*).] 0.008 secs (0.008u,0.s)
.474140577s +0kb: Chars 32103 - 32197 [eplace~(word.add~(word.add~buf...] 0.478 secs (0.478u,0.s)
.851952824s +0kb: Chars 32203 - 32223 [(repeat~straightline).] 0.851 secs (0.85u,0.s)
.394304727s +0kb: Chars 32228 - 32363 [(destruct~ip_checksum~as~[|~ip...] 0.393 secs (0.393u,0.s)
.512931855s +0kb: Chars 32368 - 32462 [eplace~(word.add~(word.add~buf...] 0.512 secs (0.512u,0.s)
.288453492s +0kb: Chars 32468 - 32481 [straightline.] 0.288 secs (0.287u,0.s)
.015700892s +0kb: Chars 32486 - 32499 [straightline.] 0.016 secs (0.015u,0.s)
.028488948s +0kb: Chars 32504 - 32517 [straightline.] 0.028 secs (0.028u,0.s)
.006869890s +0kb: Chars 32522 - 32535 [straightline.] 0.002 secs (0.002u,0.s)
.025039806s +0kb: Chars 32540 - 32553 [straightline.] 0.028 secs (0.028u,0.s)
.262368964s +0kb: Chars 32558 - 32571 [straightline.] 0.261 secs (0.261u,0.s)
.163602499s +0kb: Chars 32576 - 32589 [straightline.] 0.163 secs (0.163u,0.s)
.773217246s +0kb: Chars 32594 - 32614 [(repeat~straightline).] 0.772 secs (0.771u,0.s)
.008006589s +0kb: Chars 32619 - 32649 [subst~a7~a6~a5~a1~v9~v8~v7~v6.] 0.007 secs (0.007u,0.s)
.017456806s +0kb: Chars 32654 - 32934 [(assert~~~(ptsto_to_array~:~~~...] 0.017 secs (0.017u,0.s)
.006728826s +0kb: Chars 32939 - 32940 [{] 0. secs (0.u,0.s)
.007144828s +0kb: Chars 32941 - 32959 [(cbn[Array.array]).] 0. secs (0.u,0.s)
.006885203s +0kb: Chars 32960 - 32967 [(intros).] 0. secs (0.u,0.s)
.011745410s +0kb: Chars 32968 - 32975 [cancel.] 0.031 secs (0.031u,0.s)
.007064880s +0kb: Chars 32976 - 32977 [}] 0. secs (0.u,0.s)
.116264883s +0kb: Chars 32983 - 33356 [(assert~~~(bytearray_address_m...] 0.122 secs (0.122u,0.s)
.006702185s +0kb: Chars 33359 - 33360 [{] 0. secs (0.u,0.s)
.007260268s +0kb: Chars 33361 - 33368 [(intros).] 0. secs (0.u,0.s)
.006998439s +0kb: Chars 33373 - 33424 [replace~b~with~(word.add~start...] 0.001 secs (0.001u,0.s)
.006714587s +0kb: Chars 33429 - 33430 [{] 0. secs (0.u,0.s)
.006722024s +0kb: Chars 33431 - 33475 [(eapply~Array.bytearray_index_...] 0.03 secs (0.03u,0.s)
.006671029s +0kb: Chars 33476 - 33477 [}] 0. secs (0.u,0.s)
.007237986s +0kb: Chars 33482 - 33507 [(eapply~word.unsigned_inj).] 0.004 secs (0.004u,0.s)
.007412023s +0kb: Chars 33508 - 33555 [(rewrite~?word.unsigned_add,~?...] 0.013 secs (0.013u,0.s)
.006344880s +0kb: Chars 33560 - 33576 [(cbv[word.wrap]).] 0. secs (0.u,0.s)
.006789589s +0kb: Chars 33581 - 33607 [(rewrite~Zplus_mod_idemp_r).] 0. secs (0.u,0.s)
.006864476s +0kb: Chars 33612 - 33655 [(transitivity~(word.unsigned~b...] 0. secs (0.u,0.s)
.006830569s +0kb: Chars 33660 - 33661 [{] 0. secs (0.u,0.s)
.006386773s +0kb: Chars 33662 - 33670 [f_equal.] 0.021 secs (0.021u,0.s)
.006930345s +0kb: Chars 33672 - 33677 [ring.] 0.003 secs (0.003u,0.s)
.006349766s +0kb: Chars 33678 - 33679 [}] 0. secs (0.u,0.s)
.035363367s +0kb: Chars 33684 - 33741 [(rewrite~Z.mod_small;~trivial;...] 0.058 secs (0.058u,0.s)
.006346700s +0kb: Chars 33742 - 33743 [}] 0. secs (0.u,0.s)
1.399550379s +0kb: Chars 33747 - 33788 [(repeat~seprewrite_in~@ptsto_t...] 1.404 secs (1.403u,0.s)
1.499150801s +0kb: Chars 33791 - 33844 [(rewrite~?word.unsigned_of_Z_n...] 1.498 secs (1.497u,0.s)
6.653652514s +0kb: Chars 33847 - 33922 [(seprewrite_in_by~(@bytearray_...] 6.653 secs (6.648u,0.s)
6.606412111s +0kb: Chars 33925 - 34034 [(seprewrite_in_by~~~(fun~x~=>~...] 6.606 secs (6.601u,0.s)
.014557805s +0kb: Chars 34037 - 34064 [(rewrite~<-~app_assoc~in~H39).] 0.014 secs (0.014u,0.s)
9.864910226s +48312kb: Chars 34067 - 34176 [(seprewrite_in_by~~~(fun~x~=>~...] 9.863 secs (9.826u,0.029s)
.117135278s +792kb: Chars 34179 - 34207 [(rewrite~<-~!app_assoc~in~H39).] 0.117 secs (0.117u,0.s)
.008744421s +0kb: Chars 34210 - 34228 [(cbn[length]~in~*).] 0.008 secs (0.008u,0.s)
4.940760959s +44880kb: Chars 34231 - 34340 [(seprewrite_in_by~~~(fun~x~=>~...] 4.939 secs (4.905u,0.029s)
.132124019s +1584kb: Chars 34343 - 34371 [(rewrite~<-~!app_assoc~in~H39).] 0.132 secs (0.132u,0.s)
4.935696629s +43560kb: Chars 34374 - 34483 [(seprewrite_in_by~~~(fun~x~=>~...] 4.934 secs (4.931u,0.s)
.136571756s +1584kb: Chars 34486 - 34514 [(rewrite~<-~!app_assoc~in~H39).] 0.136 secs (0.136u,0.s)
4.905879629s +42240kb: Chars 34517 - 34626 [(seprewrite_in_by~~~(fun~x~=>~...] 4.904 secs (4.901u,0.s)
.146409734s +2112kb: Chars 34629 - 34657 [(rewrite~<-~!app_assoc~in~H39).] 0.146 secs (0.146u,0.s)
9.671959878s +85008kb: Chars 34660 - 34769 [(seprewrite_in_by~~~(fun~x~=>~...] 9.671 secs (9.633u,0.029s)
.152893636s +3432kb: Chars 34772 - 34800 [(rewrite~<-~!app_assoc~in~H39).] 0.153 secs (0.153u,0.s)
9.669767850s +87384kb: Chars 34803 - 34912 [(seprewrite_in_by~~~(fun~x~=>~...] 9.668 secs (9.641u,0.019s)
2.322026080s +34584kb: Chars 34916 - 35195 [(straightline_call;~[~ssplit;~...] 2.318 secs (2.297u,0.019s)
1.288734233s +20856kb: Chars 35199 - 35219 [(repeat~straightline).] 1.288 secs (1.277u,0.01s)
.133176907s +792kb: Chars 35223 - 35555 [replace~~((ih_const~++~~~~[byt...] 0.133 secs (0.132u,0.s)
.138534864s +1056kb: Chars 35558 - 35600 [(seprewrite_in~@Array.bytearra...] 0.138 secs (0.138u,0.s)
.148648598s +1320kb: Chars 35603 - 35671 [(seprewrite_in~(@Array.bytearr...] 0.148 secs (0.148u,0.s)
.159187675s +1056kb: Chars 35674 - 35742 [(seprewrite_in~(@Array.bytearr...] 0.158 secs (0.158u,0.s)
.193199392s +2376kb: Chars 35745 - 35813 [(rewrite~?app_length~in~H43;~c...] 0.192 secs (0.192u,0.s)
.716682543s +12408kb: Chars 35816 - 35880 [replace~(Datatypes.length~ip_i...] 0.716 secs (0.705u,0.009s)
.009084679s +0kb: Chars 35883 - 35901 [(cbn[plus]~in~H43).] 0. secs (0.u,0.s)
1.695338664s +7392kb: Chars 35904 - 36005 [(repeat~eplace~(word.add~(word...] 1.702 secs (1.701u,0.s)
.009273680s +0kb: Chars 36009 - 36025 [Import~symmetry.] 0. secs (0.u,0.s)
.139298161s +1320kb: Chars 36028 - 36109 [(seprewrite_in~~~(symmetry!~(f...] 0.148 secs (0.148u,0.s)
.167904506s +1056kb: Chars 36112 - 36193 [(seprewrite_in~~~(symmetry!~(f...] 0.167 secs (0.167u,0.s)
1.861655650s +19536kb: Chars 36197 - 36217 [(repeat~straightline).] 1.861 secs (1.849u,0.009s)
.009015267s +0kb: Chars 36220 - 36231 [revert~H40.] 0. secs (0.u,0.s)
.006892103s +0kb: Chars 36234 - 36291 [(repeat~match~goal~with~~~~~~~...] 0.015 secs (0.015u,0.s)
.213158827s +1584kb: Chars 36294 - 36314 [(repeat~straightline).] 0.212 secs (0.212u,0.s)
1.028390854s +23760kb: Chars 36318 - 36394 [(do~6~(destruct~pPP~as~[|~?~pP...] 1.028 secs (1.027u,0.s)
.241985783s +0kb: Chars 36397 - 36487 [(set~~~(X~:=~~~~(b~::~b0~::~b1...] 0.241 secs (0.241u,0.s)
.006577987s +0kb: Chars 36490 - 36513 [(cbn[Array.array]~in~X).] 0.001 secs (0.001u,0.s)
.007288902s +0kb: Chars 36514 - 36522 [subst~X.] 0. secs (0.u,0.s)
2.905261441s +11616kb: Chars 36525 - 36626 [(repeat~eplace~(word.add~(word...] 2.916 secs (2.914u,0.s)
2.487541526s +28512kb: Chars 36630 - 36650 [(repeat~straightline).] 2.487 secs (2.474u,0.009s)
.010108549s +0kb: Chars 36653 - 36697 [(pose~proof~(List.firstn_skipn...] 0. secs (0.u,0.s)
.570974781s +6864kb: Chars 36700 - 36755 [(pose~proof~(@firstn_length_le...] 0.58 secs (0.58u,0.s)
.186823224s +1056kb: Chars 36758 - 36796 [forget~(List.firstn~32~pPP)~as...] 0.186 secs (0.186u,0.s)
.182949467s +0kb: Chars 36799 - 36833 [forget~(List.skipn~32~pPP)~as~...] 0.182 secs (0.182u,0.s)
1.441871389s +5016kb: Chars 36836 - 36872 [(subst~pPP;~rewrite~?app_lengt...] 1.441 secs (1.44u,0.s)
.509498415s +2640kb: Chars 36875 - 36943 [(repeat~seprewrite_in~(@Array....] 0.509 secs (0.508u,0.s)
.139412773s +792kb: Chars 36946 - 36964 [(rewrite~?H33~in~*).] 0.139 secs (0.139u,0.s)
.013328112s +0kb: Chars 36967 - 37001 [(change~(Z.of_nat~32)~with~32~...] 0.013 secs (0.013u,0.s)
.770110460s +2112kb: Chars 37004 - 37105 [(repeat~eplace~(word.add~(word...] 0.769 secs (0.768u,0.s)
.945728256s +9768kb: Chars 37108 - 37167 [(straightline_call;~ssplit;~tr...] 0.945 secs (0.944u,0.s)
.594229865s +8184kb: Chars 37171 - 37191 [(repeat~straightline).] 0.593 secs (0.593u,0.s)
.009583275s +0kb: Chars 37195 - 37206 [revert~H37.] 0. secs (0.u,0.s)
.006772178s +0kb: Chars 37209 - 37266 [(repeat~match~goal~with~~~~~~~...] 0.006 secs (0.006u,0.s)
.006461700s +0kb: Chars 37269 - 37276 [(intros).] 0. secs (0.u,0.s)
1.574239302s +15840kb: Chars 37279 - 37320 [(repeat~seprewrite_in~@ptsto_t...] 1.588 secs (1.587u,0.s)
18.932911278s +148896kb: Chars 37323 - 37410 [(seprewrite_in_by~(fun~xs~ys~=...] 18.932 secs (18.888u,0.029s)
15.267297091s +122232kb: Chars 37413 - 37517 [(seprewrite_in_by~(fun~xs~ys~=...] 15.266 secs (15.195u,0.059s)
14.096241184s +113256kb: Chars 37520 - 37624 [(seprewrite_in_by~(fun~xs~ys~=...] 14.095 secs (14.085u,0.s)
13.028313825s +26400kb: Chars 37627 - 37731 [(seprewrite_in_by~(fun~xs~ys~=...] 13.027 secs (13.008u,0.009s)
4.350693476s +0kb: Chars 37734 - 37838 [(seprewrite_in_by~(fun~xs~ys~=...] 4.35 secs (4.347u,0.s)
3.276538743s +0kb: Chars 37841 - 37945 [(seprewrite_in_by~(fun~xs~ys~=...] 3.276 secs (3.273u,0.s)
9.771183834s +0kb: Chars 37948 - 38052 [(seprewrite_in_by~(fun~xs~ys~=...] 9.77 secs (9.763u,0.s)
9.829626488s +0kb: Chars 38055 - 38159 [(seprewrite_in_by~(fun~xs~ys~=...] 9.829 secs (9.822u,0.s)
9.888231819s +67056kb: Chars 38162 - 38266 [(seprewrite_in_by~(fun~xs~ys~=...] 9.887 secs (9.88u,0.s)
3.266747397s +27720kb: Chars 38269 - 38373 [(seprewrite_in_by~(fun~xs~ys~=...] 3.266 secs (3.263u,0.s)
3.306242799s +27456kb: Chars 38376 - 38480 [(seprewrite_in_by~(fun~xs~ys~=...] 3.305 secs (3.283u,0.019s)
3.307374337s +27456kb: Chars 38483 - 38587 [(seprewrite_in_by~(fun~xs~ys~=...] 3.307 secs (3.274u,0.029s)
3.248643433s +28776kb: Chars 38590 - 38694 [(seprewrite_in_by~(fun~xs~ys~=...] 3.248 secs (3.245u,0.s)
2.233545962s +18744kb: Chars 38697 - 38801 [(seprewrite_in_by~(fun~xs~ys~=...] 2.233 secs (2.211u,0.019s)
1.184015743s +9504kb: Chars 38804 - 38908 [(seprewrite_in_by~(fun~xs~ys~=...] 1.183 secs (1.182u,0.s)
6.149520842s +53064kb: Chars 38911 - 39015 [(seprewrite_in_by~(fun~xs~ys~=...] 6.149 secs (6.134u,0.009s)
.008774132s +0kb: Chars 39019 - 39041 [subst~v6~v7~v8~v9~v10.] 0.002 secs (0.002u,0.s)
.007152509s +0kb: Chars 39044 - 39065 [rename~x3~into~ipchk.] 0. secs (0.u,0.s)
1.789263130s +27192kb: Chars 39068 - 39148 [(rewrite~?word.unsigned_sru_no...] 1.801 secs (1.8u,0.s)
.471015190s +5808kb: Chars 39152 - 39215 [(straightline_call;~[~ssplit;~...] 0.47 secs (0.47u,0.s)
.008873591s +0kb: Chars 39218 - 39219 [{] 0. secs (0.u,0.s)
.026921102s +0kb: Chars 39220 - 39258 [(rewrite~?app_length,~?length_...] 0.036 secs (0.036u,0.s)
.546863043s +6864kb: Chars 39259 - 39284 [SepAutoArray.listZnWords.] 0.546 secs (0.546u,0.s)
.008816596s +0kb: Chars 39285 - 39286 [}] 0. secs (0.u,0.s)
.007231326s +0kb: Chars 39289 - 39290 [{] 0. secs (0.u,0.s)
.637336683s +8448kb: Chars 39291 - 39299 [ZnWords.] 0.652 secs (0.642u,0.009s)
.009269441s +0kb: Chars 39300 - 39301 [}] 0. secs (0.u,0.s)
.006492332s +0kb: Chars 39305 - 39408 [(pose~proof~~~(length_le_split...] 0. secs (0.u,0.s)
2.401013294s +21120kb: Chars 39411 - 39515 [(seprewrite_in_by~(fun~xs~ys~=...] 2.415 secs (2.403u,0.009s)
2.247467990s +22968kb: Chars 39518 - 39622 [(seprewrite_in_by~(fun~xs~ys~=...] 2.247 secs (2.245u,0.s)
.459370677s +7920kb: Chars 39626 - 39646 [(repeat~straightline).] 0.459 secs (0.458u,0.s)
.127667326s +1584kb: Chars 39649 - 39705 [(destruct~H35;~repeat~straight...] 0.127 secs (0.127u,0.s)
.007424249s +0kb: Chars 39708 - 39709 [{] 0. secs (0.u,0.s)
.006739632s +0kb: Chars 39710 - 39726 [(eexists;~ssplit).] 0.007 secs (0.007u,0.s)
1.652471279s +28248kb: Chars 39727 - 39753 [(eexists~_,_;~ssplit;~slv).] 1.658 secs (1.656u,0.s)
.008768307s +0kb: Chars 39758 - 39774 [(eexists;~ssplit).] 0.006 secs (0.006u,0.s)
.006621845s +0kb: Chars 39775 - 39784 [subst~a4.] 0. secs (0.u,0.s)
.006794684s +0kb: Chars 39785 - 39793 [subst~a.] 0.001 secs (0.001u,0.s)
.007017063s +0kb: Chars 39794 - 39812 [(rewrite~app_assoc).] 0.003 secs (0.003u,0.s)
.006390406s +0kb: Chars 39813 - 39825 [reflexivity.] 0.001 secs (0.001u,0.s)
.007007351s +0kb: Chars 39830 - 39846 [(eexists;~ssplit).] 0.006 secs (0.006u,0.s)
.006859404s +0kb: Chars 39847 - 39879 [(eapply~Forall2_app;~eassumpti...] 0.007 secs (0.007u,0.s)
.113193921s +4488kb: Chars 39884 - 39924 [eauto~using~TracePredicate.any...] 0.134 secs (0.134u,0.s)
.006694610s +0kb: Chars 39925 - 39926 [}] 0. secs (0.u,0.s)
.050547081s +0kb: Chars 39930 - 39946 [(ssplit;~trivial).] 0.056 secs (0.056u,0.s)
1.661863442s +25080kb: Chars 39949 - 39978 [(eexists~_,_,_;~ssplit;~slv).] 1.66 secs (1.649u,0.009s)
.009972244s +0kb: Chars 39981 - 39997 [(eexists;~ssplit).] 0.008 secs (0.u,0.008s)
.006671362s +0kb: Chars 39998 - 40007 [subst~a4.] 0. secs (0.u,0.s)
.006762651s +0kb: Chars 40008 - 40016 [subst~a.] 0.001 secs (0.u,0.s)
.006754688s +0kb: Chars 40017 - 40035 [(rewrite~app_assoc).] 0.003 secs (0.003u,0.s)
.007142257s +0kb: Chars 40036 - 40048 [reflexivity.] 0.001 secs (0.001u,0.s)
.007048710s +0kb: Chars 40051 - 40067 [(eexists;~ssplit).] 0.006 secs (0.006u,0.s)
.006912809s +0kb: Chars 40068 - 40100 [(eapply~Forall2_app;~eassumpti...] 0.007 secs (0.007u,0.s)
.007404941s +0kb: Chars 40103 - 40109 [right.] 0.002 secs (0.002u,0.s)
.006720156s +0kb: Chars 40110 - 40116 [right.] 0.002 secs (0.002u,0.s)
.006467716s +0kb: Chars 40120 - 40196 [(exists~(from_list~6~mac_local...] 0.009 secs (0.009u,0.s)
.006521430s +0kb: Chars 40199 - 40276 [(exists~(from_list~6~mac_remot...] 0.01 secs (0.01u,0.s)
.007000835s +0kb: Chars 40279 - 40300 [(cbv~beta~delta~[be2]).] 0. secs (0.u,0.s)
.006738995s +0kb: Chars 40303 - 40390 [(exists~(le_combine~[ethertype...] 0.029 secs (0.029u,0.s)
.006438840s +0kb: Chars 40393 - 40468 [(exists~(from_list~2~ih_const~...] 0.009 secs (0.009u,0.s)
.039019999s +5016kb: Chars 40471 - 40558 [(exists~(le_combine~[ip_length...] 0.039 secs (0.039u,0.s)
.559783630s +7128kb: Chars 40561 - 40632 [(exists~(from_list~5~ip_idff~_...] 0.558 secs (0.558u,0.s)
.040527467s +5016kb: Chars 40635 - 40724 [(exists~(le_combine~[ip_checks...] 0.04 secs (0.04u,0.s)
.010084524s +0kb: Chars 40727 - 40802 [(exists~(from_list~4~ip_local~...] 0.01 secs (0.01u,0.s)
.010185364s +0kb: Chars 40805 - 40881 [(exists~(from_list~4~ip_remote...] 0.009 secs (0.009u,0.s)
.009963990s +0kb: Chars 40884 - 40960 [(exists~(from_list~2~udp_local...] 0.009 secs (0.009u,0.s)
.016356500s +0kb: Chars 40963 - 41040 [(exists~(from_list~2~udp_remot...] 0.016 secs (0.016u,0.s)
.029159692s +0kb: Chars 41043 - 41109 [(exists~(le_combine~[b0;~b]);~...] 0.028 secs (0.028u,0.s)
.035693774s +3696kb: Chars 41112 - 41179 [(exists~(le_combine~[b2;~b1]);...] 0.035 secs (0.035u,0.s)
.010626315s +0kb: Chars 41182 - 41246 [(exists~(from_list~2~[b3;~b4]~...] 0.01 secs (0.01u,0.s)
.006637142s +0kb: Chars 41249 - 41273 [exists~(_pkpad~++~pPPP).] 0.002 secs (0.002u,0.s)
.006373438s +0kb: Chars 41277 - 41306 [(assert~(Hp~:~x11~=~ipproto)).] 0. secs (0.u,0.s)
.006944796s +0kb: Chars 41307 - 41308 [{] 0. secs (0.u,0.s)
.006878011s +0kb: Chars 41309 - 41334 [(eapply~byte.unsigned_inj).] 0. secs (0.u,0.s)
.007133419s +0kb: Chars 41335 - 41346 [(rewrite~E1).] 0. secs (0.u,0.s)
.006853593s +0kb: Chars 41347 - 41355 [trivial.] 0.021 secs (0.021u,0.s)
.006972814s +0kb: Chars 41356 - 41357 [}] 0. secs (0.u,0.s)
.006404440s +0kb: Chars 41360 - 41372 [(destruct~Hp).] 0.012 secs (0.012u,0.s)
.006695237s +0kb: Chars 41376 - 41382 [right.] 0.001 secs (0.001u,0.s)
.049131949s +0kb: Chars 41385 - 41401 [(ssplit;~trivial).] 0.069 secs (0.069u,0.s)
.006682017s +0kb: Chars 41404 - 41437 [(eapply~TracePredicate.concat_...] 0. secs (0.u,0.s)
.307076790s +1848kb: Chars 41440 - 41516 [all:~~(match~goal~with~~~|~|-~...] 0.312 secs (0.312u,0.s)
.009283799s +0kb: Chars 41519 - 41612 [(assert~(app_singleton_l~:~for...] 0. secs (0.u,0.s)
.007444830s +528kb: Chars 41615 - 41639 [2:~(simpl~le_split~at~1).] 0. secs (0.u,0.s)
.006710099s +0kb: Chars 41642 - 41658 [all:~(cbn[rev]).] 0. secs (0.u,0.s)
.220616947s +3168kb: Chars 41661 - 41745 [all:~~(repeat~~~~rewrite~<-~?a...] 0.241 secs (0.241u,0.s)
.193804644s +9504kb: Chars 41748 - 41784 [all:~(trivial;~repeat~(f_equal...] 0.193 secs (0.183u,0.009s)
.084953449s +11352kb: Chars 41788 - 41989 [(match~goal~with~~|~c:=Impl.ip...] 0.084 secs (0.084u,0.s)
.007940126s +0kb: Chars 41992 - 41996 [2:~{] 0. secs (0.u,0.s)
.011358159s +0kb: Chars 42001 - 42079 [(repeat~~~rewrite~<-~?app_asso...] 0.019 secs (0.018u,0.s)
.021833441s +0kb: Chars 42084 - 42092 [trivial.] 0.021 secs (0.021u,0.s)
.006867796s +0kb: Chars 42093 - 42094 [}] 0. secs (0.u,0.s)
.119069446s +0kb: Chars 42097 - 42134 [(remember~(Spec.ip_checksum~_)...] 0.125 secs (0.125u,0.s)
.006898294s +0kb: Chars 42137 - 42158 [(unfold~le_split~at~1).] 0. secs (0.u,0.s)
.006745086s +0kb: Chars 42161 - 42239 [(repeat~~~rewrite~<-~?app_asso...] 0.013 secs (0.013u,0.s)
.021696480s +0kb: Chars 42242 - 42250 [trivial.] 0.021 secs (0.021u,0.s)
.007058273s +0kb: Chars 42251 - 42252 [}] 0. secs (0.u,0.s)
.006313777s +0kb: Chars 42256 - 42265 [Unshelve.] 0. secs (0.u,0.s)
14.457730528s +144936kb: Chars 42268 - 42303 [all:~(try~SepAutoArray.listZnW...] 14.47 secs (14.409u,0.049s)
38.786915628s +101112kb: Chars 12819 - 12886 [Import~SetEvars~coqutil.Tactic...] 0. secs (0.u,0.s)
.008866422s +0kb: Chars 36009 - 36025 [Import~symmetry.] 0. secs (0.u,0.s)
67.127166250s +241304kb: Chars 42304 - 42308 [Qed.] 67.135 secs (67.034u,0.069s)
.009456922s +0kb: Chars 42310 - 42382 [Require~Import~Crypto.Bedrock....] 0.002 secs (0.002u,0.s)
.007990459s +0kb: Chars 42383 - 42406 [Import~bedrock2.Syntax.] 0. secs (0.u,0.s)
.006672953s +0kb: Chars 42568 - 42640 [Definition~init~:~func~:=~("in...] 0. secs (0.u,0.s)
.006440411s +0kb: Chars 42641 - 42713 [Definition~loop~:~func~:=~("lo...] 0. secs (0.u,0.s)
.006917186s +0kb: Chars 42715 - 42978 [Definition~funcs~:~list~Syntax...] 0. secs (0.u,0.s)
.006754014s +0kb: Chars 42980 - 43080 [Lemma~chacha20_ok~:~~~forall~f...] 0. secs (0.u,0.s)
.007087593s +792kb: Chars 43081 - 43090 [Admitted.] 0. secs (0.u,0.s)
.006701941s +0kb: Chars 43092 - 43103 [Import~SPI.] 0. secs (0.u,0.s)
.007155216s +0kb: Chars 43104 - 43145 [Lemma~link_loopfn~:~spec_of_lo...] 0. secs (0.u,0.s)
.006549075s +0kb: Chars 43146 - 43152 [Proof.] 0. secs (0.u,0.s)
.718430603s +264kb: Chars 43155 - 43227 [(eapply~loopfn_ok;~try~eapply~...] 0.783 secs (0.782u,0.s)
5.244336293s +16632kb: Chars 43232 - 43403 [(repeat~eapply~recvEthernet_ok...] 5.243 secs (5.24u,0.s)
.008799044s +0kb: Chars 43408 - 43445 [(eapply~ip_checksum_br2fn_ok;~...] 0.003 secs (0.003u,0.s)
1.386203460s +2904kb: Chars 43450 - 43575 [(eapply~x25519_base_ok;~try~ea...] 1.39 secs (1.389u,0.s)
2.127076102s +3960kb: Chars 43580 - 43703 [(eapply~lan9250_tx_ok;~try~eap...] 2.126 secs (2.125u,0.s)
3.392609630s +12936kb: Chars 43708 - 43829 [(eapply~x25519_ok;~try~eapply~...] 3.392 secs (3.39u,0.s)
.008630351s +0kb: Chars 43834 - 43853 [(eapply~chacha20_ok).] 0.006 secs (0.006u,0.s)
.127472223s +1320kb: Chars 43854 - 43858 [Qed.] 0.129 secs (0.128u,0.s)
.007263535s +0kb: Chars 43860 - 43890 [Require~compiler.ToplevelLoop.] 0.001 secs (0.001u,0.s)
.007235672s +0kb: Chars 43891 - 44285 [Definition~ml~:~MemoryLayout.M...] 0.001 secs (0.001u,0.s)
.007152208s +0kb: Chars 44287 - 44332 [Lemma~ml_ok~:~MemoryLayout.Mem...] 0. secs (0.u,0.s)
.006900797s +0kb: Chars 44333 - 44339 [Proof.] 0. secs (0.u,0.s)
.082478834s +3960kb: Chars 44340 - 44373 [(split;~compute;~trivial;~inve...] 0.106 secs (0.106u,0.s)
.008826466s +264kb: Chars 44374 - 44378 [Qed.] 0.008 secs (0.008u,0.s)
.006864361s +264kb: Chars 44380 - 44457 [#[local]~Instance:~(FlatToRisc...] 0. secs (0.u,0.s)
.006818897s +0kb: Chars 44458 - 44678 [Derive~<genarg:identref>~SuchT...] 0. secs (0.u,0.s)
.006653824s +0kb: Chars 44679 - 44685 [Proof.] 0. secs (0.u,0.s)
.006384875s +0kb: Chars 44688 - 44746 [(match~goal~with~~|~x:=_:_~|-~...] 0. secs (0.u,0.s)
8.736204370s +7128kb: Chars 44749 - 44760 [(vm_compute).] 8.76 secs (8.749u,0.009s)
.225636110s +264kb: Chars 44763 - 44875 [(match~goal~with~~|~|-~@Succes...] 0.225 secs (0.225u,0.s)
7.395484587s +46200kb: Chars 44876 - 44880 [Qed.] 7.327 secs (7.325u,0.s)
.009452883s +0kb: Chars 44882 - 44949 [Definition~garagedoor_stack_si...] 0. secs (0.u,0.s)
.006470661s +0kb: Chars 44950 - 45018 [Definition~garagedoor_finfo~:=...] 0. secs (0.u,0.s)
.006418373s +0kb: Chars 45019 - 45087 [Definition~garagedoor_insns~:=...] 0. secs (0.u,0.s)
.006971627s +0kb: Chars 45088 - 45157 [Definition~garagedoor_bytes~:=...] 0. secs (0.u,0.s)
.006393499s +0kb: Chars 45158 - 45236 [Definition~garagedoor_symbols~...] 0. secs (0.u,0.s)
.006870221s +0kb: Chars 45238 - 45280 [Require~Import~compiler.Compil...] 0.002 secs (0.002u,0.s)
.006915723s +0kb: Chars 45281 - 45330 [Require~Import~compiler.NaiveR...] 0. secs (0.u,0.s)
.007344993s +0kb: Chars 45331 - 45376 [#[local]Existing~Instance~Sort...] 0. secs (0.u,0.s)
.006243698s +0kb: Chars 45378 - 45489 [Lemma~compiler_emitted_valid_i...] 0. secs (0.u,0.s)
.006318240s +1584kb: Chars 45490 - 45496 [Proof.] 0. secs (0.u,0.s)
.006680727s +2904kb: Chars 45497 - 45508 [(vm_compute).] 0.035 secs (0.035u,0.s)
.006692811s +0kb: Chars 45509 - 45521 [reflexivity.] 0. secs (0.u,0.s)
.006609191s +0kb: Chars 45522 - 45526 [Qed.] 0.045 secs (0.045u,0.s)
.006652873s +0kb: Chars 45528 - 45674 [Definition~good_trace~s~t~s'~:...] 0.001 secs (0.001u,0.s)
.006742542s +0kb: Chars 45675 - 45703 [Import~ExprImpEventLoopSpec.] 0. secs (0.u,0.s)
.006908387s +0kb: Chars 45704 - 45981 [Definition~garagedoor_spec~:~P...] 0.001 secs (0.001u,0.s)
.006844003s +0kb: Chars 45983 - 46136 [Lemma~good_trace_from_isRead~a...] 0. secs (0.u,0.s)
.006938159s +0kb: Chars 46137 - 46143 [Proof.] 0. secs (0.u,0.s)
.006657428s +0kb: Chars 46146 - 46203 [(cbv[isReady~goodTrace~garaged...] 0.002 secs (0.002u,0.s)
.006943162s +0kb: Chars 46206 - 46237 [(destruct~H~as~(?,~(?,~(?,~(?,...] 0.003 secs (0.003u,0.s)
.006680621s +0kb: Chars 46238 - 46242 [Qed.] 0.005 secs (0.005u,0.s)
.007105628s +0kb: Chars 46244 - 46285 [Lemma~link_initfn~:~spec_of_in...] 0. secs (0.u,0.s)
.006340306s +0kb: Chars 46286 - 46292 [Proof.] 0. secs (0.u,0.s)
.006809728s +0kb: Chars 46295 - 46312 [(eapply~initfn_ok).] 0.002 secs (0.002u,0.s)
.006787078s +0kb: Chars 46315 - 46334 [(eapply~memconst_ok).] 0.003 secs (0.003u,0.s)
8.968542306s +18480kb: Chars 46337 - 46580 [(eapply~lan9250_init_ok;~~~try...] 9.029 secs (9.013u,0.009s)
.107062663s +264kb: Chars 46581 - 46585 [Qed.] 0.106 secs (0.106u,0.s)
.033852181s +0kb: Chars 46587 - 46622 [Import~ToplevelLoop~GoFlatToRi...] 0.033 secs (0.033u,0.s)
.006957451s +0kb: Chars 46623 - 46696 [#[local]Notation~invariant~:=~...] 0. secs (0.u,0.s)
.006912877s +0kb: Chars 46697 - 47729 [Lemma~invariant_proof~:~~~fora...] 0.009 secs (0.009u,0.s)
.006558214s +0kb: Chars 47730 - 47736 [Proof.] 0. secs (0.u,0.s)
.006813819s +0kb: Chars 47739 - 47746 [(intros).] 0. secs (0.u,0.s)
.006454243s +2112kb: Chars 47750 - 47861 [(unshelve~~~(epose~proof~(comp...] 0.006 secs (0.006u,0.s)
.006303138s +792kb: Chars 47864 - 47865 [{] 0. secs (0.u,0.s)
.006871984s +0kb: Chars 47866 - 47900 [exact~(naive_word_riscv_ok~5%n...] 0. secs (0.u,0.s)
.006824113s +0kb: Chars 47901 - 47902 [}] 0. secs (0.u,0.s)
.007186146s +0kb: Chars 47905 - 47906 [{] 0. secs (0.u,0.s)
.007045502s +0kb: Chars 47907 - 47934 [(eapply~SortedListString.ok).] 0. secs (0.u,0.s)
.006480113s +0kb: Chars 47935 - 47936 [}] 0. secs (0.u,0.s)
.006626323s +0kb: Chars 47939 - 47940 [{] 0. secs (0.u,0.s)
.006926188s +0kb: Chars 47941 - 47973 [(eapply~compile_ext_call_corre...] 0.001 secs (0.001u,0.s)
.006925248s +0kb: Chars 47974 - 47975 [}] 0. secs (0.u,0.s)
.006866468s +0kb: Chars 47978 - 47979 [{] 0. secs (0.u,0.s)
.006585099s +0kb: Chars 47980 - 47987 [(intros).] 0. secs (0.u,0.s)
.009152728s +0kb: Chars 47988 - 48061 [(cbv[compile_ext_call~compile_...] 0.096 secs (0.095u,0.s)
.006421962s +0kb: Chars 48062 - 48063 [}] 0. secs (0.u,0.s)
.006770247s +0kb: Chars 48066 - 48067 [{] 0. secs (0.u,0.s)
.006855377s +0kb: Chars 48068 - 48080 [exact~ml_ok.] 0. secs (0.u,0.s)
.007036939s +0kb: Chars 48081 - 48082 [}] 0. secs (0.u,0.s)
.173930347s +2904kb: Chars 48085 - 48131 [(ssplit;~intros;~ssplit;~eappl...] 0.2 secs (0.2u,0.s)
.006834181s +0kb: Chars 48135 - 48148 [econstructor.] 0.003 secs (0.003u,0.s)
.006577302s +0kb: Chars 48151 - 48176 [eexists~garagedoor_insns.] 0.003 secs (0.003u,0.s)
.007161538s +0kb: Chars 48179 - 48204 [eexists~garagedoor_finfo.] 0.003 secs (0.003u,0.s)
.006245988s +0kb: Chars 48207 - 48237 [eexists~garagedoor_stack_size.] 0.003 secs (0.003u,0.s)
.191954283s +31416kb: Chars 48240 - 48337 [(rewrite~garagedoor_compiler_r...] 0.205 secs (0.205u,0.s)
.345111603s +0kb: Chars 48340 - 48368 [2,~3:~(vm_compute;~inversion~1).] 0.344 secs (0.334u,0.009s)
.009836877s +0kb: Chars 48371 - 48411 [econstructor.] 0.001 secs (0.001u,0.s)
.007703289s +0kb: Chars 48414 - 48441 [1:~(vm_compute;~reflexivity).] 0. secs (0.u,0.s)
.007427888s +0kb: Chars 48444 - 48479 [1:~instantiate~(~1~:=~(snd~(sn...] 0. secs (0.u,0.s)
.006766617s +0kb: Chars 48482 - 48517 [3:~instantiate~(~1~:=~(snd~(sn...] 0. secs (0.u,0.s)
.049386994s +264kb: Chars 48520 - 48539 [1,~3:~exact~eq_refl.] 0.078 secs (0.078u,0.s)
.007491019s +0kb: Chars 48542 - 48616 [1,~2:~(cbv[hl_inv];~intros;~ea...] 0.007 secs (0.007u,0.s)
.007022618s +0kb: Chars 48619 - 48694 [1,~3:~(eapply~Crypto.Util.Bool...] 0.006 secs (0.006u,0.s)
.069492940s +1320kb: Chars 48698 - 48736 [all:~(repeat~straightline;~sub...] 0.068 secs (0.068u,0.s)
.006722662s +0kb: Chars 48739 - 48740 [{] 0. secs (0.u,0.s)
.007230196s +0kb: Chars 48741 - 48761 [(repeat~straightline).] 0.001 secs (0.001u,0.s)
.006394675s +0kb: Chars 48766 - 48831 [(cbv[LowerPipeline.mem_availab...] 0. secs (0.u,0.s)
.006626645s +0kb: Chars 48836 - 48921 [(cbv[datamem_pastend~datamem_s...] 0. secs (0.u,0.s)
.061431144s +2376kb: Chars 48926 - 48968 [(SeparationLogic.extract_ex1_a...] 0.085 secs (0.084u,0.s)
.006962477s +0kb: Chars 48973 - 49049 [(change~(BinIntDef.Z.of_nat~(D...] 0.001 secs (0.001u,0.s)
.019303871s +0kb: Chars 49054 - 49157 [(Tactics.rapply~WeakestPrecond...] 0.024 secs (0.024u,0.s)
.006572321s +0kb: Chars 49162 - 49166 [2:~{] 0. secs (0.u,0.s)
.006839526s +0kb: Chars 49173 - 49223 [(rewrite~<-~(List.firstn_skipn...] 0.001 secs (0.001u,0.s)
.007007658s +0kb: Chars 49230 - 49295 [(rewrite~<-~(List.firstn_skipn...] 0.005 secs (0.005u,0.s)
.168896557s +2904kb: Chars 49302 - 49348 [(do~2~seprewrite_in~@Array.byt...] 0.181 secs (0.181u,0.s)
.063639046s +0kb: Chars 49355 - 49438 [(rewrite~2!firstn_length,~skip...] 0.063 secs (0.063u,0.s)
.006967165s +0kb: Chars 49445 - 49451 [split.] 0. secs (0.u,0.s)
.006528836s +0kb: Chars 49458 - 49459 [{] 0. secs (0.u,0.s)
.006553095s +0kb: Chars 49460 - 49479 [use_sep_assumption.] 0.001 secs (0.001u,0.s)
.006545000s +0kb: Chars 49480 - 49487 [cancel.] 0.009 secs (0.009u,0.s)
.006908468s +0kb: Chars 49488 - 49540 [(cancel_seps_at_indices~0%nat~...] 0.006 secs (0.006u,0.s)
.207478173s +4224kb: Chars 49549 - 49567 [Morphisms.f_equiv.] 0.221 secs (0.211u,0.009s)
.007009418s +0kb: Chars 49568 - 49569 [}] 0. secs (0.u,0.s)
.007004869s +0kb: Chars 49576 - 49577 [{] 0. secs (0.u,0.s)
.006572974s +0kb: Chars 49578 - 49614 [(rewrite~firstn_length,~skipn_...] 0.002 secs (0.002u,0.s)
.006903926s +0kb: Chars 49615 - 49623 [Lia.lia.] 0.019 secs (0.019u,0.s)
.006880004s +0kb: Chars 49624 - 49625 [}] 0. secs (0.u,0.s)
.007135535s +1320kb: Chars 49632 - 49633 [{] 0. secs (0.u,0.s)
.006864593s +0kb: Chars 49634 - 49642 [Lia.lia.] 0.015 secs (0.015u,0.s)
.006957927s +0kb: Chars 49643 - 49644 [}] 0. secs (0.u,0.s)
.006568311s +0kb: Chars 49645 - 49646 [}] 0. secs (0.u,0.s)
.039312419s +0kb: Chars 49651 - 49718 [(intros~?~?~?~?;~repeat~straig...] 0.062 secs (0.062u,0.s)
.007276812s +0kb: Chars 49723 - 49750 [(subst~a;~rewrite~app_nil_r).] 0.001 secs (0.001u,0.s)
.016126338s +0kb: Chars 49755 - 49822 [(rewrite~<-~(List.firstn_skipn...] 0.021 secs (0.021u,0.s)
.024116650s +2112kb: Chars 49827 - 49900 [(rewrite~<-~(List.firstn_skipn...] 0.023 secs (0.023u,0.s)
.687659373s +18744kb: Chars 49905 - 49952 [(do~2~seprewrite_in~@Array.byt...] 0.686 secs (0.676u,0.009s)
.537494257s +11880kb: Chars 49957 - 50043 [(rewrite~?firstn_length,~?skip...] 0.537 secs (0.537u,0.s)
.008435513s +0kb: Chars 50048 - 50089 [(cbv[isReady~garagedoor_spec~g...] 0. secs (0.u,0.s)
.091962138s +0kb: Chars 50090 - 50116 [(eexists~(_,~_),(_,~_);~fwd).] 0.099 secs (0.099u,0.s)
.008025478s +0kb: Chars 50117 - 50123 [eauto.] 0.008 secs (0.008u,0.s)
.007319298s +1056kb: Chars 50128 - 50129 [{] 0. secs (0.u,0.s)
.006874110s +0kb: Chars 50130 - 50150 [(rewrite~<-~app_nil_l).] 0. secs (0.u,0.s)
.006330267s +0kb: Chars 50151 - 50191 [(eapply~TracePredicate.concat_...] 0.012 secs (0.012u,0.s)
.007255655s +0kb: Chars 50192 - 50205 [econstructor.] 0. secs (0.u,0.s)
.006873235s +0kb: Chars 50206 - 50207 [}] 0. secs (0.u,0.s)
.007349033s +0kb: Chars 50212 - 50225 [(cbv[memrep]).] 0. secs (0.u,0.s)
.007230548s +0kb: Chars 50226 - 50233 [ssplit.] 0.008 secs (0.008u,0.s)
.007840135s +0kb: Chars 50238 - 50239 [{] 0. secs (0.u,0.s)
.007074379s +0kb: Chars 50240 - 50259 [use_sep_assumption.] 0.004 secs (0.004u,0.s)
.080602279s +2904kb: Chars 50260 - 50267 [cancel.] 0.115 secs (0.115u,0.s)
.014535022s +0kb: Chars 50274 - 50325 [(cancel_seps_at_indices~0%nat~...] 0.014 secs (0.014u,0.s)
.014134510s +0kb: Chars 50332 - 50383 [(cancel_seps_at_indices~0%nat~...] 0.013 secs (0.013u,0.s)
.018453874s +1056kb: Chars 50390 - 50441 [(cancel_seps_at_indices~0%nat~...] 0.018 secs (0.018u,0.s)
.006605871s +0kb: Chars 50448 - 50461 [ecancel_done.] 0.005 secs (0.005u,0.s)
.006912673s +0kb: Chars 50462 - 50463 [}] 0. secs (0.u,0.s)
.496281545s +13464kb: Chars 50468 - 50532 [all:~(repeat~rewrite~?firstn_l...] 0.502 secs (0.492u,0.009s)
.009629698s +792kb: Chars 50533 - 50534 [}] 0. secs (0.u,0.s)
.006908604s +0kb: Chars 50538 - 50539 [{] 0. secs (0.u,0.s)
.006811676s +0kb: Chars 50541 - 50595 [(match~goal~with~~|~H:goodTrac...] 0. secs (0.u,0.s)
.016737929s +0kb: Chars 50600 - 50677 [(cbv[isReady~goodTrace~good_tr...] 0.04 secs (0.039u,0.s)
.009859358s +0kb: Chars 50682 - 50716 [(DestructHead.destruct_head'~s...] 0.009 secs (0.009u,0.s)
.036692838s +0kb: Chars 50721 - 50824 [(Tactics.rapply~WeakestPrecond...] 0.036 secs (0.036u,0.s)
.084421828s +1584kb: Chars 50829 - 50896 [(intros~?~?~?~?;~repeat~straig...] 0.083 secs (0.083u,0.s)
.027558457s +0kb: Chars 50901 - 50931 [(eexists;~fwd;~try~eassumption).] 0.027 secs (0.027u,0.s)
.009419950s +0kb: Chars 50936 - 50979 [(cbv[good_trace]~in~*;~repeat~...] 0.009 secs (0.009u,0.s)
.006850034s +0kb: Chars 50984 - 50985 [{] 0. secs (0.u,0.s)
.006326202s +1848kb: Chars 50986 - 50994 [subst~a.] 0. secs (0.u,0.s)
.009503555s +0kb: Chars 50996 - 51043 [(eexists;~split;~[~eapply~Fora...] 0.022 secs (0.022u,0.s)
.014235350s +0kb: Chars 51050 - 51099 [(eapply~stateful_app_r,~statef...] 0.013 secs (0.013u,0.s)
.006926762s +0kb: Chars 51100 - 51101 [}] 0. secs (0.u,0.s)
.006599163s +0kb: Chars 51102 - 51103 [}] 0. secs (0.u,0.s)
.006481458s +0kb: Chars 51107 - 51116 [Unshelve.] 0. secs (0.u,0.s)
.006700010s +0kb: Chars 51119 - 51159 [all:~trivial~using~SortedListS...] 0.001 secs (0.001u,0.s)
3.096026318s +35112kb: Chars 51160 - 51164 [Qed.] 3.041 secs (3.039u,0.s)

The heaviest individual lines, memoy-wise, are

42240 kb 4.905879629s: Chars 34517 - 34626 [(seprewrite_in_by~~~(fun~x~=>~...] 4.904 secs (4.901u,0.s)
43032 kb 2.331045788s: Chars 11906 - 12121 [(rewrite~word.unsigned_ltu,~?w...] 2.33 secs (2.309u,0.019s)
43560 kb 4.935696629s: Chars 34374 - 34483 [(seprewrite_in_by~~~(fun~x~=>~...] 4.934 secs (4.931u,0.s)
43824 kb 3.953769337s: Chars 20868 - 20946 [(eexists~_,_,_;~ssplit;~try~ec...] 3.952 secs (3.9u,0.049s)
44880 kb 4.940760959s: Chars 34231 - 34340 [(seprewrite_in_by~~~(fun~x~=>~...] 4.939 secs (4.905u,0.029s)
46200 kb 7.395484587s: Chars 44876 - 44880 [Qed.] 7.327 secs (7.325u,0.s)
48312 kb 9.864910226s: Chars 34067 - 34176 [(seprewrite_in_by~~~(fun~x~=>~...] 9.863 secs (9.826u,0.029s)
50424 kb 2.078699421s: Chars 16113 - 16251 [(destr~Z.eqb;~rewrite~?word.un...] 2.078 secs (2.067u,0.01s)
52800 kb 2.545997135s: Chars 13830 - 14046 [(rewrite~word.unsigned_ltu,~?w...] 2.545 secs (2.524u,0.019s)
53064 kb 6.149520842s: Chars 38911 - 39015 [(seprewrite_in_by~(fun~xs~ys~=...] 6.149 secs (6.134u,0.009s)
59400 kb 2.071407786s: Chars 15099 - 15237 [(destr~Z.eqb;~rewrite~?word.un...] 2.071 secs (2.059u,0.01s)
60828 kb .064876508s: Chars 66 - 99 [Require~Import~Coq.ZArith.ZArith.] 0.072 secs (0.051u,0.02s)
62300 kb .177013846s: Chars 211 - 244 [Require~Import~compiler.Pipeline.] 0.182 secs (0.161u,0.021s)
67056 kb 9.888231819s: Chars 38162 - 38266 [(seprewrite_in_by~(fun~xs~ys~=...] 9.887 secs (9.88u,0.s)
71544 kb .068535884s: Chars 100 - 138 [Require~Import~Crypto.Spec.Cur...] 0.068 secs (0.058u,0.009s)
85008 kb 9.671959878s: Chars 34660 - 34769 [(seprewrite_in_by~~~(fun~x~=>~...] 9.671 secs (9.633u,0.029s)
87384 kb 9.669767850s: Chars 34803 - 34912 [(seprewrite_in_by~~~(fun~x~=>~...] 9.668 secs (9.641u,0.019s)
101112 kb 38.786915628s: Chars 12819 - 12886 [Import~SetEvars~coqutil.Tactic...] 0. secs (0.u,0.s)
113256 kb 14.096241184s: Chars 37520 - 37624 [(seprewrite_in_by~(fun~xs~ys~=...] 14.095 secs (14.085u,0.s)
122232 kb 15.267297091s: Chars 37413 - 37517 [(seprewrite_in_by~(fun~xs~ys~=...] 15.266 secs (15.195u,0.059s)
144936 kb 14.457730528s: Chars 42268 - 42303 [all:~(try~SepAutoArray.listZnW...] 14.47 secs (14.409u,0.049s)
148896 kb 18.932911278s: Chars 37323 - 37410 [(seprewrite_in_by~(fun~xs~ys~=...] 18.932 secs (18.888u,0.029s)
188040 kb .206445801s: Chars 0 - 34 [Require~Import~Coq.Strings.Str...] 0.123 secs (0.081u,0.042s)
192716 kb .422204029s: Chars 401 - 460 [Require~Import~Crypto.Bedrock....] 0.421 secs (0.35u,0.07s)
241304 kb 67.127166250s: Chars 42304 - 42308 [Qed.] 67.135 secs (67.034u,0.069s)
412264 kb 1.635113554s: Chars 461 - 530 [Require~Import~Crypto.Bedrock....] 1.634 secs (1.514u,0.119s)

Timewise, the slowest lines are

4.350693476 s 0 kb: Chars 37734 - 37838 [(seprewrite_in_by~(fun~xs~ys~=...] 4.35 secs (4.347u,0.s)
4.905879629 s 42240 kb: Chars 34517 - 34626 [(seprewrite_in_by~~~(fun~x~=>~...] 4.904 secs (4.901u,0.s)
4.935696629 s 43560 kb: Chars 34374 - 34483 [(seprewrite_in_by~~~(fun~x~=>~...] 4.934 secs (4.931u,0.s)
4.940760959 s 44880 kb: Chars 34231 - 34340 [(seprewrite_in_by~~~(fun~x~=>~...] 4.939 secs (4.905u,0.029s)
5.244336293 s 16632 kb: Chars 43232 - 43403 [(repeat~eapply~recvEthernet_ok...] 5.243 secs (5.24u,0.s)
5.790857036 s 6072 kb: Chars 19052 - 19072 [(repeat~straightline).] 5.79 secs (5.787u,0.s)
6.149520842 s 53064 kb: Chars 38911 - 39015 [(seprewrite_in_by~(fun~xs~ys~=...] 6.149 secs (6.134u,0.009s)
6.606412111 s 0 kb: Chars 33925 - 34034 [(seprewrite_in_by~~~(fun~x~=>~...] 6.606 secs (6.601u,0.s)
6.653652514 s 0 kb: Chars 33847 - 33922 [(seprewrite_in_by~(@bytearray_...] 6.653 secs (6.648u,0.s)
7.395484587 s 46200 kb: Chars 44876 - 44880 [Qed.] 7.327 secs (7.325u,0.s)
8.736204370 s 7128 kb: Chars 44749 - 44760 [(vm_compute).] 8.76 secs (8.749u,0.009s)
8.968542306 s 18480 kb: Chars 46337 - 46580 [(eapply~lan9250_init_ok;~~~try...] 9.029 secs (9.013u,0.009s)
9.669767850 s 87384 kb: Chars 34803 - 34912 [(seprewrite_in_by~~~(fun~x~=>~...] 9.668 secs (9.641u,0.019s)
9.671959878 s 85008 kb: Chars 34660 - 34769 [(seprewrite_in_by~~~(fun~x~=>~...] 9.671 secs (9.633u,0.029s)
9.771183834 s 0 kb: Chars 37948 - 38052 [(seprewrite_in_by~(fun~xs~ys~=...] 9.77 secs (9.763u,0.s)
9.829626488 s 0 kb: Chars 38055 - 38159 [(seprewrite_in_by~(fun~xs~ys~=...] 9.829 secs (9.822u,0.s)
9.864910226 s 48312 kb: Chars 34067 - 34176 [(seprewrite_in_by~~~(fun~x~=>~...] 9.863 secs (9.826u,0.029s)
9.888231819 s 67056 kb: Chars 38162 - 38266 [(seprewrite_in_by~(fun~xs~ys~=...] 9.887 secs (9.88u,0.s)
11.407465406 s 8976 kb: Chars 13436 - 13555 [rewrite_strat~bottomup~(terms~...] 11.435 secs (11.415u,0.009s)
13.028313825 s 26400 kb: Chars 37627 - 37731 [(seprewrite_in_by~(fun~xs~ys~=...] 13.027 secs (13.008u,0.009s)
14.096241184 s 113256 kb: Chars 37520 - 37624 [(seprewrite_in_by~(fun~xs~ys~=...] 14.095 secs (14.085u,0.s)
14.457730528 s 144936 kb: Chars 42268 - 42303 [all:~(try~SepAutoArray.listZnW...] 14.47 secs (14.409u,0.049s)
15.267297091 s 122232 kb: Chars 37413 - 37517 [(seprewrite_in_by~(fun~xs~ys~=...] 15.266 secs (15.195u,0.059s)
18.932911278 s 148896 kb: Chars 37323 - 37410 [(seprewrite_in_by~(fun~xs~ys~=...] 18.932 secs (18.888u,0.029s)
38.786915628 s 101112 kb: Chars 12819 - 12886 [Import~SetEvars~coqutil.Tactic...] 0. secs (0.u,0.s)
67.127166250 s 241304 kb: Chars 42304 - 42308 [Qed.] 67.135 secs (67.034u,0.069s)

andres-erbsen · 2022-10-13T20:00:12Z

2332608 ko after #1431

andres-erbsen · 2022-10-13T20:04:55Z

https://gitlab.com/coq/coq/-/jobs/3168928488 is a CI job off of coq/coq#16648 . I restarted the pipeline before merging #1431 but as the particular job hasn't started I'd guess it'll pick up fiat-crypto master anyway. If it passes, I think we're "good" on this issue.

JasonGross · 2022-10-14T06:32:46Z

It passes at https://github.com/coq/coq/pull/16648/checks?check_run_id=8884687370

Thanks all!

This was referenced Oct 13, 2022

Remove useless "New" wrapper modules coq/coq#16638

Merged

Less Memory-Hungry, More Principled Solution for Decidable Side-Conditions mit-plv/bedrock2#285

Closed

samuelgruetter mentioned this issue Oct 13, 2022

use vm_compute instead of Ltac to check instruction bounds #1429

Merged

andres-erbsen changed the title ~~GarageDoor breaks Coq CI~~ GarageDoor does not fit within Coq CI memory limit Oct 13, 2022

JasonGross closed this as completed Oct 14, 2022

JasonGross mentioned this issue Oct 14, 2022

Less memory-hungry build #1434

Open

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

GarageDoor does not fit within Coq CI memory limit #1427

GarageDoor does not fit within Coq CI memory limit #1427

JasonGross commented Oct 12, 2022

andres-erbsen commented Oct 13, 2022

JasonGross commented Oct 13, 2022

andres-erbsen commented Oct 13, 2022

JasonGross commented Oct 13, 2022

andres-erbsen commented Oct 13, 2022 •

edited

JasonGross commented Oct 13, 2022 •

edited

andres-erbsen commented Oct 13, 2022 •

edited

andres-erbsen commented Oct 13, 2022

JasonGross commented Oct 14, 2022

GarageDoor does not fit within Coq CI memory limit #1427

GarageDoor does not fit within Coq CI memory limit #1427

Comments

JasonGross commented Oct 12, 2022

andres-erbsen commented Oct 13, 2022

JasonGross commented Oct 13, 2022

andres-erbsen commented Oct 13, 2022

JasonGross commented Oct 13, 2022

andres-erbsen commented Oct 13, 2022 • edited

JasonGross commented Oct 13, 2022 • edited

andres-erbsen commented Oct 13, 2022 • edited

andres-erbsen commented Oct 13, 2022

JasonGross commented Oct 14, 2022

andres-erbsen commented Oct 13, 2022 •

edited

JasonGross commented Oct 13, 2022 •

edited

andres-erbsen commented Oct 13, 2022 •

edited