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-05-09 22:52:10 -07:00
3d2a507f2f Almost prove correctness
82027ecd04 Move predecessor computation into Graphs
734e82ff6d Wrap generated graphs to ensure entry and exit nodes have no extra edges
69d1ecebae Prove that the bottom map's valyes are all bottoms
b78cb91f2a Strengthen lemma about IterProd bottom to definition equality
Compare 14 commits »
DanilaFe pushed to main at DanilaFe/agda-spa 2024-05-08 23:38:41 -07:00
f0b0d51b48 Add unproven lemma about fold implication
8ff88f9f9e Move helper code into separate function
c1581075d3 Add more test programs
838aaf9c58 Start end-to-end proof of correctness
Compare 4 commits »
DanilaFe pushed to main at DanilaFe/agda-spa 2024-05-08 22:53:56 -07:00
4ac9dffa9b Prove that the var->lattice maps respect equality
3f5551d70c Add a lemma about the effect of joinAll
5837fdf19b Prove that 'updateAll' has preservation
4350919871 Add proof about setVariablesForState
7fe46b014c Slightly simplify evaluation code
Compare 12 commits »
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 »