Commit Graph

Select branches

Hide Pull Requests

dag-lattice-builder

fable-lean-migration

main

Mono Color

• b16f14fdfd Lean migration: typeclass-based parameter passing, as in the Agda original fable-lean-migration Danila Fedorin 2026-06-09 23:32:38 -07:00
• b26d6b5acd Lean migration: final notes — Lean output verified identical to Agda Danila Fedorin 2026-06-09 20:54:59 -07:00
• a82d54666a Lean migration: Phase 7 (Sign + Constant analyses, executable) Danila Fedorin 2026-06-09 20:52:08 -07:00
• 739fbb503c Lean migration: Phase 6 (forward analysis framework) Danila Fedorin 2026-06-09 20:14:53 -07:00
• 2cfd0a2fb7 Lean migration: Phase 5 (language, CFGs, traces, Program) Danila Fedorin 2026-06-09 19:30:42 -07:00
• 781d7947e0 Lean migration: Phase 4 (IterProd + FiniteMap lattices) Danila Fedorin 2026-06-09 19:12:39 -07:00
• 4c337afa9c Lean migration: Phase 3 (Unit, Prod, AboveBelow lattices) Danila Fedorin 2026-06-09 18:48:02 -07:00
• ae030386b4 Lean migration: Phases 0-2 (core lattice/chain, fixpoint, transport) Danila Fedorin 2026-06-09 18:36:43 -07:00
• 1c2bcc2d92 Require bottom element to actually be bottom; finish proof dag-lattice-builder Danila Fedorin 2026-02-16 20:15:10 -08:00
• da2b6dd5c6 Make code less brittle for when \McL changes Danila Fedorin 2026-02-16 19:43:10 -08:00
• c64504b819 Fix broken code by moving fins to utils Danila Fedorin 2026-02-16 19:33:56 -08:00
• 4a9e7492f4 Prove the other direction for associativity Danila Fedorin 2026-02-16 19:31:39 -08:00
• ba57e2558d Add more cases for associativity lemma Danila Fedorin 2026-02-16 17:41:48 -08:00
• 1c37141234 Add more properties about lattices Danila Fedorin 2026-02-16 17:41:26 -08:00
• 9072da4ab6 Add some cases for associativity lemma Danila Fedorin 2026-02-16 15:08:57 -08:00
• 3f923c2d7d Clean up some definitions Danila Fedorin 2026-02-16 12:57:59 -08:00
• 01555ee203 Make progress on properties of the dependent product Danila Fedorin 2026-02-16 01:08:34 -08:00
• a083f2f4ae Construct proofs of 'basic' lattices Danila Fedorin 2026-02-14 14:40:15 -08:00
• 27f65c10f7 Prove absroption laws Danila Fedorin 2026-02-14 14:22:27 -08:00
• c6e525ad7c Add associativity proofs Danila Fedorin 2026-02-14 13:47:39 -08:00
• ccc3c7d5c7 Add meet/join operation and some properties Danila Fedorin 2026-02-12 20:16:02 -08:00
• 05c55498ce Extend proofs to meet as well as join Danila Fedorin 2026-02-12 17:12:01 -08:00
• 6b462f1a83 Prove that having a total join function is decidable Danila Fedorin 2026-02-05 16:54:22 -08:00
• 7382c632bc Add some proofs about predecessors Danila Fedorin 2026-02-05 16:16:12 -08:00
• aa32706120 Fix typo Danila Fedorin 2025-12-23 14:07:45 -08:00
• 4b0541caf5 Use "top" instead of T Danila Fedorin 2025-12-23 14:06:28 -08:00
• 299938d97e Add decidability proofs for properties Danila Fedorin 2025-12-07 22:25:47 -08:00
• 927030c337 Prove that having a top and bottom element is decidable Danila Fedorin 2025-12-07 19:28:56 -08:00
• ef3c351bb0 Add some utility proofs about uniqueness etc. Danila Fedorin 2025-12-07 19:28:27 -08:00
• 84c4ea6936 Prove final postulate about cycles in graphs Danila Fedorin 2025-11-29 22:46:49 -08:00
• a277c8f969 Prove walk splitting Danila Fedorin 2025-11-29 21:34:39 -08:00
• d1700f23fa Add some helpers Danila Fedorin 2025-11-29 13:24:27 -08:00
• eb2d64f3b5 Properly state all-paths property using simple walks Danila Fedorin 2025-11-28 21:31:54 -08:00
• 14214ab5e7 Reorder definitions to be in the order the graph is built up Danila Fedorin 2025-11-28 17:09:57 -08:00
• baece236d3 Re-define 'interior' Danila Fedorin 2025-11-28 17:09:14 -08:00
• 6f642d85e0 Put self-paths into the adjacency graph Danila Fedorin 2025-11-28 17:08:56 -08:00
• 25fa0140f0 Switch to a path definition that allows trivial self-loops Danila Fedorin 2025-11-28 16:30:10 -08:00
• 27621992ad Rename a helper Danila Fedorin 2025-11-28 16:25:46 -08:00
• e409cceae5 Start on an initial implementation of DAG-based builder Danila Fedorin 2025-11-28 16:24:48 -08:00
• 8cb082e3c5 Delete original builder (lol) Danila Fedorin 2025-11-28 16:24:29 -08:00
• c199e9616f Factor some code out into Utils Danila Fedorin 2025-11-28 16:22:17 -08:00
• f5457d8841 Move proof of least element into FiniteHeightLattice main Danila Fedorin 2025-07-26 13:16:22 +02:00
• d99d4a2893 [WIP] Demonstrate partial lattice construction Danila Fedorin 2025-07-25 19:51:27 +02:00
• fbb98de40f Prove the other absorption law Danila Fedorin 2025-07-25 19:26:03 +02:00
• 706b593d1d Write a lemma to wrangle PartialAbsorb proofs Danila Fedorin 2025-07-25 19:14:49 +02:00
• 45606679f5 Prove one of the absorption laws Danila Fedorin 2025-07-25 18:32:23 +02:00
• 7e099a2561 Delete debugging code Danila Fedorin 2025-07-25 17:18:31 +02:00
• 2808759338 Add instances of semilattice proofs Danila Fedorin 2025-07-25 17:18:19 +02:00
• 42bb8f8792 Extend laws on Path' to Path versions Danila Fedorin 2025-07-25 17:17:59 +02:00
• 05e693594d Prove idempotence of meet and join Danila Fedorin 2025-07-25 17:17:25 +02:00
• 90e0046707 Prove missing congruence law Danila Fedorin 2025-07-25 17:17:01 +02:00
• 13eee93255 Remove whitespace errors Danila Fedorin 2025-07-25 15:26:41 +02:00
• 6243326665 Prove associativity of meet Danila Fedorin 2025-07-25 15:21:59 +02:00
• 7b2114cd0f Use a convenience function for creating the "greatest path" Danila Fedorin 2025-07-25 15:21:43 +02:00
• 36ae125e1e Prove associativity Danila Fedorin 2025-07-22 18:05:08 +02:00
• 6055a79e6a Prove a side lemma about nothing/just Danila Fedorin 2025-07-22 18:04:53 +02:00
• 01f7f678d3 Prove congruence of various operations Danila Fedorin 2025-07-22 18:02:45 +02:00
• 14f1494fc3 Provide a definition of partial congruence Danila Fedorin 2025-07-22 18:01:48 +02:00
• d3bac2fe60 Switch to representing least/greatest with absorption Danila Fedorin 2025-07-22 17:59:54 +02:00
• 5705f256fd Prove some quasi-homomorphism properties Danila Fedorin 2025-07-11 15:49:56 +02:00
• d59ae90cef Lock down more equivalence relation proofs Danila Fedorin 2025-07-11 15:46:18 +02:00
• c1c34c69a5 Strengthen absorption laws Danila Fedorin 2025-07-11 15:44:29 +02:00
• d2faada90a Add a left and right version of identity Danila Fedorin 2025-07-11 15:43:27 +02:00
• 7fdbf0397d Prove idempotence of value combining Danila Fedorin 2025-07-05 16:55:11 -07:00
• fdef8c0a60 Prove commutativity and associativity of value joining Danila Fedorin 2025-07-05 16:49:38 -07:00
• c48bd0272e Define "less than or equal" for partial lattices and prove some properties Danila Fedorin 2025-07-05 14:53:00 -07:00
• d251915772 Show that lifted equality preserves equivalences Danila Fedorin 2025-07-05 14:52:40 -07:00
• da6e82d04b Add helper definitions for partial commutativity, associativity, reflexivity Danila Fedorin 2025-07-02 15:11:12 -05:00
• dd101c6e9b Start working on a general lattice builder framework Danila Fedorin 2025-06-29 10:35:37 -07:00
• a611dd0f31 Add 'ExtendBelow' lattice, which adds new bottom to lattices Danila Fedorin 2025-04-20 19:13:07 -07:00
• 33cc0f9fe9 Implement constant analysis Danila Fedorin 2025-01-05 19:38:55 -08:00
• 9f2790c500 Actually force proof of 'analyze-correct' Danila Fedorin 2025-01-05 19:35:56 -08:00
• 105321971f Slightly help along implicit inference by moving binary less-than Danila Fedorin 2025-01-05 19:12:34 -08:00
• 236c92a5ef Add definitions about monotonicity to Lattice Danila Fedorin 2025-01-05 19:36:42 -08:00
• ca375976b7 Re-export members of isLattice together with the record where needed Danila Fedorin 2025-01-04 22:43:13 -08:00
• c0238fea25 Clean up how proofs of fixed height are imported Danila Fedorin 2025-01-04 22:34:49 -08:00
• 1432dfa669 Clean up FiniteMap module structure a bit Danila Fedorin 2025-01-04 22:28:47 -08:00
• ffe9d193d9 Parameterize FiniteMap by its keys right away Danila Fedorin 2025-01-04 22:19:02 -08:00
• cf824dc744 Switch product to using instances Danila Fedorin 2025-01-04 21:33:59 -08:00
• 70847d51db Swich AboveBelow to using instances Danila Fedorin 2025-01-04 21:23:07 -08:00
• d96eb97b69 Switch maps (and consequently most of the code) to using instances Danila Fedorin 2025-01-04 21:16:22 -08:00
• d90b544436 Use binary operator for decidable equality consistently Danila Fedorin 2025-01-04 19:08:28 -08:00
• b0488c9cc6 Make 'IsDecidable' into a record to aid instance search Danila Fedorin 2025-01-04 18:58:56 -08:00
• 8abf6f8670 Make 'isLattice' for simple types be an instance Danila Fedorin 2025-01-04 17:27:38 -08:00
• 4da9b6d3cd Fuse 'FiniteMap' and 'FiniteValueMap' Danila Fedorin 2024-12-31 19:21:23 -08:00
• c2c04e3ecd Rewrite Forward analysis to use statement-based evaluators. Danila Fedorin 2024-12-31 17:31:01 -08:00
• f01df5af4b Slightly tweak module style in Forward.agda Danila Fedorin 2024-12-31 12:55:29 -08:00
• b28994e1d2 Tighten exported definitions in Forward.agda Danila Fedorin 2024-12-31 00:29:39 -08:00
• 10332351ea Use instance search to avoid multiply-nested modules Danila Fedorin 2024-12-31 00:21:10 -08:00
• 9131214880 Slightly clean up import for in-dec for Graph edges Danila Fedorin 2024-11-16 15:15:42 -08:00
• 4fba1fe79a Remove unused 'singleton' calls for if/else CFGs Danila Fedorin 2024-11-16 14:42:16 -08:00
• 828b652d3b Rename 'a' to 'b' in fixedpoint algorithm proof Danila Fedorin 2024-08-18 10:28:45 -10:00
• 12971450e3 Add guardedness to Main directly Danila Fedorin 2024-08-08 13:28:25 -07:00
• 7d2928ed81 Prove that the sign analysis is correct Danila Fedorin 2024-05-10 22:31:47 -07:00
• 5f946de5e8 Remove last remaining assumption for correctness Danila Fedorin 2024-05-10 21:30:56 -07:00
• 04bafb2d55 Prove that the inputs to wrap are empty Danila Fedorin 2024-05-10 21:25:40 -07:00
• e0248397b7 Prove that predecessors imply edges Danila Fedorin 2024-05-09 23:18:51 -07:00
• 41ada43047 Move predecessor code into Graphs Danila Fedorin 2024-05-09 23:13:49 -07:00
• a081edb881 Add a proof about filter's distributivity Danila Fedorin 2024-05-09 23:06:49 -07:00
• 3d2a507f2f Almost prove correctness Danila Fedorin 2024-05-09 22:49:53 -07:00