# Can the seL4 proofs handle recursive functions?

**URL:** <https://sel4.discourse.group/t/can-the-sel4-proofs-handle-recursive-functions/96>\
**Category:** Verification\
**Created:** [June 14, 2019, 2:06pm UTC](https://sel4.discourse.group/t/can-the-sel4-proofs-handle-recursive-functions/96 "2019-06-14T14:06:46Z")\
**Posts on this page:** 4\
**Page:** 1

<div class="post-metadata">

**Author:** ![robert.vanvossen](https://yyz2.discourse-cdn.com/free1/user_avatar/sel4.discourse.group/robert.vanvossen/32/19_2.png) [@robert.vanvossen](https://sel4.discourse.group/u/robert.vanvossen)\
**Post date:** [June 14, 2019, 2:06pm UTC](https://sel4.discourse.group/t/can-the-sel4-proofs-handle-recursive-functions/96/1 "2019-06-14T14:06:46Z")

</div>

We are writing some code for the seL4\_libs where a recursive function makes the most sense. I know that part of the code is not verified, but it got me curious as to whether the seL4 proofs could handle recursive functions.

---

<div class="post-metadata">

**Author:** ![gerwin.klein](https://yyz2.discourse-cdn.com/free1/user_avatar/sel4.discourse.group/gerwin.klein/32/46_2.png) [@gerwin.klein](https://sel4.discourse.group/u/gerwin.klein)\
**Post date:** [June 14, 2019, 10:12pm UTC](https://sel4.discourse.group/t/can-the-sel4-proofs-handle-recursive-functions/96/2 "2019-06-14T22:12:37Z")

</div>

It can, yes.

The more abstract proof levels in Isabelle/HOL make natural use of recursion all the time (lists etc), and the C level also supports recursion. There is even an in-kernel function that is nominally recursive that makes use of that; the maximum recursion depth in that case is only 3, but it looks as recursive to the verification environment as a “real” recursive function.

---

<div class="post-metadata">

**Author:** ![Jack.Chen](https://avatars.discourse-cdn.com/v4/letter/j/c68b51/32.png) [@Jack.Chen](https://sel4.discourse.group/u/Jack.Chen)\
**Post date:** [June 27, 2023, 6:54am UTC](https://sel4.discourse.group/t/can-the-sel4-proofs-handle-recursive-functions/96/3 "2023-06-27T06:54:52Z")

</div>

I’m coming back to this thread to confirm the maximum depth of recursion currently within the seL4 microkernel. **I haven’t found a recursion of depth 3 mentioned by Gerwin.**

> [@gerwin.klein](#):
>
> the maximum recursion depth in that case is only 3

The obvious one is the recursive deletion of a container (CNode/TCB), which I believe has a maximum recursive depth of **1** :  
_cteDelete → finaliseSlot → reduceZombie → cteDelete → finaliseSlot → reduceZombie → cteSwapForDelete (breaks recursion)_

Also mentioned in the [Blackham\_SCRH\_11](https://trustworthy.systems/publications/nicta_full_text/4863.pdf) paper,

> “The formal proof guarantees termination, proving that the functions do not call themselves more than once.”

meaning the recursive depth does not exceed 1.

So where is the recursion with a depth of 3?

---

<div class="post-metadata">

**Author:** ![gerwin.klein](https://yyz2.discourse-cdn.com/free1/user_avatar/sel4.discourse.group/gerwin.klein/32/46_2.png) [@gerwin.klein](https://sel4.discourse.group/u/gerwin.klein)\
**Post date:** [June 28, 2023, 8:06am UTC](https://sel4.discourse.group/t/can-the-sel4-proofs-handle-recursive-functions/96/4 "2023-06-28T08:06:32Z")

</div>

It is perfectly possible that the depth in C is just 1 – some of the functions are consolidated in the spec into one larger function, so the depth there is larger (e.g. reduceZombie is just a case of cteDelete in the spec – that is probably all there is, because that gets you to 3).