# Verify a intrusive linked list is memory safe with Coq

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.

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`

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.

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.
``````

The next step is probably to learn about Hoare Logic (SF Vol. 2: Programming Languages Foundations, first 4 chapters), and Separation Logic (SF Vol. 6).

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 .

Indeed, Coq functions are total, while you are trying to program in a partial language. You need to construct a model of your intended programming language (Rust) that accounts for partiality. You can take inspiration from the Imp language introduced in Logical Foundations.

Thanks a lot.
I now know what is wrong with my attempt.
I tried finding some tools translating Rust to a more easily verifable form to avoid implementing Rust on my own.
I guess I have to.
Thanks again.

Are you aware of the work around Rust in Coq? I second @Lyxia’s recommendation to read Software Foundations, but it might still be interesting to have a look at the RustBelt project, with RustBelt: Securing the Foundations of the Rust Programming Language (POPL 2018) being the initial paper and Ralf Jung’s PhD thesis probably having longer explanations.

Yes, I am aware of that.
Actually I tried MIRAI and Electrosis, but they lack the support of low level features such as returning a raw reference.
These low level access is crucial to system programming.
Now I am considering may be C would be a better fit to translate into Coq XD.