---
# System prepended metadata

title: '2021.06.08: RefinedC'
tags: [reading]

---

# 2021.06.08: RefinedC

[Sammler, Lepigre, Krebbers, Memarian, Dreyer, Garg, [2021] "RefinedC: Automating the Foundational Verification of C Code with Refined Ownership Types"](https://plv.mpi-sws.org/refinedc/)

_presenter: Nikita_

* adds refinement types to C
* both foundational & automated reasoning
* based on Iris
* syntax looks inspired by Rust

## Hackernews discussion

https://news.ycombinator.com/item?id=27265329

## 1. Introduction

* Memory allocator example
* Uses new C2x annotation syntax
* Embeds Iris/Coq code into annotations
* Several parts:
  * Lithium - decidable assertions
  * Caesium - deep embedding of C 

## 2. RefinedC by Example

* What is `uninit`? 
  * Rust-style tag for indicating that the client should initialize the memory? 
* Ownership types: (de)allocation and write access
  * line 7: acquire ownershop, line 9: release ownership
* What is `own p`?
  * https://gitlab.mpi-sws.org/iris/refinedc/-/blob/master/ANNOTATIONS.md#constraints
* Embed `null`s into optional types (so you can't pass unguarded `null`)
* Another allocator for showing lists and loop invariants 

## 3. RefinedC Front End and Caesium

## 4. RefinedC Types and Specifications

## 5. Lithium: Separation Logic Programming

* Decidable fragment of separation logic, **no backtracking**
* Split goal into left and right subterms (restricted on the left)
* Can be extended?
* Not complete, so the automation argument is a bit weak - for some programs you'd still need to manually work out additional annotations

## 6. Examples of RefinedC Typing Rules

## 7. Evaluation and Case Studies

* Cheating with overhead? They ignore the Spec
* No numbers on running time for checking

## 8. Related Work

> uses Mezzo-like [71] alias types [83,101] instead of Rust’s lifetimes and mutable references

## 9. Limitations and Future Work

* not full C (floats/casts)
* liveness (transfinite Iris)
