Commit Graph

Select branches

Hide Pull Requests

main

Mono Color

• d99d4a2893 [WIP] Demonstrate partial lattice construction main Danila Fedorin 2025-07-25 19:51:27 +0200
• fbb98de40f Prove the other absorption law Danila Fedorin 2025-07-25 19:26:03 +0200
• 706b593d1d Write a lemma to wrangle PartialAbsorb proofs Danila Fedorin 2025-07-25 19:14:49 +0200
• 45606679f5 Prove one of the absorption laws Danila Fedorin 2025-07-25 18:32:23 +0200
• 7e099a2561 Delete debugging code Danila Fedorin 2025-07-25 17:18:31 +0200
• 2808759338 Add instances of semilattice proofs Danila Fedorin 2025-07-25 17:18:19 +0200
• 42bb8f8792 Extend laws on Path' to Path versions Danila Fedorin 2025-07-25 17:17:59 +0200
• 05e693594d Prove idempotence of meet and join Danila Fedorin 2025-07-25 17:17:25 +0200
• 90e0046707 Prove missing congruence law Danila Fedorin 2025-07-25 17:17:01 +0200
• 13eee93255 Remove whitespace errors Danila Fedorin 2025-07-25 15:26:41 +0200
• 6243326665 Prove associativity of meet Danila Fedorin 2025-07-25 15:21:59 +0200
• 7b2114cd0f Use a convenience function for creating the "greatest path" Danila Fedorin 2025-07-25 15:21:43 +0200
• 36ae125e1e Prove associativity Danila Fedorin 2025-07-22 18:05:08 +0200
• 6055a79e6a Prove a side lemma about nothing/just Danila Fedorin 2025-07-22 18:04:53 +0200
• 01f7f678d3 Prove congruence of various operations Danila Fedorin 2025-07-22 18:02:45 +0200
• 14f1494fc3 Provide a definition of partial congruence Danila Fedorin 2025-07-22 18:01:48 +0200
• d3bac2fe60 Switch to representing least/greatest with absorption Danila Fedorin 2025-07-22 17:59:54 +0200
• 5705f256fd Prove some quasi-homomorphism properties Danila Fedorin 2025-07-11 15:49:56 +0200
• d59ae90cef Lock down more equivalence relation proofs Danila Fedorin 2025-07-11 15:46:18 +0200
• c1c34c69a5 Strengthen absorption laws Danila Fedorin 2025-07-11 15:44:29 +0200
• d2faada90a Add a left and right version of identity Danila Fedorin 2025-07-11 15:43:27 +0200
• 7fdbf0397d Prove idempotence of value combining Danila Fedorin 2025-07-05 16:55:11 -0700
• fdef8c0a60 Prove commutativity and associativity of value joining Danila Fedorin 2025-07-05 16:49:38 -0700
• c48bd0272e Define "less than or equal" for partial lattices and prove some properties Danila Fedorin 2025-07-05 14:53:00 -0700
• d251915772 Show that lifted equality preserves equivalences Danila Fedorin 2025-07-05 14:52:40 -0700
• da6e82d04b Add helper definitions for partial commutativity, associativity, reflexivity Danila Fedorin 2025-07-02 15:11:12 -0500
• dd101c6e9b Start working on a general lattice builder framework Danila Fedorin 2025-06-29 10:35:37 -0700
• a611dd0f31 Add 'ExtendBelow' lattice, which adds new bottom to lattices Danila Fedorin 2025-04-20 19:13:07 -0700
• 33cc0f9fe9 Implement constant analysis 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