DanilaFe
/
agda-spa
1
0
Fork 0
Code Issues Pull Requests Packages Projects Releases Wiki Activity
278 Commits 1 Branch 0 Tags 1.6 MiB
Commit Graph

43 Commits

Author SHA1 Message Date
Danila Fedorin 5f946de5e8 Remove last remaining assumption for correctness 
Signed-off-by: Danila Fedorin <danila.fedorin@gmail.com>
 2024-05-10 21:30:56 -07:00
Danila Fedorin 41ada43047 Move predecessor code into Graphs 
Signed-off-by: Danila Fedorin <danila.fedorin@gmail.com>
 2024-05-09 23:13:49 -07:00
Danila Fedorin 3d2a507f2f Almost prove correctness 
Signed-off-by: Danila Fedorin <danila.fedorin@gmail.com>
 2024-05-09 22:49:53 -07:00
Danila Fedorin 82027ecd04 Move predecessor computation into Graphs 
Signed-off-by: Danila Fedorin <danila.fedorin@gmail.com>
 2024-05-09 21:26:32 -07:00
Danila Fedorin 734e82ff6d Wrap generated graphs to ensure entry and exit nodes have no extra edges 
Signed-off-by: Danila Fedorin <danila.fedorin@gmail.com>
 2024-05-09 21:08:32 -07:00
Danila Fedorin b3a62da1fb Add a proof that edges lead to 'incoming' inclusion 
Signed-off-by: Danila Fedorin <danila.fedorin@gmail.com>
 2024-05-09 16:56:45 -07:00
Danila Fedorin 838aaf9c58 Start end-to-end proof of correctness 
Signed-off-by: Danila Fedorin <danila.fedorin@gmail.com>
 2024-05-08 23:30:03 -07:00
Danila Fedorin c00c8e3e85 Use different graph operations to implement construction 
Signed-off-by: Danila Fedorin <danila.fedorin@gmail.com>
 2024-04-25 23:10:41 -07:00
Danila Fedorin 6e3f06ca5d Add a new 'properties' module 
Signed-off-by: Danila Fedorin <danila.fedorin@gmail.com>
 2024-04-20 20:25:40 -07:00
Danila Fedorin fc27b045d3 Remove nested module from Graphs 
Signed-off-by: Danila Fedorin <danila.fedorin@gmail.com>
 2024-04-13 19:33:58 -07:00
Danila Fedorin de956cdc6a Split the Language file into modules 
Signed-off-by: Danila Fedorin <danila.fedorin@gmail.com>
 2024-04-13 18:39:38 -07:00
Danila Fedorin 7ed7f20227 Add missing edge 
Signed-off-by: Danila Fedorin <danila.fedorin@gmail.com>
 2024-04-13 15:30:07 -07:00
Danila Fedorin 163108b9b3 Add precedence to some language constructs 
Signed-off-by: Danila Fedorin <danila.fedorin@gmail.com>
 2024-04-13 15:29:50 -07:00
Danila Fedorin 8dc5c40eae Get everything compiling 
Signed-off-by: Danila Fedorin <danila.fedorin@gmail.com>
 2024-04-13 14:13:44 -07:00
Danila Fedorin 44f04e4020 Get forward analysis working again 
Signed-off-by: Danila Fedorin <danila.fedorin@gmail.com>
 2024-04-13 14:08:40 -07:00
Danila Fedorin 4fe0d147fa Adjust 'Program' to have a graph and basic blocks 
Signed-off-by: Danila Fedorin <danila.fedorin@gmail.com>
 2024-04-13 13:39:15 -07:00
Danila Fedorin ba1c9b3ec8 Remove sketch if proof since the proof is done 
Signed-off-by: Danila Fedorin <danila.fedorin@gmail.com>
 2024-04-13 12:31:04 -07:00
Danila Fedorin b6e357787f Add proof about 'both' and pairing 
Signed-off-by: Danila Fedorin <danila.fedorin@gmail.com>
 2024-04-13 12:25:59 -07:00
Danila Fedorin ce3fa182fe Start formalizing monotonic function predicates 
Signed-off-by: Danila Fedorin <danila.fedorin@gmail.com>
 2024-04-12 23:49:33 -07:00
Danila Fedorin 71cb97ad8c Reorder some definitions 
Signed-off-by: Danila Fedorin <danila.fedorin@gmail.com>
 2024-04-12 23:27:17 -07:00
Danila Fedorin 57606636a7 Slightly format some code 
Signed-off-by: Danila Fedorin <danila.fedorin@gmail.com>
 2024-04-12 23:22:31 -07:00
Danila Fedorin da2f7f51d7 Get Language typechecking again, finally 
Signed-off-by: Danila Fedorin <danila.fedorin@gmail.com>
 2024-04-12 23:21:05 -07:00
Danila Fedorin 2db11dcfc7 Use concatenation to represent adding new nodes 
Signed-off-by: Danila Fedorin <danila.fedorin@gmail.com>
 2024-04-12 22:04:43 -07:00
Danila Fedorin 3e2719d45f Turn old proof into a hole to clean up later. 
Signed-off-by: Danila Fedorin <danila.fedorin@gmail.com>
 2024-04-08 22:45:04 -07:00
Danila Fedorin 78252b6c9e Add proof of node preservation for adding edges. 
Signed-off-by: Danila Fedorin <danila.fedorin@gmail.com>
 2024-04-08 22:43:07 -07:00
Danila Fedorin 85fdf544b9 Translate informal proof of (node) transitivity into formal one. 
Signed-off-by: Danila Fedorin <danila.fedorin@gmail.com>
 2024-04-08 20:57:08 -07:00
Danila Fedorin 4f14a7b765 Successfully prove that monotonic updates preserve existing indices 
Signed-off-by: Danila Fedorin <danila.fedorin@gmail.com>
 2024-04-08 00:24:52 -07:00
Danila Fedorin bc5b4b7d9e Explicitly write metas for missing functions 
Signed-off-by: Danila Fedorin <danila.fedorin@gmail.com>
 2024-04-08 00:16:10 -07:00
Danila Fedorin 520b2b514c Clear up vector reindexing 
Signed-off-by: Danila Fedorin <danila.fedorin@gmail.com>
 2024-04-08 00:12:50 -07:00
Danila Fedorin f7ac22257e Beat head against the vector-cast wall. 
Signed-off-by: Danila Fedorin <danila.fedorin@gmail.com>
 2024-04-07 23:44:35 -07:00
Danila Fedorin b72ad070ba Try using index-based comparisons 
Signed-off-by: Danila Fedorin <danila.fedorin@gmail.com>
 2024-04-07 23:18:46 -07:00
Danila Fedorin 195537fe15 Implement graph construction using <*>, map, and update. 
Signed-off-by: Danila Fedorin <danila.fedorin@gmail.com>
 2024-04-07 20:26:38 -07:00
Danila Fedorin d4b0796715 Intermediate commit. Switch to *-based definition of <=. 
Signed-off-by: Danila Fedorin <danila.fedorin@gmail.com>
 2024-04-07 19:51:59 -07:00
Danila Fedorin b505063771 Start working on proofs of Graph-related things 
Signed-off-by: Danila Fedorin <danila.fedorin@gmail.com>
 2024-04-04 20:34:28 -07:00
Danila Fedorin 844c99336a Intermediate commit: add while loops and start trying to formalize them. 2024-04-03 22:31:23 -07:00
Danila Fedorin 3e88a64ed9 Add some debugging code to sign analysis to print the results 
Signed-off-by: Danila Fedorin <danila.fedorin@gmail.com>
 2024-03-10 22:23:45 -07:00
Danila Fedorin 3305de4710 Remove need for explicit arguments in map derivatives 
Signed-off-by: Danila Fedorin <danila.fedorin@gmail.com>
 2024-03-10 18:35:29 -07:00
Danila Fedorin f21ebdcf46 Start working on the evaluation operation. 
Proving monotonicity is the main hurdle here.

Signed-off-by: Danila Fedorin <danila.fedorin@gmail.com>
 2024-03-10 18:13:01 -07:00
Danila Fedorin 0705df708e Prove that variables in a program all come from the program's code 
Signed-off-by: Danila Fedorin <danila.fedorin@gmail.com>
 2024-03-10 16:41:21 -07:00
Danila Fedorin fdc40632bf Add a way to retrieve the code for a particular state 
Signed-off-by: Danila Fedorin <danila.fedorin@gmail.com>
 2024-03-09 23:09:50 -08:00
Danila Fedorin f84a1c923c Prove that the 'join' transformation is monotonic 
Signed-off-by: Danila Fedorin <danila.fedorin@gmail.com>
 2024-03-09 23:06:47 -08:00
Danila Fedorin 75f981cb75 Define simple sequential-only programs 
Signed-off-by: Danila Fedorin <danila.fedorin@gmail.com>
 2024-03-09 13:59:48 -08:00
Danila Fedorin a55c786a51 Tentatively start working on a language to analyze 2024-02-07 22:51:08 -08:00