Commit Graph

Select branches

Hide Pull Requests

dag-lattice-builder

fable-lean-migration

main

Mono Color

• 904f6375be Consolidate per-operator trace lifting into GGraph.Embed + Trace.embed fable-lean-migration Danila Fedorin 2026-07-02 15:06:40 -05:00
• 8cd053a242 Migrate Reaching.lean to projections via a generic Trace.steps Danila Fedorin 2026-07-02 09:01:09 -05:00
• 0e6976f9b4 Migrate most of the codebase (sans Reaching.lean / LICM left) to projections Danila Fedorin 2026-07-01 22:56:29 -05:00
• 10b8fa97ca Add left-and-right open traces to help formalization Danila Fedorin 2026-07-01 16:35:07 -05:00
• 8ed48cf444 Add non-state parameterized 'Reaches' relation Danila Fedorin 2026-07-01 13:02:39 -05:00
• 37d88f070a Remove 'prog.code s = some bs' argument to eval Danila Fedorin 2026-06-30 23:21:00 -05:00
• 6c05e401c1 Document Program.lean Danila Fedorin 2026-06-29 10:42:01 -05:00
• fe5098095a Reorganize proofs to make 'Program' accessible to files in Language/ Danila Fedorin 2026-06-29 10:30:39 -05:00
• 59afbdaf71 Rename StateInterp to match the style of the rest of the codebase Danila Fedorin 2026-06-29 10:00:01 -05:00
• 490c472d22 Start documenting FiniteMap.lean Danila Fedorin 2026-06-29 08:59:51 -05:00
• d1a11a9b2c Use alpha and beta for FiniteMap type variables Danila Fedorin 2026-06-29 08:59:37 -05:00
• 2598df690c Slightly tweak AboveBelow proofs Danila Fedorin 2026-06-29 08:16:55 -05:00
• 47d54f5b4b Further simplify proofs in AboveBelow Danila Fedorin 2026-06-28 15:01:24 -05:00
• 8fa822b2e6 Improve performance by caching CFG building Danila Fedorin 2026-06-28 14:39:14 -05:00
• d66a7d0e3e Clean up and document AboveBelow Danila Fedorin 2026-06-28 14:31:27 -05:00
• 778e974dfb Prove that analysis results apply to all states, not just the final one Danila Fedorin 2026-06-28 14:24:46 -05:00
• 319fa272ac Switch Reaching analysis to use Finset for more efficiency Danila Fedorin 2026-06-28 09:46:54 -05:00
• 86bc33ee26 Register cases rules on lattice carriers for aesop automation Danila Fedorin 2026-06-27 20:01:01 -05:00
• 9e0702b5f5 Replace AboveBelow lattice-axiom case bashes with aesop Danila Fedorin 2026-06-27 19:49:13 -05:00
• 445187837c Add Trace.concat notation and apply at call sites Danila Fedorin 2026-06-27 19:45:45 -05:00
• 1a49689edc Apply aesop to reduce proofs Danila Fedorin 2026-06-27 19:30:01 -05:00
• b1b3b0d2fe Add more documentation Danila Fedorin 2026-06-27 19:20:23 -05:00
• 379438ec17 Add more documentation Danila Fedorin 2026-06-27 18:52:41 -05:00
• 1120e01605 Add some documentation Danila Fedorin 2026-06-27 18:11:19 -05:00
• b6b30958aa Add proof of reaching definition analysis Danila Fedorin 2026-06-27 16:29:16 -05:00
• 5737805125 Remove maximal chain witness from FiniteHeightLattice Danila Fedorin 2026-06-26 15:04:18 -05:00
• e738eb4294 Usw OrderBot / OrderTop for lattice witnesses Danila Fedorin 2026-06-26 14:49:57 -05:00
• 6a6ed521ca Slightly tweak LICM implementation Danila Fedorin 2026-06-25 14:40:25 -05:00
• c38c10fe9e Add a sketch of loop invariant code motion Danila Fedorin 2026-06-25 14:30:07 -05:00
• c367f130cf Add tagging machinery to assign unique IDs to AST nodes Danila Fedorin 2026-06-25 14:29:37 -05:00
• a5f533d67a Use a direct N-way unzip instead of induction over product size Danila Fedorin 2026-06-26 11:54:34 -05:00
• c281d78d1d Add documentation for IterProd Danila Fedorin 2026-06-26 10:49:16 -05:00
• 1a843747bf Delete unused code and moved some lemmas into Lattice.lean Danila Fedorin 2026-06-26 10:17:25 -05:00
• 352e0bb8cc Fold Isomorphism module into Lattice.lean Danila Fedorin 2026-06-26 08:52:31 -05:00
• a12b6c0c3c Write more documentation Danila Fedorin 2026-06-25 19:36:14 -05:00
• cbad43efdc Make FiniteHeightLattice extend Lattice and derive Top/Bot Danila Fedorin 2026-06-25 18:42:28 -05:00
• acef0f202b Add titles to documented modules Danila Fedorin 2026-06-25 17:05:21 -05:00
• c2ad0db668 Update comments in Graph and make map be a Functor instance Danila Fedorin 2026-06-25 17:01:27 -05:00
• a5235f6fbc Add documentation to some modules. Danila Fedorin 2026-06-25 15:39:51 -05:00
• e2df847139 Adopt lemma as the default keyword Danila Fedorin 2026-06-25 13:59:08 -05:00
• 5c9c8ac55c Fix formatting nits in Lattice.lean and Unit.lean Danila Fedorin 2026-06-25 13:56:44 -05:00
• ec2e789d5c Spell out evalB as evalBasicStmt Danila Fedorin 2026-06-25 13:55:46 -05:00
• a3ecefd415 Rename IterProd instances off the inst* prefix Danila Fedorin 2026-06-25 13:55:00 -05:00
• 5ac881559d Switch FiniteMap Fin n -> L representation This helps automatically derive lattice laws for it Danila Fedorin 2026-06-25 13:28:30 -05:00
• c4e5747b6d Turn buildCfg into a method Danila Fedorin 2026-06-25 09:45:30 -05:00
• 341a0b80b4 Add computation lemmas on GGraphs + map to Graphs.lean Danila Fedorin 2026-06-25 09:25:35 -05:00
• 4506f7c242 Delete dead code from Base.lean Danila Fedorin 2026-06-25 08:56:31 -05:00
• 94278a6389 Add computational reaching-definitions analysis Danila Fedorin 2026-06-23 15:12:37 -05:00
• a721a8be8b Generalize graphs over their node content Danila Fedorin 2026-06-24 16:02:49 -05:00
• 9ab43b34ef Use mathlib definition of inverses for Isomorphism.lean Danila Fedorin 2026-06-24 14:30:00 -05:00
• 97a9150bf3 Simplify the strict-step extraction in LTSeries.exists_unzip Danila Fedorin 2026-06-24 14:22:24 -05:00
• 93f913a699 Clean up namespaces in the analysis framework Danila Fedorin 2026-06-24 13:54:37 -05:00
• 7fb9d9aa19 Clean up Lattice.lean's namespaces Danila Fedorin 2026-06-24 13:30:27 -05:00
• f23705a93e Add scoped quotation syntax for object-language programs Danila Fedorin 2026-06-23 14:17:11 -05:00
• b1dc725ced Apply some cleanups to Graphs.lean Danila Fedorin 2026-06-23 14:00:06 -05:00
• ed88f4ce94 Use 'interp' to add [[ bla ]] notation for analysis Danila Fedorin 2026-06-23 13:29:54 -05:00
• 8ce6e5e4e4 Have LatticeInterpretation extend Interp Danila Fedorin 2026-06-23 13:01:53 -05:00
• 6afa7df444 Remove unused plus/minus mono_left/mono_right projections Danila Fedorin 2026-06-23 12:42:53 -05:00
• 7f753a4f38 Delete more LLM-generated comments from the migration Danila Fedorin 2026-06-23 12:29:46 -05:00
• 21b2e3dd98 Rename longest_chain to longestChain for convention Danila Fedorin 2026-06-23 11:49:45 -05:00
• 5e0c002fd5 Delete 'Agda:' migration comments from Forward Danila Fedorin 2026-06-23 11:44:50 -05:00
• 20daf817e4 Clean up Sign correctness proofs Danila Fedorin 2026-06-23 11:44:33 -05:00
• 2044d4b2b6 Start working on notation for formalization Danila Fedorin 2026-06-23 10:23:44 -05:00
• 8c37a4c049 Lean: inline BoundedChains.no_longer into FixedHeight.bot_le Danila Fedorin 2026-06-22 18:46:58 -05:00
• 2ee32580a2 Lean migration cleanup: collapse FixedHeight struct into FiniteHeightLattice typeclass Danila Fedorin 2026-06-22 18:33:48 -05:00
• b16f14fdfd Lean migration: typeclass-based parameter passing, as in the Agda original 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