[spectec] Formalise binding semantics for let premises (#2109)

Author: rossberg

spectec/Makefile

@@ -113,6 +113,12 @@ sync%:
 	(cd ../specification && make $@)
 
 
+# Semantics checks
+
+sem:
+	(cd doc/semantics/il && make check)
+
+
 # Cleanup
 
 .PHONY: clean distclean

spectec/doc/example/output/NanoWasm.pdf

@@ -31,8 +31,9 @@ syntax deftyp =
   | VARIANT typcase*
 
 syntax typbind = id `: typ
-syntax typfield = atom `: typ `- `{quant*} prem*
-syntax typcase = mixop `: typ `- `{quant*} prem*
+syntax typfield = atom `: typprems
+syntax typcase = mixop `: typprems
+syntax typprems = typ `- `{quant*} prem*
 
 
 ;; Iterators
@@ -130,6 +131,8 @@ syntax exp =
 
 syntax expfield = atom `= exp
 syntax exppull = id `: typ `<- exp
+syntax exppush = exp `-> id `: typ
+syntax expprems = exp `- prem*
 
 syntax path =
   | ROOT               ;;
@@ -174,8 +177,8 @@ syntax prem =
   | IF exp
   | ELSE
   | NOT prem
-  | LET exp `= exp  ;; TODO: variables/quantifiers?
-  | ITER prem iter exppull*
+  | LET `{quant*} exp `= exp
+  | ITER prem iter exppull* exppush*
 
 syntax dec =
   | TYP id param* `= inst*
@@ -185,9 +188,9 @@ syntax dec =
   | REC dec*
 
 syntax inst = INST `{quant*} arg* `=> deftyp
-syntax rul = RULE `{quant*} exp `- prem*
-syntax clause = CLAUSE `{quant*} arg* `=> exp `- prem*
-syntax prod = PROD `{quant*} sym `=> exp `- prem*
+syntax rul = RULE `{quant*} expprems
+syntax clause = CLAUSE `{quant*} arg* `=> expprems
+syntax prod = PROD `{quant*} sym `=> expprems
 
 
 ;; Scripts

spectec/doc/semantics/il/1-syntax.spectec

@@ -107,12 +107,38 @@ def $refresh_exppulls(ep*) = (ep', $composesubsts(s*))
   -- (if (ep', s) = $refresh_exppull(ep))*
 
 
+def $refresh_exppush(exppush) : (exppush, subst)
+def $refresh_exppushs(exppush*) : (exppush*, subst)
+
+def $refresh_exppush(e `-> x `: t) = (e `-> x' `: t, s)
+  -- if (x', s) = $refresh_expid(x)
+
+def $refresh_exppushs(eq*) = (eq', $composesubsts(s*))
+  -- (if (eq', s) = $refresh_exppush(eq))*
+
+
 def $refresh_iter(iter) : (iter, subst)
 
 def $refresh_iter(QUEST) = (QUEST, {})
 def $refresh_iter(STAR) = (STAR, {})
 def $refresh_iter(PLUS) = (PLUS, {})
-def $refresh_iter(SUP x e) = (SUP x' e, s) -- if (x', s) = $refresh_expid(x)
+def $refresh_iter(SUP x e) = (SUP x' e, s)
+  -- if (x', s) = $refresh_expid(x)
+
+
+def $refresh_prem(prem) : (prem, subst)
+def $refresh_prems(prem*) : (prem*, subst)
+
+def $refresh_prem(REL x a* `: e) = (REL x a* `: e, {})
+def $refresh_prem(IF e) = (IF e, {})
+def $refresh_prem(ELSE) = (ELSE, {})
+def $refresh_prem(LET `{q*} e_1 `= e_2) = (LET `{q'*} $subst_exp(s, e_1) `= e_2, s)
+  -- if (q'*, s) = $refresh_params(q*)
+def $refresh_prem(ITER pr it ep* eq*) = (ITER pr it ep* eq'*, s)
+  -- if (eq'*, s) = $refresh_exppushs(eq*)
+
+def $refresh_prems(pr*) =
+  $refresh_list(prem, $refresh_prem, $subst_prem, pr*)
 
 
 ;; Lists
@@ -142,12 +168,8 @@ def $subst_typ(s, MATCH x a* WITH inst*) = MATCH x $subst_arg(s, a)*  WITH $subs
 
 def $subst_deftyp(subst, deftyp) : deftyp
 def $subst_deftyp(s, ALIAS t) = ALIAS $subst_typ(s, t)
-def $subst_deftyp(s, STRUCT (a `: t `- `{q*} pr*)*) = STRUCT (a `: $subst_typ(s, t') `- `{$subst_param(s ++ s', q')*} $subst_prem(s ++ s' ++ s'', pr)*)*
-  -- if (t', s') = $refresh_typ(t)
-  -- if (q'*, s'') = $refresh_params(q*)
-def $subst_deftyp(s, VARIANT (m `: t `- `{q*} pr*)*) = VARIANT (m `: $subst_typ(s, t') `- `{$subst_param(s ++ s', q')*} $subst_prem(s ++ s' ++ s'', pr)*)*
-  -- if (t', s') = $refresh_typ(t)
-  -- if (q'*, s'') = $refresh_params(q*)
+def $subst_deftyp(s, STRUCT (a `: tpr)*) = STRUCT (a `: $subst_typprems(s, tpr))*
+def $subst_deftyp(s, VARIANT (m `: tpr)*) = VARIANT (m `: $subst_typprems(s, tpr))*
 
 def $subst_typbind(subst, typbind) : typbind
 def $subst_typbind(s, x `: t) = x' `: $subst_typ(s, t)
@@ -164,6 +186,9 @@ def $subst_iter(s, SUP x e) = SUP x $subst_exp(s, e)
 def $subst_exppull(subst, exppull) : exppull
 def $subst_exppull(s, x `: t `<- e') = x `: $subst_typ(s, t) `<- $subst_exp(s, e')
 
+def $subst_exppush(subst, exppush) : exppush
+def $subst_exppush(s, e' `-> x `: t) = $subst_exp(s, e') `-> x `: $subst_typ(s, t)
+
 
 ;; Expressions
 
@@ -223,7 +248,7 @@ def $subst_sym(s, ITER g it ep*) = ITER $subst_sym(s ++ s' ++ s'', g) $subst_ite
   -- if (ep'*, s'') = $refresh_exppulls(ep*)
 
 
-;; Definitions
+;; Arguments and Parameters
 
 def $subst_arg(subst, arg) : arg
 def $subst_arg(s, TYP t) = TYP $subst_typ(s, t)
@@ -239,30 +264,49 @@ def $subst_param(s, FUN x `: p* `-> t) = FUN x `: $subst_param(s, p')* `-> $subs
 def $subst_param(s, GRAM x `: p* `-> t) = GRAM x `: $subst_param(s, p')* `-> $subst_typ(s ++ s', t)
   -- if (p'*, s') = $refresh_params(p*)
 
+
+;; Premises
+
 def $subst_prem(subst, prem) : prem
 def $subst_prem(s, REL x a* `: e) = REL x $subst_arg(s, a)* `: $subst_exp(s, e)
 def $subst_prem(s, IF e) = IF $subst_exp(s, e)
 def $subst_prem(s, ELSE) = ELSE
-def $subst_prem(s, LET e_1 `= e_2) = LET $subst_exp(s, e_1) `= $subst_exp(s, e_2)
-def $subst_prem(s, ITER pr it ep*) = ITER $subst_prem(s ++ s' ++ s'', pr) $subst_iter(s, it') $subst_exppull(s, ep')*
+def $subst_prem(s, LET `{q*} e_1 `= e_2) = LET `{$subst_param(s, q)*} $subst_exp(s, e_1) `= $subst_exp(s, e_2)
+  ;; Assume: q* fresh (from caller $subst_typprems, $subst_expprems)
+def $subst_prem(s, ITER pr it ep* eq*) = ITER $subst_prem(s ++ s' ++ s'', pr') $subst_iter(s, it') $subst_exppull(s, ep')* $subst_exppush(s ++ s''', eq')*
+  ;; Assume: eq* fresh (from caller $subst_typprems, $subst_expprems)
   -- if (it', s') = $refresh_iter(it)
   -- if (ep'*, s'') = $refresh_exppulls(ep*)
+  -- if (pr', s''') = $refresh_prem(pr)
+
 
+def $subst_typprems(subst, typprems) : typprems
+def $subst_typprems(s, t `- `{q*} pr*) = $subst_typ(s, t') `- `{$subst_param(s ++ s', q')*} $subst_prem(s ++ s' ++ s'', pr')*
+  -- if (t', s') = $refresh_typ(t)
+  -- if (q'*, s'') = $refresh_params(q*)
+  -- if (pr'*, s''') = $refresh_prems(pr*)
+
+def $subst_expprems(subst, expprems) : expprems
+def $subst_expprems(s, e `- pr*) = $subst_exp(s ++ s', e) `- $subst_prem(s, pr)*
+  -- if (pr'*, s') = $refresh_prems(pr*)
+
+
+;; Definitions
 
 def $subst_inst(subst, inst) : inst
 def $subst_inst(s, INST `{q*} a* `=> dt) = INST `{$subst_param(s, q')*} $subst_arg(s ++ s', a)* `=> $subst_deftyp(s ++ s', dt)
   -- if (q'*, s') = $refresh_params(q*)
 
 def $subst_rule(subst, rul) : rul
-def $subst_rule(s, RULE `{q*} e `- pr*) = RULE `{$subst_param(s, q')*} $subst_exp(s ++ s', e) `- $subst_prem(s ++ s', pr)*
+def $subst_rule(s, RULE `{q*} epr) = RULE `{$subst_param(s, q')*} $subst_expprems(s ++ s', epr)
   -- if (q'*, s') = $refresh_params(q*)
 
 def $subst_clause(subst, clause) : clause
-def $subst_clause(s, CLAUSE `{q*} a* `=> e `- pr*) = CLAUSE `{$subst_param(s, q')*} $subst_arg(s ++ s', a)* `=> $subst_exp(s ++ s', e) `- $subst_prem(s ++ s', pr)*
+def $subst_clause(s, CLAUSE `{q*} a* `=> epr) = CLAUSE `{$subst_param(s, q')*} $subst_arg(s ++ s', a)* `=> $subst_expprems(s ++ s', epr)
   -- if (q'*, s') = $refresh_params(q*)
 
 def $subst_prod(subst, prod) : prod
-def $subst_prod(s, PROD `{q*} g `=> e `- pr*) = PROD `{$subst_param(s, q')*} $subst_sym(s ++ s', g) `=> $subst_exp(s ++ s', e) `- $subst_prem(s ++ s', pr)*
+def $subst_prod(s, PROD `{q*} g `=> epr) = PROD `{$subst_param(s, q')*} $subst_sym(s ++ s', g) `=> $subst_expprems(s ++ s', epr)
   -- if (q'*, s') = $refresh_params(q*)
 
 

spectec/doc/semantics/il/4-subst.spectec

@@ -80,6 +80,7 @@ rule Step_typ/ITER-ctx:
 
 relation Step_iter: S |- iter ~> iter
 relation Step_exppull: S |- exppull ~> exppull
+relation Step_exppush: S |- exppush ~> exppush
 
 rule Step_iter/SUP-ctx:
   S |- SUP x e ~> SUP x e'
@@ -94,6 +95,14 @@ rule Step_exppull/ctx2:
   S |- x `: t `<- e  ~>  x `: t `<- e'
   -- Step_exp: S |- e ~> e'
 
+rule Step_exppush/ctx1:
+  S |- e `-> x `: t  ~>  e' `-> x `: t
+  -- Step_exp: S |- e ~> e'
+
+rule Step_exppush/ctx2:
+  S |- e `-> x `: t  ~>  e `-> x `: t'
+  -- Step_typ: S |- t ~> t'
+
 
 ;; Expressions
 
@@ -442,9 +451,9 @@ rule Step_exp/MATCH-ctx2:
   -- Step_clause: S |- clause*[n] ~> clause'_n
 
 rule Step_exp/MATCH-match:
-  S |- MATCH a* WITH (CLAUSE `{q*} a'* `=> e `- pr*) clause* ~>
+  S |- MATCH a* WITH (CLAUSE `{q*} a'* `=> epr) clause* ~>
     MATCH a''* WITH
-      (CLAUSE `{q'*} a'''* `=> $subst_exp(s, e) `- $subst_prem(s, pr)*)
+      (CLAUSE `{q'*} a'''* `=> $subst_expprems(s, epr))
       (CLAUSE `{} a''* `=> (MATCH a* WITH clause*) `- eps)
   -- Step_argmatch: S |- `{q*} (a / a')*  ~>_s  `{q'*} (a'' / a''')*
 
@@ -695,6 +704,7 @@ rule Step_expmatch_plain/STR-fail:
   S |- STR ef* / STR ef'* ~> FAIL
   -- otherwise
 
+
 rule Step_expmatch_plain/ITER-PLUS:
   S |- LIST e* / ITER e' PLUS (x `: t `<- e_p)* ~>
     LIST e* / ITER e' STAR (x `: t `<- e_p)*
@@ -743,8 +753,8 @@ rule Step_clause/CLAUSE-ctx2:
   -- Step_exp: S |- e ~> e'
 
 rule Step_clause/CLAUSE-ctx3:
-  S |- CLAUSE `{q*} a* `=> e `- pr* ~> CLAUSE `{q*} a* `=> e `- pr'*
-  -- Step_prems: S |- pr* ~> pr'*
+  S |- CLAUSE `{q*} a* `=> e `- pr* ~> CLAUSE `{q*} a* `=> $subst_exp(s, e) `- pr'*
+  -- Step_prems: S |- pr* ~>_s pr'*
 
 
 ;; Arguments
@@ -782,7 +792,7 @@ rule Step_arg/TYP-ctx:
 ;; Premises
 
 relation Reduce_prems: S |- prem* ~>* prem*
-relation Step_prems: S |- prem* ~> prem*
+relation Step_prems: S |- prem* ~>_subst prem*
 relation Eq_prems: S |- prem* == prem*
 
 
@@ -798,74 +808,96 @@ rule Reduce_prems/refl:
 
 rule Reduce_prems/step:
   S |- pr* ~>* pr''*
-  -- Step_prems: S |- pr* ~> pr'*
+  -- Step_prems: S |- pr* ~>_s pr'*
   -- Reduce_prems: S |- pr'* ~>* pr''*
 
 
-rule Step_prems/ctx:
-  S |- pr* ~> pr*[0 : n] pr'_n* pr*[n : |pr*| - n]
-  -- Step_prems: S |- pr*[n] ~> pr'_n*
+rule Step_prems/seq:
+  S |- pr_1* pr pr_2* ~>_(s ++ s') pr_1* pr'* $subst_prem(s, pr'_2)*
+  -- Step_prems: S |- pr ~>_s pr'*
+  -- if (pr'_2*, s') = $refresh_prems(pr_2*)
 
 
 rule Step_prems/REL:
-  S |- REL x a* `: e ~> $subst_prem(s, pr)* (IF (CMP EQ $subst_exp(s, e') e))
+  S |- REL x a* `: e ~>_{} pr'* (IF (CMP EQ $subst_exp(s ++ s', e') e))
   -- if (x, p* `-> t `= rul*) <- S.REL
-  -- if (RULE `{q*} e' `- pr*) <- $subst_rule($args_for_params(a*, p*), rul)*
+  -- if (RULE `{q*} (e' `- pr*)) <- $subst_rule($args_for_params(a*, p*), rul)*
   -- Ok_subst: $storeenv(S) |- s : q*
+  -- if (pr'*, s') = $refresh_prems(pr*)
   ;; Note: non-computational rule
 
 rule Step_prems/IF-ctx:
-  S |- IF e ~> IF e'
+  S |- IF e ~>_{} IF e'
   -- Step_exp: S |- e ~> e'
 
 rule Step_prems/IF-true:
-  S |- IF (BOOL true) ~> eps
+  S |- IF (BOOL true) ~>_{} eps
 
 rule Step_prems/ELSE:
-  S |- ELSE ~> IF (BOOL true)
+  S |- ELSE ~>_{} IF (BOOL true)
 
 rule Step_prems/LET-ctx:
-  S |- LET e_1 `= e_2 ~> LET e_1 `= e'_2
+  S |- LET `{q*} e_1 `= e_2 ~>_{} LET `{q*} e_1 `= e'_2
   -- Step_exp: S |- e_2 ~> e'_2
 
 rule Step_prems/LET:
-  S |- LET e `= e ~> eps
+  S |- LET `{(EXP x `: t)*} e_1 `= e_2 ~>_{EXP (x, e)*} eps
+  -- (if e = MATCH (EXP e_2) WITH (CLAUSE `{(EXP x `: t)*} (EXP e_1) `=> (VAR x) `- eps))*
+  ;; TODO: Propagate false in case of match failure
 
 rule Step_prems/NOT-ctx:
-  S |- NOT pr ~> NOT pr'
-  -- Step_prems: S |- pr ~> pr'
+  S |- NOT pr ~>_{} NOT pr'
+  -- Step_prems: S |- pr ~>_s pr'
 
 rule Step_prems/NOT-true:
-  S |- NOT (IF (BOOL true)) ~> IF (BOOL false)
+  S |- NOT (IF (BOOL true)) ~>_{} IF (BOOL false)
 
 rule Step_prems/NOT-false:
-  S |- NOT (IF (BOOL false)) ~> IF (BOOL true)
+  S |- NOT (IF (BOOL false)) ~>_{} IF (BOOL true)
+
+var ep : exppull
+var eq : exppush
 
 rule Step_prems/ITER-ctx1:
-  S |- ITER pr it ep* ~> ITER pr' it ep*
-  -- Step_prems: S |- pr ~> pr'
+  S |- ITER pr it ep* eq* ~>_{} ITER pr' it ep* $subst_exppush(s, eq)*
+  -- Step_prems: S |- pr ~>_s pr'
 
 rule Step_prems/ITER-ctx2:
-  S |- ITER pr it ep* ~> ITER pr it' ep*
+  S |- ITER pr it ep* eq* ~>_{} ITER pr it' ep* eq*
   -- Step_iter: S |- it ~> it'
 
 rule Step_prems/ITER-ctx3:
-  S |- ITER pr it ep* ~> ITER pr it ep*[[n] = ep'_n]
+  S |- ITER pr it ep* eq* ~>_{} ITER pr it ep*[[n] = ep'_n] eq*
   -- Step_exppull: S |- ep*[n] ~> ep'_n
 
+rule Step_prems/ITER-ctx4:
+  S |- ITER pr it ep* eq* ~>_{} ITER pr it ep* eq*[[n] = eq'_n]
+  -- Step_exppush: S |- eq*[n] ~> eq'_n
+
 rule Step_prems/ITER-QUEST:
-  S |- ITER pr QUEST (x `: t `<- OPT e?)* ~> $subst_prem({EXP (x, e')*}, pr)?
-  -- if e'*? = $transpose_(exp, e?*)
+  S |- ITER pr QUEST (x_1 `: t_1 `<- OPT e_1?)* (e_2 `-> x_2 `: t_2)* ~>_({EXP (x_2, OPT $subst_exp(s', e''_2)?)*} ++ s')
+    $subst_prem({EXP (x_1, e'_1)*}, pr')?
+  -- if e'_1*? = $transpose_(exp, e_1?*)
+  -- if e'_2*? = $transpose_(exp, e''_2?*)
+  -- (if |e_1?| = |e''_2?|)*
+  -- (if e'_2 = e_2)*?
+  -- if (pr', s') = $refresh_prem(pr)
 
 rule Step_prems/ITER-PLUS:
-  S |- ITER pr PLUS (x `: t `<- LIST e*)* ~> ITER pr STAR (x `: t `<- LIST e*)*
-  -- if |e**[0]| >= 1
+  S |- ITER pr PLUS (x_1 `: t_1 `<- LIST e_1*)* (e_2 `-> x_2 `: t_2)* ~>_{}
+    ITER pr STAR (x_1 `: t_1 `<- LIST e_1*)* (e_2 `-> x_2 `: t_2)*
+  -- if |e_1**[0]| >= 1
 
 rule Step_prems/ITER-STAR:
-  S |- ITER pr STAR (x `: t `<- LIST e*)* ~> ITER pr (SUP y (NAT n)) (x `: t `<- LIST e*)*
-  -- if |e**[0]| = n
+  S |- ITER pr STAR (x_1 `: t_1 `<- LIST e_1*)* (e_2 `-> x_2 `: t_2)* ~>_{}
+    ITER pr (SUP y (NAT n)) (x_1 `: t_1 `<- LIST e_1*)* (e_2 `-> x_2 `: t_2)*
+  -- if |e_1**[0]| = n
   -- Fresh_id: y FRESH
 
 rule Step_prems/ITER-SUP:
-  S |- ITER pr (SUP y (NAT n)) (x `: t `<- LIST e^n)* ~> $subst_prem({EXP (x, e')* (y, NAT i)}, pr)^(i<n)
-  -- if e'*^n = $transpose_(exp, e^n*)
+  S |- ITER pr (SUP y (NAT n)) (x_1 `: t_1 `<- LIST e_1^n)* ~>_({EXP (x_2, LIST $subst_exp(s', e''_2)^n)*} ++ s')
+    $subst_prem({EXP (x_1, e'_1)* (y, NAT i)}, pr')^(i<n)
+  -- if e'_1*^n = $transpose_(exp, e_1^n*)
+  -- if e'_2*^n = $transpose_(exp, e''_2^n*)
+  -- (if e'_2 = e_2)*^n
+  -- if (pr', s') = $refresh_prem(pr)