From 271a8aba3041e4f712f3331fd1610cdf31fbb4c9 Mon Sep 17 00:00:00 2001
From: Alasdair Armstrong
Date: Tue, 9 Apr 2019 18:30:37 +0100
Subject: SMT: Refactor Jib values to make inlining work

Had to change the hundreds and hundreds of places such values were
used. However this now lets us automatically prove cheri-concentrate
properties. Such as showing

function prop_cap_round_trip(cap: bits(128)) -> bool = {
  let cap_rt = capToBits(capBitsToCapability(true, cap));
  cap == cap_rt
}

is always true.
---
 language/jib.ott | 36 ++++++++++++++++++------------------
 1 file changed, 18 insertions(+), 18 deletions(-)

(limited to 'language')

diff --git a/language/jib.ott b/language/jib.ott
index d7a8b188..8177ae3a 100644
--- a/language/jib.ott
+++ b/language/jib.ott
@@ -41,6 +41,10 @@ metavar value ::=
   {{ lem vl }}
   {{ ocaml vl }}
 
+metavar alpha ::=
+  {{ phantom }}
+  {{ lem 'a }}
+
 embed
 {{ lem
 
@@ -60,19 +64,20 @@ name :: '' ::=
 % Fragments are small pure snippets of (abstract) C code, mostly
 % expressions, used by the aval (ANF) and cval (Jib) types.
 
-fragment :: 'F_' ::=
-  | name                                             :: :: id
-  | '&' name                                         :: :: ref
-  | value                                            :: :: lit
-  | fragment != kind id ( ctyp0 , ... , ctypn ) ctyp :: :: ctor_kind
-  | unwrap id ( ctyp0 , ... , ctypn ) fragment       :: :: ctor_unwrap
-  | fragment op fragment'                            :: :: op
-  | fragment nat0 nat1                               :: :: tuple_member
-  | op fragment                                      :: :: unary
-  | string ( fragment0 , ... , fragmentn )           :: :: call
-  | fragment . string                                :: :: field
-  | string                                           :: :: raw
-  | poly fragment                                    :: :: poly
+cval :: 'V_' ::=
+  | name : ctyp                                  :: :: id
+  | '&' name : ctyp                              :: :: ref
+  | value : ctyp                                 :: :: lit
+  | cval != kind id ( ctyp0 , ... , ctypn ) ctyp :: :: ctor_kind
+  | unwrap id cval ( ctyp0 , ... , ctypn ) ctyp  :: :: ctor_unwrap
+  | cval op cval'                                :: :: op
+  | cval nat0 nat1                               :: :: tuple_member
+  | op cval                                      :: :: unary
+  | string ( cval0 , ... , cvaln )               :: :: call
+  | cval . string                                :: :: field
+  | hd ( cval )                                  :: :: hd
+  | tl ( cval )                                  :: :: tl
+  | poly cval ctyp                               :: :: poly
 
 % Note that init / clear are sometimes refered to as create / kill
 
@@ -135,11 +140,6 @@ ctyp :: 'CT_' ::=
 % lbits, and this must work without compiling to type incorrect C.
   | poly                           :: :: poly
 
-
-cval :: 'CV_' ::=
-  {{ ocaml fragment * ctyp }}
-  {{ lem fragment * ctyp }}
-
 clexp :: 'CL_' ::=
   | name : ctyp              :: :: id
   | name0 rmw name1 : ctyp   :: :: rmw
-- 
cgit v1.2.3