Commit Graph

Select branches

Hide Pull Requests

main

Mono Color

• 33cc0f9fe9 Implement constant analysis main Danila Fedorin 2025-01-05 19:38:55 -0800
• 9f2790c500 Actually force proof of 'analyze-correct' Danila Fedorin 2025-01-05 19:35:56 -0800
• 105321971f Slightly help along implicit inference by moving binary less-than Danila Fedorin 2025-01-05 19:12:34 -0800
• 236c92a5ef Add definitions about monotonicity to Lattice Danila Fedorin 2025-01-05 19:36:42 -0800
• ca375976b7 Re-export members of isLattice together with the record where needed Danila Fedorin 2025-01-04 22:43:13 -0800
• c0238fea25 Clean up how proofs of fixed height are imported Danila Fedorin 2025-01-04 22:34:49 -0800
• 1432dfa669 Clean up FiniteMap module structure a bit Danila Fedorin 2025-01-04 22:28:47 -0800
• ffe9d193d9 Parameterize FiniteMap by its keys right away Danila Fedorin 2025-01-04 22:19:02 -0800
• cf824dc744 Switch product to using instances Danila Fedorin 2025-01-04 21:33:59 -0800
• 70847d51db Swich AboveBelow to using instances Danila Fedorin 2025-01-04 21:23:07 -0800
• d96eb97b69 Switch maps (and consequently most of the code) to using instances Danila Fedorin 2025-01-04 21:16:22 -0800
• d90b544436 Use binary operator for decidable equality consistently Danila Fedorin 2025-01-04 19:08:28 -0800
• b0488c9cc6 Make 'IsDecidable' into a record to aid instance search Danila Fedorin 2025-01-04 18:58:56 -0800
• 8abf6f8670 Make 'isLattice' for simple types be an instance Danila Fedorin 2025-01-04 17:27:38 -0800
• 4da9b6d3cd Fuse 'FiniteMap' and 'FiniteValueMap' Danila Fedorin 2024-12-31 19:21:23 -0800
• c2c04e3ecd Rewrite Forward analysis to use statement-based evaluators. Danila Fedorin 2024-12-31 17:31:01 -0800
• f01df5af4b Slightly tweak module style in Forward.agda Danila Fedorin 2024-12-31 12:55:29 -0800
• b28994e1d2 Tighten exported definitions in Forward.agda Danila Fedorin 2024-12-31 00:29:39 -0800
• 10332351ea Use instance search to avoid multiply-nested modules Danila Fedorin 2024-12-31 00:21:10 -0800
• 9131214880 Slightly clean up import for in-dec for Graph edges 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