Skip to content

Instantly share code, notes, and snippets.

View Blaisorblade's full-sized avatar

Paolo G. Giarrusso Blaisorblade

191 followers · 191 following
View GitHub Profile
@Blaisorblade
Blaisorblade / Makefile
Last active December 22, 2023 12:43
C++ compilation does not preserve abstraction
CXX := g++
CXXFLAGS := -std=c++11
prog: evil_client.o module.o
$(CXX) $(CXXFLAGS) -o $@ $^
# Redundant, but included for completeness
%.o: %.cpp
$(CXX) $(CXXFLAGS) -c -o $@ $^
@Blaisorblade
Blaisorblade / countable_setoid.v
Created August 4, 2023 11:40
stdpp countable setoids are LeibnizEquiv
From stdpp Require Import prelude countable ssreflect.
Section test.
Context `{CA : Countable A} `{!Equiv A} `{!Equivalence (≡@{A})}.
Goal Proper (equiv ==> eq) (encode (A := A)) -> LeibnizEquiv A.
Proof. intros HP x y H. apply: (inj encode). by rewrite H. Qed.
End test.
@Blaisorblade
Blaisorblade / iris_setoid_rewrite.v
Last active May 18, 2023 19:18
A sketch of Iris-internal setoid rewriting
(** Iris-internal setoid rewriting, theory. *)
Require Import iris.proofmode.proofmode.
(** * Notation for functions in the Iris scope. To upstream,
per https://gitlab.mpi-sws.org/iris/iris/-/issues/320. *)
Notation "'λI' x .. y , t" := (fun x => .. (fun y => t%I) ..)
(at level 200, x binder, y binder, right associativity,
only parsing) : function_scope.
Section with_prop.
@Blaisorblade
Blaisorblade / iris_tac.v
Created April 5, 2023 11:50
Automation over coq-iris's IPM/MoSeL: Demonstrate how to generate patterns programmatically for proof automation
Require Import iris.proofmode.proofmode.
Require Import iris.proofmode.intro_patterns.
Section foo.
Context {PROP : bi}.
Context (P R : PROP) (lem : P ⊢ P ∗ R).
Goal True. let x := intro_pat.parse "[A B]" in idtac x. Abort.
(* output: *)
(* [IList [[IIdent "A"; IIdent "B"]]]. *)
@Blaisorblade
Blaisorblade / 0 Non-Reproducible Coq Analysis.md
Last active January 25, 2023 01:12
New example of Coq non-reproducibility

Source file: theories/proofmode/cpp/heap_pred.v, only depends on https://github.com/bedrocksystems/BRiCk/.

The key change appears that d46b4e13047a81276314694ce9a04719-library.txt has two copies of thread_info:

0x0032::S:"thread_info"
...
0x0046::B:0[1]{0x0047}
0x0047::S:"thread_info"
@Blaisorblade
Blaisorblade / safe_per_rewriting.v
Created January 17, 2023 18:34
(*
An answer to https://coq.zulipchat.com/#narrow/stream/237977-Coq-users/topic/rewriting.20with.20PERs.
Instances PER_valid_l and PER_valid_r are optimized to be safest.
*)
From Coq Require Import Relations RelationClasses Setoid Morphisms.
Class ByEassumption (P : Prop) := {
by_eassumption : P
}.
@Blaisorblade
Blaisorblade / 71d94098174fd126280ab786a9d3fbef
Last active January 13, 2023 11:34
Coq non-reproducible builds of https://github.com/bedrocksystems/BRiCk/blob/b668f6d062d49deff9d0de27bbdb1df70dd9f0b8/theories/prelude/avl.v
@Blaisorblade
Blaisorblade / decide_True_broke.v
Last active December 16, 2022 08:05
Minimized problem with `rewrite decide_True` and ssreflect
(*
Tested with:
Coq 8.15.0, Iris dev.2022-01-24.0.72a4bd62.
Coq 8.16.0, Iris 4.0.0
*)
From iris.prelude Require Import prelude.
Lemma bar : (if decide (0 = 0) then 0 else 0) = 0.
Proof.
@Blaisorblade
Blaisorblade / ExtraSettings.tex
Created February 2, 2012 11:13
LaTeX listings: add support for Scala
% Other listings-related settings from
% http://lampsvn.epfl.ch/trac/scala/export/26099/scala-tool-support/trunk/src/latex/scaladoc.sty
% activate the language and predefine settings
\lstset{
language=Scala,%
xleftmargin=4mm,%
aboveskip=3mm,%
belowskip=3mm,%
fontadjust=true,%
columns=[c]fixed,%
@Blaisorblade
Blaisorblade / reflect_bool_decide.v
Created December 5, 2022 01:14
From stdlib's reflect to stdpp's Decision
Require Import iris.prelude.prelude.
Definition reflect_bool_decide b {P} : reflect P b -> Decision P.
refine (
match b with
| true => λ r, left _
| false => λ r, right _
end).
all: abstract by inversion r.
Defined.