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

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 

Definition push (m: memory) (l: LinkedList) (item: nat) :=
  match l with
  | node s n => ((add item (node item n) m), node s item)

Definition pop (m: memory) (l: LinkedList) :=
  match (is_empty m l) with
  | true => None
  | false => match l with
             | node s n => Some n

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.

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.