diff --git a/.github/workflows/acl2.yml b/.github/workflows/acl2.yml
index 68a0b47624..f027739300 100644
--- a/.github/workflows/acl2.yml
+++ b/.github/workflows/acl2.yml
@@ -1,6 +1,6 @@
name: Leo-ACL2
on: workflow_dispatch
-env:
+env:
RUST_BACKTRACE: 1
# This job can only be run on linux (Ubuntu)
@@ -28,35 +28,37 @@ jobs:
- name: Pull tgc executable
run: |
mkdir acl2 && cd acl2;
- wget $(curl -s https://api.github.com/repos/AleoHQ/leo-acl2-bin/releases/latest \
- | grep "browser_download_url.*.tgz" \
- | cut -d : -f 2,3 \
- | tr -d \" \
- | xargs)
+ wget $( curl -s https://api.github.com/repos/AleoHQ/leo-acl2-bin/releases/latest \
+ | jq -r '.assets[0].browser_download_url' )
+ echo "Unpacking $(ls):"
tar -xvzf $(ls)
-
- # Using the prepared ASTs and the pulled and unzipped tgc run theorem generation.
+
+ # Run theorem generation and checking using the prepared ASTs and the pulled and unzipped leo-acl2 tarball.
- name: Run tgc over ASTs
run: |
canonicalization_errors=();
type_inference_errors=();
+ num_dirs=0;
for dir in `ls tmp/tgc`;
do
cd tmp/tgc/$dir; # enter the directory
+ num_dirs=$((num_dirs + 1));
./../../../acl2/tgc canonicalization initial_ast.json canonicalization_ast.json canonicalization-theorem.lisp > canonicalization_result.out || canonicalization_errors+=("$dir");
- # Disabling Type inference for now
./../../../acl2/tgc type-inference canonicalization_ast.json type_inferenced_ast.json type-inference-theorem.lisp > type_inference_result.out || type_inference_errors+=("$dir");
cd ../../..
done;
+ echo "----------------"
+ echo "Ran tgc in ${num_dirs} directories."
+ echo "----------------"
if [ ${#canonicalization_errors[@]} -eq 0 ]; then
echo "Canonicalization - Success!"
else
- echo "Canonicalization Failures:";
+ echo "Canonicalization Failures (total: ${#canonicalization_errors[@]}):"
for dir in ${canonicalization_errors[@]};
do
- echo $dir;
+ echo $dir
done;
#echo "Attaching logs:"
@@ -65,16 +67,16 @@ jobs:
# cat tmp/tgc/$dir/canonicalization_result.out
# cat tmp/tgc/$dir/canonicalization-theorem.lisp
#done;
- exit 1
fi
+ echo "----------------"
if [ ${#type_inference_errors[@]} -eq 0 ]; then
echo "Type Inference - Success!"
else
- echo "Type Inference Failures:";
+ echo "Type Inference Failures (total: ${#type_inference_errors[@]}):"
for dir in ${type_inference_errors[@]};
do
- echo $dir;
+ echo $dir
done;
#echo "Attaching logs:"
@@ -82,6 +84,10 @@ jobs:
#do
# cat tmp/tgc/$dir/type_inference_result.out
#done;
+ fi
+ if [[ ${#canonicalization_errors[@]} -ne 0 || ${#type_inference_errors[@]} -ne 0 ]]; then
+ echo "----------------"
+ echo "Exiting with status 1 due to at least one tgc error."
exit 1
fi
diff --git a/Cargo.lock b/Cargo.lock
index 0af4ad8d82..00ca564213 100644
--- a/Cargo.lock
+++ b/Cargo.lock
@@ -590,9 +590,9 @@ dependencies = [
[[package]]
name = "dirs"
-version = "3.0.2"
+version = "4.0.0"
source = "registry+https://github.com/rust-lang/crates.io-index"
-checksum = "30baa043103c9d0c2a57cf537cc2f35623889dc0d405e6c3cccfadbc81c71309"
+checksum = "ca3aa72a6f96ea37bbc5aa912f6788242832f75369bdfdadcb0e38423f100059"
dependencies = [
"dirs-sys",
]
@@ -925,6 +925,12 @@ version = "0.25.0"
source = "registry+https://github.com/rust-lang/crates.io-index"
checksum = "f0a01e0497841a3b2db4f8afa483cce65f7e96a3498bd6c541734792aeac8fe7"
+[[package]]
+name = "glob"
+version = "0.3.0"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "9b919933a397b79c37e33b77bb2aa3dc8eb6e165ad809e58ff75bc7db2e34574"
+
[[package]]
name = "h2"
version = "0.3.3"
@@ -1065,6 +1071,30 @@ dependencies = [
"unicode-normalization",
]
+[[package]]
+name = "include_dir"
+version = "0.6.2"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "24b56e147e6187d61e9d0f039f10e070d0c0a887e24fe0bb9ca3f29bfde62cab"
+dependencies = [
+ "glob",
+ "include_dir_impl",
+ "proc-macro-hack",
+]
+
+[[package]]
+name = "include_dir_impl"
+version = "0.6.2"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "0a0c890c85da4bab7bce4204c707396bbd3c6c8a681716a51c8814cfc2b682df"
+dependencies = [
+ "anyhow",
+ "proc-macro-hack",
+ "proc-macro2 1.0.27",
+ "quote 1.0.9",
+ "syn 1.0.73",
+]
+
[[package]]
name = "indenter"
version = "0.3.3"
@@ -1239,6 +1269,7 @@ dependencies = [
"leo-ast",
"leo-errors",
"leo-parser",
+ "leo-stdlib",
]
[[package]]
@@ -1300,7 +1331,6 @@ name = "leo-imports"
version = "1.5.3"
dependencies = [
"indexmap",
- "leo-asg",
"leo-ast",
"leo-ast-passes",
"leo-errors",
@@ -1342,6 +1372,7 @@ dependencies = [
"leo-package",
"leo-parser",
"leo-state",
+ "leo-stdlib",
"leo-synthesizer",
"notify",
"rand 0.8.4",
@@ -1416,6 +1447,17 @@ dependencies = [
"snarkvm-utilities",
]
+[[package]]
+name = "leo-stdlib"
+version = "1.5.3"
+dependencies = [
+ "include_dir",
+ "indexmap",
+ "leo-ast",
+ "leo-errors",
+ "leo-parser",
+]
+
[[package]]
name = "leo-synthesizer"
version = "1.5.3"
@@ -1441,8 +1483,10 @@ dependencies = [
"leo-ast",
"leo-ast-passes",
"leo-compiler",
+ "leo-errors",
"leo-imports",
"leo-parser",
+ "regex",
"serde",
"serde_json",
"serde_yaml",
@@ -2007,6 +2051,12 @@ dependencies = [
"version_check",
]
+[[package]]
+name = "proc-macro-hack"
+version = "0.5.19"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "dbf0c48bc1d91375ae5c3cd81e3722dff1abcf81a30960240640d223f59fe0e5"
+
[[package]]
name = "proc-macro2"
version = "0.4.30"
@@ -2997,9 +3047,9 @@ checksum = "360dfd1d6d30e05fda32ace2c8c70e9c0a9da713275777f5a4dbb8a1893930c6"
[[package]]
name = "tracing"
-version = "0.1.26"
+version = "0.1.28"
source = "registry+https://github.com/rust-lang/crates.io-index"
-checksum = "09adeb8c97449311ccd28a427f96fb563e7fd31aabf994189879d9da2394b89d"
+checksum = "84f96e095c0c82419687c20ddf5cb3eadb61f4e1405923c9dc8e53a1adacbda8"
dependencies = [
"cfg-if 1.0.0",
"pin-project-lite",
@@ -3009,9 +3059,9 @@ dependencies = [
[[package]]
name = "tracing-attributes"
-version = "0.1.15"
+version = "0.1.16"
source = "registry+https://github.com/rust-lang/crates.io-index"
-checksum = "c42e6fa53307c8a17e4ccd4dc81cf5ec38db9209f59b222210375b54ee40d1e2"
+checksum = "98863d0dd09fa59a1b79c6750ad80dbda6b75f4e71c437a6a1a8cb91a8bcbd77"
dependencies = [
"proc-macro2 1.0.27",
"quote 1.0.9",
@@ -3020,9 +3070,9 @@ dependencies = [
[[package]]
name = "tracing-core"
-version = "0.1.18"
+version = "0.1.20"
source = "registry+https://github.com/rust-lang/crates.io-index"
-checksum = "a9ff14f98b1a4b289c6248a023c1c2fa1491062964e9fed67ab29c4e4da4a052"
+checksum = "46125608c26121c81b0c6d693eab5a420e416da7e43c426d2e8f7df8da8a3acf"
dependencies = [
"lazy_static",
]
diff --git a/Cargo.toml b/Cargo.toml
index 4b3827e6b3..546d98e64f 100644
--- a/Cargo.toml
+++ b/Cargo.toml
@@ -39,6 +39,7 @@ members = [
"package",
"parser",
"state",
+ "stdlib",
"synthesizer",
"test-framework",
"wasm"
@@ -76,6 +77,10 @@ version = "1.5.3"
path = "./state"
version = "1.5.3"
+[dependencies.leo-stdlib]
+path = "./stdlib"
+version = "1.5.3"
+
[dependencies.leo-synthesizer]
path = "./synthesizer"
version = "1.5.3"
@@ -111,7 +116,7 @@ color-backtrace = "0.5.1"
version = "2.0"
[dependencies.dirs]
-version = "3.0.2"
+version = "4.0.0"
[dependencies.console]
version = "0.14.0"
diff --git a/asg/src/expression/lengthof.rs b/asg/src/expression/lengthof.rs
new file mode 100644
index 0000000000..ee8c883ebb
--- /dev/null
+++ b/asg/src/expression/lengthof.rs
@@ -0,0 +1,89 @@
+// Copyright (C) 2019-2021 Aleo Systems Inc.
+// This file is part of the Leo library.
+
+// The Leo library is free software: you can redistribute it and/or modify
+// it under the terms of the GNU General Public License as published by
+// the Free Software Foundation, either version 3 of the License, or
+// (at your option) any later version.
+
+// The Leo library is distributed in the hope that it will be useful,
+// but WITHOUT ANY WARRANTY; without even the implied warranty of
+// MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
+// GNU General Public License for more details.
+
+// You should have received a copy of the GNU General Public License
+// along with the Leo library. If not, see .
+
+use crate::{ConstValue, Expression, ExpressionNode, FromAst, IntegerType, Node, PartialType, Scope, Type};
+pub use leo_ast::UnaryOperation;
+use leo_errors::{Result, Span};
+
+use std::cell::Cell;
+
+#[derive(Clone)]
+pub struct LengthOfExpression<'a> {
+ pub parent: Cell