JoJoDeveloping

From Coq Require Import Nat List Extraction. 
Import ListNotations.

Definition EqDec (A:Type) := forall (a b : A), {a = b} + {a <> b}.
Existing Class EqDec.
Definition eq_dec {A : Type} `{EqDec A} : EqDec A := _.

(* Defining these is somewhat annoying since you need to prove their correctness at the same time. *)
Program Instance eq_dec_option {A} {H : EqDec A} : EqDec (option A) := fun a b => match a, b with
  None, None => left _

JoJoDeveloping

From iris.algebra Require Export ofe monoid cmra.
From iris.prelude Require Import options.
Locate pmap_omap.
Section restrict_validity.
  Definition restrictV (A : Type) (P : nat → A → Prop) := A.
  Local Instance restrictV_validN A P : ValidN (restrictV A P) := P.
  Local Instance restrictV_valid A P : Valid (restrictV A P) := λ a, ∀ n, P n a.

  Definition restrictV_cmra {A : cmra} PvalidN
  (* the new validity restricts the old one *)

JoJoDeveloping

From iris.prelude Require Import prelude.
From stdpp Require Import option fin_maps fin_map_dom fin_sets.
From stdpp Require Import strings pmap gmap.
From iris.prelude Require Import options.

Definition address := list nat.

Unset Elimination Schemes.
Inductive tree {X:Type} := Node  { data : X; children : gmap nat tree }.
Set Elimination Schemes.

JoJoDeveloping

// adapted from tiny_skia, see https://github.com/RazrFalcon/tiny-skia/blob/master/src/pixmap.rs#L121
extern "Rust" {
    pub fn miri_get_alloc_id(ptr: *const ()) -> u64;
    pub fn miri_print_borrow_state(alloc_id: u64, show_unnamed: bool);
    pub fn miri_pointer_name(ptr: *const (), nth_parent: u8, name: &[u8]);
    pub fn miri_run_provenance_gc();
}

pub fn gc() {
    unsafe { miri_run_provenance_gc() }

JoJoDeveloping

Require Import Coq.Lists.List.
Require Import Coq.Relations.Relation_Operators.
Require Import Coq.Wellfounded.Lexicographic_Product.
Require Import Coq.Arith.Wf_nat.
Require Import Arith.

Import ListNotations.

Require Import Coq.Init.Nat.
Require Import Lia.

JoJoDeveloping

From Coq Require Import Arith Lia List.

Definition UIP (T:Type) := forall (x y:T) (H1 H2 : x = y), H1 = H2.

Definition sigma {X:Type} {x y : X} (H : x=y) : y=x := match H in (_=z) return z=x with eq_refl _ => eq_refl end.
Definition tau {X:Type} {x y z: X} (H1 : x=y) : y=z -> x=z := match H1 in (_=w) return w=z->x=z with eq_refl _ => fun H => H end.

(* A hedberg function yields a constant path if both arguments are equal
   (i.e. the output path does not depend on the input path)
   Usually these are constructed using an equalitiy decider.

JoJoDeveloping

Require Import Arith Lia List Bool Eqdep_dec EqdepFacts.
From Undecidability.Shared.Libs.DLW 
  Require Import utils_tac utils_nat utils_list finite pos vec.
From Undecidability.Synthetic Require Import Definitions DecidabilityFacts EnumerabilityFacts ListEnumerabilityFacts ReducibilityFacts.
From Undecidability Require Import Shared.ListAutomation Shared.Dec.
From Undecidability Require Import Shared.Libs.PSL.Vectors.Vectors.
Import ListAutomationNotations.

Require Import Undecidability.MuRec.recalg.

JoJoDeveloping

From iris.base_logic Require Import invariants.
From iris.base_logic.lib Require Import mono_nat.
From iris.heap_lang Require Import lang primitive_laws notation.
From iris.prelude Require Import options.
From iris.proofmode Require Import tactics.
(* You might need to uncomment resource_algebras in your _CoqMakefile *)
From semantics.axiomatic Require Import invariant_lib ghost_state_lib hoare_lib ra_lib ipm resource_algebras.
From semantics.axiomatic.heap_lang Require Import adequacy proofmode primitive_laws.
From semantics.axiomatic.program_logic Require Import notation.

JoJoDeveloping

INFO:  JVM info: Oracle Corporation - 1.8.0_242 - 25.242-b08
INFO:  Adding File to context from classpath: /mnt/workfs/johannes/Minecraft/Forge/114/MCPConfig/build/libraries/net/minecraftforge/forgeflower/1.5.380.45/forgeflower-1.5.380.45.jar
INFO:  Adding Archive: /mnt/workfs/johannes/Minecraft/Forge/114/MCPConfig/build/libraries/net/minecraftforge/forgeflower/1.5.380.45/forgeflower-1.5.380.45.jar
INFO:    Loading Class: org/jetbrains/java/decompiler/struct/IDecompiledData.class
INFO:    Loading Class: org/jetbrains/java/decompiler/struct/StructMember.class
INFO:    Loading Class: org/jetbrains/java/decompiler/struct/match/MatchEngine.class
INFO:    Loading Class: org/jetbrains/java/decompiler/struct/match/MatchNode.class
INFO:    Loading Class: org/jetbrains/java/decompiler/struct/match/MatchEngine$1.class
INFO:    Loading Class: org/jetbrains/java/decompiler/struct/match/MatchNode$RuleValue.class
INFO:    Loading Class: org/jetbrains/java/decompiler/struct/match/IMatchable$MatchProperties.class

JoJoDeveloping

INFO:  JVM info: Oracle Corporation - 1.8.0_242 - 25.242-b08
INFO:  Adding File to context from classpath: /mnt/workfs/johannes/Minecraft/Forge/114/MCPConfig/build/libraries/net/minecraftforge/forgeflower/1.5.380.45/forgeflower-1.5.380.45.jar
INFO:  Adding Archive: /mnt/workfs/johannes/Minecraft/Forge/114/MCPConfig/build/libraries/net/minecraftforge/forgeflower/1.5.380.45/forgeflower-1.5.380.45.jar
INFO:    Loading Class: org/jetbrains/java/decompiler/struct/IDecompiledData.class
INFO:    Loading Class: org/jetbrains/java/decompiler/struct/StructMember.class
INFO:    Loading Class: org/jetbrains/java/decompiler/struct/match/MatchEngine.class
INFO:    Loading Class: org/jetbrains/java/decompiler/struct/match/MatchNode.class
INFO:    Loading Class: org/jetbrains/java/decompiler/struct/match/MatchEngine$1.class
INFO:    Loading Class: org/jetbrains/java/decompiler/struct/match/MatchNode$RuleValue.class
INFO:    Loading Class: org/jetbrains/java/decompiler/struct/match/IMatchable$MatchProperties.class