Skip to content

Instantly share code, notes, and snippets.

View utaal's full-sized avatar

Andrea Lattuada utaal

View GitHub Profile
module Pulse.Lib.DoublyLinkedList
open Pulse.Lib.Pervasives
open Pulse.Lib.Stick.Util
open FStar.List.Tot
module T = FStar.Tactics
module I = Pulse.Lib.Stick.Util
module FA = Pulse.Lib.Forall.Util
noeq
type node (t:Type0) = {
@utaal
utaal / ghost_proto.rs
Last active May 6, 2024 12:26
Prototype of `GhostDeref` trait at the type level
#![allow(dead_code)]
#![allow(unused_variables)]
trait GhostDeref {
/* ghost */ fn ghost_deref(self) -> Self::Target;
type Target;
}
struct Snap<T> { p: core::marker::PhantomData<(T,)>, }
use vstd::prelude::*;
verus! {
use vstd::ptr::PPtr;
// ** each executable line is preceded by a comment with the equivalent regular rust unsafe code **
fn main() {
// let ptr = std::alloc::alloc(std::alloc::Layout::new:: <u64>()) as *mut u64;
@utaal
utaal / Goals.md
Last active April 13, 2021 19:24
iron language design

This fork of Rust is for developing an experimental verification framework for Rust-like code. The main goal is to verify full functional correctness of low-level systems code, building on ideas from existing verification frameworks like Dafny, Boogie, F*, VCC, Prusti, Cogent, Coq, and Isabelle/HOL.

Goals:

  • provide a pure mathematical language for expressing specifications (like Dafny, F*, Coq, Isabelle/HOL)
  • provide a mathematical language for expressing proofs (like Dafny, F*, Coq, Isabelle/HOL) based exclusively on classical logic (like Dafny)
  • provide a low-level, imperative language for expressing executable code (like VCC), based on Rust (like Prusti)
# errors
# move_errors
move_errors "Mid(bb2[4])" "mp1"
# subset_errors
# restricts
# restricts_anywhere
# origin_live_on_entry
origin_live_on_entry "Start(bb0[0])" "\'_#0r"
origin_live_on_entry "Start(bb0[0])" "\'_#1r"
origin_live_on_entry "Mid(bb0[0])" "\'_#0r"
@utaal
utaal / ble_frame_collisions.md
Last active April 23, 2020 09:11
BLE advertisement frame successful exchange rate in scenarios with many advertising devices

This is based on my partial knowledge of radio networks, and on very incomplete knowledge of the BLE stack.

AFAIK BLE scans in short intervals on one of 3 channels. With >50 devices in advertisement mode it may be hard to get non-colliding frames to the receiver.

  • I don’t think Bluetooth LE was designed to have hundreds of devices in discoverable mode sending out garbage identity frames.
  • Increasing the radio wake time may not be a solution either because you end up with flat batteries too quickly.

Protocol

  • 3 advertising channels;
@utaal
utaal / grant_data_race.rs
Created April 14, 2020 14:04
spsc-bip-buffer potential data race
fn grant_data_race() {
for i in 0..128 {
let (mut writer, mut reader) = bip_buffer_from(vec![0u8; 16].into_boxed_slice());
let mut reservation = writer.reserve(8);
let sender = std::thread::spawn(move || {
writer.reserve(8).as_mut().expect("reserve").copy_from_slice(&[10, 11, 12, 13, 14, 15, 16, i]);
});
reservation.as_mut().expect("reserve").copy_from_slice(&[1, 2, 3, 4, 5, 6, 7, 8]);
let receiver = std::thread::spawn(move || {
@utaal
utaal / doop-graph.html
Created May 27, 2019 08:57
Frank's epic doop dataflow
<body>
<style>
body, text {
font-weight: 300;
font-family: "Helvetica Neue", Helvetica, Arial, sans-serf;
font-size: 14px;
}
#graph {
width: 100%;
#!/usr/bin/env python3
import experiments
def experiment_setup(experiment_name, n, w, **config):
experiments.ensuredir(experiment_name)
return "{}/{}_n={}_w={}_{}".format(
experiments.experdir(experiment_name),
experiment_name,
n,