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