Skip to content

Instantly share code, notes, and snippets.

View Nadrieril's full-sized avatar

Nadrieril Nadrieril

  • Inria
  • Paris, France
  • 05:24 (UTC +02:00)
  • X @nadrieril
View GitHub Profile
@Nadrieril
Nadrieril / demo.json
Created May 13, 2025 15:32
JSON GOSIM chaorn demo
This file has been truncated, but you can view the full file.
{
"charon_version": "0.1.88",
"translated": {
"crate_name": "test_crate",
"options": {
"ullbc": false,
"lib": false,
"bin": null,
"mir_promoted": false,
@Nadrieril
Nadrieril / pattern-opsem.md
Last active April 27, 2025 20:23
Operational semantics of patterns in Rust (working model)

Patterns have a funky place in the efforts to specify/formalize the semantics of Rust code: as far as I know these efforts (like MiniRust) center on formalizing the meaning of MIR, the main intermediate representation of the Rust compiler. But patterns don't exist in MIR; they've already been translated into discriminant reads and switches.

Hence there's currently very little in the way of describing the precise semantics of patterns. In my capacity as the contributor most involved with everything pattern-related, I'd like to share my working model.

This is not exactly what's implemented today, instead that's what I'd like to become the normative specification. See at the end for differences.

Setting

Patterns can be used in the following syntactic locations:

  • match expressions;
@Nadrieril
Nadrieril / closed_ghost_cell.rs
Last active January 31, 2025 13:42
API to pack a GhostCell-based datastructure to hide the brand
use std::{
collections::HashSet,
marker::PhantomData,
rc::{Rc, Weak},
};
use ghost_cell::{GhostCell, GhostToken};
pub trait GhostCellContainer {
type Open<'brand>;
@Nadrieril
Nadrieril / omega.rs
Last active January 22, 2025 13:16
Fun unsoundness in Rust
//! Riffing on a recently-discovered unsoundness in rustc due to the type system not having a
//! termination checker: https://github.com/rust-lang/rust/issues/135011.
//! Based on https://github.com/rust-lang/rust/issues/135011#issuecomment-2577585549.
//!
//! The core of the issue is that the type system does not enforce termination of its terms. We
//! can use a classic trick to construct a non-terminating associated type that works as a
//! proof of a trait bound of our choice. We use this to prove any two types equal.
/// Type-level equality. Using two separate traits for clarity.
trait IdA {
@Nadrieril
Nadrieril / patterns.rs
Created December 5, 2024 10:20
Lesser-known rust pattern-matching features
// Destructuring assignment
fn fibonacci(n: u64) -> u64 {
let mut a = 1;
let mut b = 1;
for _ in 0..n {
(a, b) = (a + b, a);
}
b
}
@Nadrieril
Nadrieril / buffer_allocator.rs
Last active August 14, 2024 21:34
`&mut [u8]` as `Allocator`
#![feature(allocator_api)]
#![feature(slice_ptr_get)]
#![feature(strict_provenance)]
use core::{alloc::Layout, ptr::NonNull, sync::atomic::AtomicUsize};
use std::alloc::{AllocError, Allocator};
use std::marker::PhantomData;
/// Allocator backed by a provided buffer. Once the buffer is full, all subsequent allocations fail.
pub struct BufferAllocator<'a> {
/// The backing buffer.
@Nadrieril
Nadrieril / iterator_visitor.rs
Last active June 15, 2024 15:29
This is a sketch written for https://github.com/nikis05/derive-visitor/issues/13 of a visitor interface that is polled externally
// I wrote https://github.com/Nadrieril/type-walker to replace this
@Nadrieril
Nadrieril / arbitrary_self_types.rs
Created November 23, 2023 22:35
Test the method selection algorithm of `arbitrary_self_types`
#![feature(arbitrary_self_types)]
#![allow(dead_code)]
macro_rules! assert_priority {
(prefer method on $expected:ident given: $($rest:tt)*) => {
{
// Define one wrapper per entry, with any `foo` methods specified.
assert_priority!(@define_ptrs, $($rest)*);
// This is the `P<Q<...>>` type we want to play with.
type Combined = assert_priority!(@combined_type, $($rest)*);
@Nadrieril
Nadrieril / x.sh
Last active January 8, 2021 19:59
My `x.py` for rustc development
#!/usr/bin/env bash
# Wrapper around `x.py`. Assumes it's being run from the root of the rustc repo.
RUSTC_REPO="$(realpath "$PWD")"
RUSTC_PERF_REPO="$RUSTC_REPO/../rustc-perf"
X_PY="$RUSTC_REPO/x.py"
RUSTC="$RUSTC_REPO/build/x86_64-unknown-linux-gnu/stage1/bin/rustc"
RUSTFMT="$RUSTC_REPO/build/x86_64-unknown-linux-gnu/stage0/bin/rustfmt"
cd $RUSTC_REPO || exit
@Nadrieril
Nadrieril / shell.nix
Last active May 6, 2025 10:11
Building LineageOS on NixOS
# I used this shell.nix to build LineageOS 13.0 for my maguro (Samsung Galaxy Nexus GSM) phone
# The build instructions for normal Linuxes are here: https://wiki.lineageos.org/devices/maguro/build
# For NixOS, follow those instructions but skip anything related to installing packages
# Detailed instructions:
# cd into an empty directory of your choice
# copy this file there
# in nix-shell:
# $ repo init -u https://github.com/LineageOS/android.git -b cm-13.0
# $ repo sync
# $ source build/envsetup.sh