Commit Graph

Select branches

Hide Pull Requests

main

Mono Color

• 9131214880 Slightly clean up import for in-dec for Graph edges main Danila Fedorin 2024-11-16 15:15:42 -0800
• 4fba1fe79a Remove unused 'singleton' calls for if/else CFGs Danila Fedorin 2024-11-16 14:42:16 -0800
• 828b652d3b Rename 'a' to 'b' in fixedpoint algorithm proof Danila Fedorin 2024-08-18 10:28:45 -1000
• 12971450e3 Add guardedness to Main directly Danila Fedorin 2024-08-08 13:28:25 -0700
• 7d2928ed81 Prove that the sign analysis is correct Danila Fedorin 2024-05-10 22:31:47 -0700
• 5f946de5e8 Remove last remaining assumption for correctness Danila Fedorin 2024-05-10 21:30:56 -0700
• 04bafb2d55 Prove that the inputs to wrap are empty Danila Fedorin 2024-05-10 21:25:40 -0700
• e0248397b7 Prove that predecessors imply edges Danila Fedorin 2024-05-09 23:18:51 -0700
• 41ada43047 Move predecessor code into Graphs Danila Fedorin 2024-05-09 23:13:49 -0700
• a081edb881 Add a proof about filter's distributivity Danila Fedorin 2024-05-09 23:06:49 -0700
• 3d2a507f2f Almost prove correctness Danila Fedorin 2024-05-09 22:49:53 -0700
• 82027ecd04 Move predecessor computation into Graphs Danila Fedorin 2024-05-09 21:26:32 -0700
• 734e82ff6d Wrap generated graphs to ensure entry and exit nodes have no extra edges Danila Fedorin 2024-05-09 21:08:32 -0700
• 69d1ecebae Prove that the bottom map's valyes are all bottoms Danila Fedorin 2024-05-09 20:48:32 -0700
• b78cb91f2a Strengthen lemma about IterProd bottom to definition equality Danila Fedorin 2024-05-09 20:20:11 -0700
• 16fa4cd1d8 Use records rather than nested pairs to represent 'fixed height' Danila Fedorin 2024-05-09 20:11:04 -0700
• 95669b2c65 Prove that the iterated product is made from iterated bottom elements Danila Fedorin 2024-05-09 19:45:15 -0700
• 6857f60465 Rename the min/max elements top bottom and top in Prod Danila Fedorin 2024-05-09 19:08:46 -0700
• f4392b32c0 Finish the last proof obligation for trace walking Danila Fedorin 2024-05-09 19:01:36 -0700
• 794c04eee9 Prove the foldr-implies lemma Danila Fedorin 2024-05-09 18:37:50 -0700
• 80069e76e6 Prove the recursive step of trace walking Danila Fedorin 2024-05-09 17:56:47 -0700
• a22c0c9252 Prove a property of multi-key lookup Danila Fedorin 2024-05-09 17:56:26 -0700
• 20dc99ba1f Re-indent some code to take up less horizontal space Danila Fedorin 2024-05-09 16:57:03 -0700
• b3a62da1fb Add a proof that edges lead to 'incoming' inclusion Danila Fedorin 2024-05-09 16:56:45 -0700
• f0b0d51b48 Add unproven lemma about fold implication Danila Fedorin 2024-05-08 23:38:23 -0700
• 8ff88f9f9e Move helper code into separate function Danila Fedorin 2024-05-08 23:35:02 -0700
• c1581075d3 Add more test programs Danila Fedorin 2024-05-08 23:30:23 -0700
• 838aaf9c58 Start end-to-end proof of correctness Danila Fedorin 2024-05-08 23:30:03 -0700
• 4ac9dffa9b Prove that the var->lattice maps respect equality Danila Fedorin 2024-05-08 22:53:21 -0700
• 3f5551d70c Add a lemma about the effect of joinAll Danila Fedorin 2024-05-08 22:34:02 -0700
• 5837fdf19b Prove that 'updateAll' has preservation Danila Fedorin 2024-05-08 22:29:36 -0700
• 4350919871 Add proof about setVariablesForState Danila Fedorin 2024-05-08 22:09:56 -0700
• 7fe46b014c Slightly simplify evaluation code Danila Fedorin 2024-05-08 22:05:50 -0700
• 66d229c493 Prove that multi-statement evaluation "preserves" the validity of the analysis Danila Fedorin 2024-05-08 21:51:53 -0700
• 1b8bea8957 Use foldl in multi-statement evaluation Danila Fedorin 2024-05-08 21:50:38 -0700
• dd8cdcd10c Add proofs about monotonicity of foldl Danila Fedorin 2024-05-08 21:48:41 -0700
• ad4592d4d2 Switch to using implicit arguments where needed Danila Fedorin 2024-05-08 21:34:17 -0700
• 8d0d87d2d9 Start on proofs of correctness Danila Fedorin 2024-05-08 20:50:21 -0700
• cfa3375de5 Expose more functions from FiniteMap Danila Fedorin 2024-05-08 20:50:05 -0700
• 6b116ed960 Forward some map function to Finite{,Value}Map Danila Fedorin 2024-05-08 20:34:15 -0700
• 3859826293 Define interpretation of the sign lattice Danila Fedorin 2024-04-30 21:58:41 -0700
• be50c76cb1 Add more higher-order primitives Danila Fedorin 2024-04-30 21:56:34 -0700
• 112a5087ef Tentative start on proving correctness Danila Fedorin 2024-04-30 19:20:02 -0700
• ccb7abc501 Remove unused code from Utils Danila Fedorin 2024-04-30 19:15:38 -0700
• 91b5d108f6 Simplify proofs about 'loop' using concatenation lemma Danila Fedorin 2024-04-29 21:28:21 -0700
• c574ca9c56 Prove that graphs build by buildCfg are sufficient Danila Fedorin 2024-04-29 20:57:43 -0700
• bbfba34e05 Prove another (simple) case Danila Fedorin 2024-04-28 13:37:03 -0700
• aec15573fc Add properties of end-to-end traces on loops Danila Fedorin 2024-04-28 12:53:25 -0700
• b4d395767d Simplify operations used for constructing graphs Danila Fedorin 2024-04-28 12:40:50 -0700
• 07550bc214 Prove 'sufficiency' for if-else. Danila Fedorin 2024-04-28 12:10:12 -0700
• 9366ec4a97 Allow promoting end-to-end traces too Danila Fedorin 2024-04-28 12:00:06 -0700
• 0fb884eb07 Use implicit arguments for more things Danila Fedorin 2024-04-28 11:43:49 -0700
• 6b44ac1feb Make graph arguments implicit where possible Danila Fedorin 2024-04-28 11:37:08 -0700
• 69a4e8eb5c Add some helpers and rewrite code Danila Fedorin 2024-04-27 17:43:16 -0700
• 4fee16413a Define end-to-end path concatenation and prove one more case Danila Fedorin 2024-04-27 17:34:50 -0700
• 316e56f2bc Dip toes into creating end-to-end traces Danila Fedorin 2024-04-27 15:27:46 -0700
• ab40a27e78 Formulate correctness of buildCfg using end-to-end traces Danila Fedorin 2024-04-27 14:56:19 -0700
• f555947184 Promote traces through loop Danila Fedorin 2024-04-27 14:38:07 -0700
• 660f6594fd Allow promoting traces through graph composition Danila Fedorin 2024-04-27 14:28:00 -0700
• fb32315f58 Allow traces to be promoted through graph overlaying Danila Fedorin 2024-04-27 14:18:16 -0700
• 037358308f Fix up Graph construction Danila Fedorin 2024-04-27 13:50:06 -0700
• f2b8084a9c Delete code that won't be used for this approach Danila Fedorin 2024-04-25 23:13:15 -0700
• c00c8e3e85 Use different graph operations to implement construction Danila Fedorin 2024-04-25 23:10:41 -0700
• b134c143ca Start working on proving 'sufficiency' Danila Fedorin 2024-04-20 21:37:28 -0700
• e218d1b7a3 Add formalization of 'traces through graph' Danila Fedorin 2024-04-20 21:36:58 -0700
• 6e3f06ca5d Add a new 'properties' module Danila Fedorin 2024-04-20 20:25:40 -0700
• 54b11d21b0 Start working on proving facts about graph construction Danila Fedorin 2024-04-20 19:31:47 -0700
• f3e0d5f2e3 Use 'data' instead of aliases to prove reasoning properties Danila Fedorin 2024-04-20 19:31:13 -0700
• 855bf3f56c Add functions to reason about the 'monotonic state' operations Danila Fedorin 2024-04-20 18:09:01 -0700
• 2f91ca113e Make 'MonotonicPredicate' into another typeclass Danila Fedorin 2024-04-13 20:56:56 -0700
• 7571cb7451 Extract 'monotonic state' into its own module Danila Fedorin 2024-04-13 20:46:30 -0700
• fc27b045d3 Remove nested module from Graphs Danila Fedorin 2024-04-13 19:33:58 -0700
• de956cdc6a Split the Language file into modules Danila Fedorin 2024-04-13 18:39:38 -0700
• 7ed7f20227 Add missing edge Danila Fedorin 2024-04-13 15:30:07 -0700
• 163108b9b3 Add precedence to some language constructs Danila Fedorin 2024-04-13 15:29:50 -0700
• 8dc5c40eae Get everything compiling Danila Fedorin 2024-04-13 14:13:44 -0700
• 44f04e4020 Get forward analysis working again Danila Fedorin 2024-04-13 14:08:40 -0700
• 4fe0d147fa Adjust 'Program' to have a graph and basic blocks Danila Fedorin 2024-04-13 13:39:15 -0700
• ba1c9b3ec8 Remove sketch if proof since the proof is done Danila Fedorin 2024-04-13 12:31:04 -0700
• b6e357787f Add proof about 'both' and pairing Danila Fedorin 2024-04-13 12:25:59 -0700
• ce3fa182fe Start formalizing monotonic function predicates Danila Fedorin 2024-04-12 23:49:33 -0700
• 71cb97ad8c Reorder some definitions Danila Fedorin 2024-04-12 23:27:17 -0700
• 57606636a7 Slightly format some code Danila Fedorin 2024-04-12 23:22:31 -0700
• da2f7f51d7 Get Language typechecking again, finally Danila Fedorin 2024-04-12 23:21:05 -0700
• 2db11dcfc7 Use concatenation to represent adding new nodes Danila Fedorin 2024-04-12 22:04:43 -0700
• 3e2719d45f Turn old proof into a hole to clean up later. Danila Fedorin 2024-04-08 22:45:04 -0700
• 78252b6c9e Add proof of node preservation for adding edges. Danila Fedorin 2024-04-08 22:43:07 -0700
• 85fdf544b9 Translate informal proof of (node) transitivity into formal one. Danila Fedorin 2024-04-08 20:57:08 -0700
• 4f14a7b765 Successfully prove that monotonic updates preserve existing indices Danila Fedorin 2024-04-08 00:24:52 -0700
• bc5b4b7d9e Explicitly write metas for missing functions Danila Fedorin 2024-04-08 00:16:10 -0700
• 520b2b514c Clear up vector reindexing Danila Fedorin 2024-04-08 00:12:50 -0700
• f7ac22257e Beat head against the vector-cast wall. Danila Fedorin 2024-04-07 23:44:35 -0700
• b72ad070ba Try using index-based comparisons Danila Fedorin 2024-04-07 23:18:46 -0700
• 195537fe15 Implement graph construction using <*>, map, and update. Danila Fedorin 2024-04-07 20:26:38 -0700
• d4b0796715 Intermediate commit. Switch to *-based definition of <=. Danila Fedorin 2024-04-07 19:51:59 -0700
• b505063771 Start working on proofs of Graph-related things Danila Fedorin 2024-04-04 20:34:08 -0700
• 844c99336a Intermediate commit: add while loops and start trying to formalize them. Danila Fedorin 2024-04-03 22:29:58 -0700
• 5d56a7ce2d Fix comments in Forward.agda Danila Fedorin 2024-03-23 12:09:14 -0700
• 2e096bd64e Extract common parts of forward analyses into Forward.agda Danila Fedorin 2024-03-22 17:50:29 -0700
• 1a7b2a1736 Adjust behavior of eval to not require constant 'k in vars' threading Danila Fedorin 2024-03-22 17:15:40 -0700