# Verify a intrusive linked list is memory safe with Coq

**URL:** <https://discourse.rocq-prover.org/t/verify-a-intrusive-linked-list-is-memory-safe-with-coq/1585>\
**Category:** Using Rocq\
**Created:** [March 6, 2022, 1:38pm UTC](https://discourse.rocq-prover.org/t/verify-a-intrusive-linked-list-is-memory-safe-with-coq/1585 "2022-03-06T13:38:12Z")\
**Posts on this page:** 5\
**Page:** 1

<div class="post-metadata">

**Author:** ![jwnhy](https://sea1.discourse-cdn.com/flex001/user_avatar/discourse.rocq-prover.org/jwnhy/32/649_2.png) [@jwnhy](https://discourse.rocq-prover.org/u/jwnhy)\
**Post date:** [March 6, 2022, 1:38pm UTC](https://discourse.rocq-prover.org/t/verify-a-intrusive-linked-list-is-memory-safe-with-coq/1585/1 "2022-03-06T13:38:12Z")

</div>

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.

```auto
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](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.

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

```

---

<div class="post-metadata">

**Author:** ![Lyxia](https://sea1.discourse-cdn.com/flex001/user_avatar/discourse.rocq-prover.org/lyxia/32/75_2.png) [@Lyxia](https://discourse.rocq-prover.org/u/Lyxia)\
**Post date:** [March 6, 2022, 10:04pm UTC](https://discourse.rocq-prover.org/t/verify-a-intrusive-linked-list-is-memory-safe-with-coq/1585/2 "2022-03-06T22:04:47Z")

</div>

The next step is probably to learn about Hoare Logic ([SF Vol. 2: Programming Languages Foundations, first 4 chapters](https://softwarefoundations.cis.upenn.edu/plf-current/index.html)), and Separation Logic ([SF Vol. 6](https://softwarefoundations.cis.upenn.edu/slf-current/index.html)).

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

---

<div class="post-metadata">

**Author:** ![jwnhy](https://sea1.discourse-cdn.com/flex001/user_avatar/discourse.rocq-prover.org/jwnhy/32/649_2.png) [@jwnhy](https://discourse.rocq-prover.org/u/jwnhy)\
**Post date:** [March 7, 2022, 2:07am UTC](https://discourse.rocq-prover.org/t/verify-a-intrusive-linked-list-is-memory-safe-with-coq/1585/3 "2022-03-07T02:07:50Z")

</div>

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.

---

<div class="post-metadata">

**Author:** ![yforster](https://sea1.discourse-cdn.com/flex001/user_avatar/discourse.rocq-prover.org/yforster/32/30_2.png) [@yforster](https://discourse.rocq-prover.org/u/yforster)\
**Post date:** [March 7, 2022, 9:05am UTC](https://discourse.rocq-prover.org/t/verify-a-intrusive-linked-list-is-memory-safe-with-coq/1585/4 "2022-03-07T09:05:20Z")

</div>

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](https://plv.mpi-sws.org/rustbelt/) project, with [RustBelt: Securing the Foundations of the Rust Programming Language (POPL 2018)](https://plv.mpi-sws.org/rustbelt/popl18/) being the initial paper and [Ralf Jung’s PhD thesis](https://www.ralfj.de/research/thesis.html) probably having longer explanations.

---

<div class="post-metadata">

**Author:** ![jwnhy](https://sea1.discourse-cdn.com/flex001/user_avatar/discourse.rocq-prover.org/jwnhy/32/649_2.png) [@jwnhy](https://discourse.rocq-prover.org/u/jwnhy)\
**Post date:** [March 7, 2022, 1:10pm UTC](https://discourse.rocq-prover.org/t/verify-a-intrusive-linked-list-is-memory-safe-with-coq/1585/5 "2022-03-07T13:10:19Z")

</div>

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.