Hello, I am new to this community and just finish reading Logic Foundation & TAPL.
After reading these two books, I plan to prove something in my own field, system programming.
So I took a “intrusive list” implementation and hope to prove some property of it.
As it is related to memory, I decide to use a
FMapList to represent the memory.
Inductive LinkedList : Type := | node (self: nat) (n: nat). Definition memory : Type := M.t LinkedList.
self represents the address of the node itself while
n represents the address of next node.
However, I found my proof is some sort of hard and I cannot even build a
len function for my list as it may result in infinite loop.
I have defined three basic operations and prove some basic property of them.
But I doubt whether this is the right way to approach such a problem.
So I wonder is there a more formal/approachable way to deal with memory/low-level stuff in Coq?
Here is my complete code.
The code is in Rust and the verification is in Coq.
I tried a few auto converting tools for Rust. They seems rather uncompatible to low level code like
Thanks in advance for your help.
Some snippet of my verification.
Definition is_empty (m: memory) (l: LinkedList) : bool := match l with node _ n => match (find n m) with | Some _ => false | None => true end end. Definition push (m: memory) (l: LinkedList) (item: nat) := match l with | node s n => ((add item (node item n) m), node s item) end. Definition pop (m: memory) (l: LinkedList) := match (is_empty m l) with | true => None | false => match l with | node s n => Some n end end. Theorem pop_on_non_empty: forall (m: memory) (l: LinkedList) (item: nat), is_empty m l = false -> pop m l <> None. Proof. Admitted. Theorem non_empty_after_push: forall (m: memory) (l: LinkedList) (item: nat), let res := (push m l item) in is_empty (fst res) (snd res) = false. Proof. Admitted.