diff --git a/Arm/MemoryProofs.lean b/Arm/MemoryProofs.lean index a083ee75..89d80460 100644 --- a/Arm/MemoryProofs.lean +++ b/Arm/MemoryProofs.lean @@ -26,22 +26,6 @@ open Std.BitVec ---------------------------------------------------------------------- -- Key theorem: read_mem_bytes_of_write_mem_bytes_same -/- -theorem read_mem_of_write_mem_bytes_different1 (hn1 : n <= 2^64) - (h : mem_separate addr1 addr1 addr2 (addr2 + (n - 1)#64)) : - read_mem addr1 (write_mem_bytes n addr2 v s) = read_mem addr1 s := by - induction n generalizing addr2 s - case zero => simp [write_mem_bytes] - case succ => - rename_i n n_ih - simp [write_mem_bytes] - rw [n_ih (by omega)] - · rw [read_mem_of_write_mem_different] - apply mem_separate_starting_addresses_neq h - · simp_all - sorry --/ - theorem mem_separate_preserved_second_start_addr_add_one (h0 : 0 < m) (h1 : m < 2^64) (h2 : mem_separate a b c (c + m#64)) : @@ -62,7 +46,7 @@ theorem read_mem_of_write_mem_bytes_different (hn1 : n <= 2^64) case pos => -- n = 0 subst n; simp [write_mem_bytes] case neg => -- n ≠ 0 - have hn0' : 0 < n := by exact Nat.pos_of_ne_zero hn0 + have hn0' : 0 < n := by omega induction n, hn0' using Nat.le_induction generalizing addr2 s case base => have h' : addr1 ≠ addr2 := by apply mem_separate_starting_addresses_neq h diff --git a/Proofs/Proofs.lean b/Proofs/Proofs.lean index cd36244f..4a4e161c 100644 --- a/Proofs/Proofs.lean +++ b/Proofs/Proofs.lean @@ -6,4 +6,5 @@ import «Proofs».MultiInsts import «Proofs».Test import «Proofs».Sha512_block_armv8_rules import «Proofs».Sha512_block_armv8 +import «Proofs».Sha512_AssocRepr diff --git a/Proofs/SHA512_AssocRepr.lean b/Proofs/SHA512_AssocRepr.lean new file mode 100644 index 00000000..986f6ead --- /dev/null +++ b/Proofs/SHA512_AssocRepr.lean @@ -0,0 +1,572 @@ +/- +Copyright (c) 2024 Amazon.com, Inc. or its affiliates. All Rights Reserved. +Author(s): Shilpi Goel +-/ +import Arm.Exec +import Arm.MemoryProofs +import Std.Data.AssocList + +section SHA512_proof + +open Std.BitVec +open Std.AssocList + +def sha512_program : Std.AssocList (BitVec 64) (BitVec 32) := + [(0x1264c0#64 , 0xa9bf7bfd#32), -- stp x29, x30, [sp, #-16]! + (0x1264c4#64 , 0x910003fd#32), -- mov x29, sp + (0x1264c8#64 , 0x4cdf2030#32), -- ld1 {v16.16b-v19.16b}, [x1], #64 + (0x1264cc#64 , 0x4cdf2034#32), -- ld1 {v20.16b-v23.16b}, [x1], #64 + (0x1264d0#64 , 0x4c402c00#32), -- ld1 {v0.2d-v3.2d}, [x0] + (0x1264d4#64 , 0xd0000463#32), -- adrp x3, 1b4000 + (0x1264d8#64 , 0x910c0063#32), -- add x3, x3, #0x300 + (0x1264dc#64 , 0x4e200a10#32), -- rev64 v16.16b, v16.16b + (0x1264e0#64 , 0x4e200a31#32), -- rev64 v17.16b, v17.16b + (0x1264e4#64 , 0x4e200a52#32), -- rev64 v18.16b, v18.16b + (0x1264e8#64 , 0x4e200a73#32), -- rev64 v19.16b, v19.16b + (0x1264ec#64 , 0x4e200a94#32), -- rev64 v20.16b, v20.16b + (0x1264f0#64 , 0x4e200ab5#32), -- rev64 v21.16b, v21.16b + (0x1264f4#64 , 0x4e200ad6#32), -- rev64 v22.16b, v22.16b + (0x1264f8#64 , 0x4e200af7#32), -- rev64 v23.16b, v23.16b + (0x1264fc#64 , 0x14000001#32), -- b 126500 + (0x126500#64 , 0x4cdf7c78#32), -- ld1 {v24.2d}, [x3], #16 + (0x126504#64 , 0xf1000442#32), -- subs x2, x2, #0x1 + (0x126508#64 , 0xd1020024#32), -- sub x4, x1, #0x80 + (0x12650c#64 , 0x4ea01c1a#32), -- mov v26.16b, v0.16b + (0x126510#64 , 0x4ea11c3b#32), -- mov v27.16b, v1.16b + (0x126514#64 , 0x4ea21c5c#32), -- mov v28.16b, v2.16b + (0x126518#64 , 0x4ea31c7d#32), -- mov v29.16b, v3.16b + (0x12651c#64 , 0x9a841021#32), -- csel x1, x1, x4, ne // ne = any + (0x126520#64 , 0x4ef08718#32), -- add v24.2d, v24.2d, v16.2d + (0x126524#64 , 0x4cdf7c79#32), -- ld1 {v25.2d}, [x3], #16 + (0x126528#64 , 0x6e184318#32), -- ext v24.16b, v24.16b, v24.16b, #8 + (0x12652c#64 , 0x6e034045#32), -- ext v5.16b, v2.16b, v3.16b, #8 + (0x126530#64 , 0x6e024026#32), -- ext v6.16b, v1.16b, v2.16b, #8 + (0x126534#64 , 0x4ef88463#32), -- add v3.2d, v3.2d, v24.2d + (0x126538#64 , 0xcec08230#32), -- sha512su0 v16.2d, v17.2d + (0x12653c#64 , 0x6e154287#32), -- ext v7.16b, v20.16b, v21.16b, #8 + (0x126540#64 , 0xce6680a3#32), -- sha512h q3, q5, v6.2d + (0x126544#64 , 0xce678af0#32), -- sha512su1 v16.2d, v23.2d, v7.2d + (0x126548#64 , 0x4ee38424#32), -- add v4.2d, v1.2d, v3.2d + (0x12654c#64 , 0xce608423#32), -- sha512h2 q3, q1, v0.2d + (0x126550#64 , 0x4ef18739#32), -- add v25.2d, v25.2d, v17.2d + (0x126554#64 , 0x4cdf7c78#32), -- ld1 {v24.2d}, [x3], #16 + (0x126558#64 , 0x6e194339#32), -- ext v25.16b, v25.16b, v25.16b, #8 + (0x12655c#64 , 0x6e024085#32), -- ext v5.16b, v4.16b, v2.16b, #8 + (0x126560#64 , 0x6e044006#32), -- ext v6.16b, v0.16b, v4.16b, #8 + (0x126564#64 , 0x4ef98442#32), -- add v2.2d, v2.2d, v25.2d + (0x126568#64 , 0xcec08251#32), -- sha512su0 v17.2d, v18.2d + (0x12656c#64 , 0x6e1642a7#32), -- ext v7.16b, v21.16b, v22.16b, #8 + (0x126570#64 , 0xce6680a2#32), -- sha512h q2, q5, v6.2d + (0x126574#64 , 0xce678a11#32), -- sha512su1 v17.2d, v16.2d, v7.2d + (0x126578#64 , 0x4ee28401#32), -- add v1.2d, v0.2d, v2.2d + (0x12657c#64 , 0xce638402#32), -- sha512h2 q2, q0, v3.2d + (0x126580#64 , 0x4ef28718#32), -- add v24.2d, v24.2d, v18.2d + (0x126584#64 , 0x4cdf7c79#32), -- ld1 {v25.2d}, [x3], #16 + (0x126588#64 , 0x6e184318#32), -- ext v24.16b, v24.16b, v24.16b, #8 + (0x12658c#64 , 0x6e044025#32), -- ext v5.16b, v1.16b, v4.16b, #8 + (0x126590#64 , 0x6e014066#32), -- ext v6.16b, v3.16b, v1.16b, #8 + (0x126594#64 , 0x4ef88484#32), -- add v4.2d, v4.2d, v24.2d + (0x126598#64 , 0xcec08272#32), -- sha512su0 v18.2d, v19.2d + (0x12659c#64 , 0x6e1742c7#32), -- ext v7.16b, v22.16b, v23.16b, #8 + (0x1265a0#64 , 0xce6680a4#32), -- sha512h q4, q5, v6.2d + (0x1265a4#64 , 0xce678a32#32), -- sha512su1 v18.2d, v17.2d, v7.2d + (0x1265a8#64 , 0x4ee48460#32), -- add v0.2d, v3.2d, v4.2d + (0x1265ac#64 , 0xce628464#32), -- sha512h2 q4, q3, v2.2d + (0x1265b0#64 , 0x4ef38739#32), -- add v25.2d, v25.2d, v19.2d + (0x1265b4#64 , 0x4cdf7c78#32), -- ld1 {v24.2d}, [x3], #16 + (0x1265b8#64 , 0x6e194339#32), -- ext v25.16b, v25.16b, v25.16b, #8 + (0x1265bc#64 , 0x6e014005#32), -- ext v5.16b, v0.16b, v1.16b, #8 + (0x1265c0#64 , 0x6e004046#32), -- ext v6.16b, v2.16b, v0.16b, #8 + (0x1265c4#64 , 0x4ef98421#32), -- add v1.2d, v1.2d, v25.2d + (0x1265c8#64 , 0xcec08293#32), -- sha512su0 v19.2d, v20.2d + (0x1265cc#64 , 0x6e1042e7#32), -- ext v7.16b, v23.16b, v16.16b, #8 + (0x1265d0#64 , 0xce6680a1#32), -- sha512h q1, q5, v6.2d + (0x1265d4#64 , 0xce678a53#32), -- sha512su1 v19.2d, v18.2d, v7.2d + (0x1265d8#64 , 0x4ee18443#32), -- add v3.2d, v2.2d, v1.2d + (0x1265dc#64 , 0xce648441#32), -- sha512h2 q1, q2, v4.2d + (0x1265e0#64 , 0x4ef48718#32), -- add v24.2d, v24.2d, v20.2d + (0x1265e4#64 , 0x4cdf7c79#32), -- ld1 {v25.2d}, [x3], #16 + (0x1265e8#64 , 0x6e184318#32), -- ext v24.16b, v24.16b, v24.16b, #8 + (0x1265ec#64 , 0x6e004065#32), -- ext v5.16b, v3.16b, v0.16b, #8 + (0x1265f0#64 , 0x6e034086#32), -- ext v6.16b, v4.16b, v3.16b, #8 + (0x1265f4#64 , 0x4ef88400#32), -- add v0.2d, v0.2d, v24.2d + (0x1265f8#64 , 0xcec082b4#32), -- sha512su0 v20.2d, v21.2d + (0x1265fc#64 , 0x6e114207#32), -- ext v7.16b, v16.16b, v17.16b, #8 + (0x126600#64 , 0xce6680a0#32), -- sha512h q0, q5, v6.2d + (0x126604#64 , 0xce678a74#32), -- sha512su1 v20.2d, v19.2d, v7.2d + (0x126608#64 , 0x4ee08482#32), -- add v2.2d, v4.2d, v0.2d + (0x12660c#64 , 0xce618480#32), -- sha512h2 q0, q4, v1.2d + (0x126610#64 , 0x4ef58739#32), -- add v25.2d, v25.2d, v21.2d + (0x126614#64 , 0x4cdf7c78#32), -- ld1 {v24.2d}, [x3], #16 + (0x126618#64 , 0x6e194339#32), -- ext v25.16b, v25.16b, v25.16b, #8 + (0x12661c#64 , 0x6e034045#32), -- ext v5.16b, v2.16b, v3.16b, #8 + (0x126620#64 , 0x6e024026#32), -- ext v6.16b, v1.16b, v2.16b, #8 + (0x126624#64 , 0x4ef98463#32), -- add v3.2d, v3.2d, v25.2d + (0x126628#64 , 0xcec082d5#32), -- sha512su0 v21.2d, v22.2d + (0x12662c#64 , 0x6e124227#32), -- ext v7.16b, v17.16b, v18.16b, #8 + (0x126630#64 , 0xce6680a3#32), -- sha512h q3, q5, v6.2d + (0x126634#64 , 0xce678a95#32), -- sha512su1 v21.2d, v20.2d, v7.2d + (0x126638#64 , 0x4ee38424#32), -- add v4.2d, v1.2d, v3.2d + (0x12663c#64 , 0xce608423#32), -- sha512h2 q3, q1, v0.2d + (0x126640#64 , 0x4ef68718#32), -- add v24.2d, v24.2d, v22.2d + (0x126644#64 , 0x4cdf7c79#32), -- ld1 {v25.2d}, [x3], #16 + (0x126648#64 , 0x6e184318#32), -- ext v24.16b, v24.16b, v24.16b, #8 + (0x12664c#64 , 0x6e024085#32), -- ext v5.16b, v4.16b, v2.16b, #8 + (0x126650#64 , 0x6e044006#32), -- ext v6.16b, v0.16b, v4.16b, #8 + (0x126654#64 , 0x4ef88442#32), -- add v2.2d, v2.2d, v24.2d + (0x126658#64 , 0xcec082f6#32), -- sha512su0 v22.2d, v23.2d + (0x12665c#64 , 0x6e134247#32), -- ext v7.16b, v18.16b, v19.16b, #8 + (0x126660#64 , 0xce6680a2#32), -- sha512h q2, q5, v6.2d + (0x126664#64 , 0xce678ab6#32), -- sha512su1 v22.2d, v21.2d, v7.2d + (0x126668#64 , 0x4ee28401#32), -- add v1.2d, v0.2d, v2.2d + (0x12666c#64 , 0xce638402#32), -- sha512h2 q2, q0, v3.2d + (0x126670#64 , 0x4ef78739#32), -- add v25.2d, v25.2d, v23.2d + (0x126674#64 , 0x4cdf7c78#32), -- ld1 {v24.2d}, [x3], #16 + (0x126678#64 , 0x6e194339#32), -- ext v25.16b, v25.16b, v25.16b, #8 + (0x12667c#64 , 0x6e044025#32), -- ext v5.16b, v1.16b, v4.16b, #8 + (0x126680#64 , 0x6e014066#32), -- ext v6.16b, v3.16b, v1.16b, #8 + (0x126684#64 , 0x4ef98484#32), -- add v4.2d, v4.2d, v25.2d + (0x126688#64 , 0xcec08217#32), -- sha512su0 v23.2d, v16.2d + (0x12668c#64 , 0x6e144267#32), -- ext v7.16b, v19.16b, v20.16b, #8 + (0x126690#64 , 0xce6680a4#32), -- sha512h q4, q5, v6.2d + (0x126694#64 , 0xce678ad7#32), -- sha512su1 v23.2d, v22.2d, v7.2d + (0x126698#64 , 0x4ee48460#32), -- add v0.2d, v3.2d, v4.2d + (0x12669c#64 , 0xce628464#32), -- sha512h2 q4, q3, v2.2d + (0x1266a0#64 , 0x4ef08718#32), -- add v24.2d, v24.2d, v16.2d + (0x1266a4#64 , 0x4cdf7c79#32), -- ld1 {v25.2d}, [x3], #16 + (0x1266a8#64 , 0x6e184318#32), -- ext v24.16b, v24.16b, v24.16b, #8 + (0x1266ac#64 , 0x6e014005#32), -- ext v5.16b, v0.16b, v1.16b, #8 + (0x1266b0#64 , 0x6e004046#32), -- ext v6.16b, v2.16b, v0.16b, #8 + (0x1266b4#64 , 0x4ef88421#32), -- add v1.2d, v1.2d, v24.2d + (0x1266b8#64 , 0xcec08230#32), -- sha512su0 v16.2d, v17.2d + (0x1266bc#64 , 0x6e154287#32), -- ext v7.16b, v20.16b, v21.16b, #8 + (0x1266c0#64 , 0xce6680a1#32), -- sha512h q1, q5, v6.2d + (0x1266c4#64 , 0xce678af0#32), -- sha512su1 v16.2d, v23.2d, v7.2d + (0x1266c8#64 , 0x4ee18443#32), -- add v3.2d, v2.2d, v1.2d + (0x1266cc#64 , 0xce648441#32), -- sha512h2 q1, q2, v4.2d + (0x1266d0#64 , 0x4ef18739#32), -- add v25.2d, v25.2d, v17.2d + (0x1266d4#64 , 0x4cdf7c78#32), -- ld1 {v24.2d}, [x3], #16 + (0x1266d8#64 , 0x6e194339#32), -- ext v25.16b, v25.16b, v25.16b, #8 + (0x1266dc#64 , 0x6e004065#32), -- ext v5.16b, v3.16b, v0.16b, #8 + (0x1266e0#64 , 0x6e034086#32), -- ext v6.16b, v4.16b, v3.16b, #8 + (0x1266e4#64 , 0x4ef98400#32), -- add v0.2d, v0.2d, v25.2d + (0x1266e8#64 , 0xcec08251#32), -- sha512su0 v17.2d, v18.2d + (0x1266ec#64 , 0x6e1642a7#32), -- ext v7.16b, v21.16b, v22.16b, #8 + (0x1266f0#64 , 0xce6680a0#32), -- sha512h q0, q5, v6.2d + (0x1266f4#64 , 0xce678a11#32), -- sha512su1 v17.2d, v16.2d, v7.2d + (0x1266f8#64 , 0x4ee08482#32), -- add v2.2d, v4.2d, v0.2d + (0x1266fc#64 , 0xce618480#32), -- sha512h2 q0, q4, v1.2d + (0x126700#64 , 0x4ef28718#32), -- add v24.2d, v24.2d, v18.2d + (0x126704#64 , 0x4cdf7c79#32), -- ld1 {v25.2d}, [x3], #16 + (0x126708#64 , 0x6e184318#32), -- ext v24.16b, v24.16b, v24.16b, #8 + (0x12670c#64 , 0x6e034045#32), -- ext v5.16b, v2.16b, v3.16b, #8 + (0x126710#64 , 0x6e024026#32), -- ext v6.16b, v1.16b, v2.16b, #8 + (0x126714#64 , 0x4ef88463#32), -- add v3.2d, v3.2d, v24.2d + (0x126718#64 , 0xcec08272#32), -- sha512su0 v18.2d, v19.2d + (0x12671c#64 , 0x6e1742c7#32), -- ext v7.16b, v22.16b, v23.16b, #8 + (0x126720#64 , 0xce6680a3#32), -- sha512h q3, q5, v6.2d + (0x126724#64 , 0xce678a32#32), -- sha512su1 v18.2d, v17.2d, v7.2d + (0x126728#64 , 0x4ee38424#32), -- add v4.2d, v1.2d, v3.2d + (0x12672c#64 , 0xce608423#32), -- sha512h2 q3, q1, v0.2d + (0x126730#64 , 0x4ef38739#32), -- add v25.2d, v25.2d, v19.2d + (0x126734#64 , 0x4cdf7c78#32), -- ld1 {v24.2d}, [x3], #16 + (0x126738#64 , 0x6e194339#32), -- ext v25.16b, v25.16b, v25.16b, #8 + (0x12673c#64 , 0x6e024085#32), -- ext v5.16b, v4.16b, v2.16b, #8 + (0x126740#64 , 0x6e044006#32), -- ext v6.16b, v0.16b, v4.16b, #8 + (0x126744#64 , 0x4ef98442#32), -- add v2.2d, v2.2d, v25.2d + (0x126748#64 , 0xcec08293#32), -- sha512su0 v19.2d, v20.2d + (0x12674c#64 , 0x6e1042e7#32), -- ext v7.16b, v23.16b, v16.16b, #8 + (0x126750#64 , 0xce6680a2#32), -- sha512h q2, q5, v6.2d + (0x126754#64 , 0xce678a53#32), -- sha512su1 v19.2d, v18.2d, v7.2d + (0x126758#64 , 0x4ee28401#32), -- add v1.2d, v0.2d, v2.2d + (0x12675c#64 , 0xce638402#32), -- sha512h2 q2, q0, v3.2d + (0x126760#64 , 0x4ef48718#32), -- add v24.2d, v24.2d, v20.2d + (0x126764#64 , 0x4cdf7c79#32), -- ld1 {v25.2d}, [x3], #16 + (0x126768#64 , 0x6e184318#32), -- ext v24.16b, v24.16b, v24.16b, #8 + (0x12676c#64 , 0x6e044025#32), -- ext v5.16b, v1.16b, v4.16b, #8 + (0x126770#64 , 0x6e014066#32), -- ext v6.16b, v3.16b, v1.16b, #8 + (0x126774#64 , 0x4ef88484#32), -- add v4.2d, v4.2d, v24.2d + (0x126778#64 , 0xcec082b4#32), -- sha512su0 v20.2d, v21.2d + (0x12677c#64 , 0x6e114207#32), -- ext v7.16b, v16.16b, v17.16b, #8 + (0x126780#64 , 0xce6680a4#32), -- sha512h q4, q5, v6.2d + (0x126784#64 , 0xce678a74#32), -- sha512su1 v20.2d, v19.2d, v7.2d + (0x126788#64 , 0x4ee48460#32), -- add v0.2d, v3.2d, v4.2d + (0x12678c#64 , 0xce628464#32), -- sha512h2 q4, q3, v2.2d + (0x126790#64 , 0x4ef58739#32), -- add v25.2d, v25.2d, v21.2d + (0x126794#64 , 0x4cdf7c78#32), -- ld1 {v24.2d}, [x3], #16 + (0x126798#64 , 0x6e194339#32), -- ext v25.16b, v25.16b, v25.16b, #8 + (0x12679c#64 , 0x6e014005#32), -- ext v5.16b, v0.16b, v1.16b, #8 + (0x1267a0#64 , 0x6e004046#32), -- ext v6.16b, v2.16b, v0.16b, #8 + (0x1267a4#64 , 0x4ef98421#32), -- add v1.2d, v1.2d, v25.2d + (0x1267a8#64 , 0xcec082d5#32), -- sha512su0 v21.2d, v22.2d + (0x1267ac#64 , 0x6e124227#32), -- ext v7.16b, v17.16b, v18.16b, #8 + (0x1267b0#64 , 0xce6680a1#32), -- sha512h q1, q5, v6.2d + (0x1267b4#64 , 0xce678a95#32), -- sha512su1 v21.2d, v20.2d, v7.2d + (0x1267b8#64 , 0x4ee18443#32), -- add v3.2d, v2.2d, v1.2d + (0x1267bc#64 , 0xce648441#32), -- sha512h2 q1, q2, v4.2d + (0x1267c0#64 , 0x4ef68718#32), -- add v24.2d, v24.2d, v22.2d + (0x1267c4#64 , 0x4cdf7c79#32), -- ld1 {v25.2d}, [x3], #16 + (0x1267c8#64 , 0x6e184318#32), -- ext v24.16b, v24.16b, v24.16b, #8 + (0x1267cc#64 , 0x6e004065#32), -- ext v5.16b, v3.16b, v0.16b, #8 + (0x1267d0#64 , 0x6e034086#32), -- ext v6.16b, v4.16b, v3.16b, #8 + (0x1267d4#64 , 0x4ef88400#32), -- add v0.2d, v0.2d, v24.2d + (0x1267d8#64 , 0xcec082f6#32), -- sha512su0 v22.2d, v23.2d + (0x1267dc#64 , 0x6e134247#32), -- ext v7.16b, v18.16b, v19.16b, #8 + (0x1267e0#64 , 0xce6680a0#32), -- sha512h q0, q5, v6.2d + (0x1267e4#64 , 0xce678ab6#32), -- sha512su1 v22.2d, v21.2d, v7.2d + (0x1267e8#64 , 0x4ee08482#32), -- add v2.2d, v4.2d, v0.2d + (0x1267ec#64 , 0xce618480#32), -- sha512h2 q0, q4, v1.2d + (0x1267f0#64 , 0x4ef78739#32), -- add v25.2d, v25.2d, v23.2d + (0x1267f4#64 , 0x4cdf7c78#32), -- ld1 {v24.2d}, [x3], #16 + (0x1267f8#64 , 0x6e194339#32), -- ext v25.16b, v25.16b, v25.16b, #8 + (0x1267fc#64 , 0x6e034045#32), -- ext v5.16b, v2.16b, v3.16b, #8 + (0x126800#64 , 0x6e024026#32), -- ext v6.16b, v1.16b, v2.16b, #8 + (0x126804#64 , 0x4ef98463#32), -- add v3.2d, v3.2d, v25.2d + (0x126808#64 , 0xcec08217#32), -- sha512su0 v23.2d, v16.2d + (0x12680c#64 , 0x6e144267#32), -- ext v7.16b, v19.16b, v20.16b, #8 + (0x126810#64 , 0xce6680a3#32), -- sha512h q3, q5, v6.2d + (0x126814#64 , 0xce678ad7#32), -- sha512su1 v23.2d, v22.2d, v7.2d + (0x126818#64 , 0x4ee38424#32), -- add v4.2d, v1.2d, v3.2d + (0x12681c#64 , 0xce608423#32), -- sha512h2 q3, q1, v0.2d + (0x126820#64 , 0x4ef08718#32), -- add v24.2d, v24.2d, v16.2d + (0x126824#64 , 0x4cdf7c79#32), -- ld1 {v25.2d}, [x3], #16 + (0x126828#64 , 0x6e184318#32), -- ext v24.16b, v24.16b, v24.16b, #8 + (0x12682c#64 , 0x6e024085#32), -- ext v5.16b, v4.16b, v2.16b, #8 + (0x126830#64 , 0x6e044006#32), -- ext v6.16b, v0.16b, v4.16b, #8 + (0x126834#64 , 0x4ef88442#32), -- add v2.2d, v2.2d, v24.2d + (0x126838#64 , 0xcec08230#32), -- sha512su0 v16.2d, v17.2d + (0x12683c#64 , 0x6e154287#32), -- ext v7.16b, v20.16b, v21.16b, #8 + (0x126840#64 , 0xce6680a2#32), -- sha512h q2, q5, v6.2d + (0x126844#64 , 0xce678af0#32), -- sha512su1 v16.2d, v23.2d, v7.2d + (0x126848#64 , 0x4ee28401#32), -- add v1.2d, v0.2d, v2.2d + (0x12684c#64 , 0xce638402#32), -- sha512h2 q2, q0, v3.2d + (0x126850#64 , 0x4ef18739#32), -- add v25.2d, v25.2d, v17.2d + (0x126854#64 , 0x4cdf7c78#32), -- ld1 {v24.2d}, [x3], #16 + (0x126858#64 , 0x6e194339#32), -- ext v25.16b, v25.16b, v25.16b, #8 + (0x12685c#64 , 0x6e044025#32), -- ext v5.16b, v1.16b, v4.16b, #8 + (0x126860#64 , 0x6e014066#32), -- ext v6.16b, v3.16b, v1.16b, #8 + (0x126864#64 , 0x4ef98484#32), -- add v4.2d, v4.2d, v25.2d + (0x126868#64 , 0xcec08251#32), -- sha512su0 v17.2d, v18.2d + (0x12686c#64 , 0x6e1642a7#32), -- ext v7.16b, v21.16b, v22.16b, #8 + (0x126870#64 , 0xce6680a4#32), -- sha512h q4, q5, v6.2d + (0x126874#64 , 0xce678a11#32), -- sha512su1 v17.2d, v16.2d, v7.2d + (0x126878#64 , 0x4ee48460#32), -- add v0.2d, v3.2d, v4.2d + (0x12687c#64 , 0xce628464#32), -- sha512h2 q4, q3, v2.2d + (0x126880#64 , 0x4ef28718#32), -- add v24.2d, v24.2d, v18.2d + (0x126884#64 , 0x4cdf7c79#32), -- ld1 {v25.2d}, [x3], #16 + (0x126888#64 , 0x6e184318#32), -- ext v24.16b, v24.16b, v24.16b, #8 + (0x12688c#64 , 0x6e014005#32), -- ext v5.16b, v0.16b, v1.16b, #8 + (0x126890#64 , 0x6e004046#32), -- ext v6.16b, v2.16b, v0.16b, #8 + (0x126894#64 , 0x4ef88421#32), -- add v1.2d, v1.2d, v24.2d + (0x126898#64 , 0xcec08272#32), -- sha512su0 v18.2d, v19.2d + (0x12689c#64 , 0x6e1742c7#32), -- ext v7.16b, v22.16b, v23.16b, #8 + (0x1268a0#64 , 0xce6680a1#32), -- sha512h q1, q5, v6.2d + (0x1268a4#64 , 0xce678a32#32), -- sha512su1 v18.2d, v17.2d, v7.2d + (0x1268a8#64 , 0x4ee18443#32), -- add v3.2d, v2.2d, v1.2d + (0x1268ac#64 , 0xce648441#32), -- sha512h2 q1, q2, v4.2d + (0x1268b0#64 , 0x4ef38739#32), -- add v25.2d, v25.2d, v19.2d + (0x1268b4#64 , 0x4cdf7c78#32), -- ld1 {v24.2d}, [x3], #16 + (0x1268b8#64 , 0x6e194339#32), -- ext v25.16b, v25.16b, v25.16b, #8 + (0x1268bc#64 , 0x6e004065#32), -- ext v5.16b, v3.16b, v0.16b, #8 + (0x1268c0#64 , 0x6e034086#32), -- ext v6.16b, v4.16b, v3.16b, #8 + (0x1268c4#64 , 0x4ef98400#32), -- add v0.2d, v0.2d, v25.2d + (0x1268c8#64 , 0xcec08293#32), -- sha512su0 v19.2d, v20.2d + (0x1268cc#64 , 0x6e1042e7#32), -- ext v7.16b, v23.16b, v16.16b, #8 + (0x1268d0#64 , 0xce6680a0#32), -- sha512h q0, q5, v6.2d + (0x1268d4#64 , 0xce678a53#32), -- sha512su1 v19.2d, v18.2d, v7.2d + (0x1268d8#64 , 0x4ee08482#32), -- add v2.2d, v4.2d, v0.2d + (0x1268dc#64 , 0xce618480#32), -- sha512h2 q0, q4, v1.2d + (0x1268e0#64 , 0x4ef48718#32), -- add v24.2d, v24.2d, v20.2d + (0x1268e4#64 , 0x4cdf7c79#32), -- ld1 {v25.2d}, [x3], #16 + (0x1268e8#64 , 0x6e184318#32), -- ext v24.16b, v24.16b, v24.16b, #8 + (0x1268ec#64 , 0x6e034045#32), -- ext v5.16b, v2.16b, v3.16b, #8 + (0x1268f0#64 , 0x6e024026#32), -- ext v6.16b, v1.16b, v2.16b, #8 + (0x1268f4#64 , 0x4ef88463#32), -- add v3.2d, v3.2d, v24.2d + (0x1268f8#64 , 0xcec082b4#32), -- sha512su0 v20.2d, v21.2d + (0x1268fc#64 , 0x6e114207#32), -- ext v7.16b, v16.16b, v17.16b, #8 + (0x126900#64 , 0xce6680a3#32), -- sha512h q3, q5, v6.2d + (0x126904#64 , 0xce678a74#32), -- sha512su1 v20.2d, v19.2d, v7.2d + (0x126908#64 , 0x4ee38424#32), -- add v4.2d, v1.2d, v3.2d + (0x12690c#64 , 0xce608423#32), -- sha512h2 q3, q1, v0.2d + (0x126910#64 , 0x4ef58739#32), -- add v25.2d, v25.2d, v21.2d + (0x126914#64 , 0x4cdf7c78#32), -- ld1 {v24.2d}, [x3], #16 + (0x126918#64 , 0x6e194339#32), -- ext v25.16b, v25.16b, v25.16b, #8 + (0x12691c#64 , 0x6e024085#32), -- ext v5.16b, v4.16b, v2.16b, #8 + (0x126920#64 , 0x6e044006#32), -- ext v6.16b, v0.16b, v4.16b, #8 + (0x126924#64 , 0x4ef98442#32), -- add v2.2d, v2.2d, v25.2d + (0x126928#64 , 0xcec082d5#32), -- sha512su0 v21.2d, v22.2d + (0x12692c#64 , 0x6e124227#32), -- ext v7.16b, v17.16b, v18.16b, #8 + (0x126930#64 , 0xce6680a2#32), -- sha512h q2, q5, v6.2d + (0x126934#64 , 0xce678a95#32), -- sha512su1 v21.2d, v20.2d, v7.2d + (0x126938#64 , 0x4ee28401#32), -- add v1.2d, v0.2d, v2.2d + (0x12693c#64 , 0xce638402#32), -- sha512h2 q2, q0, v3.2d + (0x126940#64 , 0x4ef68718#32), -- add v24.2d, v24.2d, v22.2d + (0x126944#64 , 0x4cdf7c79#32), -- ld1 {v25.2d}, [x3], #16 + (0x126948#64 , 0x6e184318#32), -- ext v24.16b, v24.16b, v24.16b, #8 + (0x12694c#64 , 0x6e044025#32), -- ext v5.16b, v1.16b, v4.16b, #8 + (0x126950#64 , 0x6e014066#32), -- ext v6.16b, v3.16b, v1.16b, #8 + (0x126954#64 , 0x4ef88484#32), -- add v4.2d, v4.2d, v24.2d + (0x126958#64 , 0xcec082f6#32), -- sha512su0 v22.2d, v23.2d + (0x12695c#64 , 0x6e134247#32), -- ext v7.16b, v18.16b, v19.16b, #8 + (0x126960#64 , 0xce6680a4#32), -- sha512h q4, q5, v6.2d + (0x126964#64 , 0xce678ab6#32), -- sha512su1 v22.2d, v21.2d, v7.2d + (0x126968#64 , 0x4ee48460#32), -- add v0.2d, v3.2d, v4.2d + (0x12696c#64 , 0xce628464#32), -- sha512h2 q4, q3, v2.2d + (0x126970#64 , 0x4ef78739#32), -- add v25.2d, v25.2d, v23.2d + (0x126974#64 , 0x4cdf7c78#32), -- ld1 {v24.2d}, [x3], #16 + (0x126978#64 , 0x6e194339#32), -- ext v25.16b, v25.16b, v25.16b, #8 + (0x12697c#64 , 0x6e014005#32), -- ext v5.16b, v0.16b, v1.16b, #8 + (0x126980#64 , 0x6e004046#32), -- ext v6.16b, v2.16b, v0.16b, #8 + (0x126984#64 , 0x4ef98421#32), -- add v1.2d, v1.2d, v25.2d + (0x126988#64 , 0xcec08217#32), -- sha512su0 v23.2d, v16.2d + (0x12698c#64 , 0x6e144267#32), -- ext v7.16b, v19.16b, v20.16b, #8 + (0x126990#64 , 0xce6680a1#32), -- sha512h q1, q5, v6.2d + (0x126994#64 , 0xce678ad7#32), -- sha512su1 v23.2d, v22.2d, v7.2d + (0x126998#64 , 0x4ee18443#32), -- add v3.2d, v2.2d, v1.2d + (0x12699c#64 , 0xce648441#32), -- sha512h2 q1, q2, v4.2d + (0x1269a0#64 , 0x4ef08718#32), -- add v24.2d, v24.2d, v16.2d + (0x1269a4#64 , 0x4cdf7c79#32), -- ld1 {v25.2d}, [x3], #16 + (0x1269a8#64 , 0x6e184318#32), -- ext v24.16b, v24.16b, v24.16b, #8 + (0x1269ac#64 , 0x6e004065#32), -- ext v5.16b, v3.16b, v0.16b, #8 + (0x1269b0#64 , 0x6e034086#32), -- ext v6.16b, v4.16b, v3.16b, #8 + (0x1269b4#64 , 0x4ef88400#32), -- add v0.2d, v0.2d, v24.2d + (0x1269b8#64 , 0xcec08230#32), -- sha512su0 v16.2d, v17.2d + (0x1269bc#64 , 0x6e154287#32), -- ext v7.16b, v20.16b, v21.16b, #8 + (0x1269c0#64 , 0xce6680a0#32), -- sha512h q0, q5, v6.2d + (0x1269c4#64 , 0xce678af0#32), -- sha512su1 v16.2d, v23.2d, v7.2d + (0x1269c8#64 , 0x4ee08482#32), -- add v2.2d, v4.2d, v0.2d + (0x1269cc#64 , 0xce618480#32), -- sha512h2 q0, q4, v1.2d + (0x1269d0#64 , 0x4ef18739#32), -- add v25.2d, v25.2d, v17.2d + (0x1269d4#64 , 0x4cdf7c78#32), -- ld1 {v24.2d}, [x3], #16 + (0x1269d8#64 , 0x6e194339#32), -- ext v25.16b, v25.16b, v25.16b, #8 + (0x1269dc#64 , 0x6e034045#32), -- ext v5.16b, v2.16b, v3.16b, #8 + (0x1269e0#64 , 0x6e024026#32), -- ext v6.16b, v1.16b, v2.16b, #8 + (0x1269e4#64 , 0x4ef98463#32), -- add v3.2d, v3.2d, v25.2d + (0x1269e8#64 , 0xcec08251#32), -- sha512su0 v17.2d, v18.2d + (0x1269ec#64 , 0x6e1642a7#32), -- ext v7.16b, v21.16b, v22.16b, #8 + (0x1269f0#64 , 0xce6680a3#32), -- sha512h q3, q5, v6.2d + (0x1269f4#64 , 0xce678a11#32), -- sha512su1 v17.2d, v16.2d, v7.2d + (0x1269f8#64 , 0x4ee38424#32), -- add v4.2d, v1.2d, v3.2d + (0x1269fc#64 , 0xce608423#32), -- sha512h2 q3, q1, v0.2d + (0x126a00#64 , 0x4ef28718#32), -- add v24.2d, v24.2d, v18.2d + (0x126a04#64 , 0x4cdf7c79#32), -- ld1 {v25.2d}, [x3], #16 + (0x126a08#64 , 0x6e184318#32), -- ext v24.16b, v24.16b, v24.16b, #8 + (0x126a0c#64 , 0x6e024085#32), -- ext v5.16b, v4.16b, v2.16b, #8 + (0x126a10#64 , 0x6e044006#32), -- ext v6.16b, v0.16b, v4.16b, #8 + (0x126a14#64 , 0x4ef88442#32), -- add v2.2d, v2.2d, v24.2d + (0x126a18#64 , 0xcec08272#32), -- sha512su0 v18.2d, v19.2d + (0x126a1c#64 , 0x6e1742c7#32), -- ext v7.16b, v22.16b, v23.16b, #8 + (0x126a20#64 , 0xce6680a2#32), -- sha512h q2, q5, v6.2d + (0x126a24#64 , 0xce678a32#32), -- sha512su1 v18.2d, v17.2d, v7.2d + (0x126a28#64 , 0x4ee28401#32), -- add v1.2d, v0.2d, v2.2d + (0x126a2c#64 , 0xce638402#32), -- sha512h2 q2, q0, v3.2d + (0x126a30#64 , 0x4ef38739#32), -- add v25.2d, v25.2d, v19.2d + (0x126a34#64 , 0x4cdf7c78#32), -- ld1 {v24.2d}, [x3], #16 + (0x126a38#64 , 0x6e194339#32), -- ext v25.16b, v25.16b, v25.16b, #8 + (0x126a3c#64 , 0x6e044025#32), -- ext v5.16b, v1.16b, v4.16b, #8 + (0x126a40#64 , 0x6e014066#32), -- ext v6.16b, v3.16b, v1.16b, #8 + (0x126a44#64 , 0x4ef98484#32), -- add v4.2d, v4.2d, v25.2d + (0x126a48#64 , 0xcec08293#32), -- sha512su0 v19.2d, v20.2d + (0x126a4c#64 , 0x6e1042e7#32), -- ext v7.16b, v23.16b, v16.16b, #8 + (0x126a50#64 , 0xce6680a4#32), -- sha512h q4, q5, v6.2d + (0x126a54#64 , 0xce678a53#32), -- sha512su1 v19.2d, v18.2d, v7.2d + (0x126a58#64 , 0x4ee48460#32), -- add v0.2d, v3.2d, v4.2d + (0x126a5c#64 , 0xce628464#32), -- sha512h2 q4, q3, v2.2d + (0x126a60#64 , 0x4ef48718#32), -- add v24.2d, v24.2d, v20.2d + (0x126a64#64 , 0x4cdf7c79#32), -- ld1 {v25.2d}, [x3], #16 + (0x126a68#64 , 0x6e184318#32), -- ext v24.16b, v24.16b, v24.16b, #8 + (0x126a6c#64 , 0x6e014005#32), -- ext v5.16b, v0.16b, v1.16b, #8 + (0x126a70#64 , 0x6e004046#32), -- ext v6.16b, v2.16b, v0.16b, #8 + (0x126a74#64 , 0x4ef88421#32), -- add v1.2d, v1.2d, v24.2d + (0x126a78#64 , 0xcec082b4#32), -- sha512su0 v20.2d, v21.2d + (0x126a7c#64 , 0x6e114207#32), -- ext v7.16b, v16.16b, v17.16b, #8 + (0x126a80#64 , 0xce6680a1#32), -- sha512h q1, q5, v6.2d + (0x126a84#64 , 0xce678a74#32), -- sha512su1 v20.2d, v19.2d, v7.2d + (0x126a88#64 , 0x4ee18443#32), -- add v3.2d, v2.2d, v1.2d + (0x126a8c#64 , 0xce648441#32), -- sha512h2 q1, q2, v4.2d + (0x126a90#64 , 0x4ef58739#32), -- add v25.2d, v25.2d, v21.2d + (0x126a94#64 , 0x4cdf7c78#32), -- ld1 {v24.2d}, [x3], #16 + (0x126a98#64 , 0x6e194339#32), -- ext v25.16b, v25.16b, v25.16b, #8 + (0x126a9c#64 , 0x6e004065#32), -- ext v5.16b, v3.16b, v0.16b, #8 + (0x126aa0#64 , 0x6e034086#32), -- ext v6.16b, v4.16b, v3.16b, #8 + (0x126aa4#64 , 0x4ef98400#32), -- add v0.2d, v0.2d, v25.2d + (0x126aa8#64 , 0xcec082d5#32), -- sha512su0 v21.2d, v22.2d + (0x126aac#64 , 0x6e124227#32), -- ext v7.16b, v17.16b, v18.16b, #8 + (0x126ab0#64 , 0xce6680a0#32), -- sha512h q0, q5, v6.2d + (0x126ab4#64 , 0xce678a95#32), -- sha512su1 v21.2d, v20.2d, v7.2d + (0x126ab8#64 , 0x4ee08482#32), -- add v2.2d, v4.2d, v0.2d + (0x126abc#64 , 0xce618480#32), -- sha512h2 q0, q4, v1.2d + (0x126ac0#64 , 0x4ef68718#32), -- add v24.2d, v24.2d, v22.2d + (0x126ac4#64 , 0x4cdf7c79#32), -- ld1 {v25.2d}, [x3], #16 + (0x126ac8#64 , 0x6e184318#32), -- ext v24.16b, v24.16b, v24.16b, #8 + (0x126acc#64 , 0x6e034045#32), -- ext v5.16b, v2.16b, v3.16b, #8 + (0x126ad0#64 , 0x6e024026#32), -- ext v6.16b, v1.16b, v2.16b, #8 + (0x126ad4#64 , 0x4ef88463#32), -- add v3.2d, v3.2d, v24.2d + (0x126ad8#64 , 0xcec082f6#32), -- sha512su0 v22.2d, v23.2d + (0x126adc#64 , 0x6e134247#32), -- ext v7.16b, v18.16b, v19.16b, #8 + (0x126ae0#64 , 0xce6680a3#32), -- sha512h q3, q5, v6.2d + (0x126ae4#64 , 0xce678ab6#32), -- sha512su1 v22.2d, v21.2d, v7.2d + (0x126ae8#64 , 0x4ee38424#32), -- add v4.2d, v1.2d, v3.2d + (0x126aec#64 , 0xce608423#32), -- sha512h2 q3, q1, v0.2d + (0x126af0#64 , 0x4ef78739#32), -- add v25.2d, v25.2d, v23.2d + (0x126af4#64 , 0x4cdf7c78#32), -- ld1 {v24.2d}, [x3], #16 + (0x126af8#64 , 0x6e194339#32), -- ext v25.16b, v25.16b, v25.16b, #8 + (0x126afc#64 , 0x6e024085#32), -- ext v5.16b, v4.16b, v2.16b, #8 + (0x126b00#64 , 0x6e044006#32), -- ext v6.16b, v0.16b, v4.16b, #8 + (0x126b04#64 , 0x4ef98442#32), -- add v2.2d, v2.2d, v25.2d + (0x126b08#64 , 0xcec08217#32), -- sha512su0 v23.2d, v16.2d + (0x126b0c#64 , 0x6e144267#32), -- ext v7.16b, v19.16b, v20.16b, #8 + (0x126b10#64 , 0xce6680a2#32), -- sha512h q2, q5, v6.2d + (0x126b14#64 , 0xce678ad7#32), -- sha512su1 v23.2d, v22.2d, v7.2d + (0x126b18#64 , 0x4ee28401#32), -- add v1.2d, v0.2d, v2.2d + (0x126b1c#64 , 0xce638402#32), -- sha512h2 q2, q0, v3.2d + (0x126b20#64 , 0x4cdf7c79#32), -- ld1 {v25.2d}, [x3], #16 + (0x126b24#64 , 0x4ef08718#32), -- add v24.2d, v24.2d, v16.2d + (0x126b28#64 , 0x4cdf7030#32), -- ld1 {v16.16b}, [x1], #16 + (0x126b2c#64 , 0x6e184318#32), -- ext v24.16b, v24.16b, v24.16b, #8 + (0x126b30#64 , 0x6e044025#32), -- ext v5.16b, v1.16b, v4.16b, #8 + (0x126b34#64 , 0x6e014066#32), -- ext v6.16b, v3.16b, v1.16b, #8 + (0x126b38#64 , 0x4ef88484#32), -- add v4.2d, v4.2d, v24.2d + (0x126b3c#64 , 0xce6680a4#32), -- sha512h q4, q5, v6.2d + (0x126b40#64 , 0x4e200a10#32), -- rev64 v16.16b, v16.16b + (0x126b44#64 , 0x4ee48460#32), -- add v0.2d, v3.2d, v4.2d + (0x126b48#64 , 0xce628464#32), -- sha512h2 q4, q3, v2.2d + (0x126b4c#64 , 0x4cdf7c78#32), -- ld1 {v24.2d}, [x3], #16 + (0x126b50#64 , 0x4ef18739#32), -- add v25.2d, v25.2d, v17.2d + (0x126b54#64 , 0x4cdf7031#32), -- ld1 {v17.16b}, [x1], #16 + (0x126b58#64 , 0x6e194339#32), -- ext v25.16b, v25.16b, v25.16b, #8 + (0x126b5c#64 , 0x6e014005#32), -- ext v5.16b, v0.16b, v1.16b, #8 + (0x126b60#64 , 0x6e004046#32), -- ext v6.16b, v2.16b, v0.16b, #8 + (0x126b64#64 , 0x4ef98421#32), -- add v1.2d, v1.2d, v25.2d + (0x126b68#64 , 0xce6680a1#32), -- sha512h q1, q5, v6.2d + (0x126b6c#64 , 0x4e200a31#32), -- rev64 v17.16b, v17.16b + (0x126b70#64 , 0x4ee18443#32), -- add v3.2d, v2.2d, v1.2d + (0x126b74#64 , 0xce648441#32), -- sha512h2 q1, q2, v4.2d + (0x126b78#64 , 0x4cdf7c79#32), -- ld1 {v25.2d}, [x3], #16 + (0x126b7c#64 , 0x4ef28718#32), -- add v24.2d, v24.2d, v18.2d + (0x126b80#64 , 0x4cdf7032#32), -- ld1 {v18.16b}, [x1], #16 + (0x126b84#64 , 0x6e184318#32), -- ext v24.16b, v24.16b, v24.16b, #8 + (0x126b88#64 , 0x6e004065#32), -- ext v5.16b, v3.16b, v0.16b, #8 + (0x126b8c#64 , 0x6e034086#32), -- ext v6.16b, v4.16b, v3.16b, #8 + (0x126b90#64 , 0x4ef88400#32), -- add v0.2d, v0.2d, v24.2d + (0x126b94#64 , 0xce6680a0#32), -- sha512h q0, q5, v6.2d + (0x126b98#64 , 0x4e200a52#32), -- rev64 v18.16b, v18.16b + (0x126b9c#64 , 0x4ee08482#32), -- add v2.2d, v4.2d, v0.2d + (0x126ba0#64 , 0xce618480#32), -- sha512h2 q0, q4, v1.2d + (0x126ba4#64 , 0x4cdf7c78#32), -- ld1 {v24.2d}, [x3], #16 + (0x126ba8#64 , 0x4ef38739#32), -- add v25.2d, v25.2d, v19.2d + (0x126bac#64 , 0x4cdf7033#32), -- ld1 {v19.16b}, [x1], #16 + (0x126bb0#64 , 0x6e194339#32), -- ext v25.16b, v25.16b, v25.16b, #8 + (0x126bb4#64 , 0x6e034045#32), -- ext v5.16b, v2.16b, v3.16b, #8 + (0x126bb8#64 , 0x6e024026#32), -- ext v6.16b, v1.16b, v2.16b, #8 + (0x126bbc#64 , 0x4ef98463#32), -- add v3.2d, v3.2d, v25.2d + (0x126bc0#64 , 0xce6680a3#32), -- sha512h q3, q5, v6.2d + (0x126bc4#64 , 0x4e200a73#32), -- rev64 v19.16b, v19.16b + (0x126bc8#64 , 0x4ee38424#32), -- add v4.2d, v1.2d, v3.2d + (0x126bcc#64 , 0xce608423#32), -- sha512h2 q3, q1, v0.2d + (0x126bd0#64 , 0x4cdf7c79#32), -- ld1 {v25.2d}, [x3], #16 + (0x126bd4#64 , 0x4ef48718#32), -- add v24.2d, v24.2d, v20.2d + (0x126bd8#64 , 0x4cdf7034#32), -- ld1 {v20.16b}, [x1], #16 + (0x126bdc#64 , 0x6e184318#32), -- ext v24.16b, v24.16b, v24.16b, #8 + (0x126be0#64 , 0x6e024085#32), -- ext v5.16b, v4.16b, v2.16b, #8 + (0x126be4#64 , 0x6e044006#32), -- ext v6.16b, v0.16b, v4.16b, #8 + (0x126be8#64 , 0x4ef88442#32), -- add v2.2d, v2.2d, v24.2d + (0x126bec#64 , 0xce6680a2#32), -- sha512h q2, q5, v6.2d + (0x126bf0#64 , 0x4e200a94#32), -- rev64 v20.16b, v20.16b + (0x126bf4#64 , 0x4ee28401#32), -- add v1.2d, v0.2d, v2.2d + (0x126bf8#64 , 0xce638402#32), -- sha512h2 q2, q0, v3.2d + (0x126bfc#64 , 0x4cdf7c78#32), -- ld1 {v24.2d}, [x3], #16 + (0x126c00#64 , 0x4ef58739#32), -- add v25.2d, v25.2d, v21.2d + (0x126c04#64 , 0x4cdf7035#32), -- ld1 {v21.16b}, [x1], #16 + (0x126c08#64 , 0x6e194339#32), -- ext v25.16b, v25.16b, v25.16b, #8 + (0x126c0c#64 , 0x6e044025#32), -- ext v5.16b, v1.16b, v4.16b, #8 + (0x126c10#64 , 0x6e014066#32), -- ext v6.16b, v3.16b, v1.16b, #8 + (0x126c14#64 , 0x4ef98484#32), -- add v4.2d, v4.2d, v25.2d + (0x126c18#64 , 0xce6680a4#32), -- sha512h q4, q5, v6.2d + (0x126c1c#64 , 0x4e200ab5#32), -- rev64 v21.16b, v21.16b + (0x126c20#64 , 0x4ee48460#32), -- add v0.2d, v3.2d, v4.2d + (0x126c24#64 , 0xce628464#32), -- sha512h2 q4, q3, v2.2d + (0x126c28#64 , 0x4cdf7c79#32), -- ld1 {v25.2d}, [x3], #16 + (0x126c2c#64 , 0x4ef68718#32), -- add v24.2d, v24.2d, v22.2d + (0x126c30#64 , 0x4cdf7036#32), -- ld1 {v22.16b}, [x1], #16 + (0x126c34#64 , 0x6e184318#32), -- ext v24.16b, v24.16b, v24.16b, #8 + (0x126c38#64 , 0x6e014005#32), -- ext v5.16b, v0.16b, v1.16b, #8 + (0x126c3c#64 , 0x6e004046#32), -- ext v6.16b, v2.16b, v0.16b, #8 + (0x126c40#64 , 0x4ef88421#32), -- add v1.2d, v1.2d, v24.2d + (0x126c44#64 , 0xce6680a1#32), -- sha512h q1, q5, v6.2d + (0x126c48#64 , 0x4e200ad6#32), -- rev64 v22.16b, v22.16b + (0x126c4c#64 , 0x4ee18443#32), -- add v3.2d, v2.2d, v1.2d + (0x126c50#64 , 0xce648441#32), -- sha512h2 q1, q2, v4.2d + (0x126c54#64 , 0xd10a0063#32), -- sub x3, x3, #0x280 + (0x126c58#64 , 0x4ef78739#32), -- add v25.2d, v25.2d, v23.2d + (0x126c5c#64 , 0x4cdf7037#32), -- ld1 {v23.16b}, [x1], #16 + (0x126c60#64 , 0x6e194339#32), -- ext v25.16b, v25.16b, v25.16b, #8 + (0x126c64#64 , 0x6e004065#32), -- ext v5.16b, v3.16b, v0.16b, #8 + (0x126c68#64 , 0x6e034086#32), -- ext v6.16b, v4.16b, v3.16b, #8 + (0x126c6c#64 , 0x4ef98400#32), -- add v0.2d, v0.2d, v25.2d + (0x126c70#64 , 0xce6680a0#32), -- sha512h q0, q5, v6.2d + (0x126c74#64 , 0x4e200af7#32), -- rev64 v23.16b, v23.16b + (0x126c78#64 , 0x4ee08482#32), -- add v2.2d, v4.2d, v0.2d + (0x126c7c#64 , 0xce618480#32), -- sha512h2 q0, q4, v1.2d + (0x126c80#64 , 0x4efa8400#32), -- add v0.2d, v0.2d, v26.2d + (0x126c84#64 , 0x4efb8421#32), -- add v1.2d, v1.2d, v27.2d + (0x126c88#64 , 0x4efc8442#32), -- add v2.2d, v2.2d, v28.2d + (0x126c8c#64 , 0x4efd8463#32), -- add v3.2d, v3.2d, v29.2d + (0x126c90#64 , 0xb5ffc382#32), -- cbnz x2, 126500 + (0x126c94#64 , 0x4c002c00#32), -- st1 {v0.2d-v3.2d}, [x0] + (0x126c98#64 , 0xf84107fd#32), -- ldr x29, [sp], #16 + (0x126c9c#64 , 0xd65f03c0#32)].toAssocList + +theorem fetch_inst_from_assoclist + {address: BitVec 64} {program : Std.AssocList (BitVec 64) (BitVec 32)} + (h_program : s.program = program.find?) : + fetch_inst address s = program.find? address := by + unfold fetch_inst read_store + simp_all! + +theorem sha512_block_armv8_new_program (s : ArmState) + (h_s_ok : read_err s = StateError.None) + (h_sp_aligned : CheckSPAlignment s = true) + (h_pc : read_pc s = 0x1264c0#64) + (h_program : s.program = sha512_program.find?) + (h_s' : s' = run 506 s) : + read_err s' = StateError.None := by + -- (FIXME) simp_all below fails with a nested error: + -- maximum recursion depth has been reached (use `set_option maxRecDepth ` to increase limit) + -- simp_all + -- (WORKAROUND) I manually do subst and simp at individual hypotheses. + subst s' + simp at h_s_ok h_pc + unfold run + simp [stepi, h_pc] + rw [fetch_inst_from_assoclist h_program] + -- (FIXME) Wish this output from simp/ground wasn't so noisy. + simp (config := {ground := true}) only + simp [exec_inst, *] + -- (FIXME) At this point, we have an if in the goal whose condition + -- is comprised of ground terms. However, simp/ground below fails + -- with a max. recursion depth error again. + -- simp (config := {ground := true}) only + -- (WORKAROUND) I manually split and attempt to make progress. + split + · rename_i h + simp (config := {ground := true}) at h + · rename_i h; simp (config := {ground := true}) at h + unfold run + simp [stepi] + rw [fetch_inst_from_assoclist h_program] + conv => + pattern find? .. + simp (config := {ground := true}) only + simp [*] + conv => + pattern decode_raw_inst .. + simp (config := {ground := true}) only + simp only + simp [exec_inst, *] + + unfold run + simp [stepi, h_pc] + sorry + +end SHA512_proof