fix a few more things in the daml-lf spec #11851
Merged
Conversation
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
CHANGELOG_BEGIN CHANGELOG_END
andreaslochbihler-da
requested review from
cocreature and
remyhaemmerle-da
as code owners
remyhaemmerle-da
approved these changes
Nov 24, 2021
There was a problem hiding this comment.
Thanks a lot.
@sofiafaro-da could you check that my amendments are correct ?
daml-lf/spec/daml-lf-1.rst
Outdated
| @@ -1231,9 +1231,9 @@ Then we define *well-formed expressions*. :: | |||
| ——————————————————————————————————————————————————————————————— ExpFromAnyException [Daml-LF ≥ 1.14] | |||
| Γ ⊢ 'from_any_exception' @τ e : 'Optional' τ | |||
|
|
|||
| Γ ⊢ τ : ⋆ Γ ⊢ e : τ | |||
| τ₁ ↠ τ₁' Γ ⊢ τ' : ⋆ Γ ⊢ e : τ' | |||
There was a problem hiding this comment.
Suggested change
| τ₁ ↠ τ₁' Γ ⊢ τ' : ⋆ Γ ⊢ e : τ' | |
| τ ↠ τ' Γ ⊢ τ' : ⋆ Γ ⊢ e : τ' |
daml-lf/spec/daml-lf-1.rst
Outdated
| ⊢ᵥ LitRoundingMode | ||
|
|
||
|
|
||
| ┌────────┐ | ||
| Update Values │ ⊢ᵥᵤ u │ | ||
| └────────┘ | ||
|
|
||
| ⊢ᵥ e | ||
| ⊢ᵥᵤ e |
There was a problem hiding this comment.
It think this one is correct.
Suggested change
| ⊢ᵥᵤ e | |
| ⊢ᵥ e |
There was a problem hiding this comment.
For well-typed terms, the two are equivalent. But I find it easier to understand if we require an update value here rather than an arbitrary value.
There was a problem hiding this comment.
With your change, 'pure' @Unit () is not anymore a (update) value.
There was a problem hiding this comment.
By the way, we need to add an extra @τ in UpdPure and ScnPure typing rules.
There was a problem hiding this comment.
This one should be ⊢ᵥ e since any value can appear in a pure.
There was a problem hiding this comment.
You're right. 🤦♂️
| ——————————————————————————————————————————————————— ValUpdatePure | ||
| ⊢ᵥᵤ 'pure' @τ e | ||
|
|
||
| ⊢ᵥ e₁ | ||
| ⊢ᵥᵤ e₁ |
There was a problem hiding this comment.
problably better like that, but note that thanks to ValUpdate rule this was actually correct as well before your changed.
There was a problem hiding this comment.
For well-typed terms, the two are equivalent. But I find it easier to understand if we require an update value here rather than an arbitrary value.
In this case, I agree.
daml-lf/spec/daml-lf-1.rst
Outdated
Comment on lines
2973
to
2982
| 'tpl' (x : T) | ||
| ↦ { 'choices' { …, 'choice' ChKind Ch (y : 'ContractId' Mod:T) (z : τ) : σ 'by' eₚ 'observers' eₒ ↦ eₐ, … }, … } ∈ 〚Ξ〛Mod | ||
| cid ∈ dom(st₀) | ||
| st(cid) = (Mod':T', vₜ, 'inactive') | ||
| Mod:T ≠ Mod':T' | ||
| —————————————————————————————————————————————————————————————————————— EvUpdExercWrongTemplate | ||
| 'exercise' Mod:T.Ch cid v₁ ‖ (st; keys₀) | ||
| ⇓ᵤ | ||
| (Err (Fatal "Exercise on contract of wrong template"), ε) | ||
|
|
There was a problem hiding this comment.
Good catch. However, I think it should go between EvUpdExercNestingArgErr and EvUpdExercBodyEvalErr,
Suggested change
| 'tpl' (x : T) | |
| ↦ { 'choices' { …, 'choice' ChKind Ch (y : 'ContractId' Mod:T) (z : τ) : σ 'by' eₚ 'observers' eₒ ↦ eₐ, … }, … } ∈ 〚Ξ〛Mod | |
| cid ∈ dom(st₀) | |
| st(cid) = (Mod':T', vₜ, 'inactive') | |
| Mod:T ≠ Mod':T' | |
| —————————————————————————————————————————————————————————————————————— EvUpdExercWrongTemplate | |
| 'exercise' Mod:T.Ch cid v₁ ‖ (st; keys₀) | |
| ⇓ᵤ | |
| (Err (Fatal "Exercise on contract of wrong template"), ε) | |
| 'tpl' (x : T) | |
| ↦ { 'choices' { …, 'choice' ChKind Ch (y : 'ContractId' Mod:T) (z : τ) : σ 'by' eₚ 'observers' eₒ ↦ eₐ, … }, … } ∈ 〚Ξ〛Mod | |
| cid ∈ dom(st₀) | |
| st₀(cid) = (Mod':T', vₜ, 'active') | |
| eₚ[x ↦ vₜ, z ↦ v₁] ⇓ Ok vₚ | |
| eₒ[x ↦ vₜ, z ↦ v₁] ⇓ Ok vₒ | |
| |v₁| ≤ 100 | |
| Mod:T ≠ Mod':T' | |
| —————————————————————————————————————————————————————————————————————— EvUpdExercWrongTemplate | |
| 'exercise' Mod:T.Ch cid v₁ ‖ (st; keys₀) | |
| ⇓ᵤ | |
| (Err (Fatal "Exercise on contract of wrong template"), ε) | |
There was a problem hiding this comment.
In addition, the lines
st₀(cid) = (Mod:T, vₜ, 'active')
should be changed by
st₀(cid) = (Mod':T', vₜ, 'active')
in the rules from EvUpdExercInactive to EvUpdExercNestingArgErr (both included).
There was a problem hiding this comment.
I'd like this rule added to compiler/damlc/tests/daml-test-files/SemanticsEvalOrder.daml (and a test for EvUpdNestingArgErr as well...). We can add these in a separate PR.
There was a problem hiding this comment.
I'd like this rule added to compiler/damlc/tests/daml-test-files/SemanticsEvalOrder.daml (and a test for EvUpdNestingArgErr as well...). We can add these in a separate PR.
Problably not a job for @andreaslochbihler-da. Should we create an issue ?
There was a problem hiding this comment.
Good idea, here is the issue: #11861
daml-lf/spec/daml-lf-1.rst
Outdated
Comment on lines
3135
to
3142
| 'tpl' (x : T) ↦ … ∈ 〚Ξ〛Mod | ||
| cid ∈ dom(st) | ||
| st(cid) = (Mod':T', vₜ, 'inactive') | ||
| Mod:T ≠ Mod':T' | ||
| —————————————————————————————————————————————————————————————————————— EvUpdFetchWrongTemplate | ||
| 'fetch' @Mod:T cid ‖ (st; keys) | ||
| ⇓ᵤ | ||
| (Err (Fatal "Fetch on contract of wrong template"), ε) |
There was a problem hiding this comment.
Same here, this is the last check, i.e. is going after EvUpFetchInactive
Suggested change
| 'tpl' (x : T) ↦ … ∈ 〚Ξ〛Mod | |
| cid ∈ dom(st) | |
| st(cid) = (Mod':T', vₜ, 'inactive') | |
| Mod:T ≠ Mod':T' | |
| —————————————————————————————————————————————————————————————————————— EvUpdFetchWrongTemplate | |
| 'fetch' @Mod:T cid ‖ (st; keys) | |
| ⇓ᵤ | |
| (Err (Fatal "Fetch on contract of wrong template"), ε) | |
| 'tpl' (x : T) ↦ … ∈ 〚Ξ〛Mod | |
| cid ∈ dom(st) | |
| st(cid) = (Mod:T, vₜ, 'active') | |
| Mod:T ≠ Mod':T' | |
| —————————————————————————————————————————————————————————————————————— EvUpdFetchWrongTemplate | |
| 'fetch' @Mod:T cid ‖ (st; keys) | |
| ⇓ᵤ | |
| (Err (Fatal "Fetch on contract of wrong template"), ε) |
There was a problem hiding this comment.
Similarly the line
st(cid) = (Mod:T, vₜ, 'active')
should be changed by
st(cid) = (Mod':T', vₜ, 'active')
in EvUpdFetchInactive.
remyhaemmerle-da
force-pushed
the
lf-spec-more-fixes
branch
from
8e90167 to
ea3000e
Compare
|
@moritzkiefer-da @cocreature could you review ea3000e ? |
cocreature
reviewed
Nov 24, 2021
| @@ -2982,7 +2973,7 @@ as described by the ledger model:: | |||
| 'tpl' (x : T) | |||
| ↦ { 'choices' { …, 'choice' ChKind Ch (y : 'ContractId' Mod:T) (z : τ) : σ 'by' eₚ 'observers' eₒ ↦ eₐ, … }, … } ∈ 〚Ξ〛Mod | |||
| cid ∈ dom(st₀) | |||
| st₀(cid) = (Mod:T, vₜ, 'inactive') | |||
| st₀(cid) = (Mod':T', vₜ, 'inactive') | |||
There was a problem hiding this comment.
As mentioned in person, I am not sure if we really evaluate controllers before checking for template id mismatches.
There was a problem hiding this comment.
I think you are right. It should be just after Inactive rule.
azure-pipelines bot
pushed a commit
that referenced
this pull request
Dec 1, 2021
This PR has been created by a script, which is not very smart and does not have all the context. Please do double-check that the version prefix is correct before merging. @SamirTalwar-DA is in charge of this release. Commit log: ``` 683ab87 Move ghc-lib{,-parser} to bazel-haskell-deps (#11775) 9350632 Fix releasing of resources in case connection initialization failed (#11915) e1559af Update `ModelConformanceValidator` comments and prevent them from getting outdated easily (#11924) 16a41f7 Avoid package validation in speedy compilation benchmark. (#11927) 16135e6 Limit supported input versions in damlc to >= LF 1.8 (#11905) 0ee4154 Use Absolute-indexes as keys for the Env-mapping during closure-conversion (#11912) 1d7bca8 Add optional typerep argument in UExerciseInterface. (#11910) c2c22f8 kvutils: Protos no longer depend on the Daml-LF transaction proto [KVL-1166] (#11909) 5641948 [Docs] Add labels to error codes to support references to them (#11913) 0e77676 Update protobuf docs template to handle oneOf (#11887) 5a9481f unify heading markup according to README.md (#11919) 61334cf kvutils - Add Writer which can handle deduplication periods as offsets [KVL-1172] (#11900) 0b9d57b Add ContractDoesntImplementInterface error. (#11884) 49e5d41 align index.rst files for HTML and PDF (#11907) dbbb05f Split daml-lf encode/decode Haskell libraries (#11906) e5d3902 iface: support for fixed choices in TS codegen (#11630) 31cc540 Turn package name & version warnings into an error (#11859) 4e50060 self-service compat: set branch name to not main (#11902) 2f4aa47 refactor to avoid impossible code path (#11901) a81995c switch dev images to Temurin (#11895) f3a0e2e Set scalafmt dialect explicitly (#11898) 60e372d Don't run pruning tests on H2, they time-out (#11897) 58e69ad LF: replace "dev" LF version by "1.dev" in bazel files (#11894) 8ef348d Use absolute stack locations in SExpr1 (#11877) 071bcf7 update NOTICES file (#11892) a1705d6 participant-state - Add an implicit logging context to the write service [kvl-1072] (#11838) 9ff64f7 Change daml script’s sleep to sleep for a minimum amount of time (#11886) 132c277 Add a Canton sandbox to the SDK (#11881) 68a2343 Only run self-service compat job on PRs (#11893) c27406c [DPP-762][Self-service error codes] Automate generation of inventory of error categories. #11879 1379722 Adapt the compatibility exclusions (#11872) d66ecc9 LF: Drop Archive Snapshot for LF < 1.14 (#11820) abc141b Increase pruning tests timeout (#11891) 66b4074 Update protobuf docs plugin (#11880) b0dda53 LF check stable proto with buf and md5sum. (#11888) 056fc52 Log while processing base64 encoded server key [DPP-761] (#11835) dbda67b bump JVM in Docker image (#11883) f69bd68 ledger-api-bench-tool: Fix flaky `MetricsCollectorSpec` (#11750) cb758e8 Fix call to experimental interface signatory builtin (#11882) 024400b Error when fetching the wrong template id (via fetch by interface). (#11862) 0852c8f Make DA.List.Total return Optional instead (#11878) df37346 [JSON-API] Add query store metrics (#11809) 2f8f69e Drop DA.Next.Set and DA.Next.Map (#11864) 5f3a4d2 [Self-service error codes] Fix section numbering in pdf for error codes section by moving it a level higher. (#11867) cf3ac01 [Self-service error codes] Do not return error code id and definite_answer in metadata for security sensitive errors (#11828) 026b92a Add gRPC definitions for participant user management service (#11818) 2fde30d Disable writing volatile bits in Scala statsfile (#11875) 4ed9ded Remove xxd from dev-env (#11876) eaded41 remove mergify (#11866) 3cd5028 fix a few more things in the daml-lf spec (#11851) beca0ee Refactor StandaloneApiServer factory (#11842) 6356f13 Properly upgrade gRPC to 1.41.0 (#11858) f6accd3 Release 1.18 RC2 (#11869) d858873 fix main (#11868) da8dd7e rotate release duty after 1.18.0-snapshot.20211123.8463.0.bd2a6852 (#11845) 066da4f [Self-service error codes] Small fixes for docs/scripts/live-preview.sh (#11856) 258fb65 Document how to deal with HTTP JSON API schema changes (#11336) b8937ad ci: self-service compat test start (#11853) de8d15f fix Nix install on macOS nodes (#11696) b3d1d40 Expose submissionId via the Java bindings (#11839) (#11847) 86da6e8 LF: Test scala interface type checking (#11833) 5f52f00 increase linux cluster size (#11860) 5c12d75 Add a guard when exercising by interface. (#11836) 7c3a2a7 Add a new KV submission failure error (#11854) aebc5a7 All packages must be valid (#11850) 0374843 speedy compilation benchmark (#11852) 393893a LF encoder: make package validation optional (#11849) 25b476f DPP-726 Add string interning unit tests (#11841) 59eb0d2 kvutils - For duplicate command rejections, add the submission id as metadata [KVL-1175] (#11848) 970243d Ensure stack-safety during closure-conversion. (#11778) e63c80d update LATEST (#11846) db42521 libs-scala: Change `SourceQueueResourceOwner` to `BoundedSourceQueueResourceOwner` [KVL-1177] (#11832) 109b606 Make the `InstrumentedSource.queue` use the `BoundedSourceQueue` [KVL-1177] (#11807) ``` Changelog: ``` - [Daml Compiler] The supported input LF versions for data-dependencies are now limited to LF 1.8 and newer. - [Daml2js] DARs with LF version < 1.8 are no longer supported. - [Integration Kit] kvutils protos no longer depend on the Daml-LF transaction proto - [Daml Standard Library] DA.List.Total functions now return Optional instead of being polymorphic in the return type. DA.Optional.Total has been removed. - [JSON-API] added metrics to separately track: - time taken to update query-store ACS (from ledger) - lookup times for the query store - [Daml Standard Library] DA.Next.Map and DA.Next.Set have been removed after being deprecated since Daml-LF 1.11 - [Ledger API] Introduce gRPC definitions for experimental user managament service to manage users and their rights for interacting with the Ledger API served by a participant node. [HTTP JSON API] [Docs] Document lack of data continuity guarantees and how to deal with schema changes [Java Bindings] submissionId is now exposed via the bindings, see issue #11705 [Integration Kit] Add a new SUBMISSION_FAILED internal error kvutils - For duplicate command rejections, the submission id of the already accepted transaction is returning as part of the gRPC metadata. The submission id will be included under the key `existing_submission_id`. - [Integration Kit] `SourceQueueResourceOwner` has been renamed to `BoundedSourceQueueResourceOwner` and takes a `BoundedSourceQueue` from now on - [Integration Kit] InstrumentedSource.queue.offer no longer returns a Future ``` CHANGELOG_BEGIN CHANGELOG_END
cocreature
added a commit
that referenced
this pull request
Dec 1, 2021
* release 2.0.0-snapshot.20211130.8536.0.683ab871 This PR has been created by a script, which is not very smart and does not have all the context. Please do double-check that the version prefix is correct before merging. @SamirTalwar-DA is in charge of this release. Commit log: ``` 683ab87 Move ghc-lib{,-parser} to bazel-haskell-deps (#11775) 9350632 Fix releasing of resources in case connection initialization failed (#11915) e1559af Update `ModelConformanceValidator` comments and prevent them from getting outdated easily (#11924) 16a41f7 Avoid package validation in speedy compilation benchmark. (#11927) 16135e6 Limit supported input versions in damlc to >= LF 1.8 (#11905) 0ee4154 Use Absolute-indexes as keys for the Env-mapping during closure-conversion (#11912) 1d7bca8 Add optional typerep argument in UExerciseInterface. (#11910) c2c22f8 kvutils: Protos no longer depend on the Daml-LF transaction proto [KVL-1166] (#11909) 5641948 [Docs] Add labels to error codes to support references to them (#11913) 0e77676 Update protobuf docs template to handle oneOf (#11887) 5a9481f unify heading markup according to README.md (#11919) 61334cf kvutils - Add Writer which can handle deduplication periods as offsets [KVL-1172] (#11900) 0b9d57b Add ContractDoesntImplementInterface error. (#11884) 49e5d41 align index.rst files for HTML and PDF (#11907) dbbb05f Split daml-lf encode/decode Haskell libraries (#11906) e5d3902 iface: support for fixed choices in TS codegen (#11630) 31cc540 Turn package name & version warnings into an error (#11859) 4e50060 self-service compat: set branch name to not main (#11902) 2f4aa47 refactor to avoid impossible code path (#11901) a81995c switch dev images to Temurin (#11895) f3a0e2e Set scalafmt dialect explicitly (#11898) 60e372d Don't run pruning tests on H2, they time-out (#11897) 58e69ad LF: replace "dev" LF version by "1.dev" in bazel files (#11894) 8ef348d Use absolute stack locations in SExpr1 (#11877) 071bcf7 update NOTICES file (#11892) a1705d6 participant-state - Add an implicit logging context to the write service [kvl-1072] (#11838) 9ff64f7 Change daml script’s sleep to sleep for a minimum amount of time (#11886) 132c277 Add a Canton sandbox to the SDK (#11881) 68a2343 Only run self-service compat job on PRs (#11893) c27406c [DPP-762][Self-service error codes] Automate generation of inventory of error categories. #11879 1379722 Adapt the compatibility exclusions (#11872) d66ecc9 LF: Drop Archive Snapshot for LF < 1.14 (#11820) abc141b Increase pruning tests timeout (#11891) 66b4074 Update protobuf docs plugin (#11880) b0dda53 LF check stable proto with buf and md5sum. (#11888) 056fc52 Log while processing base64 encoded server key [DPP-761] (#11835) dbda67b bump JVM in Docker image (#11883) f69bd68 ledger-api-bench-tool: Fix flaky `MetricsCollectorSpec` (#11750) cb758e8 Fix call to experimental interface signatory builtin (#11882) 024400b Error when fetching the wrong template id (via fetch by interface). (#11862) 0852c8f Make DA.List.Total return Optional instead (#11878) df37346 [JSON-API] Add query store metrics (#11809) 2f8f69e Drop DA.Next.Set and DA.Next.Map (#11864) 5f3a4d2 [Self-service error codes] Fix section numbering in pdf for error codes section by moving it a level higher. (#11867) cf3ac01 [Self-service error codes] Do not return error code id and definite_answer in metadata for security sensitive errors (#11828) 026b92a Add gRPC definitions for participant user management service (#11818) 2fde30d Disable writing volatile bits in Scala statsfile (#11875) 4ed9ded Remove xxd from dev-env (#11876) eaded41 remove mergify (#11866) 3cd5028 fix a few more things in the daml-lf spec (#11851) beca0ee Refactor StandaloneApiServer factory (#11842) 6356f13 Properly upgrade gRPC to 1.41.0 (#11858) f6accd3 Release 1.18 RC2 (#11869) d858873 fix main (#11868) da8dd7e rotate release duty after 1.18.0-snapshot.20211123.8463.0.bd2a6852 (#11845) 066da4f [Self-service error codes] Small fixes for docs/scripts/live-preview.sh (#11856) 258fb65 Document how to deal with HTTP JSON API schema changes (#11336) b8937ad ci: self-service compat test start (#11853) de8d15f fix Nix install on macOS nodes (#11696) b3d1d40 Expose submissionId via the Java bindings (#11839) (#11847) 86da6e8 LF: Test scala interface type checking (#11833) 5f52f00 increase linux cluster size (#11860) 5c12d75 Add a guard when exercising by interface. (#11836) 7c3a2a7 Add a new KV submission failure error (#11854) aebc5a7 All packages must be valid (#11850) 0374843 speedy compilation benchmark (#11852) 393893a LF encoder: make package validation optional (#11849) 25b476f DPP-726 Add string interning unit tests (#11841) 59eb0d2 kvutils - For duplicate command rejections, add the submission id as metadata [KVL-1175] (#11848) 970243d Ensure stack-safety during closure-conversion. (#11778) e63c80d update LATEST (#11846) db42521 libs-scala: Change `SourceQueueResourceOwner` to `BoundedSourceQueueResourceOwner` [KVL-1177] (#11832) 109b606 Make the `InstrumentedSource.queue` use the `BoundedSourceQueue` [KVL-1177] (#11807) ``` Changelog: ``` - [Daml Compiler] The supported input LF versions for data-dependencies are now limited to LF 1.8 and newer. - [Daml2js] DARs with LF version < 1.8 are no longer supported. - [Integration Kit] kvutils protos no longer depend on the Daml-LF transaction proto - [Daml Standard Library] DA.List.Total functions now return Optional instead of being polymorphic in the return type. DA.Optional.Total has been removed. - [JSON-API] added metrics to separately track: - time taken to update query-store ACS (from ledger) - lookup times for the query store - [Daml Standard Library] DA.Next.Map and DA.Next.Set have been removed after being deprecated since Daml-LF 1.11 - [Ledger API] Introduce gRPC definitions for experimental user managament service to manage users and their rights for interacting with the Ledger API served by a participant node. [HTTP JSON API] [Docs] Document lack of data continuity guarantees and how to deal with schema changes [Java Bindings] submissionId is now exposed via the bindings, see issue #11705 [Integration Kit] Add a new SUBMISSION_FAILED internal error kvutils - For duplicate command rejections, the submission id of the already accepted transaction is returning as part of the gRPC metadata. The submission id will be included under the key `existing_submission_id`. - [Integration Kit] `SourceQueueResourceOwner` has been renamed to `BoundedSourceQueueResourceOwner` and takes a `BoundedSourceQueue` from now on - [Integration Kit] InstrumentedSource.queue.offer no longer returns a Future ``` CHANGELOG_BEGIN CHANGELOG_END * bump to include fix for damlc package validation changelog_begin changelog_end Co-authored-by: Azure Pipelines Daml Build <support@digitalasset.com> Co-authored-by: Moritz Kiefer <moritz.kiefer@purelyfunctional.org>
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
Add this suggestion to a batch that can be applied as a single commit.
This suggestion is invalid because no changes were made to the code.
Suggestions cannot be applied while the pull request is closed.
Suggestions cannot be applied while viewing a subset of changes.
Only one suggestion per line can be applied in a batch.
Add this suggestion to a batch that can be applied as a single commit.
Applying suggestions on deleted lines is not supported.
You must change the existing code in this line in order to create a valid suggestion.
Outdated suggestions cannot be applied.
This suggestion has been applied or marked resolved.
Suggestions cannot be applied from pending reviews.
Suggestions cannot be applied on multi-line comments.
Suggestions cannot be applied while the pull request is queued to merge.
Suggestion cannot be applied right now. Please check back later.
Pull Request Checklist
CHANGELOG_BEGINandCHANGELOG_ENDtagsNOTE: CI is not automatically run on non-members pull-requests for security
reasons. The reviewer will have to comment with
/AzurePipelines runtotrigger the build.