[IL Semantics] Meta-theory in rocq

spectec/metatheory/Makefile

@@ -0,0 +1,5 @@
+default:
+	opam install .
+
+clean:
+	dune clean

spectec/metatheory/dune-project

@@ -0,0 +1,12 @@
+(lang dune 3.11)
+(using coq 0.8)
+(generate_opam_files true)
+
+(package
+  (name metatheory)
+  (synopsis "Spectec Wasm formalisation in Rocq")
+  (depends
+    (coq (>= 9.0))
+    (coq-mathcomp-ssreflect (and (>= 2.0.0) (<= 2.4.0)))
+  )
+)

spectec/metatheory/metatheory.opam

@@ -0,0 +1,23 @@
+# This file is generated by dune, edit dune-project instead
+opam-version: "2.0"
+synopsis: "Spectec Wasm formalisation in Rocq"
+depends: [
+  "dune" {>= "3.11"}
+  "coq" {>= "9.0"}
+  "coq-mathcomp-ssreflect" {>= "2.0.0" & <= "2.4.0"}
+  "odoc" {with-doc}
+]
+build: [
+  ["dune" "subst"] {dev}
+  [
+    "dune"
+    "build"
+    "-p"
+    name
+    "-j"
+    jobs
+    "@install"
+    "@runtest" {with-test}
+    "@doc" {with-doc}
+  ]
+]

spectec/metatheory/theories/dune

@@ -0,0 +1,7 @@
+(coq.theory
+  (name MetaSpectec)
+  (theories Stdlib mathcomp HB elpi elpi_elpi)
+  (package metatheory)
+  (flags -w -notation-overridden -w -abstract-large-number -w -ambiguous-paths
+         -w -unused-pattern-matching-variable -w -non-recursive
+         ))

spectec/metatheory/theories/env.v

@@ -0,0 +1,107 @@
+From Stdlib Require Import List String Reals.
+From mathcomp Require Import ssreflect ssrfun ssrnat ssrbool seq eqtype rat ssrint.
+Require Import Stdlib.FSets.FMapAVL.
+Require Import Stdlib.Structures.OrderedTypeEx.
+From MetaSpectec Require Import syntax.
+Import ListNotations.
+
+Declare Scope env_scope.
+Module StringMap := FMapAVL.Make(String_as_OT).
+
+Definition union {A}
+  (m1 m2 : StringMap.t A) : StringMap.t A :=
+  StringMap.fold (fun k v => StringMap.add k v) m1 m2.
+
+Definition singleton {A} (k : string) (v : A) : StringMap.t A :=
+  StringMap.add k v (StringMap.empty A).
+
+(* TYPING *)
+
+Definition var_def : Type := il_typ.
+Definition typ_def : Type := list il_param * list il_inst.
+Definition rel_def : Type := list il_param * il_typ * list il_rule.
+Definition definition_def : Type := list il_param * il_typ * list il_clause.
+
+(* Typing context *)
+
+Record il_env := {
+  VARS : StringMap.t var_def;
+  TYPS : StringMap.t typ_def;
+  DEFS : StringMap.t definition_def;
+  RELS : StringMap.t rel_def
+}.
+
+Definition empty_vars : StringMap.t var_def := StringMap.empty var_def.
+Definition empty_typs : StringMap.t typ_def := StringMap.empty typ_def.
+Definition empty_defs : StringMap.t definition_def := StringMap.empty definition_def.
+Definition empty_rels : StringMap.t rel_def := StringMap.empty rel_def.
+
+Definition env_empty : il_env := {| VARS := empty_vars; TYPS := empty_typs; DEFS := empty_defs; RELS := empty_rels |}.
+
+Definition append_env (e1 e2 : il_env) : il_env :=
+{|
+  VARS := union e1.(VARS) e2.(VARS);
+  TYPS := union e1.(TYPS) e2.(TYPS);
+  DEFS := union e1.(DEFS) e2.(DEFS);
+  RELS := union e1.(RELS) e2.(RELS) 
+|}.
+
+Definition single_var (x : il_id) (t : il_typ) : il_env :=
+  {| VARS := singleton x t; TYPS := empty_typs; DEFS := empty_defs; RELS := empty_rels |}.
+
+Fixpoint many_vars (xs : list (il_id * il_typ)) : il_env :=
+  match xs with
+  | [] => env_empty
+  | (x, t) :: xs' => append_env (single_var x t) (many_vars xs')
+  end
+.  
+
+Definition single_envtyp (x : il_id) (ps : list il_param) (insts : list il_inst) : il_env :=
+  {| VARS := empty_vars; TYPS := singleton x (ps, insts); DEFS := empty_defs; RELS := empty_rels |}.
+
+Definition single_def (x : il_id) (ps : list il_param) (rt : il_typ) (clauses : list il_clause) : il_env :=
+  {| VARS := empty_vars; TYPS := empty_typs; DEFS := singleton x (ps, rt, clauses); RELS := empty_rels |}.
+
+Definition single_rel (x : il_id) (ps : list il_param) (t : il_typ) (rules : list il_rule) : il_env :=
+  {| VARS := empty_vars; TYPS := empty_typs; DEFS := empty_defs; RELS := singleton x (ps, t, rules) |}.
+
+Notation "x [ i ]v = t" := (StringMap.find i (VARS x) = Some t) (at level 20) : env_scope.
+Notation "x [ i ]t = t" := (StringMap.find i (TYPS x) = Some t) (at level 20) : env_scope.
+Notation "x [ i ]d = t" := (StringMap.find i (DEFS x) = Some t) (at level 20) : env_scope.
+Notation "x [ i ]r = t" := (StringMap.find i (RELS x) = Some t) (at level 20) : env_scope.
+Notation "x @@ y" := (append_env x y) (at level 20) : env_scope.
+
+Record store := {
+  S_TYPS : StringMap.t typ_def;
+  S_DEFS : StringMap.t definition_def;
+  S_RELS : StringMap.t rel_def
+}.
+
+Definition store_to_env (s : store) : il_env :=
+  {| VARS := empty_vars; TYPS := s.(S_TYPS); DEFS := s.(S_DEFS); RELS := s.(S_RELS) |}.
+
+Definition env_to_store (e : il_env) : store :=
+  {| S_TYPS := e.(TYPS); S_DEFS := e.(DEFS); S_RELS := e.(RELS) |}.
+
+Fixpoint composeenvs (envs : list il_env) : il_env :=
+  match envs with
+  | [] => env_empty
+  | e1 :: es => append_env e1 (composeenvs es)
+  end
+.
+
+Definition tupenv (t : il_typ) : il_env :=
+  match t with
+  | TupT tups => composeenvs (List.map (fun '(x, t) => single_var x t) tups)
+  | _ => env_empty
+  end
+.
+
+Fixpoint paramenv (ps : list il_param) : il_env :=
+  match ps with
+  | [] => env_empty
+  | ExpP x t :: ps' => append_env (single_var x t) (paramenv ps')
+  | TypP x :: ps' => append_env (single_envtyp x [] []) (paramenv ps')
+  | DefP x ps' rt :: ps'' => append_env (single_def x ps' rt []) (paramenv ps'')
+  end
+. 

spectec/metatheory/theories/numerics.v

@@ -0,0 +1,166 @@
+From Stdlib Require Import List String.
+From mathcomp Require Import all_ssreflect all_algebra ssrnat ssrint.
+Import GRing.Theory.
+From MetaSpectec Require Import syntax.
+
+Coercion absz : int >-> nat.
+
+Coercion ratz: int >-> rat.
+
+(* Booleans *)
+
+Definition boolun (op : boolunop) (b : bool) : bool :=
+  match op with
+  | NotOp => negb b
+  end
+.
+
+Definition boolbin (op : boolbinop) (b1 b2 : bool) : bool :=
+  match op with
+  | AndOp => b1 && b2
+  | OrOp => b1 || b2
+  | ImplOp => b1 ==> b2
+  | EquivOp => b1 ==> b2 && b2 ==> b1
+  end
+.
+
+Definition iszero (x : il_num) : bool := 
+  match x with
+  | NatE n => n == 0%nat
+  | IntE i => i == 0%R
+  | RatE r => r == 0%R
+  | RealE r => r == 0%R
+  end
+.
+
+Definition isone (x : il_num) : bool := 
+  match x with
+  | NatE n => n == 1%nat
+  | IntE i => i == 1%R
+  | RatE r => r == 1%R 
+  | RealE r => r == 1%R
+  end
+.
+
+Definition isneg (x : il_num) : bool :=
+  match x with
+  | NatE n => false
+  | IntE i => (i < 0)%R
+  | RatE r => (r < 0)%R 
+  | RealE r => (r < 0)%R
+  end
+.
+
+Definition option_map {α β : Type} (f : α -> β) (x : option α) : option β :=
+	match x with
+  | Some x => Some (f x)
+  | _ => None
+	end.
+
+Definition option_join {α : Type} (x : option (option α)) : option α :=
+  match x with
+  | Some None => None
+  | None => None
+  | Some (Some x') => Some x'
+  end.
+
+(* Numerics *)
+
+Definition rat_to_int (x : rat) : option int :=
+  if isone (IntE (denq x)) then Some (numq x) else None
+.
+
+Definition int_to_nat_num (x : int) : option il_num :=
+  if (x >= 0)%R then Some (NatE x) else None.
+
+Definition to_nat (x : R) : nat :=
+  (Num.floor x).
+
+Definition rat_to_R (q : rat) : R :=
+  ((numq q)%:~R / (denq q)%:~R)%R.
+
+(* TODO finish some of the conversions - especially for reals *)
+Definition numcvt (nt : numtyp) (val : il_num) : option il_num :=
+  match nt, val with
+  | NatT, NatE n => Some (NatE n)
+  | NatT, IntE i => int_to_nat_num i
+  | NatT, RatE r => let opt := rat_to_int r in
+    option_join (option_map (fun i => int_to_nat_num i) opt)
+  | NatT, RealE r => Some (NatE (to_nat r))
+  | IntT, NatE n => Some (IntE n)
+  | IntT, IntE i => Some (IntE i)
+  | IntT, RatE r => if isone (IntE (denq r)) then Some (IntE (numq r)) else None
+  | IntT, RealE r => Some (IntE (Num.floor r))
+  | RatT, NatE n => Some (RatE (n%:Q))
+  | RatT, IntE i => Some (RatE (i%:Q))
+  | RatT, RatE r => Some (RatE r)
+  (* TODO think of a better way to cvt real to rational *)
+  | RatT, RealE r => Some (RatE (Num.floor r)%:Q)
+  | RealT, NatE n => Some (RealE (n%:R))
+  | RealT, IntE i => Some (RealE (i%:R))
+  | RealT, RatE r => Some (RealE (rat_to_R r))
+  | RealT, RealE r => Some (RealE r)
+  end
+.
+
+Definition numun (op : numunop) (val : il_num) : option il_num :=
+  match op, val with
+  | PlusOp, n => Some n
+  | MinusOp, NatE n => Some (IntE (0 - n%:R)%R) 
+  | MinusOp, IntE i => Some (IntE (0 - i)%R)
+  | MinusOp, RatE r => Some (RatE (0 - r)%R)
+  | MinusOp, RealE r => Some (RealE (0 - r)%R)
+  end
+.
+
+Definition numbin (op : numbinop) (val1 val2 : il_num) : option il_num :=
+  match op, val1, val2 with
+  | AddOp, NatE n1, NatE n2 => Some (NatE (n1 + n2)%nat)
+  | AddOp, IntE i1, IntE i2 => Some (IntE (i1 + i2)%R)
+  | AddOp, RatE r1, RatE r2 => Some (RatE (r1 + r2)%R)
+  | AddOp, RealE r1, RealE r2 => Some (RealE (r1 + r2)%R)
+  | SubOp, NatE n1, NatE n2 => if (n1 >= n2)%nat then Some (NatE (n1 - n2)%nat) else None
+  | SubOp, IntE i1, IntE i2 => Some (IntE (i1 - i2)%R)
+  | SubOp, RatE r1, RatE r2 => Some (RatE (r1 - r2)%R)
+  | SubOp, RealE r1, RealE r2 => Some (RealE (r1 - r2)%R)
+  | MulOp, NatE n1, NatE n2 => Some (NatE (n1 * n2)%nat)
+  | MulOp, IntE i1, IntE i2 => Some (IntE (i1 * i2)%R)
+  | MulOp, RatE r1, RatE r2 => Some (RatE (r1 * r2)%R)
+  | MulOp, RealE r1, RealE r2 => Some (RealE (r1 * r2)%R)
+  | DivOp, NatE n1, NatE n2 => if negb (iszero val2) then Some (NatE (Nat.div n1 n2)) else None
+  | DivOp, IntE i1, IntE i2 => if negb (iszero val2) then Some (IntE (divz i1 i2)) else None
+  | DivOp, RatE r1, RatE r2 => if negb (iszero val2) then Some (RatE (r1 / r2)%R) else None
+  | DivOp, RealE r1, RealE r2 => if negb (iszero val2) then Some (RealE (r1 / r2)%R) else None
+  | ModOp, NatE n1, NatE n2 => if negb (iszero val2) then Some (NatE (Nat.modulo n1 n2)) else None
+  | ModOp, IntE i1, IntE i2 => if negb (iszero val2) then Some (NatE (modz i1 i2)) else None
+  | PowOp, NatE n1, NatE n2 => Some (NatE (n1^n2))
+  | PowOp, IntE i1, IntE i2 => if (i2 >= 0)%R then Some (IntE (i1^i2)) else None 
+  | PowOp, RatE r1, RatE r2 => if isone (IntE (denq r2)) then Some (RatE (r1^(numq r2))) else None 
+  (* TODO - don't know how this is supposed to work: 
+  | PowOp, RealE r1, RealE r2 => RealE (r1^r2) *)
+  | _, _, _ => None
+  end
+.
+
+
+Definition numcmp (op : numcmpop) (val1 val2 : il_num) : option bool :=
+  match op, val1, val2 with
+  | LtOp, NatE n1, NatE n2 => Some ((n1 < n2)%nat)
+  | LtOp, IntE i1, IntE i2 => Some ((i1 < i2)%R)
+  | LtOp, RatE r1, RatE r2 => Some ((r1 < r2)%R)
+  | LtOp, RealE r1, RealE r2 => Some ((r1 < r2)%R)
+  | GtOp, NatE n1, NatE n2 => Some ((n1 > n2)%nat)
+  | GtOp, IntE i1, IntE i2 => Some ((i1 > i2)%R)
+  | GtOp, RatE r1, RatE r2 => Some ((r1 > r2)%R)
+  | GtOp, RealE r1, RealE r2 => Some ((r1 > r2)%R)
+  | LeOp, NatE n1, NatE n2 => Some ((n1 <= n2)%nat)
+  | LeOp, IntE i1, IntE i2 => Some ((i1 <= i2)%R)
+  | LeOp, RatE r1, RatE r2 => Some ((r1 <= r2)%R)
+  | LeOp, RealE r1, RealE r2 => Some ((r1 <= r2)%R)
+  | GeOp, NatE n1, NatE n2 => Some ((n1 >= n2)%nat)
+  | GeOp, IntE i1, IntE i2 => Some ((i1 >= i2)%R)
+  | GeOp, RatE r1, RatE r2 => Some ((r1 >= r2)%R)
+  | GeOp, RealE r1, RealE r2 => Some ((r1 >= r2)%R)
+  | _, _, _ => None
+  end
+.