Merge branch 'master' of https://github.com/input-output-hk/plutus in…

…to effectfully/builtins/both-MajorProtocolVersion-and-multiple-CostModels

.github/workflows/slack-message-broker.yml

@@ -27,7 +27,7 @@ jobs:
             core.setOutput("message", message); 
 
       - name: Notify Slack
-        uses: slackapi/slack-github-action@v1.25.0
+        uses: slackapi/slack-github-action@v1.26.0
         with:
           channel-id: my-private-channel
           payload: |

doc/notes/verified-compilation/isabelle/Inline.thy

@@ -0,0 +1,109 @@
+section \<open>Outline\<close>
+text \<open>This is just an experiment with presenting the datatypes and relations from Jacco's
+      paper in Iasbelle and working out how well (or otherwise) sledgehamemr et al. can handle
+      generating proofs for them. \<close>
+
+theory Inline
+  imports 
+    Main
+    HOL.String
+    HOL.List
+begin
+
+type_synonym Name = string
+
+section \<open>Simple Lambda Calculus\<close>
+
+text \<open>A very cut down lambda calculus with just enough to demo the functions below. \<close>
+
+text \<open>I have commented out the Let definition because it produces some slightly complicated
+      variable name shadowing issues that wouldn't really help with this demo. \<close>
+
+datatype AST = Var Name
+  | Lam Name AST
+  | App AST AST
+(*   | Let Name AST AST *) (* The definition below does some name introduction without 
+                              checking things are free, which could cause shadowing, 
+                              which in turn makes the proofs harder...*)
+
+text \<open>Simple variable substitution is useful later.\<close>
+
+fun subst :: "AST \<Rightarrow> Name \<Rightarrow> AST \<Rightarrow> AST" where
+"subst (Var n) m e = (if (n = m) then e else Var n)"
+| "subst (Lam x e) m e' = Lam x (subst e m e')"
+| "subst (App a b) m e' = App (subst a m e') (subst b m e')"
+(* | "subst (Let x xv e) m e' = (Let x (subst xv m e') (subst e m e'))" (* how should this work if x = m? *) *)
+
+text \<open>Beta reduction is just substitution when done right. 
+      This isn't actually used in this demo, but it works...\<close>
+
+fun beta_reduce :: "AST \<Rightarrow> AST" where
+"beta_reduce (App (Lam n e) x) = (subst e n x)"
+| "beta_reduce e = e"
+
+section \<open>Translation Relation\<close>
+
+text \<open>In a context, it is valid to inline variable values.\<close>
+
+type_synonym Context = "Name \<Rightarrow> AST"
+
+fun extend :: "Context \<Rightarrow> (Name * AST) \<Rightarrow> Context" where
+"extend \<Gamma> (n, ast) = (\<lambda> x . if (x = n) then ast else \<Gamma> x)"
+
+text \<open>This defintion is from figure 2 of 
+      [the paper](https://iohk.io/en/research/library/papers/translation-certification-for-smart-contracts-scp/)\<close>
+
+inductive inline :: "Context \<Rightarrow> AST \<Rightarrow> AST \<Rightarrow> bool" ("_ \<turnstile> _ \<triangleright> _" 60) where
+"\<lbrakk>(\<Gamma> x) = y ; \<Gamma> \<turnstile> y \<triangleright> y' \<rbrakk> \<Longrightarrow> \<Gamma> \<turnstile> (Var x) \<triangleright> y'"
+| "\<Gamma> \<turnstile> (Var x) \<triangleright> (Var x)"
+(* | "\<lbrakk> \<Gamma> \<turnstile> t1 \<triangleright> t1' ; (extend \<Gamma> (x,t1)) \<turnstile> t2 \<triangleright> t2' \<rbrakk> \<Longrightarrow> \<Gamma> \<turnstile> (Let x t1 t2) \<triangleright> (Let x t1' t2')" *)
+| "\<lbrakk> \<Gamma> \<turnstile> t1 \<triangleright> t1' ; \<Gamma> \<turnstile> t2 \<triangleright> t2' \<rbrakk> \<Longrightarrow> \<Gamma> \<turnstile> App t1 t2 \<triangleright> App t1' t2'"
+| "\<Gamma> \<turnstile> t1 \<triangleright> t1' \<Longrightarrow> \<Gamma> \<turnstile> Lam x t1 \<triangleright> Lam x t1'"
+
+text \<open>Idempotency is useful for resolving inductive substitutions.\<close>
+
+lemma inline_idempotent : "\<Gamma> \<turnstile> x \<triangleright> x"
+proof (induct x)
+  case (Var x)
+  then show ?case by (rule inline.intros(2))
+next
+  case (Lam x1a x)
+  then show ?case by (rule inline.intros(4))
+next
+  case (App x1 x2)
+  then show ?case by (rule inline.intros(3))
+(* This requires x1a to be free in x1 and x2, or to shadow in a consistent way, which is a hassle to demonstrate...
+next
+  case (Let x1a x1 x2)
+  then show ?case
+    apply (rule_tac ?x="x1a" in VerifiedCompilation.inline.intros(3))
+     apply simp
+*) 
+qed
+
+section \<open>Experiments\<close>
+
+text \<open>We can present some simple pairs of ASTs and ask sledgehammer to produce proofs.
+      For all of these it just works with the simplifier, since they are just applications
+      of the definition of the translation. \<close>
+
+lemma demo_inline1 : "\<lbrakk> \<Gamma> x = (Var y) \<rbrakk> \<Longrightarrow> \<Gamma> \<turnstile> (Var x) \<triangleright> (Var y)"
+  by (simp add: inline.intros(1) inline_idempotent)
+
+lemma demo_inline2 : "\<lbrakk> \<Gamma> f = (Lam x (App g (Var x))) ; \<Gamma> y = (Var b) \<rbrakk> \<Longrightarrow> \<Gamma> \<turnstile> (App (Var f) (Var y)) \<triangleright> (App (Lam x (App g (Var x))) (Var b))"
+  by (simp add: inline.intros(1) inline.intros(3) inline_idempotent)
+
+lemma demo_inline_2step : "\<lbrakk> \<Gamma> f = (Lam x (Lam y (App (Var x) (Var y)))) ; \<Gamma> b = (Var z) \<rbrakk> \<Longrightarrow> \<Gamma> \<turnstile> (App (Var f) (Var b)) \<triangleright> (App (Lam x (Lam y (App (Var x) (Var y)))) (Var z))"
+  by (simp add: inline.intros(1) inline.intros(3) inline_idempotent)
+
+lemma demo_inline_4step : "\<lbrakk> \<Gamma> f = (Lam x (Lam y (App (Var x) (Var y)))) ; \<Gamma> b = (Var c) ; \<Gamma> c = (Var d) ; \<Gamma> d = (App (Var i) (Var j)) \<rbrakk> \<Longrightarrow> \<Gamma> \<turnstile> (App (Var f) (Var b)) \<triangleright> (App (Lam x (Lam y (App (Var x) (Var y)))) (App (Var i) (Var j)))"
+  using inline.intros(1) inline.intros(3) inline_idempotent by presburger
+
+text \<open>A false example to show verification actually happen! This reqriting isn't valid and 
+       nitpick can show you a counterexample pretty quickly (although it isn't very readable).\<close>
+lemma demo_wrong_inline : "\<lbrakk> \<Gamma> f = (Lam x (Lam y (App (Var x) (Var y)))) \<rbrakk> \<Longrightarrow> \<Gamma> \<turnstile> (App (Var f) (Var z)) \<triangleright> (App (Var x) (Var y))"
+  nitpick
+  sorry
+
+end
+

doc/plutus-core-spec/builtins.tex

@@ -55,7 +55,7 @@ \subsection{Built-in types}
 The universe $\Uni$ consists entirely of \textit{names}, and the semantics of
 these names are given by \textit{denotations}. Each built-in type $\tn \in \Uni$
 is associated with some mathematical set $\denote{\tn}$, the \textit{denotation}
-of $\tn$. For example, we might have $\denote{\texttt{boolean}}=
+of $\tn$. For example, we might have $\denote{\texttt{bool}}=
 \{\mathsf{true}, \mathsf{false}\}$ and $\denote{\texttt{integer}} = \mathbb{Z}$
 and $\denote{\pairOf{a}{b}} = \denote{a} \times \denote{b}$.
 
@@ -326,7 +326,7 @@ \subsubsection{Signatures and denotations of built-in functions}
 \noindent For example, in our default set of built-in functions we have the
 functions \texttt{mkCons} with signature $[\forall a_\#, a_\#,$  %% Allow line break
   $\listOf{a_\#}] \rightarrow \listOf{a_\#}$ and \texttt{ifThenElse} with signature
-$[\forall a_*, \mathtt{boolean}, a_*, a_*] \rightarrow a_*$.  When we use
+$[\forall a_*, \mathtt{bool}, a_*, a_*] \rightarrow a_*$.  When we use
 \texttt{mkCons} its arguments must be of built-in types, but the two final
 arguments of \texttt{ifThenElse} can be any Plutus Core values.
 

doc/plutus-core-spec/cardano/builtins4.tex

@@ -8,11 +8,17 @@
   \noindent\textbf{Note \thenotenumberD. #1}
 }
 
+\newcommand{\itobsBE}{\mathsf{itobs_{BE}}}
+\newcommand{\itobsLE}{\mathsf{itobs_{LE}}}
+\newcommand{\bstoiBE}{\mathsf{bstoi_{BE}}}
+\newcommand{\bstoiLE}{\mathsf{bstoi_{LE}}}
+
 \subsection{Batch 4}
 \label{sec:default-builtins-4}
 The fourth batch of builtins adds support for
 \begin{itemize}
-\item The \texttt{Blake2b-224} and \texttt{Keccak-256} hash functions (Section \ref{sec:misc-builtins-4})
+\item The \texttt{Blake2b-224} and \texttt{Keccak-256} hash functions.
+\item Conversion functions from integers to bytestrings and vice-versa.
 \item BLS12-381 elliptic curve pairing operations
 (see~\cite{CIP-0381}, \cite{BLS12-381}, \cite[4.2.1]{IETF-pairing-friendly-curves}, \cite{BLST-library}).
  For clarity these are described separately in Sections~\ref{sec:bls-types-4} and \ref{sec:bls-builtins-4}.
@@ -21,8 +27,8 @@ \subsection{Batch 4}
 \subsubsection{Miscellaneous built-in functions}
 \label{sec:misc-builtins-4}
 
-\setlength{\LTleft}{-10mm} % Shift the table left a bit to centre it on the page
-\begin{longtable}[H]{|l|p{5cm}|p{55mm}|c|c|}
+\setlength{\LTleft}{-17mm} % Shift the table left a bit to centre it on the page
+\begin{longtable}[H]{|l|p{45mm}|p{65mm}|c|c|}
     \hline \text{Function} & \text{Signature} & \text{Denotation} & \text{Can}
     & \text{Note} \\ & & & fail?
     & \\ \hline \endfirsthead \hline \text{Function} & \text{Type}
@@ -37,13 +43,113 @@ \subsubsection{Miscellaneous built-in functions}
     \endlastfoot
 %% G1
     \hline
-    \TT{blake2b\_224} & $[\ty{bytestring}] \to \ty{bytestring}$  & \text{Hash a $\ty{bytestring}$ using}
-                                                                   \TT{Blake2b-224}~\cite{IETF-Blake2}. &  & \\
-    \TT{keccak\_256}  & $[\ty{bytestring}] \to \ty{bytestring}$  & \text{Hash a $\ty{bytestring}$ using}
-                                                                   \TT{Keccak-256}~\cite{KeccakRef3}. &  & \\
+    \TT{blake2b\_224} & $[\ty{bytestring}] \to \ty{bytestring}$  & \text{Hash a $\ty{bytestring}$ using
+                                                                   \TT{Blake2b-224}~\cite{IETF-Blake2}.} & & \\
+    \TT{keccak\_256}  & $[\ty{bytestring}] \to \ty{bytestring}$  & \text{Hash a $\ty{bytestring}$ using
+                                                                   \TT{Keccak-256}~\cite{KeccakRef3}.} & & \\
+    \hline\strut
+    \TT{integerToByteString} & $[\ty{bool}, \ty{integer}, \ty{integer}]$  \text{\: $\to \ty{bytestring}$}
+                                        & $(e, w, n) $ \text{$\mapsto \begin{cases}
+                                        \itobsLE(w,n) & \text{if $e=\mathtt{false}$}\\
+                                        \itobsBE(w,n) & \text{if $e=\mathtt{true}$}\\
+                                        \end{cases}$}
+                                        & Yes & \ref{note:itobs}\strut\\ \strut
+    \TT{byteStringToInteger} & $[\ty{bool}, \ty{bytestring}] $ \text{\: $ \to \ty{bytestring}$}
+                                        & $(e, [c_0, \ldots, c_{N-1}]) $ \text{\; $\mapsto \begin{cases}
+                                        \sum_{i=0}^{N-1}c_{i}256^i & \text{if $e=\mathtt{false}$}\\
+                                        \sum_{i=0}^{N-1}c_{i}256^{N-1-i} & \text{if $e=\mathtt{true}$}\\
+                                        \end{cases}$}
+                                        &  & \ref{note:bstoi}\\
     \hline
 \end{longtable}
 
+\note{Integer to bytestring conversion.}
+\label{note:itobs}
+The \texttt{integerToByteString} function converts non-negative integers to bytestrings.
+It takes three arguments:
+\begin{itemize}
+\item A boolean endianness flag $e$.
+\item An integer width argument $w$ with $0 \leq w < 8192$.
+\item The integer $n$ to be converted: it is required that $0 \leq n < 256^{8192} = 2^{65536}$.
+\end{itemize}
+
+\noindent The conversion is little-endian ($\mathsf{LE}$) if $e$ is
+\texttt{(con bool False)} and big-endian ($\mathsf{BE}$) if $e$ is
+\texttt{(con bool True)}. If the width $w$
+is zero then the output is a bytestring which is just large enough to hold the
+converted integer.  If $w>0$ then the output is exactly $w$ bytes long, and it
+is an error if $n$ does not fit into a bytestring of that size; if necessary,
+the output is padded with \texttt{0x00} bytes (on the right in the little-endian
+case and the left in the big-endian case) to make it the correct length.  For
+example, the five-byte little-endian representation of the
+integer \texttt{0x123456} is the bytestring \texttt{[0x56, 0x34, 0x12, 0x00,
+0x00]} and the five-byte big-endian representation is \texttt{[0x00, 0x00, 0x12,
+0x34, 0x56]}.  In all cases an error occurs error if $w$ or $n$ lies outside the
+expected range, and in particular if $n$ is negative.
+
+\newpage
+\noindent The precise semantics of \texttt{integerToByteString} are given
+by the functions $\itobsLE: \Z \times \Z \rightarrow \withError{\B^*}$ and $\itobsBE
+: \Z \times \Z \rightarrow \withError{\B^*}$.  Firstly we deal with out-of-range cases and
+the case $n=0$:
+
+$$
+\itobsLE (w,n) = \itobsBE (w,n) = 
+\begin{cases}
+  \errorX & \text{if $n<0$ or $n \geq 2^{65536}$}\\
+  \errorX & \text{if $w<0$ or $w > 8192$}\\
+  [] & \text{if $n=0$ and $0 \leq w \leq 8192$}\\
+\end{cases}
+$$
+
+\noindent  Now assume that none of the conditions above hold, so $0 < n < 2^{65536}$ and
+$0 \leq w \leq 8192$.  Since $n>0$ it has a unique base-256 expansion of the
+form $n = \sum_{i=0}^{N-1}a_{i}256^i$ with $N \geq 1$, $a_i \in \B$ for $0 \leq
+i \leq N-1$ and $a_{N-1} \ne 0$.  We then have
+
+$$
+\itobsLE (w,n) =
+\begin{cases}
+  [a_0, \ldots, a_{N-1}] & \text{if $w=0$} \\
+  [b_0, \ldots, b_{w-1}] &  \text{if $w > 0$ and $N\leq w$, where }
+      b_i = \begin{cases}
+                a_i & \text{if $i \leq N-1$} \\
+                0   & \text{if $i \geq N$}\\
+            \end{cases}\\
+  \errorX & \text{if $w > 0$ and $N > w$}
+\end{cases}
+$$
+
+\noindent and
+
+$$
+\noindent
+\itobsBE (w,n) =
+\begin{cases}
+  [a_{N-1}, \ldots, a_0] & \text{if $w=0$} \\
+  [b_0, \ldots, b_{w-1}] &  \text{if $w > 0$ and $N\leq w$, where }
+      b_i = \begin{cases}
+                0   & \text{if $i \leq w-1-N$}\\
+                a_{w-1-i} & \text{if $i \geq w-N$} \\
+            \end{cases}\\
+  \errorX & \text{if $w > 0$ and $N > w$.}
+\end{cases}
+$$
+
+\note{Bytestring to integer conversion.}
+\label{note:bstoi}
+The \texttt{byteStringToInteger} function converts bytestrings to non-negative
+integers.  It takes two arguments:
+\begin{itemize}
+\item A boolean endianness flag $e$.
+\item The bytestring $s$ to be converted.
+\end{itemize}
+\noindent  
+The conversion is little-endian if $e$ is \texttt{(con bool False)} and
+big-endian if $e$ is \texttt{(con bool True)}. In both cases the empty bytestring is
+converted to the integer 0. All bytestrings are legal inputs and there is no
+limitation on the size of $s$.
+
 \subsubsection{BLS12-381 built-in types}
 \label{sec:bls-types-4}
 

doc/plutus-core-spec/plutus-core-specification.tex

@@ -6,7 +6,7 @@
   \LARGE{\red{\textsf{DRAFT}}}
 }
 
-\date{21st December 2023}
+\date{18th April 2024}
 \author{Plutus Core Team}
 
 \input{header.tex}