diff --git a/rust/tools/authorization-logic/BUILD b/rust/tools/authorization-logic/BUILD index a3bf7e4d4..0e856367e 100644 --- a/rust/tools/authorization-logic/BUILD +++ b/rust/tools/authorization-logic/BUILD @@ -94,6 +94,7 @@ filegroup( "src/test/test_multimic_overrides.rs", "src/test/test_multiverse_handling.rs", "src/test/test_negation.rs", + "src/test/test_num_compare.rs", "src/test/test_num_string_names.rs", "src/test/test_queries.rs", "src/test/test_relation_declarations.rs", diff --git a/rust/tools/authorization-logic/src/ast.rs b/rust/tools/authorization-logic/src/ast.rs index 619f9421b..f24b2ee5b 100644 --- a/rust/tools/authorization-logic/src/ast.rs +++ b/rust/tools/authorization-logic/src/ast.rs @@ -54,6 +54,13 @@ impl PartialEq for AstPredicate { // See https://doc.rust-lang.org/std/cmp/trait.Eq.html impl Eq for AstPredicate {} +#[derive(Debug, Clone, Serialize, Deserialize)] +pub struct AstArithmeticComparison { + pub lnum: String , + pub op: AstComparisonOperator, + pub rnum: String +} + #[derive(Debug, Clone, Serialize, Deserialize)] pub enum AstVerbPhrase { AstPredPhrase { p: AstPredicate }, @@ -72,10 +79,29 @@ pub enum AstFact { AstCanSayFact { p: AstPrincipal, f: Box }, } +#[derive(Copy, Debug, Clone, Serialize, Deserialize)] +pub enum AstComparisonOperator { + LessThan, + GreaterThan, + Equals, + NotEquals, + LessOrEquals, + GreaterOrEquals +} + +// RValues are the expressions that can appear on the right hand side of a +// conditional assertion. At the time of writing these include either +// AstFlatFacts or AstArithmeticComparisons. +#[derive(Debug, Clone, Serialize, Deserialize)] +pub enum AstRValue { + FlatFactRValue { flat_fact: AstFlatFact}, + ArithCompareRValue { arith_comp: AstArithmeticComparison } +} + #[derive(Debug, Clone, Serialize, Deserialize)] pub enum AstAssertion { AstFactAssertion { f: AstFact }, - AstCondAssertion { lhs: AstFact, rhs: Vec }, + AstCondAssertion { lhs: AstFact, rhs: Vec }, } #[derive(Debug, Clone, Serialize, Deserialize)] diff --git a/rust/tools/authorization-logic/src/parsing/AuthLogic.g4 b/rust/tools/authorization-logic/src/parsing/AuthLogic.g4 index b63e15ccd..5765f5b7f 100644 --- a/rust/tools/authorization-logic/src/parsing/AuthLogic.g4 +++ b/rust/tools/authorization-logic/src/parsing/AuthLogic.g4 @@ -32,8 +32,13 @@ principal : ID ; +pred_arg + : ID + | NUMLITERAL + ; + predicate - : (NEG)? ID '(' ID (',' ID)* ')' + : (NEG)? ID '(' pred_arg (',' pred_arg )* ')' ; verbphrase @@ -50,6 +55,20 @@ flatFact | predicate #predFact ; +binop + : LESSTHAN #ltbinop + | GRTHAN #grbinop + | EQUALS #eqbinop + | NEQUALS #nebinop + | LEQ #leqbinop + | GEQ #geqbinop + ; + +rvalue + : flatFact #flatFactRvalue + | pred_arg binop pred_arg #binopRvalue + ; + fact : flatFact #flatFactFact | principal CANSAY fact #canSayFact @@ -57,7 +76,7 @@ fact assertion : fact '.' #factAssertion - | fact ':-' flatFact (',' flatFact )* '.' #hornClauseAssertion + | fact ':-' rvalue (',' rvalue )* '.' #hornClauseAssertion ; // The IDs following "Export" are path names where JSON files containing @@ -120,10 +139,19 @@ ATTRIBUTE: 'attribute'; // Identifiers wrapped in quotes are constants whereas // identifiers without quotes are variables. -ID : ('"')? [_a-zA-Z0-9/.#:]* ('"')?; +ID : ('"')? [_a-zA-Z][_a-zA-Z0-9/.#:]* ('"')?; +NUMLITERAL : [0-9]+; NEG: '!'; +// BINOPS +LESSTHAN: '<'; +GRTHAN: '>'; +EQUALS: '='; +NEQUALS: '!='; +LEQ: '<='; +GEQ: '>='; + WHITESPACE_IGNORE : [ \r\t\n]+ -> skip ; diff --git a/rust/tools/authorization-logic/src/parsing/astconstructionvisitor.rs b/rust/tools/authorization-logic/src/parsing/astconstructionvisitor.rs index 8a9c0cb7b..e73f536f4 100644 --- a/rust/tools/authorization-logic/src/parsing/astconstructionvisitor.rs +++ b/rust/tools/authorization-logic/src/parsing/astconstructionvisitor.rs @@ -48,17 +48,11 @@ fn construct_predicate(ctx: &PredicateContext) -> AstPredicate { Some(_) => Sign::Negated, None => Sign::Positive }; - // Note that ID_all() in the generated antlr-rust code is buggy - // (because all {LEX_RULE}_all() generations are buggy), - // so rather than using a more idomatic iterator, "while Some(...)" is - // used here. - let name_ = ctx.ID(0).unwrap().get_text(); - let mut args_ = Vec::new(); - let mut idx = 1; - while let Some(id) = ctx.ID(idx) { - args_.push(id.get_text()); - idx += 1; - } + let name_ = ctx.ID().unwrap().get_text(); + let args_ = (&ctx).pred_arg_all() + .iter() + .map(|arg_ctx| arg_ctx.get_text()) + .collect(); AstPredicate { sign: sign_, name: name_, @@ -70,9 +64,7 @@ fn construct_verbphrase(ctx: &VerbphraseContextAll) -> AstVerbPhrase { match ctx { VerbphraseContextAll::PredphraseContext(pctx) => construct_predphrase(pctx), VerbphraseContextAll::ActsAsPhraseContext(actx) => construct_actsasphrase(actx), - _ => { - panic!("construct_verbphrase tried to build error"); - } + _ => { panic!("construct_verbphrase tried to build error"); } } } @@ -92,9 +84,7 @@ fn construct_flat_fact(ctx: &FlatFactContextAll) -> AstFlatFact { match ctx { FlatFactContextAll::PrinFactContext(fctx) => construct_prin_fact(fctx), FlatFactContextAll::PredFactContext(pctx) => construct_pred_fact(pctx), - _ => { - panic!("construct_flat_fact tried to build error"); - } + _ => { panic!("construct_flat_fact tried to build error"); } } } @@ -116,9 +106,7 @@ fn construct_fact(ctx: &FactContextAll) -> AstFact { match ctx { FactContextAll::FlatFactFactContext(fctx) => construct_flat_fact_fact(fctx), FactContextAll::CanSayFactContext(sctx) => construct_can_say_fact(sctx), - _ => { - panic!("construct_fact tried to build error"); - } + _ => { panic!("construct_fact tried to build error"); } } } @@ -136,13 +124,43 @@ fn construct_can_say_fact(ctx: &CanSayFactContext) -> AstFact { } } +fn construct_binop(ctx: &BinopContextAll) -> AstComparisonOperator { + match ctx { + BinopContextAll::LtbinopContext(_) => AstComparisonOperator::LessThan, + BinopContextAll::GrbinopContext(_) => AstComparisonOperator::GreaterThan, + BinopContextAll::EqbinopContext(_) => AstComparisonOperator::Equals, + BinopContextAll::NebinopContext(_) => AstComparisonOperator::NotEquals, + BinopContextAll::LeqbinopContext(_) => AstComparisonOperator::LessOrEquals, + BinopContextAll::GeqbinopContext(_) => AstComparisonOperator::GreaterOrEquals, + _ => { panic!("construct_binop tried to build error"); } + } +} + +fn construct_rvalue(ctx: &RvalueContextAll) -> AstRValue { + match ctx { + RvalueContextAll::FlatFactRvalueContext(ffctx) => { + AstRValue::FlatFactRValue { + flat_fact: construct_flat_fact(&ffctx.flatFact().unwrap()) + } + }, + RvalueContextAll::BinopRvalueContext(bctx) => { + AstRValue::ArithCompareRValue { + arith_comp: AstArithmeticComparison { + lnum: bctx.pred_arg(0).unwrap().get_text(), + op: construct_binop(&bctx.binop().unwrap()), + rnum: bctx.pred_arg(1).unwrap().get_text() + } + } + } + _ => { panic!("construct_rvalue tried to build error"); } + } +} + fn construct_assertion(ctx: &AssertionContextAll) -> AstAssertion { match ctx { AssertionContextAll::FactAssertionContext(fctx) => construct_fact_assertion(fctx), AssertionContextAll::HornClauseAssertionContext(hctx) => construct_hornclause(hctx), - _ => { - panic!("construct_assertion tried to build error"); - } + _ => { panic!("construct_assertion tried to build error"); } } } @@ -153,10 +171,10 @@ fn construct_fact_assertion(ctx: &FactAssertionContext) -> AstAssertion { fn construct_hornclause(ctx: &HornClauseAssertionContext) -> AstAssertion { let lhs = construct_fact(&ctx.fact().unwrap()); - let mut rhs = Vec::new(); - for flat_fact_ctx in ctx.flatFact_all() { - rhs.push(construct_flat_fact(&flat_fact_ctx)); - } + let rhs = ctx.rvalue_all() + .iter() + .map(|rvalue_ctx| construct_rvalue(&rvalue_ctx)) + .collect(); AstAssertion::AstCondAssertion { lhs, rhs } } @@ -186,9 +204,7 @@ fn construct_says_assertion(ctx: &SaysAssertionContextAll) -> AstSaysAssertion { export_file, } } - _ => { - panic!("construct_says_assertion tried to build Error()"); - } + _ => { panic!("construct_says_assertion tried to build Error()"); } } } @@ -215,9 +231,7 @@ fn construct_keybinding(ctx: &KeyBindContextAll) -> AstKeybind { principal: construct_principal(&ctx_prime.principal().unwrap()), is_pub: true, }, - _ => { - panic!("construct_keybinding tried to build Error()"); - } + _ => { panic!("construct_keybinding tried to build Error()"); } } } @@ -237,9 +251,7 @@ fn construct_type(ctx: &AuthLogicTypeContextAll) -> AstType { AuthLogicTypeContextAll::CustomTypeContext(ctx_prime) => { AstType::CustomType { type_name: ctx_prime.ID().unwrap().get_text() } } - _ => { - panic!("construct_type tried to build error"); - } + _ => { panic!("construct_type tried to build error"); } } } diff --git a/rust/tools/authorization-logic/src/souffle/datalog_ir.rs b/rust/tools/authorization-logic/src/souffle/datalog_ir.rs index 969ee9400..d337c1fab 100644 --- a/rust/tools/authorization-logic/src/souffle/datalog_ir.rs +++ b/rust/tools/authorization-logic/src/souffle/datalog_ir.rs @@ -18,6 +18,15 @@ //! this authorization logic into datalog simpler. use crate::ast::*; +// RValues are the expressions that can appear on the right hand side of a +// conditional assertion. At the time of writing these include either +// Predicates or AstArithmeticComparisons. +#[derive(Clone)] +pub enum DLIRRValue { + PredicateRValue { predicate: AstPredicate }, + ArithCompareRValue { arith_comp: AstArithmeticComparison } +} + #[derive(Clone)] pub enum DLIRAssertion { DLIRFactAssertion { @@ -25,7 +34,7 @@ pub enum DLIRAssertion { }, DLIRCondAssertion { lhs: AstPredicate, - rhs: Vec, + rhs: Vec, }, } diff --git a/rust/tools/authorization-logic/src/souffle/lowering_ast_datalog.rs b/rust/tools/authorization-logic/src/souffle/lowering_ast_datalog.rs index 6f7f61f9f..e863babea 100644 --- a/rust/tools/authorization-logic/src/souffle/lowering_ast_datalog.rs +++ b/rust/tools/authorization-logic/src/souffle/lowering_ast_datalog.rs @@ -102,6 +102,10 @@ use crate::{ast::*, souffle::datalog_ir::*}; use std::collections::HashMap; +fn pred_to_dlir_rvalue(pred: &AstPredicate) -> DLIRRValue { + DLIRRValue::PredicateRValue { predicate: pred.clone() } +} + // Note that this puts args_ on the front of the list of arguments because // this is the conveninet way for it to work in the contexts in which it // is used. @@ -230,7 +234,10 @@ impl LoweringToDatalogPass { let gen = DLIRAssertion::DLIRCondAssertion { lhs: gen_lhs, - rhs: [s_says_x_as_p, s_says_p_v].to_vec(), + rhs: [s_says_x_as_p, s_says_p_v] + .into_iter() + .map(|pred| pred_to_dlir_rvalue(pred)) + .collect(), }; (pred, [gen].to_vec()) @@ -291,9 +298,10 @@ impl LoweringToDatalogPass { &push_prin(String::from("canSay_"), &x, &fact_plus_prime), ); // This is `p says fpf :- x says fpf, p says x canSay fpf`. - let mut rhs = Vec::new(); - rhs.push(x_says_term); - rhs.push(can_say_term); + let rhs = [x_says_term, can_say_term] + .into_iter() + .map(|pred| pred_to_dlir_rvalue(pred)) + .collect(); let gen = DLIRAssertion::DLIRCondAssertion { lhs, rhs }; collected.push(gen); @@ -314,6 +322,22 @@ impl LoweringToDatalogPass { .flatten() .collect() } + + fn rvalue_to_dlir( + &mut self, + speaker: &AstPrincipal, + rvalue: &AstRValue) -> DLIRRValue { + match rvalue { + AstRValue::FlatFactRValue { flat_fact } => { + let (flat_pred, _) = self.flat_fact_to_dlir(&flat_fact, &speaker); + pred_to_dlir_rvalue(&push_prin(String::from("says_"), + &speaker, &flat_pred)) + } + AstRValue::ArithCompareRValue { arith_comp } => { + DLIRRValue::ArithCompareRValue { arith_comp: arith_comp.clone() } + } + } + } fn says_assertion_to_dlir_inner( &mut self, @@ -328,16 +352,16 @@ impl LoweringToDatalogPass { gen_assert } AstAssertion::AstCondAssertion { lhs, rhs } => { - let mut dlir_rhs = Vec::new(); - for f in rhs { - let (flat, _) = self.flat_fact_to_dlir(&f, &speaker); - dlir_rhs.push(push_prin(String::from("says_"), &speaker, &flat)); - } let (lhs_prime, mut assertions) = self.fact_to_dlir(&lhs, &speaker); - let dlir_lhs = push_prin(String::from("says_"), &speaker, &lhs_prime); + let dlir_lhs = + push_prin(String::from("says_"), &speaker, &lhs_prime); let this_assertion = DLIRAssertion::DLIRCondAssertion { lhs: dlir_lhs, - rhs: dlir_rhs, + rhs: rhs.clone() + .into_iter() + .map(|ast_rvalue| self.rvalue_to_dlir( + &speaker, &ast_rvalue)) + .collect() }; assertions.push(this_assertion); assertions @@ -367,7 +391,10 @@ impl LoweringToDatalogPass { }; DLIRAssertion::DLIRCondAssertion { lhs: lhs, - rhs: vec![main_fact, LoweringToDatalogPass::dummy_fact()], + rhs: [main_fact, LoweringToDatalogPass::dummy_fact()] + .into_iter() + .map(|pred| pred_to_dlir_rvalue(pred)) + .collect() } } diff --git a/rust/tools/authorization-logic/src/souffle/souffle_emitter.rs b/rust/tools/authorization-logic/src/souffle/souffle_emitter.rs index 0a39b1133..6d91dc227 100644 --- a/rust/tools/authorization-logic/src/souffle/souffle_emitter.rs +++ b/rust/tools/authorization-logic/src/souffle/souffle_emitter.rs @@ -55,6 +55,26 @@ fn emit_pred(p: &AstPredicate) -> String { format!("{}{}({})", neg, &p.name, p.args.join(", ")) } +fn emit_op(operator: &AstComparisonOperator) -> String { + match operator { + AstComparisonOperator::LessThan => "<", + AstComparisonOperator::GreaterThan => ">", + AstComparisonOperator::Equals => "=", + AstComparisonOperator::NotEquals => "!=", + AstComparisonOperator::LessOrEquals => "<=", + AstComparisonOperator::GreaterOrEquals => ">=" + }.to_string() +} + +fn emit_rvalue(rvalue: &DLIRRValue) -> String { + match rvalue { + DLIRRValue::PredicateRValue { predicate } => emit_pred(predicate), + DLIRRValue::ArithCompareRValue { arith_comp } => + format!("{} {} {}", &arith_comp.lnum, + emit_op(&arith_comp.op), &arith_comp.rnum) + } +} + fn emit_assertion(a: &DLIRAssertion) -> String { match a { DLIRAssertion::DLIRFactAssertion { p } => emit_pred(p) + ".", @@ -63,7 +83,7 @@ fn emit_assertion(a: &DLIRAssertion) -> String { "{} :- {}.", emit_pred(lhs), rhs.iter() - .map(|ast_pred| emit_pred(ast_pred)) + .map(|dlir_rvalue| emit_rvalue(dlir_rvalue)) .collect::>() .join(", ") ) diff --git a/rust/tools/authorization-logic/src/souffle/universe_translation.rs b/rust/tools/authorization-logic/src/souffle/universe_translation.rs index 5c4d3fb2f..2944b08a4 100644 --- a/rust/tools/authorization-logic/src/souffle/universe_translation.rs +++ b/rust/tools/authorization-logic/src/souffle/universe_translation.rs @@ -37,13 +37,26 @@ use crate::ast::*; use std::collections::{HashMap, HashSet}; // Determine if a function argument or principal name is a constant or -// return false if this name is a variable. In the ast, all arguments are -// represented as strings, and -// they are constants if and only if they are wrapped in quotes. A better +// return false if this name is a variable. Principals are constants if +// they are wrapped in quotes and arguments are constants if they are in quotes +// or are numbers. A better // way to represent this in the future might be to add an AST node for // arguments with varibales and constants as two possible forms. fn is_name_constant(arg: &str) -> bool { - return arg.starts_with("\"") + // Anything in quotes is a constant + if arg.starts_with("\"") { + return true + } else { + // Numberic literals are constants + + // A better way to do this would be to just use a regex, but + // regexes are not in the standard library and adding new crates + // takes too long to integrate with the C++ side of Raksha. + for c in arg.chars() { + if !c.is_numeric() { return false } + } + return true + } } fn push_option_to_vec(vec: &mut Vec, elt: Option) { @@ -174,6 +187,27 @@ fn populate_constant_type_environment_prog( constant_type_environment } +fn populate_constant_type_environment_rvalue( + relation_type_environment: &RelationTypeEnv, + constant_type_environment: &mut HashMap, + rvalue: &AstRValue) { + match rvalue { + AstRValue::FlatFactRValue { flat_fact } => { + populate_constant_type_environment_flat_fact( + relation_type_environment, + constant_type_environment, + flat_fact); + }, + AstRValue::ArithCompareRValue{ arith_comp } => { + add_typing(constant_type_environment, &arith_comp.lnum, + AstType::NumberType); + add_typing(constant_type_environment, &arith_comp.rnum, + AstType::NumberType); + } + } +} + + fn populate_constant_type_environment_assertion( relation_type_environment: &RelationTypeEnv, constant_type_environment: &mut HashMap, @@ -190,11 +224,11 @@ fn populate_constant_type_environment_assertion( &relation_type_environment, constant_type_environment, lhs); - for flat_fact in rhs { - populate_constant_type_environment_flat_fact( + for rvalue in rhs { + populate_constant_type_environment_rvalue( &relation_type_environment, constant_type_environment, - flat_fact); + rvalue); } } } @@ -413,7 +447,9 @@ impl UniverseHandlingPass { lhs: fact.clone(), rhs: new_rhs_predicates .iter() - .map(|pred| AstFlatFact::AstPredFact{p: pred.clone()}) + .map(|pred| AstRValue::FlatFactRValue { + flat_fact: AstFlatFact::AstPredFact{p: pred.clone()} + }) .collect() } } else { @@ -424,7 +460,10 @@ impl UniverseHandlingPass { let mut new_rhs = rhs.clone(); for x in self.universe_conditions_fact(lhs).iter() { new_rhs.push( - AstFlatFact::AstPredFact {p: x.clone()}); + AstRValue::FlatFactRValue { + flat_fact: AstFlatFact::AstPredFact {p: x.clone()} + } + ); } AstAssertion::AstCondAssertion { lhs: lhs.clone(), diff --git a/rust/tools/authorization-logic/src/test/mod.rs b/rust/tools/authorization-logic/src/test/mod.rs index ef8bce811..bf1d285f9 100644 --- a/rust/tools/authorization-logic/src/test/mod.rs +++ b/rust/tools/authorization-logic/src/test/mod.rs @@ -24,6 +24,7 @@ mod test_negation; mod test_multimic_no_overrides; mod test_multimic_overrides; mod test_num_string_names; +mod test_num_compare; mod test_relation_declarations; mod test_type_error; mod test_multiverse_handling; diff --git a/rust/tools/authorization-logic/src/test/test_num_compare.rs b/rust/tools/authorization-logic/src/test/test_num_compare.rs new file mode 100644 index 000000000..757fc0c3e --- /dev/null +++ b/rust/tools/authorization-logic/src/test/test_num_compare.rs @@ -0,0 +1,60 @@ +/* + * Copyright 2022 Google LLC. + * + * Licensed under the Apache License, Version 2.0 (the "License"); + * you may not use this file except in compliance with the License. + * You may obtain a copy of the License at + * + * http://www.apache.org/licenses/LICENSE-2.0 + * + * Unless required by applicable law or agreed to in writing, software + * distributed under the License is distributed on an "AS IS" BASIS, + * WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied. + * See the License for the specific language governing permissions and + * limitations under the License. + */ + +#[cfg(test)] +pub mod test { + use crate::{ + ast::*, compilation_top_level::*, souffle::souffle_interface::*, + test::test_queries::test::*, + }; + + #[test] + fn test_basic_number_comparisons() { + run_query_test(QueryTest { + filename: "basic_num_comparisons", + query_expects: vec![ + ("q1", true), + ("q2", false), + ("q3", true), + ("q4", false), + ("q5", true), + ("q6", false), + ("q7", true), + ("q8", false), + ("q9", true), + ("q10", true), + ("q11", false), + ("q12", true), + ("q13", true), + ("q14", false) + ], + ..Default::default() + }); + } + + #[test] + fn test_comparisons_with_delegation() { + run_query_test(QueryTest { + filename: "comparisons_with_delegation", + query_expects: vec![ + ("q1", true), + ("q2", false), + ], + ..Default::default() + }); + } + +} diff --git a/rust/tools/authorization-logic/test_inputs/basic_num_comparisons b/rust/tools/authorization-logic/test_inputs/basic_num_comparisons new file mode 100644 index 000000000..048355dab --- /dev/null +++ b/rust/tools/authorization-logic/test_inputs/basic_num_comparisons @@ -0,0 +1,31 @@ +.decl someFact(n : Number) + +"test_principal" says someFact(1) :- 3 < 5. +"test_principal" says someFact(2) :- 3 < 0. +"test_principal" says someFact(3) :- 5 > 0. +"test_principal" says someFact(4) :- 3 > 999. +"test_principal" says someFact(5) :- 4 = 4. +"test_principal" says someFact(6) :- 47 = 42. +"test_principal" says someFact(7) :- 47 != 42. +"test_principal" says someFact(8) :- 0 != 0. +"test_principal" says someFact(9) :- 3 <= 5. +"test_principal" says someFact(10) :- 3 <= 3. +"test_principal" says someFact(11) :- 3 <= 0. +"test_principal" says someFact(12) :- 3 >= 2. +"test_principal" says someFact(13) :- 3 >= 3. +"test_principal" says someFact(14) :- 3 >= 5. + +q1 = query "test_principal" says someFact(1)? +q2 = query "test_principal" says someFact(2)? +q3 = query "test_principal" says someFact(3)? +q4 = query "test_principal" says someFact(4)? +q5 = query "test_principal" says someFact(5)? +q6 = query "test_principal" says someFact(6)? +q7 = query "test_principal" says someFact(7)? +q8 = query "test_principal" says someFact(8)? +q9 = query "test_principal" says someFact(9)? +q10 = query "test_principal" says someFact(10)? +q11 = query "test_principal" says someFact(11)? +q12 = query "test_principal" says someFact(12)? +q13 = query "test_principal" says someFact(13)? +q14 = query "test_principal" says someFact(14)? diff --git a/rust/tools/authorization-logic/test_inputs/comparisons_with_delegation b/rust/tools/authorization-logic/test_inputs/comparisons_with_delegation new file mode 100644 index 000000000..2290f8661 --- /dev/null +++ b/rust/tools/authorization-logic/test_inputs/comparisons_with_delegation @@ -0,0 +1,29 @@ +.decl expected_hash(object : Object, hash : Sha256Hash) +.decl currentTimeIs(time : Number) + +// This one is valid (and has not expired). +"EndorsementFile_OakFunctionsLoader" says { + expected_hash("OakFunctionsLoader", "sha256:cafed00d") :- + currentTimeIs(real_time), real_time > 42, real_time < 31337. + "VerifierSystemClock" canSay currentTimeIs(real_time). +} + +// This one has expired +"EndorsementFile_OakFunctionsLoader" says { + expected_hash("OakFunctionsLoader", "sha256:deadbeef") :- + currentTimeIs(real_time), real_time > 42, real_time < 1337. +} + +"VerifierSystemClock" says { + currentTimeIs(1776). +} + +"Verifier_OakFunctionsLoader" says { + "EndorsementFile_OakFunctionsLoader" canSay + expected_hash("OakFunctionsLoader", any_hash). +} + +q1 = query "Verifier_OakFunctionsLoader" says + expected_hash("OakFunctionsLoader", "sha256:cafed00d")? +q2 = query "Verifier_OakFunctionsLoader" says + expected_hash("OakFunctionsLoader", "sha256:deadbeef")?