Skip to content

Instantly share code, notes, and snippets.

View Blaisorblade's full-sized avatar

Paolo G. Giarrusso Blaisorblade

198 followers · 190 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 / 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 / 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 / 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 / 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.
@Blaisorblade
Blaisorblade / git-show-worktree-branches
Last active November 27, 2022 15:42
git: Display with git-show-branch branches that are checked out with worktrees.
#!/bin/sh
# Display with show-branch branches that are checked out with worktrees
git show-branch $(git worktree-branches)
@Blaisorblade
Blaisorblade / gist:0b312c4e76d01538f783b372052c876a
Last active November 3, 2022 21:03
Coq unification is up to convertibility but does not compute normal forms
Require Import ssreflect.
Fixpoint ackn (m : nat) (ack : nat -> nat) {struct m} :=
match m with
| O => ack 1
| S q => ack (ackn q ack)
end.
Fixpoint ack (n m : nat) {struct n} : nat :=
match n with
| O => S m