Andrea Lattuada utaal

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)

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;

Minimal hdr histogram implementation in rust

	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) = {

	#![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;

	# 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"


	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 \|\| {

	<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,