Updates spec with new builtins, etc. #182

BekaValentine · 2018-10-09T10:00:13Z

No description provided.

effectfully

These are some preliminary comments, I'll probably add more once I build the spec.

effectfully · 2018-10-09T10:42:04Z

plutus-core-spec/figures/PlutusCoreBuiltins.tex

@@ -30,112 +30,116 @@

        $unitval$ & \(\abs{\alpha}{\typeK{}}{\lam{x}{\alpha}{x}}\)\\\\

-        $boolean$ & \(\forall \alpha :: \star.\ \alpha \to \alpha \to \alpha\)\\\\
+        $boolean$ & \(\forall \alpha :: \star.\ (unit \to \alpha) \to (unit \to \alpha) \to \alpha\)\\\\


In the implementation we dropped units and use forall a. a -> a -> a and instantiate it with () -> a.

effectfully · 2018-10-09T10:46:03Z

plutus-core-spec/figures/PlutusCoreBuiltins.tex

+\begin{landscape}
+\thispagestyle{empty}
+ \begin{figure*}
+    \hspace{-8.5cm}Let $txh$ be the transaction hash, $bnum$ be the block number, and $btime$ be the block time, all as global parameters to normalization.\vspace{1em}


I thought we removed btime?

effectfully · 2018-10-09T10:49:53Z

plutus-core-spec/figures/PlutusCoreGrammar.tex

-                                  &        &     & \wrap{\alpha}{S}{M}        & \textrm{fix type's wrap}\\
+        \textrm{Term}             & L,M,N  & ::= & x                          & \textrm{variable}\\
+                                  &        &     & \con{cn}                   & \textrm{constant}\\
+                                  &        &     & \abs{\alpha}{K}{M}         & \textrm{type abstraction}\\


I thought we agreed on value restriction?

In the abstraction? Yes, but then we unagreed because it was causing problems for @michaelpj?

No, on the call where we discussed we concluded that it makes erasure easier.

So yeah, we're keeping the value restriction for now.

plutus-core-spec/figures/PlutusCoreGrammar.tex

effectfully · 2018-10-09T10:57:56Z

plutus-core-spec/figures/PlutusCoreGrammar.tex

                                  &        &     & \funT{A}{B}                & \textrm{function type}\\
                                  &        &     & \allT{\alpha}{K}{A}        & \textrm{polymorphic type}\\
                                  &        &     & \fixT{\alpha}{A}           & \textrm{fixed point type}\\
                                  &        &     & \lamT{\alpha}{K}{A}        & \textrm{$\lambda$ abstraction}\\
                                  &        &     & \appT{A}{B}                & \textrm{function application}\\
-                                  &        &     & \conT{tcn}                 & \textrm{builtin type}\\
-        \textrm{Type Value}       & R,S,T  & ::= & \funT{S}{T}                & \textrm{function type}\\
+                                  &        &     & \conT{tcn}{A}          & \textrm{type constant}\\


Could you explain what this A is about?

I think it's for alignment.

Which A? There are many in the diff that I can see. :(

In the last shown line (I normally mean the last line if I do not specify one explicitly), i.e. the "type constant" case.

Oh! I've reorgged the way builtins and constants work, so now type constants are just a name and a size (the A arg). I would have added a signature component for them too but all type constants take size args only. If you think having a signature system would be better, let me know.

mchakravarty

Sorry, I only had a quick look, but something is strange with this PR. It, for example, deletes docs/fomega/src/AlgTypes.hs and touches some other files that have nothing to do with the spec. I think, something might have gone wrong in the git massaging.

mchakravarty · 2018-10-09T12:29:10Z

docs/fomega/src/AlgTypes.hs

@@ -1,167 +0,0 @@
-{-# LANGUAGE GADTs           #-}


Why are you deleting this file?

I must have updated my fork before the most recent branch of the IOHK repo. :(

vmchale · 2018-10-09T14:57:44Z

plutus-core-spec/figures/PlutusCoreBuiltins.tex

-        \texttt{multiplyInteger}   &  \forall s :: size.\ integer_s \to integer_s \to integer_s  &  s!i_0 , s!i_1   & s!(i_0 * i_1)                     & -2^{8s-1} \leq i_0 * i_1 < 2^{8s-1}\\
-        \texttt{divideInteger}     &  \forall s :: size.\ integer_s \to integer_s \to integer_s  &  s!i_0 , s!i_1   & s!(\operatorname{div}\ i_0\ i_1)                     & i_1 \not= 0\\
-        \texttt{remainderInteger}  &  \forall s :: size.\ integer_s \to integer_s \to integer_s  &  s!i_0 , s!i_1   & s!(\operatorname{mod} \ i_0 \ i_1)                     & i_1 \not= 0\\
+        \texttt{addInteger}        &  \sig{s :: size}{integer_s, integer_s}{integer_s}  &  s & s!i_0 , s!i_1   & s!(i_0 + i_1)                     & -2^{8s-1} \leq i_0 + i_1 < 2^{8s-1}\\


Are there any efficiency sacrifices in taking the size as an argument? Or is this just rewriting the LaTeX?

I'm not entirely sure what you mean; can you elaborate on precisely what change or precise part of the spec you're referring to?

vmchale · 2018-10-09T14:58:42Z

plutus-core-spec/figures/PlutusCoreGrammar.tex

                                  &        &     & \funT{A}{B}                & \textrm{function type}\\
                                  &        &     & \allT{\alpha}{K}{A}        & \textrm{polymorphic type}\\
                                  &        &     & \fixT{\alpha}{A}           & \textrm{fixed point type}\\
                                  &        &     & \lamT{\alpha}{K}{A}        & \textrm{$\lambda$ abstraction}\\
                                  &        &     & \appT{A}{B}                & \textrm{function application}\\
-                                  &        &     & \conT{tcn}                 & \textrm{builtin type}\\
-        \textrm{Type Value}       & R,S,T  & ::= & \funT{S}{T}                & \textrm{function type}\\
+                                  &        &     & \conT{tcn}{A}          & \textrm{type constant}\\


I think it's for alignment.

vmchale · 2018-10-09T15:02:42Z

plutus-core-spec/figures/PlutusCoreReduction.tex

@@ -9,9 +9,9 @@
 \begin{figure*}
    \centering
    \[\begin{array}{lrclr}
-        \textrm{Type Frame} & f  & ::= & \inFunTLeft{\_}{A}                        & \textrm{left arrow}\\
+        \textrm{Type Frame} & f  & ::= & \inConT{tcn}{\_}                          & \textrm{type constant}\\


Why did we remove inFixT? I thought it was agreed that not normalizing inside (fix a _) was bad, and I think some of the proofs depend on being able to normalize inside them.

michaelpj · 2018-10-15T11:47:55Z

What is this waiting on?

BekaValentine · 2018-10-15T21:28:06Z

Partially clarifications from others, partially figuring out how to make sure this merges correctly. I'm going to make a new PR (I've wiped the entire repo this was pointing to so I'm not sure if this will even merge now).

* SCP-3081 added chain-index queries for transactions at address 1. Added queries to chain index. a. Query `TxOutRef`s at address. b. Find `ChainIndexTx`s for a list of `TxId`s. 2. Tested manually. * SCP-3081 added chain-index queries to plutus-contract 1. Added new queries from plutus-chain-index query effect to plutus-contract. 2. Added functions to query transaction history at address. a. `txsAt` b. `txoRefsAt` c. `txsFromTxIds` 3. Manually tested. * SCP-3081 added missing export * SCP-3081 removed lint * SCP-3081 added new query functions to request handler * SCP-3081 added chain-index queries to plutus-pab * SCP-3081 address and txs queries rebased to latest main 1. OpenApi support for `TxoRefsAtAddress` and `TxsFromTxIds`. 2. Wrapped paged response for `TxoRefsAtAddressRequest`. 3. Retested, with spot-check comparisons against db-sync. * fixed stylish haskell * fixed type mapping to purescript generated Co-authored-by: Sjoerd Visscher <[email protected]>

psygnisfive added 5 commits October 8, 2018 15:17

Updates from ShareLaTeX

113cf13

Updates from ShareLaTeX

5127356

Merge sharelatex-2018-10-08-2214 into master

ef5cdeb

Merge sharelatex-2018-10-08-2217 into master

1cc0c7a

Updates spec w/ most recent version of builtins

a5e109a

BekaValentine requested review from vmchale, michaelpj, Cubesoup and mchakravarty October 9, 2018 10:00

effectfully reviewed Oct 9, 2018

View reviewed changes

mchakravarty suggested changes Oct 9, 2018

View reviewed changes

vmchale suggested changes Oct 9, 2018

View reviewed changes

psygnisfive added 2 commits October 12, 2018 16:03

fixes some weird issues from before that broke overleaf builds

bbd4a09

Fixes a bunch of other oversights/bugs in the spec.

54062bf

BekaValentine closed this Oct 15, 2018

rmourey26 mentioned this pull request Nov 5, 2022

[Snyk] Fix for 1 vulnerabilities rmourey26/plutus#37

Open

rmourey26 mentioned this pull request Dec 26, 2022

[Snyk] Fix for 1 vulnerabilities rmourey26/plutus#50

Open

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

Updates spec with new builtins, etc. #182

Updates spec with new builtins, etc. #182

BekaValentine commented Oct 9, 2018

effectfully left a comment

effectfully Oct 9, 2018

effectfully Oct 9, 2018

effectfully Oct 9, 2018

BekaValentine Oct 12, 2018

michaelpj Oct 13, 2018 •

edited

Loading

michaelpj Oct 13, 2018

effectfully Oct 9, 2018

vmchale Oct 9, 2018

BekaValentine Oct 12, 2018

effectfully Oct 15, 2018 •

edited

Loading

BekaValentine Oct 15, 2018

mchakravarty left a comment

mchakravarty Oct 9, 2018

BekaValentine Oct 12, 2018

vmchale Oct 9, 2018

BekaValentine Oct 12, 2018

vmchale Oct 9, 2018

vmchale Oct 9, 2018

michaelpj commented Oct 15, 2018

BekaValentine commented Oct 15, 2018

Updates spec with new builtins, etc. #182

Updates spec with new builtins, etc. #182

Conversation

BekaValentine commented Oct 9, 2018

effectfully left a comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

michaelpj Oct 13, 2018 • edited Loading

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

effectfully Oct 15, 2018 • edited Loading

Choose a reason for hiding this comment

Choose a reason for hiding this comment

mchakravarty left a comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

michaelpj commented Oct 15, 2018

BekaValentine commented Oct 15, 2018

michaelpj Oct 13, 2018 •

edited

Loading

effectfully Oct 15, 2018 •

edited

Loading