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.
where 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.
https://github.com/jwnhy/linkedlist/tree/main/src
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
unsafe
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.