* Fix record update evaluation order.
This PR only fixes the evaluation order for single-constructor record
types. Fixing it for variant records, if we do, will be a major
challenge.
This PR also adds a regression test.
changelog_begin
changelog_end
* fix daml-lf-verify
The whole instPrSelf thing is just repeating what DecodeAsDependency
does. Handling unqualified TypeConNames also sounds very questionable
so I changed that as well. Sadly this doesn’t fix the issue I was
hoping to fix.
changelog_begin
changelog_end
Implementing substitution once is scary enough, let’s not implement it
twice.
Sadly this is also does not fix the bug I was hoping to address.
I would not be surprised if it does fix some bugs but given that I
don’t know which there is no new testcase.
changelog_begin
changelog_end
Verification tool update:
- Support for recursion and mutual recursion.
- Significant code cleanup and bugfixes.
- Minor improvements: keep track of more typing information, handle updates properly when called multiple times, support additional operators, more test cases etc.
* First draft of constant lifting
changelog_begin
changelog_end
* refactoring
* doing stuff
* run simplifier on template exprs
* remove merge artifact
* Fix ExerciseWithoutActors
* add comments
* fix trace order test
* prefix generated val names with their provenance
* Verification tool bugfix
During the value collection phase, when encountering a record projection on a (yet) undefined value, stop searching this branch instead of throwing an error.
* Bump pattern-match-perf memory limit with cocreature`s blessing
* bump again
* Filter generated identifiers from daml script test runner
changelog_begin
changelog_end
* Fix party literals
* Remove inlineClosedExpr for now.
* Improve comments
* Reset script test locations
* Unhashmap
* disable daml-lf-verify quickstart tests for now
Co-authored-by: Gert-Jan Bottu <gertjan.bottu@kuleuven.be>
Co-authored-by: Moritz Kiefer <moritz.kiefer@purelyfunctional.org>
* damlc: Run simplifier on templates as well
Currently, the simplifier only runs on top-level value definitions.
However, there's no good reason for not running it on all expressions
within templates as well.
This does not significantly improve the `CollectAuthority` benchmark,
but there's not much code in the templates.
CHANGELOG_BEGIN
CHANGELOG_END
* Verification tool bugfix in variable projection and substitution with… (#6344)
* Verification tool bugfix in variable projection and substitution within let expressions
* Remove redundant substitution ; apply feedback Martin
Co-authored-by: Gert-Jan Bottu <gertjanbottu@hotmail.com>
First version of static verification tool.
The current state of the tool:
- Reads DAR files.
- Partially evaluates the code.
- Generates constraints for the field and choice to be verified.
- Passes the constraints to an SMT solver.
- Some basic tests.
