Cherry-pick PRs for release 4.1.x

.github/workflows/ci.yml

@@ -30,18 +30,27 @@ jobs:
         run: |
               wget https://raw.githubusercontent.com/leanprover/elan/master/elan-init.sh
               bash elan-init.sh -y
-      - name: Build
+      - name: Download dependencies
+        working-directory: ./cedar-lean
+        shell: bash
+        run: source ~/.profile && lake -R -Kenv=dev update
+      - name: Build proofs
         working-directory: ./cedar-lean
         shell: bash
         run: source ~/.profile && lake build Cedar
-      - name: Test
+      - name: Run unit tests
         working-directory: ./cedar-lean
         shell: bash
         run: source ~/.profile && lake exe CedarUnitTests
       - name: Test CLI
         working-directory: ./cedar-lean
         shell: bash
         run: source ~/.profile && ./test_cli.sh
+      - name: Build docs
+        working-directory: ./cedar-lean
+        shell: bash
+        run: source ~/.profile && lake -R -Kenv=dev build Cedar:docs
+
 
   build_and_test_drt:
     needs: get-branch-name

.github/workflows/deploy_docs.yml

@@ -34,14 +34,14 @@ jobs:
         run: |
               wget https://raw.githubusercontent.com/leanprover/elan/master/elan-init.sh
               bash elan-init.sh -y
-      - name: Download doc-gen4
+      - name: Download dependencies
         working-directory: ./cedar-lean
         shell: bash
-        run: source ~/.profile && sed -i '/^meta if get_config? env = some "dev" then/d' lakefile.lean && lake update doc-gen4
+        run: source ~/.profile && lake -R -Kenv=dev update
       - name: Build docs
         working-directory: ./cedar-lean
         shell: bash
-        run: source ~/.profile && lake -Kenv=dev build Cedar:docs
+        run: source ~/.profile && lake -R -Kenv=dev build Cedar:docs
       - name: Move documentation to `docs/docs`
         run: |
               mkdir docs

README.md

@@ -22,6 +22,7 @@ See the README in each directory for more information.
 * Install Lean, following the instructions [here](https://leanprover.github.io/lean4/doc/setup.html).
 * `cd cedar-lean`
 * `source ../cedar-drt/set_env_vars.sh` (only required if running on AL2)
+* `lake update`
 * `lake build Cedar`
 
 ### DRT framework

cedar-drt/Cargo.toml

@@ -18,7 +18,7 @@ miette = "7.1.0"
 serde = { version = "1.0", features = ["derive"] }
 serde_json = "1.0"
 lazy_static = "1.4"
-smol_str = { version = "0.2", features = ["serde"] }
+smol_str = { version = "0.3", features = ["serde"] }
 
 [features]
 integration-testing = []

cedar-drt/build_lean_lib.sh

@@ -14,4 +14,5 @@
 # limitations under the License.
 
 # Build command needed for linking Lean lib with Rust code
+lake update
 lake build Cedar:static DiffTest:static Batteries:static

cedar-drt/fuzz/Cargo.toml

@@ -21,7 +21,7 @@ cedar-policy-formatter = { path = "../../cedar/cedar-policy-formatter", version
 cedar-testing = { path = "../../cedar/cedar-testing", version = "4.*" }
 cedar-policy-generators = { path = "../../cedar-policy-generators", version = "4.*" }
 miette = "7.1.0"
-smol_str = { version = "0.2", features = ["serde"] }
+smol_str = { version = "0.3", features = ["serde"] }
 regex = "1"
 rayon = { version = "1.5", optional = true }
 rand = { version = "0.8", features = ["small_rng"] }

cedar-drt/fuzz/fuzz_targets/convert-policy-json-to-cedar.rs

@@ -30,7 +30,8 @@ enum ESTParseError {
 }
 
 fuzz_target!(|est_json_str: String| {
-    if let Ok(ast_from_est) = serde_json::from_str::<cedar_policy_core::est::Policy>(&est_json_str)
+    if let Ok(ast_from_est) = serde_json::from_str::<serde_json::Value>(&est_json_str)
+        .and_then(|val| serde_json::from_value::<cedar_policy_core::est::Policy>(val))
         .map_err(ESTParseError::from)
         .and_then(|est| {
             est.try_into_ast_template(Some(PolicyID::from_string("policy0")))

cedar-drt/fuzz/fuzz_targets/validation-pbt-type-directed.rs

@@ -107,10 +107,12 @@ impl<'a> Arbitrary<'a> for FuzzTargetInput {
 }
 
 /// helper function that just tells us whether a policyset passes validation
-fn passes_validation(validator: &Validator, policyset: &ast::PolicySet) -> bool {
-    validator
-        .validate(policyset, ValidationMode::default())
-        .validation_passed()
+fn passes_validation(
+    validator: &Validator,
+    policyset: &ast::PolicySet,
+    mode: ValidationMode,
+) -> bool {
+    validator.validate(policyset, mode).validation_passed()
 }
 
 // The main fuzz target. This is for PBT on the validator
@@ -125,7 +127,10 @@ fuzz_target!(|input: FuzzTargetInput| {
             let mut policyset = ast::PolicySet::new();
             let policy: ast::StaticPolicy = input.policy.into();
             policyset.add_static(policy.clone()).unwrap();
-            if passes_validation(&validator, &policyset) {
+            let passes_strict = passes_validation(&validator, &policyset, ValidationMode::Strict);
+            let passes_permissive =
+                passes_validation(&validator, &policyset, ValidationMode::Permissive);
+            if passes_permissive {
                 // policy successfully validated, let's make sure we don't get any
                 // dynamic type errors
                 let authorizer = Authorizer::new();
@@ -172,6 +177,12 @@ fuzz_target!(|input: FuzzTargetInput| {
                         "validated policy produced unexpected errors {unexpected_errs:?}!\npolicies:\n{policyset}\nentities:\n{entities}\nschema:\n{schemafile_string}\nrequest:\n{q}\n",
                     )
                 }
+            } else {
+                assert_eq!(
+                    false,
+                    passes_strict,
+                    "policy fails permissive validation but passes strict validation!\npolicies:\n{policyset}\nentities:\n{entities}\nschema:\n{schemafile_string}\n",
+                );
             }
         }
     }

cedar-drt/fuzz/fuzz_targets/validation-pbt.rs

@@ -306,10 +306,12 @@ impl<'a> Arbitrary<'a> for FuzzTargetInput {
 }
 
 /// helper function that just tells us whether a policyset passes validation
-fn passes_validation(validator: &Validator, policyset: &ast::PolicySet) -> bool {
-    validator
-        .validate(policyset, ValidationMode::default())
-        .validation_passed()
+fn passes_validation(
+    validator: &Validator,
+    policyset: &ast::PolicySet,
+    mode: ValidationMode,
+) -> bool {
+    validator.validate(policyset, mode).validation_passed()
 }
 
 // The main fuzz target. This is for PBT on the validator
@@ -332,11 +334,15 @@ fuzz_target!(|input: FuzzTargetInput| {
             let mut policyset = ast::PolicySet::new();
             let policy: ast::StaticPolicy = input.policy.into();
             policyset.add_static(policy.clone()).unwrap();
-            if passes_validation(&validator, &policyset) {
+            let passes_strict = passes_validation(&validator, &policyset, ValidationMode::Strict);
+            let passes_permissive =
+                passes_validation(&validator, &policyset, ValidationMode::Permissive);
+            if passes_permissive {
                 checkpoint(LOG_FILENAME_VALIDATION_PASS);
-                maybe_log_schemastats(schemafile.as_ref(), "vyes");
-                maybe_log_hierarchystats(&input.hierarchy, "vyes");
-                maybe_log_policystats(&policy, "vyes");
+                let suffix = if passes_strict { "vyes" } else { "vpermissive" };
+                maybe_log_schemastats(schemafile.as_ref(), suffix);
+                maybe_log_hierarchystats(&input.hierarchy, suffix);
+                maybe_log_policystats(&policy, suffix);
                 // policy successfully validated, let's make sure we don't get any
                 // dynamic type errors
                 let authorizer = Authorizer::new();
@@ -387,6 +393,11 @@ fuzz_target!(|input: FuzzTargetInput| {
                 maybe_log_schemastats(schemafile.as_ref(), "vno");
                 maybe_log_hierarchystats(&input.hierarchy, "vno");
                 maybe_log_policystats(&policy, "vno");
+                assert_eq!(
+                    false,
+                    passes_strict,
+                    "policy fails permissive validation but passes strict validation!\npolicies:\n{policyset}\nentities:\n{entities}\nschema:\n{schemafile_string}\n",
+                );
             }
         }
     }