Merge branch 'master' of github.com:IntersectMBO/plutus into zliu41/i…

…ndex-budget

.github/workflows/haddock.yml

@@ -18,7 +18,7 @@ jobs:
           nix_conf: |
             experimental-features = nix-command flakes
             accept-flake-config = true
-      - name: Build haddock site
+      - name: Build Haddock Site
         run: |
           nix build .#combined-haddock
           mkdir dist

.github/workflows/plutus-tx-template.yml

@@ -0,0 +1,58 @@
+# This workflows ensures that the plutus-tx-template repository stays working 
+# even if there are changes in plutus. It checks out both the current commit of 
+# plutus and the master branch of plutus-tx-template. Then, it creates a 
+# cabal.project.local for plutus-tx-template that adjusts the plutus version. 
+# Finally, it double-checks that everything still builds correctly using cabal
+# inside the devx shell.
+
+name: Plutus Tx Template
+
+on:
+  pull_request:
+
+jobs:
+  plutus-tx-template:
+    name: Build
+    runs-on: ubuntu-latest
+    steps:
+
+      - name: Checkout plutus-tx-template
+        uses: actions/checkout@v4.1.4
+        with: 
+          repository: IntersectMBO/plutus-tx-template
+          path: plutus-tx-template 
+
+      - name: Checkout plutus
+        uses: actions/checkout@v4.1.4
+        with: 
+          path: plutus-tx-template/plutus
+
+      - name: Write cabal.project.local
+        uses: DamianReeves/write-file-action@v1.3
+        with:
+          path: plutus-tx-template/cabal.project.local
+          write-mode: overwrite
+          contents: |
+            packages: 
+              plutus/plutus-tx
+              plutus/plutus-tx-plugin
+              plutus/plutus-core
+              plutus/plutus-ledger-api
+              plutus/prettyprinter-configurable
+            
+            allow-newer:
+                plutus-tx
+              , plutus-tx-plugin
+              , plutus-core
+              , plutus-ledger-api 
+              , prettyprinter-configurable
+          
+      - name: Build Project With Docker
+        run: |
+          cd plutus-tx-template 
+          ls -la 
+          docker run \
+            -v ./.:/workspaces/plutus-tx-template \
+            -w /workspaces/plutus-tx-template \
+            -i ghcr.io/input-output-hk/devx-devcontainer:x86_64-linux.ghc96-iog \
+            bash -ic "cabal update && cabal run plutus-tx-template && test -e validator.uplc"

.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: |

CONTRIBUTING.adoc

@@ -14,7 +14,7 @@ If you _really_ cannot use Nix and still want to contribute to Plutus then xref:
 
 === Installing and setting up Nix
 
-For instructions on how to install and configure nix (including how to enable access to our binary caches), refer to link:https://github.com/input-output-hk/iogx/blob/main/doc/nix-setup-guide.md[this document]. 
+For instructions on how to install and configure nix (including how to enable access to our binary caches), refer to link:https://github.com/input-output-hk/iogx/blob/main/doc/nix-setup-guide.md[this document].
 
 If you already have nix installed and setup, you may enter the development shell by running `nix develop`.
 
@@ -204,20 +204,20 @@ There are various tools for visualizing the resulting profile, e.g. https://hack
 We have a set of supported GHC major versions, which are built in CI and which we commit to keeping working.
 
 We also have a primary development version.
-This is the version we use in the default dev shell, and the one we use day-to-day. 
+This is the version we use in the default dev shell, and the one we use day-to-day.
 The primary development version should be whichever version the Cardano node is using (or migrating towards using).
 Supported versions older than the primary development version are deprecated, and we can drop them as soon as the Cardano node has moved to a later GHC version.
 
 At the moment, our supported GHC versions are:
 - 8.10 (deprecated)
 - 9.6 (primary)
-- 9.8 
+- 9.8
 
 === Plugin support
 
 Making `plutus-tx-plugin` work on multiple GHC versions can be painful, because it uses a lot of GHC internals.
 Since the plugin is not in the dependency closure of the Cardano node, we don't _need_ to support all the GHC versions, which is helpful.
-We mostly commit to supporting our primary development version, but we _may_ support other versions as well if it is easy. 
+We mostly commit to supporting our primary development version, but we _may_ support other versions as well if it is easy.
 
 The plugin and its dependents should be marked as unbuildable with cabal conditionals on any non-supported major GHC versions.
 This makes cabal behave reasonably well (it will ignore them and not try and fail to build them).
@@ -650,14 +650,13 @@ These perform some of the same checks as Hydra, but Github Actions is often more
 == Project roles and responsibilities
 
 - The regular contributors to the Haskell code, all of whom can review and merge PRs are:
-    - @michaelpj
+    - @ana-pantilie
+    - @bezirg
     - @effectfully
     - @kwxm
-    - @bezirg
-    - @thealmarty
+    - @Unisay
     - @zliu41
-- The maintainer of the documentation is @joseph-fajen.
 - The maintainer of the Agda code is @jmchapman, @effectfully can help with small issues.
-- If you have a technical dispute that you need help resolving, you can ask @michaelpj.
-- For problems with the developer environment setup, builds, or CI, you can ask @zeme-iohk, @Pacman99, or @michaelpj.
-- The regular contributors take turns releasing our software, but if you have a specific problem ask @zliu41 or @michaelpj.
+- If you have a technical dispute that you need help resolving, you can ask @zliu41.
+- For problems with the developer environment setup, builds, or CI, you can ask @zeme-iohk or @zliu41.
+- The regular contributors take turns releasing our software, but if you have a specific problem ask @zliu41.

RELEASE.adoc

@@ -100,6 +100,12 @@ Another example is if a security audit is done on `rc1`, and the changes in `rc2
 - Update the CHaP index state in `cabal.project`.
 - Update the CHaP flake input with `nix flake update CHaP`.  If you get "error: cannot find flake 'flake:CHaP' in the flake registries" your nix installation probably needs to be updated.
 
+9. Make a PR to update the version used in `plutus-tx-template`
+- Navigate to the https://github.com/IntersectMBO/plutus-tx-template/actions/workflows/bump-plutus-version.yml[Bump Plutus Version Action] on GitHub
+- Click the `Run workflow` button on the right, enter the new release version and confirm
+- This will automatically open a PR in `plutus-tx-template` with auto-merge enabled
+- Ensure that CI is green and the PR gets merged
+
 === Patch Releases
 
 Suppose we are releasing version `x.y.z.w`.

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.