Skip to main content

Browse the archive

https://github.com/mit-plv/fiat-crypto
12 July 2022, 18:24:35 UTC
sort by:
Revision Author Date Message Commit Date
6ccc663 Jason Gross 22 March 2022, 01:49:47 UTC Fix `app_consts` Roughly the issue is that app_consts leaves over spurious x * 1 that don't get removed by subsequent passes. c.f. https://github.com/mit-plv/fiat-crypto/pull/1134#issuecomment-1074461171 22 March 2022, 14:55:46 UTC
2f04776 Jason Gross 21 March 2022, 03:40:09 UTC Slightly nicer proof 22 March 2022, 14:55:46 UTC
af54baf Jason Gross 21 March 2022, 03:29:06 UTC Fix proofs 22 March 2022, 14:55:46 UTC
b330c72 Jason Gross 21 March 2022, 02:53:24 UTC Update src/Assembly/WithBedrock/SymbolicProofs.v 22 March 2022, 14:55:46 UTC
d2426f3 Joel 21 March 2022, 01:13:02 UTC addeda print_context_and_goal (). 22 March 2022, 14:55:46 UTC
d70c006 Joel 15 March 2022, 23:02:20 UTC fix semantics of MEM in Assembly-WBedrock 22 March 2022, 14:55:46 UTC
db8eccc Jason Gross 12 March 2022, 22:02:55 UTC Finish combines_to proofs 22 March 2022, 14:55:46 UTC
5c84b22 Jason Gross 10 March 2022, 21:39:48 UTC Finish almost all of the proof of combine_consts 22 March 2022, 14:55:46 UTC
7f954bd Joel 07 March 2022, 00:05:55 UTC latest version of 'combines_to' 22 March 2022, 14:55:46 UTC
7f56f4b Joel 23 February 2022, 01:55:20 UTC adding rewrite snippet 22 March 2022, 14:55:46 UTC
9947f2a Joel 21 February 2022, 03:32:46 UTC Update src/Assembly/WithBedrock/Semantics.v Co-authored-by: Jason Gross <jasongross9@gmail.com> 22 March 2022, 14:55:46 UTC
a19a0c9 Joel 20 February 2022, 23:49:30 UTC separate cases for printing assembly 22 March 2022, 14:55:46 UTC
0f806aa Jason Gross 18 February 2022, 04:09:49 UTC Fix parsing `parse_Z_arith_strict` permits whitespace both before and after, so we were overlapping whitespace patterns. 22 March 2022, 14:55:46 UTC
a67d258 Joel 17 February 2022, 23:55:06 UTC not printing 1* in the common case 22 March 2022, 14:55:46 UTC
0f234a4 Joel 17 February 2022, 23:52:01 UTC fix renamed reg in mem-record 22 March 2022, 14:55:46 UTC
97e92ff Joel 17 February 2022, 23:51:37 UTC print mem 22 March 2022, 14:55:46 UTC
698b510 Joel 17 February 2022, 20:52:36 UTC show -> show_REG Co-authored-by: Jason Gross <jasongross9@gmail.com> 22 March 2022, 14:55:46 UTC
fcfd4e8 Joel 17 February 2022, 05:15:24 UTC fixing mul(z,r) Co-authored-by: Jason Gross <jasongross9@gmail.com> 22 March 2022, 14:55:46 UTC
66d939a Joel 17 February 2022, 04:14:32 UTC trying to mulZ z*r 22 March 2022, 14:55:46 UTC
d4d620f Joel 17 February 2022, 04:04:07 UTC fixed symtax *->, 22 March 2022, 14:55:46 UTC
6debcdd Joel 17 February 2022, 04:01:27 UTC fixed mem-parsing 22 March 2022, 14:55:46 UTC
f52401d Joel 17 February 2022, 04:00:37 UTC added comments 22 March 2022, 14:55:46 UTC
b8252e8 Joel 17 February 2022, 01:34:59 UTC new MEM-structure 22 March 2022, 14:55:46 UTC
27a3289 Joel 17 February 2022, 00:12:37 UTC showcasing new lea's [reg] (for mov reg, [rsp]) [reg +/- z ] (for mov reg, [rsp +- 0x8], spills to memory) [reg + reg] (for lea reg, [reg + reg], to calculate *2) [z * reg] (for lea reg, [2/4/8 * reg], to calculate *2, *4, *8) [reg + z * reg] (for lea reg, [reg + 2*reg] to calculat 22 March 2022, 14:55:46 UTC
a203989 Jason Gross 22 March 2022, 14:55:15 UTC Inline all functions in C, even in clang (#1165) Fixes #1164 Maybe we should do #820? 22 March 2022, 14:55:15 UTC
c148673 Jason Gross 22 March 2022, 05:35:53 UTC Preserve permissions of generated files when uploading artifacts 22 March 2022, 05:35:53 UTC
4823727 Jason Gross 21 March 2022, 20:35:56 UTC Improve errors a bit more 22 March 2022, 01:42:28 UTC
5cfb8f7 Jason Gross 21 March 2022, 17:02:02 UTC Better equivalence checking errors in the face of bad loads 22 March 2022, 01:42:28 UTC
f1ccc4b dependabot[bot] 21 March 2022, 21:41:11 UTC Bump rupicola from `60180c1` to `f5fbc4e` (#1162) 21 March 2022, 21:41:11 UTC
708ec6b Jason Gross 18 March 2022, 21:11:37 UTC Parameterize over dereference_scalar in more places This will allow us to reuse the same code to load inputs and outputs, when we want to enforce the spec of reading back and removing all of the values and then saying that the resulting symbolic memory state is empty. Some of the proofs are not quite as complete as they were before, but I hope to replace them soon with a more principled approach. 21 March 2022, 13:10:12 UTC
1da0c9d Jason Gross 20 March 2022, 21:55:36 UTC Add revert_until 21 March 2022, 13:10:12 UTC
e1a4b62 Jason Gross 20 March 2022, 19:38:26 UTC Fix for Coq 8.11 21 March 2022, 02:17:47 UTC
a6b4d85 Jason Gross 15 March 2022, 17:47:13 UTC Split off the non-bedrock-dependent part of equiv proofs This will hopefully make development a bit faster; these files are so long. 21 March 2022, 02:17:47 UTC
f7bc9e1 dependabot[bot] 18 March 2022, 21:03:47 UTC Bump rewriter from `3fc0c44` to `10c6a00` (#1160) 18 March 2022, 21:03:47 UTC
93defd9 dependabot[bot] 17 March 2022, 21:09:27 UTC Bump etc/coq-scripts from `3be05c7` to `7e68a28` (#1159) 17 March 2022, 21:09:27 UTC
37cfe57 Jason Gross 13 March 2022, 00:03:11 UTC Add some concat lemmas 13 March 2022, 00:03:11 UTC
8e98e20 Jason Gross 10 March 2022, 23:45:30 UTC Add some lemmas about Forall2 and concat 10 March 2022, 23:45:30 UTC
f43ed26 Jason Gross 10 March 2022, 23:04:05 UTC Add filter util 10 March 2022, 23:04:05 UTC
0a192c9 Jason Gross 10 March 2022, 21:42:19 UTC Add partition_eq_filter 10 March 2022, 21:42:40 UTC
a67a862 dependabot[bot] 10 March 2022, 20:52:09 UTC Bump rupicola from `aa662e1` to `60180c1` (#1155) 10 March 2022, 20:52:09 UTC
974ba64 dependabot[bot] 10 March 2022, 20:02:19 UTC Bump coqprime from `24f4101` to `de0c48a` (#1156) 10 March 2022, 20:02:19 UTC
6b0f0c6 dependabot[bot] 09 March 2022, 21:24:49 UTC Bump coqprime from `b984180` to `24f4101` (#1153) 09 March 2022, 21:24:49 UTC
b8cd846 dependabot[bot] 09 March 2022, 20:47:39 UTC Bump rupicola from `98f70f7` to `aa662e1` (#1152) 09 March 2022, 20:47:39 UTC
b6ef305 Samuel Gruetter 09 March 2022, 04:19:39 UTC bump rupicola/bedrock2 (#1151) 09 March 2022, 04:19:39 UTC
bf30d11 dependabot[bot] 04 March 2022, 20:30:57 UTC Bump actions/upload-artifact from 2.3.1 to 3 (#1149) 04 March 2022, 20:30:57 UTC
e7616fd dependabot[bot] 03 March 2022, 21:13:54 UTC Bump rupicola from `d66e50e` to `e248b81` (#1148) 03 March 2022, 21:13:54 UTC
bac2325 dependabot[bot] 03 March 2022, 20:47:13 UTC Bump rewriter from `5ca81b1` to `3fc0c44` (#1147) 03 March 2022, 20:47:13 UTC
5dd14e1 dependabot[bot] 03 March 2022, 16:27:59 UTC Bump actions/checkout from 2 to 3 (#1146) 03 March 2022, 16:27:59 UTC
df77590 Andres Erbsen 02 March 2022, 15:14:07 UTC admit riscv_word_ok instance 02 March 2022, 15:14:07 UTC
168bcc9 Andres Erbsen 02 March 2022, 12:43:24 UTC X25519: use specs of from_wrod,cswap,copy 02 March 2022, 13:18:35 UTC
e53e02b Jade Philipoom 05 December 2021, 18:19:53 UTC finish proof about compiler output and factor out remaining admits WIP, working on compiler proof compiler proof statement wip separating proof WIP wip, changed ext_spec in field25519 to be parameterized wip finish proof about compiler output and factor out remaining admits 02 March 2022, 12:47:00 UTC
514951e Andres Erbsen 02 March 2022, 01:26:54 UTC update output-tests/Crypto.Bedrock.Group.ScalarMult.MontgomeryLadder.montladder_body.expected 02 March 2022, 12:05:52 UTC
01b94d9 Andres Erbsen 23 February 2022, 21:00:42 UTC rm src/Bedrock/Field/Interface/Compilation.v 02 March 2022, 12:05:52 UTC
433c56e Andres Erbsen 22 February 2022, 19:57:12 UTC integrate from_word and cswap with montledder 02 March 2022, 12:05:52 UTC
33af4d1 Andres Erbsen 17 January 2022, 00:26:20 UTC thread through admitted fe25519_copy 02 March 2022, 12:05:52 UTC
46dbcef Andres Erbsen 15 January 2022, 20:29:54 UTC Hint Rewrite @eval_cons weight_multiples : push_eval 02 March 2022, 12:05:52 UTC
4390cb9 dependabot[bot] 28 February 2022, 21:42:57 UTC Bump actions/setup-python from 2.3.2 to 3 (#1144) 28 February 2022, 21:42:57 UTC
72a46b7 dependabot[bot] 28 February 2022, 20:02:02 UTC Bump actions/setup-go from 2.2.0 to 3 (#1143) 28 February 2022, 20:02:02 UTC
c9172da Jason Gross 25 February 2022, 18:57:19 UTC Finish SymbolicProofs proof of shlx 28 February 2022, 00:25:04 UTC
1607562 Joel 21 February 2022, 23:01:52 UTC added import to Tactics.WarnIfGoalsRemain. 28 February 2022, 00:25:04 UTC
5e92f66 Joel 21 February 2022, 21:37:45 UTC Update src/Assembly/WithBedrock/SymbolicProofs.v Co-authored-by: Jason Gross <jasongross9@gmail.com> 28 February 2022, 00:25:04 UTC
aa7d354 Joel 21 February 2022, 04:33:58 UTC adding `Show.` 28 February 2022, 00:25:04 UTC
d191296 Joel 21 February 2022, 00:00:10 UTC adding Unshelve, to see the remaining goals in the CI 28 February 2022, 00:25:04 UTC
05d1f6f Joel 18 February 2022, 06:21:07 UTC simplify 28 February 2022, 00:25:04 UTC
6f7f38d Joel 18 February 2022, 06:11:52 UTC 'most' infix... 28 February 2022, 00:25:04 UTC
b25d3f1 Joel 18 February 2022, 06:05:28 UTC negb rather than Z.z2b 28 February 2022, 00:25:04 UTC
0c700c3 Joel 18 February 2022, 05:01:52 UTC z2b'ing it back to be able to call SetFlag 28 February 2022, 00:25:04 UTC
44ed466 Joel 18 February 2022, 04:25:29 UTC using B2z to convert bool -> Z 28 February 2022, 00:25:04 UTC
ae98890 Joel 17 February 2022, 23:58:08 UTC remove space 28 February 2022, 00:25:04 UTC
970f3b4 Joel 17 February 2022, 23:29:45 UTC adding `shl,_` and `shlx,_` in DenoteNormalInstruction 28 February 2022, 00:25:04 UTC
6739378 Joel 17 February 2022, 20:57:45 UTC xor -> lxor Co-authored-by: Jason Gross <jasongross9@gmail.com> 28 February 2022, 00:25:04 UTC
6bac53a Joel 17 February 2022, 03:33:25 UTC showcasing shlx-by-2 to multiply-by-2-twice 28 February 2022, 00:25:04 UTC
25bcfb8 Joel 17 February 2022, 03:29:20 UTC fix correctness. x10 was missing 28 February 2022, 00:25:04 UTC
d278fb7 Joel 17 February 2022, 03:18:42 UTC moving shift to mul before flatten assoc 28 February 2022, 00:25:04 UTC
48917a3 Joel 17 February 2022, 03:15:22 UTC amending existing file fo showcase shlx/shl to mul 28 February 2022, 00:25:04 UTC
e93e29a Joel 17 February 2022, 03:10:00 UTC move showcase (*2*2 != *4) to existing file 28 February 2022, 00:25:04 UTC
59af4d4 Joel 17 February 2022, 03:06:08 UTC moving to other PR 28 February 2022, 00:25:04 UTC
4937bbb Joel 17 February 2022, 01:51:21 UTC resolve syntax err. Co-authored-by: Jason Gross <jasongross9@gmail.com> 28 February 2022, 00:25:04 UTC
7fb8749 Joel 17 February 2022, 01:45:28 UTC remove space Co-authored-by: Jason Gross <jasongross9@gmail.com> 28 February 2022, 00:25:04 UTC
8182d88 Joel 17 February 2022, 01:44:20 UTC Update src/Assembly/Syntax.v Co-authored-by: Jason Gross <jasongross9@gmail.com> 28 February 2022, 00:25:04 UTC
49727ae Joel 17 February 2022, 01:44:13 UTC Update src/Assembly/Parse.v Co-authored-by: Jason Gross <jasongross9@gmail.com> 28 February 2022, 00:25:04 UTC
46b1cf3 Joel 17 February 2022, 01:51:41 UTC using cnt' instead of cnt 28 February 2022, 00:25:04 UTC
2a5e8f6 Jason Gross 17 February 2022, 01:11:44 UTC Fix shift_to_mul definition and proof We need to truncate the expression when there's a bitwidth to truncate it to 28 February 2022, 00:25:04 UTC
3c1358e Joel 16 February 2022, 23:46:21 UTC adding shl->mul rewrite 28 February 2022, 00:25:04 UTC
e5498cb Joel 16 February 2022, 23:46:04 UTC reverting MEM-changes to focus on shl-mul rewrite 28 February 2022, 00:25:04 UTC
f81e5a3 Joel 14 February 2022, 07:05:47 UTC shl, shlx into Semantics.v for bedrock 28 February 2022, 00:25:04 UTC
3a28184 Joel 14 February 2022, 07:05:22 UTC lea z*reg 28 February 2022, 00:25:04 UTC
5174d20 Joel 10 February 2022, 06:38:04 UTC showcase a * 2 * 2 !== a*4 28 February 2022, 00:25:04 UTC
af52382 Joel 10 February 2022, 02:33:36 UTC added shl and shlx to parser and symbolic 28 February 2022, 00:25:04 UTC
0d92c08 Joel 10 February 2022, 02:32:52 UTC added two files, showcasing other instr. to mul * imm 28 February 2022, 00:25:04 UTC
92bd843 Jason Gross 24 February 2022, 23:16:16 UTC Add ListUtil.StdlibCompat All the lemmas in Coq.Lists.List and Coq.Sorting.Permutation present in current master (8.16?) but not in 8.11. 25 February 2022, 17:26:23 UTC
eebdaad Jason Gross 24 February 2022, 02:05:47 UTC Add groupBy and groupAllBy 25 February 2022, 17:26:23 UTC
9251ed6 dependabot[bot] 24 February 2022, 21:38:12 UTC Bump rupicola from `fb8c808` to `48820b7` (#1142) 24 February 2022, 21:38:12 UTC
bc8b294 dependabot[bot] 24 February 2022, 20:45:44 UTC Bump actions/setup-java from 2.5.0 to 3.0.0 (#1141) 24 February 2022, 20:45:44 UTC
23d85fd Ashley Lin 23 February 2022, 06:27:52 UTC reverse argument order in AdditionChains 23 February 2022, 06:27:52 UTC
1549d5a Jason Gross 22 February 2022, 21:06:23 UTC Add ListUtil.span for groupBy (#1137) 22 February 2022, 21:06:23 UTC
982f14d Jason Gross 21 February 2022, 23:50:15 UTC Include the operation when explaining the final error messages in asm 22 February 2022, 15:57:11 UTC
cfe296f Jason Gross 21 February 2022, 21:22:44 UTC Better error messages Probably if the lists are the same lengths, then we want to compare them element-wise rather than all at once. It's way too verbose to keep expanding them, so we only do that when lists are not the same length. We now get error messages such as ``` Unable to unify: [inr [378, 381, 384]] == [inr [101, 106, 108]] Could not unify the values at index 0: [#378, #381, #384] != [#101, #106, #108] index 0: #378 != #101 (slice 0 44, [#377]) != (slice 0 44, [#98]) index 0: #377 != #98 (add 64, [#345, #375]) != (add 64, [#57, #96]) index 0: #345 != #57 (slice 0 44, [#337]) != (slice 0 44, [#44]) index 0: #337 != #44 (add 64, [#41, #334]) != (add 64, [#25, #41]) index 1: #334 != #25 (mul 64, [#1, #331]) != (mul 64, [#0, #1, #22]) [(add 64, [#329, #329])] != [#0, (const 20, [])] [(add 64, [(mul 64, [#7, #328]), (mul 64, [#7, #328])])] != [#0, (const 20, [])] [(add 64, [(mul 64, [(const 2, []), (add 64, [#0, #327])]), (mul 64, [(const 2, []), (add 64, [#0, #327])])])] != [#0, (const 20, [])] [(add 64, [(mul 64, [(const 2, []), (add 64, [#0, (mul 64, [#0, #326])])]), (mul 64, [(const 2, []), (add 64, [#0, (mul 64, [#0, #326])])])])] != [#0, (const 20, [])] [(add 64, [(mul 64, [(const 2, []), (add 64, [#0, (mul 64, [#0, (const 4, [])])])]), (mul 64, [(const 2, []), (add 64, [#0, (mul 64, [#0, (const 4, [])])])])])] != [#0, (const 20, [])] [(add 64, [(mul 64, [(const 2, []), (add 64, [(old 64 0, []), (mul 64, [(old 64 0, []), (const 4, [])])])]), (mul 64, [(const 2, []), (add 64, [(old 64 0, []), (mul 64, [(old 64 0, []), (const 4, [])])])])])] != [(old 64 0, []), (const 20, [])] ``` The second to last line is generally the one to look at; the last line adds a bit more detail to it. Perhaps we should instead list out the values of indices rather than expanding one additional level? 22 February 2022, 15:57:11 UTC
1b8c820 Jason Gross 21 February 2022, 20:26:40 UTC Prefix dag indices with more # 22 February 2022, 15:57:11 UTC
a41e08c Jason Gross 21 February 2022, 17:20:37 UTC Better explanation of unification error messages 22 February 2022, 15:57:11 UTC
back to top