Andrea Lattuada utaal
utaal
/ Pulse.Lib.DoublyLinkedList.fst
Last active
June 12, 2024 09:06
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| 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
/ ghost_proto.rs
Last active
May 6, 2024 12:26
Prototype of `GhostDeref` trait at the type level
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| #![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,)>, } |
utaal
/ verus_pptr_example.rs
Created
May 1, 2024 18:25
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| 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; |
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)
utaal
/ polonius_stdout
Created
June 29, 2020 12:42
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| # 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
/ 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;
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| 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 || { |
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| <body> | |
| <style> | |
| body, text { | |
| font-weight: 300; | |
| font-family: "Helvetica Neue", Helvetica, Arial, sans-serf; | |
| font-size: 14px; | |
| } | |
| #graph { | |
| width: 100%; |
utaal
/ arrange.py
Last active
June 26, 2018 08:53
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| #!/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, |
NewerOlder