Commit Graph

Select branches

Hide Pull Requests

dag-lattice-builder

main

Mono Color

• 8d0d87d2d9 Start on proofs of correctness Danila Fedorin 2024-05-08 20:50:21 -07:00
• cfa3375de5 Expose more functions from FiniteMap Danila Fedorin 2024-05-08 20:50:05 -07:00
• 6b116ed960 Forward some map function to Finite{,Value}Map Danila Fedorin 2024-05-08 20:34:15 -07:00
• 3859826293 Define interpretation of the sign lattice Danila Fedorin 2024-04-30 21:58:41 -07:00
• be50c76cb1 Add more higher-order primitives Danila Fedorin 2024-04-30 21:56:34 -07:00
• 112a5087ef Tentative start on proving correctness Danila Fedorin 2024-04-30 19:20:02 -07:00
• ccb7abc501 Remove unused code from Utils Danila Fedorin 2024-04-30 19:15:38 -07:00
• 91b5d108f6 Simplify proofs about 'loop' using concatenation lemma Danila Fedorin 2024-04-29 21:28:21 -07:00
• c574ca9c56 Prove that graphs build by buildCfg are sufficient Danila Fedorin 2024-04-29 20:57:43 -07:00
• bbfba34e05 Prove another (simple) case Danila Fedorin 2024-04-28 13:37:03 -07:00
• aec15573fc Add properties of end-to-end traces on loops Danila Fedorin 2024-04-28 12:53:25 -07:00
• b4d395767d Simplify operations used for constructing graphs Danila Fedorin 2024-04-28 12:40:50 -07:00
• 07550bc214 Prove 'sufficiency' for if-else. Danila Fedorin 2024-04-28 12:10:12 -07:00
• 9366ec4a97 Allow promoting end-to-end traces too Danila Fedorin 2024-04-28 12:00:06 -07:00
• 0fb884eb07 Use implicit arguments for more things Danila Fedorin 2024-04-28 11:43:49 -07:00
• 6b44ac1feb Make graph arguments implicit where possible Danila Fedorin 2024-04-28 11:37:08 -07:00
• 69a4e8eb5c Add some helpers and rewrite code Danila Fedorin 2024-04-27 17:43:16 -07:00
• 4fee16413a Define end-to-end path concatenation and prove one more case Danila Fedorin 2024-04-27 17:34:50 -07:00
• 316e56f2bc Dip toes into creating end-to-end traces Danila Fedorin 2024-04-27 15:27:46 -07:00
• ab40a27e78 Formulate correctness of buildCfg using end-to-end traces Danila Fedorin 2024-04-27 14:56:19 -07:00
• f555947184 Promote traces through loop Danila Fedorin 2024-04-27 14:38:07 -07:00
• 660f6594fd Allow promoting traces through graph composition Danila Fedorin 2024-04-27 14:28:00 -07:00
• fb32315f58 Allow traces to be promoted through graph overlaying Danila Fedorin 2024-04-27 14:18:16 -07:00
• 037358308f Fix up Graph construction Danila Fedorin 2024-04-27 13:50:06 -07:00
• f2b8084a9c Delete code that won't be used for this approach Danila Fedorin 2024-04-25 23:13:15 -07:00
• c00c8e3e85 Use different graph operations to implement construction Danila Fedorin 2024-04-25 23:10:41 -07:00
• b134c143ca Start working on proving 'sufficiency' Danila Fedorin 2024-04-20 21:37:28 -07:00
• e218d1b7a3 Add formalization of 'traces through graph' Danila Fedorin 2024-04-20 21:36:58 -07:00
• 6e3f06ca5d Add a new 'properties' module Danila Fedorin 2024-04-20 20:25:40 -07:00
• 54b11d21b0 Start working on proving facts about graph construction Danila Fedorin 2024-04-20 19:31:47 -07:00
• f3e0d5f2e3 Use 'data' instead of aliases to prove reasoning properties Danila Fedorin 2024-04-20 19:31:13 -07:00
• 855bf3f56c Add functions to reason about the 'monotonic state' operations Danila Fedorin 2024-04-20 18:09:01 -07:00
• 2f91ca113e Make 'MonotonicPredicate' into another typeclass Danila Fedorin 2024-04-13 20:56:56 -07:00
• 7571cb7451 Extract 'monotonic state' into its own module Danila Fedorin 2024-04-13 20:46:30 -07:00
• fc27b045d3 Remove nested module from Graphs Danila Fedorin 2024-04-13 19:33:58 -07:00
• de956cdc6a Split the Language file into modules Danila Fedorin 2024-04-13 18:39:38 -07:00
• 7ed7f20227 Add missing edge Danila Fedorin 2024-04-13 15:30:07 -07:00
• 163108b9b3 Add precedence to some language constructs Danila Fedorin 2024-04-13 15:29:50 -07:00
• 8dc5c40eae Get everything compiling Danila Fedorin 2024-04-13 14:13:44 -07:00
• 44f04e4020 Get forward analysis working again Danila Fedorin 2024-04-13 14:08:40 -07:00
• 4fe0d147fa Adjust 'Program' to have a graph and basic blocks Danila Fedorin 2024-04-13 13:39:15 -07:00
• ba1c9b3ec8 Remove sketch if proof since the proof is done Danila Fedorin 2024-04-13 12:31:04 -07:00
• b6e357787f Add proof about 'both' and pairing Danila Fedorin 2024-04-13 12:25:59 -07:00
• ce3fa182fe Start formalizing monotonic function predicates Danila Fedorin 2024-04-12 23:49:33 -07:00
• 71cb97ad8c Reorder some definitions Danila Fedorin 2024-04-12 23:27:17 -07:00
• 57606636a7 Slightly format some code Danila Fedorin 2024-04-12 23:22:31 -07:00
• da2f7f51d7 Get Language typechecking again, finally Danila Fedorin 2024-04-12 23:21:05 -07:00
• 2db11dcfc7 Use concatenation to represent adding new nodes Danila Fedorin 2024-04-12 22:04:43 -07:00
• 3e2719d45f Turn old proof into a hole to clean up later. Danila Fedorin 2024-04-08 22:45:04 -07:00
• 78252b6c9e Add proof of node preservation for adding edges. Danila Fedorin 2024-04-08 22:43:07 -07:00
• 85fdf544b9 Translate informal proof of (node) transitivity into formal one. Danila Fedorin 2024-04-08 20:57:08 -07:00
• 4f14a7b765 Successfully prove that monotonic updates preserve existing indices Danila Fedorin 2024-04-08 00:24:52 -07:00
• bc5b4b7d9e Explicitly write metas for missing functions Danila Fedorin 2024-04-08 00:16:10 -07:00
• 520b2b514c Clear up vector reindexing Danila Fedorin 2024-04-08 00:12:50 -07:00
• f7ac22257e Beat head against the vector-cast wall. Danila Fedorin 2024-04-07 23:44:35 -07:00
• b72ad070ba Try using index-based comparisons Danila Fedorin 2024-04-07 23:18:46 -07:00
• 195537fe15 Implement graph construction using <*>, map, and update. Danila Fedorin 2024-04-07 20:26:38 -07:00
• d4b0796715 Intermediate commit. Switch to *-based definition of <=. Danila Fedorin 2024-04-07 19:51:59 -07:00
• b505063771 Start working on proofs of Graph-related things Danila Fedorin 2024-04-04 20:34:08 -07:00
• 844c99336a Intermediate commit: add while loops and start trying to formalize them. Danila Fedorin 2024-04-03 22:29:58 -07:00
• 5d56a7ce2d Fix comments in Forward.agda Danila Fedorin 2024-03-23 12:09:14 -07:00
• 2e096bd64e Extract common parts of forward analyses into Forward.agda Danila Fedorin 2024-03-22 17:50:29 -07:00
• 1a7b2a1736 Adjust behavior of eval to not require constant 'k in vars' threading Danila Fedorin 2024-03-22 17:15:40 -07:00
• f0da9a9020 Move more code out of Sign and into Main Danila Fedorin 2024-03-11 13:07:42 -07:00
• 040c13caba Use instances to simplify printing code Danila Fedorin 2024-03-11 12:50:05 -07:00
• 56da61b339 Delete the bundles since they did not turn out all that useful Danila Fedorin 2024-03-11 12:14:53 -07:00
• 3e88a64ed9 Add some debugging code to sign analysis to print the results Danila Fedorin 2024-03-10 22:23:45 -07:00
• 8a85c4497c Prove that evaluation is monotonic and complete sign analysis Danila Fedorin 2024-03-10 21:25:46 -07:00
• 8964ba59a1 Prove monotonicity of eval Danila Fedorin 2024-03-10 20:29:05 -07:00
• 96f3ceaeb2 Use the previous join function directly in GeneralizedUpdate Danila Fedorin 2024-03-10 19:41:02 -07:00
• 237250cf72 Stop using modules in 'Sign' analysis Danila Fedorin 2024-03-10 19:23:48 -07:00
• 8515491327 Simplify AboveBelow a bit to avoid nested modules Danila Fedorin 2024-03-10 18:43:10 -07:00
• 3305de4710 Remove need for explicit arguments in map derivatives Danila Fedorin 2024-03-10 18:35:29 -07:00
• f21ebdcf46 Start working on the evaluation operation. Danila Fedorin 2024-03-10 18:13:01 -07:00
• 0705df708e Prove that variables in a program all come from the program's code Danila Fedorin 2024-03-10 16:41:21 -07:00
• 51accb6438 Define 'minus', too -- with no monotonicity proof. Danila Fedorin 2024-03-10 16:40:49 -07:00
• afe5bac2dc Commit result of (unsuccessfully) trying to prove monotonicity of plus. Danila Fedorin 2024-03-10 13:54:19 -07:00
• fdc40632bf Add a way to retrieve the code for a particular state Danila Fedorin 2024-03-09 23:09:50 -08:00
• f84a1c923c Prove that the 'join' transformation is monotonic Danila Fedorin 2024-03-09 23:06:47 -08:00
• 1b1b80465c Use named modules to avoid having to pass redundant parameters Danila Fedorin 2024-03-09 21:46:15 -08:00
• 56c72e1388 Delete unused homomorphism proof that was broken by an Agda update. Danila Fedorin 2024-03-09 14:07:56 -08:00
• 0c30f8be48 Start on sign analysis (mostly just imports) Danila Fedorin 2024-03-09 14:00:10 -08:00
• 75f981cb75 Define simple sequential-only programs Danila Fedorin 2024-03-09 13:59:48 -08:00
• ca99e18184 Tweak exports from finite value bundle to avoid (some) redundant arguments Danila Fedorin 2024-03-09 13:59:22 -08:00
• 702cf2c298 Expose more functionaity from the set lattice Danila Fedorin 2024-03-09 13:58:40 -08:00
• 0c088ca2ae Prove multi-key access monotonicity in finite maps Danila Fedorin 2024-03-09 13:58:07 -08:00
• bc138d87f0 Prove things about key-based access in map Danila Fedorin 2024-03-09 13:57:29 -08:00
• 311ed75186 Expose more helpers from 'Map' Danila Fedorin 2024-03-09 13:57:02 -08:00
• 1ccc6f08e5 Add more properties of uniqueness Danila Fedorin 2024-03-09 13:54:01 -08:00
• 332b7616cf Prove that foldr is monotonic when input lists are pairwise monotonic Danila Fedorin 2024-03-07 21:53:45 -08:00
• 7905d106e2 Tweak signature of 'forget' to simplify proofs Danila Fedorin 2024-03-07 20:04:33 -08:00
• 34203840c8 Use the new provenance function to clean up some proofs Danila Fedorin 2024-03-07 19:59:14 -08:00
• 48983c55b1 Prove exercise 4.26 from the textbook Danila Fedorin 2024-03-06 00:35:29 -08:00
• fa0282ff6f Prove that the identity function is monotonic Danila Fedorin 2024-03-06 00:35:06 -08:00
• 164fc3636f Prove that constant functions are monotonic Danila Fedorin 2024-03-03 17:23:57 -08:00
• c932210d37 Re-expert monotonicity from Lattice Danila Fedorin 2024-03-03 17:04:18 -08:00
• a8d26b1c48 Prove that join is monotonic in both arguments Danila Fedorin 2024-03-03 16:51:57 -08:00
• 2ddac38c3f Update with new changes to Agda Danila Fedorin 2024-03-03 16:44:10 -08:00
• f00dabfc93 More cleanup to FiniteValueMap Danila Fedorin 2024-03-02 16:15:20 -08:00
• 01f4e02026 More cleanup to FiniteValueMap Danila Fedorin 2024-03-02 16:05:42 -08:00