| 20ff71d | Andres Erbsen | 10 October 2021, 19:29:49 UTC | Update coq.yml | 10 October 2021, 19:29:49 UTC |
| 16c0c9b | Andres Erbsen | 10 October 2021, 16:12:39 UTC | Update coq.yml | 10 October 2021, 16:12:39 UTC |
| 0d2d908 | Frank Denis | 09 October 2021, 18:22:38 UTC | Zig: use @import("builtin") instead of the deprecated reexport Fixes #1029 | 10 October 2021, 00:30:53 UTC |
| 9f2514e | Jason Gross | 09 October 2021, 03:42:21 UTC | Finish most of the proof on init_symbolic_state | 09 October 2021, 18:06:40 UTC |
| cb40372 | Jason Gross | 09 October 2021, 02:57:55 UTC | Add lemmas about dag_gensym_n | 09 October 2021, 18:06:40 UTC |
| dd63ba3 | Jason Gross | 09 October 2021, 02:20:20 UTC | Rearrange code a bit | 09 October 2021, 18:06:40 UTC |
| 42eeb35 | Jason Gross | 09 October 2021, 02:08:26 UTC | Prove gensym part of asm equivalence checker | 09 October 2021, 18:06:40 UTC |
| 44771e0 | Jason Gross | 09 October 2021, 01:35:27 UTC | Remove foldmap from indexof | 09 October 2021, 01:35:34 UTC |
| a67c2b5 | Jason Gross | 09 October 2021, 00:22:06 UTC | Add indexof_None, indexof_app | 09 October 2021, 00:22:21 UTC |
| 3daf3e7 | Andres Erbsen | 08 October 2021, 23:01:58 UTC | src/Assembly: remove names from todos | 08 October 2021, 23:01:58 UTC |
| e21cfd6 | Jason Gross | 08 October 2021, 21:10:04 UTC | Add reflect<->BoolSpec | 08 October 2021, 21:10:04 UTC |
| 85b1261 | Jason Gross | 05 October 2021, 23:44:18 UTC | Remove probably incorrect comment | 07 October 2021, 22:22:47 UTC |
| f7393ae | Jason Gross | 05 October 2021, 23:43:20 UTC | Remove dead code | 07 October 2021, 22:22:47 UTC |
| 47e535d | Jason Gross | 05 October 2021, 23:32:59 UTC | Make explicit that asm proofs depend on bedrock2 | 07 October 2021, 22:22:47 UTC |
| 639757d | Jason Gross | 05 October 2021, 23:25:33 UTC | WIP | 07 October 2021, 22:22:47 UTC |
| 708998d | Jason Gross | 05 October 2021, 23:18:53 UTC | Mostly finish proving build_inputs | 07 October 2021, 22:22:47 UTC |
| 09683e1 | Jason Gross | 05 October 2021, 21:34:04 UTC | WIP | 07 October 2021, 22:22:47 UTC |
| 985c603 | Jason Gross | 05 October 2021, 18:26:20 UTC | Flip the sense of name mismatch flag Rename `--asm-ignore-unique-name-mismatch` to `--asm-error-on-unique-name-mismatch`, flipping the sense of the flag in the process. | 07 October 2021, 22:22:47 UTC |
| 1a4e8db | Jason Gross | 05 October 2021, 05:37:43 UTC | A bit more factoring of proofs | 07 October 2021, 22:22:47 UTC |
| 0211e0d | Jason Gross | 05 October 2021, 05:15:31 UTC | Revert "Refactor check_equivalence a bit more" This reverts commit 1e57702edd8bfe49702681560e99510ffb3a5123. | 07 October 2021, 22:22:47 UTC |
| ce7f016 | Jason Gross | 05 October 2021, 05:08:01 UTC | Refactor check_equivalence a bit more So that most of it happens inside the symex monad | 07 October 2021, 22:22:47 UTC |
| e777223 | Jason Gross | 05 October 2021, 00:55:33 UTC | Remove dead code | 07 October 2021, 22:22:47 UTC |
| 7ed7db8 | Jason Gross | 05 October 2021, 00:55:05 UTC | Refactor symex_asm_func | 07 October 2021, 22:22:47 UTC |
| 0366eab | Jason Gross | 04 October 2021, 23:05:42 UTC | Some WIP on specing build_inputs | 07 October 2021, 22:22:47 UTC |
| 05f77e5 | Jason Gross | 04 October 2021, 20:42:21 UTC | Merge gensym state with dag | 07 October 2021, 22:22:47 UTC |
| ecaf006 | Jason Gross | 04 October 2021, 18:50:18 UTC | Make default assembly stack size 0, as per email suggestion from Joel | 07 October 2021, 22:22:47 UTC |
| 054fa29 | Jason Gross | 30 September 2021, 23:00:43 UTC | Use `--asm-ignore-unique-name-mismatch` | 07 October 2021, 22:22:47 UTC |
| 0c3adc3 | Jason Gross | 29 September 2021, 22:56:08 UTC | Fix import qualification | 07 October 2021, 22:22:47 UTC |
| 3036ee7 | Jason Gross | 28 September 2021, 22:49:54 UTC | Factor utility lemmas from x86 out of asm files | 07 October 2021, 22:22:47 UTC |
| a5e1c2f | Jason Gross | 28 September 2021, 21:46:56 UTC | Compat with Coq 8.11 | 07 October 2021, 22:22:47 UTC |
| d975e93 | Jason Gross | 28 September 2021, 20:32:31 UTC | Also clean up after the tests in the clean target | 07 October 2021, 22:22:47 UTC |
| 7e7ec28 | Jason Gross | 28 September 2021, 20:28:41 UTC | Improve amd64 output tests Now, they can be run in parallel, and are integrated into the makefile. Also, with the updated rebase, all of them pass. | 07 October 2021, 22:22:47 UTC |
| e7163d0 | Jason Gross | 28 September 2021, 17:50:02 UTC | Some imports changed when rebasing | 07 October 2021, 22:22:47 UTC |
| 5607cbd | Jason Gross | 28 September 2021, 02:07:05 UTC | Add amd64 test to CI | 07 October 2021, 22:22:47 UTC |
| 83f8a68 | Jason Gross | 14 September 2021, 23:42:38 UTC | Remove now duplicated lemmas | 07 October 2021, 22:22:47 UTC |
| bf7031d | Andres Erbsen | 18 August 2021, 14:09:05 UTC | Asssembly.Symbolic: prove last admits | 07 October 2021, 22:22:47 UTC |
| 11a475d | Andres Erbsen | 18 August 2021, 12:11:46 UTC | cleanup (repr, reveals) | 07 October 2021, 22:22:47 UTC |
| f37616d | ChuyueSun | 18 August 2021, 03:19:59 UTC | clean up | 07 October 2021, 22:22:47 UTC |
| a6bf252 | Andres Erbsen | 18 August 2021, 02:41:25 UTC | verify bound_expr | 07 October 2021, 22:22:47 UTC |
| e0e0e78 | Andres Erbsen | 17 August 2021, 21:31:25 UTC | Assembly.Symbolic: refactor and prove some rewrite rules | 07 October 2021, 22:22:47 UTC |
| c6f0757 | Andres Erbsen | 17 August 2021, 15:24:20 UTC | flatten_associative_ok | 07 October 2021, 22:22:47 UTC |
| bcac2e4 | Andres Erbsen | 17 August 2021, 14:19:04 UTC | fix and prove slice_set_slice | 07 October 2021, 22:22:47 UTC |
| 5de97f9 | Andres Erbsen | 17 August 2021, 13:28:27 UTC | SymexLines_R | 07 October 2021, 22:22:47 UTC |
| cffc76e | Andres Erbsen | 17 August 2021, 12:41:58 UTC | work around Qed looping (cbn bind -> rewrite) | 07 October 2021, 22:22:47 UTC |
| 087348e | Andres Erbsen | 17 August 2021, 02:23:13 UTC | memory symex proofs | 07 October 2021, 22:22:47 UTC |
| 578485d | ChuyueSun | 17 August 2021, 02:20:36 UTC | eval_bound_expr' unfinished | 07 October 2021, 22:22:47 UTC |
| 672cbd3 | ChuyueSun | 16 August 2021, 19:58:32 UTC | add_small_ok add_smallbyte_ok | 07 October 2021, 22:22:47 UTC |
| 5a1f7f1 | Andres Erbsen | 15 August 2021, 21:57:05 UTC | Assembly.SymbolicProofs: operation_size_cases | 07 October 2021, 22:22:47 UTC |
| d4f7080 | Andres Erbsen | 15 August 2021, 19:00:23 UTC | Assembly: special-case ret, step through remaining instructions | 07 October 2021, 22:22:47 UTC |
| 0edc1ce | Andres Erbsen | 15 August 2021, 13:37:05 UTC | new test from Joel | 07 October 2021, 22:22:47 UTC |
| 1553400 | Andres Erbsen | 15 August 2021, 04:50:16 UTC | Assembly.Semantics: use Z | 07 October 2021, 22:22:47 UTC |
| 31b9487 | Andres Erbsen | 15 August 2021, 01:22:06 UTC | SymbolicProof.Address_R: break out cases | 07 October 2021, 22:22:47 UTC |
| 7ffb9b6 | Andres Erbsen | 15 August 2021, 00:07:45 UTC | SymbolicProofs: reg bound invariant | 07 October 2021, 22:22:47 UTC |
| f8ac181 | Andres Erbsen | 14 August 2021, 22:15:14 UTC | Assembly.Symbolic: bzhi clears OF | 07 October 2021, 22:22:47 UTC |
| fd2f9c9 | Andres Erbsen | 14 August 2021, 16:46:17 UTC | refactor SymbolicProofs, start at shift amount truncation | 07 October 2021, 22:22:47 UTC |
| 90f0195 | Andres Erbsen | 12 August 2021, 19:58:11 UTC | SymbolicProofs: and case | 07 October 2021, 22:22:47 UTC |
| bc8ab71 | Andres Erbsen | 12 August 2021, 19:43:52 UTC | Tuple__nth_default_to_list | 07 October 2021, 22:22:47 UTC |
| fa5a0bc | Andres Erbsen | 12 August 2021, 19:15:46 UTC | Assembly.Symbolic: fix const parsing width | 07 October 2021, 22:22:47 UTC |
| 976294b | Andres Erbsen | 12 August 2021, 00:25:01 UTC | fixup (break out sub case) | 07 October 2021, 22:22:47 UTC |
| 52db865 | ChuyueSun | 11 August 2021, 22:16:31 UTC | typo | 07 October 2021, 22:22:47 UTC |
| ee45c5b | ChuyueSun | 11 August 2021, 22:06:25 UTC | delete rcr | 07 October 2021, 22:22:47 UTC |
| 9c30c6a | Andres Erbsen | 11 August 2021, 19:57:06 UTC | break out sub case | 07 October 2021, 22:22:47 UTC |
| 9226375 | Andres Erbsen | 11 August 2021, 18:16:12 UTC | subborrowZ | 07 October 2021, 22:22:47 UTC |
| 8313486 | Andres Erbsen | 11 August 2021, 15:44:12 UTC | indexof_Some, node_beq_sound | 07 October 2021, 22:22:47 UTC |
| 7a7f188 | Andres Erbsen | 11 August 2021, 15:33:05 UTC | remove rcr rule | 07 October 2021, 22:22:47 UTC |
| c5ee50a | Andres Erbsen | 11 August 2021, 15:15:02 UTC | expr_beq_spec | 07 October 2021, 22:22:47 UTC |
| 0fe34ea | Andres Erbsen | 11 August 2021, 14:48:15 UTC | kludge shr bounds Edited by Jason when rebasing: the kludge has been merged upstream, so we just remove the adjustment here. Also the adjustment to the tight upperbounds fraction has been moved into command line arguments. | 07 October 2021, 22:22:47 UTC |
| 8626f2f | Andres Erbsen | 11 August 2021, 14:27:24 UTC | fiat-amd64/gentest.py: redirect asm output to /dev/null | 07 October 2021, 22:22:47 UTC |
| 181fb2c | ChuyueSun | 11 August 2021, 07:37:41 UTC | fix truncate small proof | 07 October 2021, 22:22:47 UTC |
| 35293c4 | Andres Erbsen | 10 August 2021, 23:17:03 UTC | prove symex_ident_correct except for sbb, UNSOUND_widen_shr | 07 October 2021, 22:22:47 UTC |
| 2994c1e | ChuyueSun | 10 August 2021, 21:35:12 UTC | truncate small proof | 07 October 2021, 22:22:47 UTC |
| 75d7843 | Andres Erbsen | 10 August 2021, 16:11:48 UTC | Assembly.Symbolic: use implicit truncation, eliminate mulhuu | 07 October 2021, 22:22:47 UTC |
| 14bbae7 | Andres Erbsen | 10 August 2021, 00:45:34 UTC | generalize dag nodes from N to Z | 07 October 2021, 22:22:47 UTC |
| 2e6533c | Andres Erbsen | 09 August 2021, 19:07:52 UTC | refactor Assembly.Symbolic.simplify_expr | 07 October 2021, 22:22:47 UTC |
| 6727f61 | Andres Erbsen | 09 August 2021, 16:21:24 UTC | Assembly.Symbolic: fix inconsistent handling of nonzero/iszero | 07 October 2021, 22:22:47 UTC |
| ed7f280 | Andres Erbsen | 09 August 2021, 15:50:29 UTC | SymbolicProofs: break out all instrs | 07 October 2021, 22:22:47 UTC |
| c0aac36 | Andres Erbsen | 09 August 2021, 03:08:18 UTC | SymbolicProofs: sar, rcr | 07 October 2021, 22:22:47 UTC |
| 0a0219e | Andres Erbsen | 08 August 2021, 20:45:27 UTC | SymbolicProof: GetFlag/GetRegister, setc/seto | 07 October 2021, 22:22:47 UTC |
| 29e3630 | Andres Erbsen | 08 August 2021, 14:22:51 UTC | Assembly.SymbolicProofs: R_subsumed, R_clc | 07 October 2021, 22:22:47 UTC |
| ea86fab | Andres Erbsen | 05 August 2021, 16:23:47 UTC | Assembly.SymbolicProofs: simulation relation | 07 October 2021, 22:22:47 UTC |
| ff8a9e1 | Jason Gross | 04 August 2021, 18:52:22 UTC | Improve merge{,_node} automation in symex_ident_correct | 07 October 2021, 22:22:47 UTC |
| fd4176b | Jason Gross | 04 August 2021, 18:00:06 UTC | Massively speed up symex_ident_correct and improve warning messages `inversion` on `ErrorT` types was taking forever, so now we use a dedicated tactic. Additionally, some goals that were previously proven by my automation no longer are, so I've added some warning messages marking these cases. In particular, the automation does not currently handle nested `merge`/`merge_node` calls in a single branch, because there's no clear way to determine automatically what the subcalls should evaluate to. Perhaps the automation should be tweaked to leave over evars for unknown evaluations? | 07 October 2021, 22:22:47 UTC |
| ebbecbc | Jason Gross | 04 August 2021, 18:04:24 UTC | Add more proof using | 07 October 2021, 22:22:47 UTC |
| d7c866a | Jason Gross | 04 August 2021, 17:09:26 UTC | Fix bug introduced by 1f995e2fd080f73423a30419bccdd166d7879a5e I forgot to update `simplify_base_runtime` when updating `simplify_base_var`. Oops. | 07 October 2021, 22:22:47 UTC |
| a901249 | Jason Gross | 04 August 2021, 17:08:47 UTC | Add some Proof using annotations From '(coq-accept-proof-using-suggestion 'always) | 07 October 2021, 22:22:47 UTC |
| 047e7aa | Andres Erbsen | 03 August 2021, 22:25:31 UTC | Assembly.Semantics: rcr | 07 October 2021, 22:22:47 UTC |
| 80a28a0 | Andres Erbsen | 03 August 2021, 17:33:11 UTC | bitblast addcarry/addoverflow of bit+const; tests pass | 07 October 2021, 22:22:47 UTC |
| 8a7d254 | Andres Erbsen | 03 August 2021, 17:03:13 UTC | Assembly.Symbolic: not all commutative operations are associativite | 07 October 2021, 22:22:47 UTC |
| e34149d | Andres Erbsen | 03 August 2021, 14:02:40 UTC | Assembly.Symbolic: add small, sbb, Load byte | 07 October 2021, 22:22:47 UTC |
| e52f8fd | ChuyueSun | 02 August 2021, 23:07:53 UTC | fix | 07 October 2021, 22:22:47 UTC |
| 37c4d50 | ChuyueSun | 02 August 2021, 23:05:22 UTC | symexNormalInstruction | 07 October 2021, 22:22:47 UTC |
| 61557da | ChuyueSun | 02 August 2021, 23:04:28 UTC | symexNormalInstruction | 07 October 2021, 22:22:47 UTC |
| 16bfbb6 | Andres Erbsen | 02 August 2021, 22:26:25 UTC | fix bzhi | 07 October 2021, 22:22:47 UTC |
| 5df9130 | ChuyueSun | 02 August 2021, 22:51:17 UTC | rcr desugar | 07 October 2021, 22:22:47 UTC |
| bc55349 | Andres Erbsen | 02 August 2021, 21:58:24 UTC | more bounds | 07 October 2021, 22:22:47 UTC |
| 4f39ba0 | Andres Erbsen | 02 August 2021, 21:47:03 UTC | more rewrites | 07 October 2021, 22:22:47 UTC |
| 4cd9c90 | Andres Erbsen | 02 August 2021, 21:12:33 UTC | fold simplify_and into identity, deduplicate bzhi,sar | 07 October 2021, 22:22:47 UTC |
| bee0b80 | Andres Erbsen | 02 August 2021, 20:31:25 UTC | Assembly.Symbolic: some flag handling | 07 October 2021, 22:22:47 UTC |
| d94d9d2 | ChuyueSun | 02 August 2021, 16:39:00 UTC | add sar rewrite rule | 07 October 2021, 22:22:47 UTC |
| 42bb195 | ChuyueSun | 02 August 2021, 15:53:41 UTC | add rcr rewrite rule | 07 October 2021, 22:22:47 UTC |
