Danila Fedorin DanilaFe
0 Followers · 0 Following
Repositories
11
 Projects Packages Code Public Activity Starred Repositories
DanilaFe pushed to main at DanilaFe/agda-spa 2024-04-30 22:15:54 -07:00
3859826293 Define interpretation of the sign lattice
be50c76cb1 Add more higher-order primitives
112a5087ef Tentative start on proving correctness
ccb7abc501 Remove unused code from Utils
Compare 4 commits »
DanilaFe pushed to main at DanilaFe/agda-spa 2024-04-29 21:28:45 -07:00
91b5d108f6 Simplify proofs about 'loop' using concatenation lemma
c574ca9c56 Prove that graphs build by buildCfg are sufficient
Compare 2 commits »
DanilaFe pushed to main at DanilaFe/agda-spa 2024-04-28 15:16:35 -07:00
bbfba34e05 Prove another (simple) case
aec15573fc Add properties of end-to-end traces on loops
b4d395767d Simplify operations used for constructing graphs
Compare 3 commits »
DanilaFe pushed to main at DanilaFe/agda-spa 2024-04-28 12:25:19 -07:00
07550bc214 Prove 'sufficiency' for if-else.
9366ec4a97 Allow promoting end-to-end traces too
0fb884eb07 Use implicit arguments for more things
6b44ac1feb Make graph arguments implicit where possible
Compare 4 commits »
DanilaFe pushed to main at DanilaFe/agda-spa 2024-04-28 00:27:06 -07:00
69a4e8eb5c Add some helpers and rewrite code
4fee16413a Define end-to-end path concatenation and prove one more case
316e56f2bc Dip toes into creating end-to-end traces
ab40a27e78 Formulate correctness of buildCfg using end-to-end traces
f555947184 Promote traces through loop
Compare 8 commits »
DanilaFe pushed to main at DanilaFe/agda-spa 2024-04-25 23:22:17 -07:00
f2b8084a9c Delete code that won't be used for this approach
c00c8e3e85 Use different graph operations to implement construction
Compare 2 commits »
DanilaFe pushed to main at DanilaFe/agda-spa 2024-04-20 21:42:53 -07:00
b134c143ca Start working on proving 'sufficiency'
e218d1b7a3 Add formalization of 'traces through graph'
6e3f06ca5d Add a new 'properties' module
54b11d21b0 Start working on proving facts about graph construction
f3e0d5f2e3 Use 'data' instead of aliases to prove reasoning properties
Compare 6 commits »
DanilaFe pushed to main at Everything-I-Know.../bergamot-elm 2024-04-20 14:10:26 -07:00
14b63fccc2 Revert "Reduce gas for proof search"
DanilaFe pushed to main at Everything-I-Know.../bergamot-elm 2024-04-20 14:08:33 -07:00
6a952f8a15 Reduce gas for proof search
DanilaFe pushed to main at DanilaFe/agda-spa 2024-04-13 23:44:33 -07:00
2f91ca113e Make 'MonotonicPredicate' into another typeclass
7571cb7451 Extract 'monotonic state' into its own module
fc27b045d3 Remove nested module from Graphs
Compare 3 commits »
DanilaFe pushed to main at DanilaFe/agda-spa 2024-04-13 18:43:00 -07:00
de956cdc6a Split the Language file into modules
DanilaFe pushed to main at DanilaFe/agda-spa 2024-04-13 15:30:32 -07:00
7ed7f20227 Add missing edge
163108b9b3 Add precedence to some language constructs
Compare 2 commits »
DanilaFe pushed to main at DanilaFe/agda-spa 2024-04-13 14:13:53 -07:00
8dc5c40eae Get everything compiling
44f04e4020 Get forward analysis working again
4fe0d147fa Adjust 'Program' to have a graph and basic blocks
ba1c9b3ec8 Remove sketch if proof since the proof is done
b6e357787f Add proof about 'both' and pairing
Compare 10 commits »
DanilaFe pushed to main at DanilaFe/agda-spa 2024-04-08 22:49:57 -07:00
3e2719d45f Turn old proof into a hole to clean up later.
78252b6c9e Add proof of node preservation for adding edges.
Compare 2 commits »
DanilaFe pushed to main at DanilaFe/agda-spa 2024-04-08 22:21:45 -07:00
85fdf544b9 Translate informal proof of (node) transitivity into formal one.
DanilaFe pushed to main at DanilaFe/agda-spa 2024-04-08 00:30:58 -07:00
4f14a7b765 Successfully prove that monotonic updates preserve existing indices
bc5b4b7d9e Explicitly write metas for missing functions
520b2b514c Clear up vector reindexing
f7ac22257e Beat head against the vector-cast wall.
b72ad070ba Try using index-based comparisons
Compare 7 commits »
DanilaFe pushed to main at DanilaFe/agda-spa 2024-04-04 22:34:38 -07:00
b505063771 Start working on proofs of Graph-related things
844c99336a Intermediate commit: add while loops and start trying to formalize them.
Compare 2 commits »
DanilaFe pushed to main at DanilaFe/agda-spa 2024-03-24 12:11:10 -07:00
5d56a7ce2d Fix comments in Forward.agda
2e096bd64e Extract common parts of forward analyses into Forward.agda
1a7b2a1736 Adjust behavior of eval to not require constant 'k in vars' threading
Compare 3 commits »
DanilaFe pushed to master at Web-Projects/blog-static 2024-03-14 22:25:39 -07:00
c6e2ecb996 Add first section of Agda program analysis article
DanilaFe pushed to master at Web-Projects/blog-static 2024-03-13 16:04:33 -07:00
2130b00752 Narrow some of the tags