From ef4dbbb984ab2483642a90574928cd1a16376077 Mon Sep 17 00:00:00 2001 From: Nikolay Yakimov Date: Wed, 22 Nov 2023 12:48:02 +0300 Subject: [PATCH] MIR: LAMBDA and LAMBDA_REC instructions --- contrib/mir/src/ast.rs | 1 + contrib/mir/src/gas.rs | 1 + contrib/mir/src/interpreter.rs | 4 ++ contrib/mir/src/typechecker.rs | 96 ++++++++++++++++++++++++++++++++-- 4 files changed, 98 insertions(+), 4 deletions(-) diff --git a/contrib/mir/src/ast.rs b/contrib/mir/src/ast.rs index 6850f911d382..60540d6ed83c 100644 --- a/contrib/mir/src/ast.rs +++ b/contrib/mir/src/ast.rs @@ -308,6 +308,7 @@ pub enum Instruction<'a> { Slice(overloads::Slice), Left, Right, + Lambda(Lambda<'a>), } #[derive(Debug, Clone, PartialEq, Eq)] diff --git a/contrib/mir/src/gas.rs b/contrib/mir/src/gas.rs index 51c776d4b0b1..aacd34c5d238 100644 --- a/contrib/mir/src/gas.rs +++ b/contrib/mir/src/gas.rs @@ -239,6 +239,7 @@ pub mod interpret_cost { // Gas costs obtained from https://gitlab.com/tezos/tezos/-/blob/9875fbebe032a8c5ce62b3b3cb1588ca9855a37e/src/proto_017_PtNairob/lib_protocol/michelson_v1_gas_costs_generated.ml pub const TRANSFER_TOKENS: u32 = 60; pub const SET_DELEGATE: u32 = 60; + pub const LAMBDA: u32 = 10; pub const INTERPRET_RET: u32 = 15; // corresponds to KNil in the Tezos protocol pub const LOOP_ENTER: u32 = 10; // corresponds to KLoop_in in the Tezos protocol diff --git a/contrib/mir/src/interpreter.rs b/contrib/mir/src/interpreter.rs index e65bfa8c16eb..d7f23c4329ed 100644 --- a/contrib/mir/src/interpreter.rs +++ b/contrib/mir/src/interpreter.rs @@ -542,6 +542,10 @@ fn interpret_one<'a>( let right = pop!(); stack.push(V::new_or(Or::Right(right))); } + I::Lambda(lam) => { + ctx.gas.consume(interpret_cost::LAMBDA)?; + stack.push(V::Lambda(lam.clone())); + } I::Seq(nested) => interpret(nested, ctx, stack)?, } Ok(()) diff --git a/contrib/mir/src/typechecker.rs b/contrib/mir/src/typechecker.rs index c30f68544b7e..b10090f77481 100644 --- a/contrib/mir/src/typechecker.rs +++ b/contrib/mir/src/typechecker.rs @@ -524,10 +524,12 @@ pub(crate) fn typecheck_instruction<'a>( }; } - /// Pattern synonym matching any number of slice elements _except_ the number - /// passed as the argument. If the number is suffixed with `seq`, the pattern - /// will also match the number of elements equal to the argument iff either of - /// those isn't `Micheline::Seq`. + /// Pattern synonym matching any number of slice elements _except_ the + /// number passed as the argument. If the number is suffixed with `seq`, the + /// pattern will also match the number of elements equal to the argument iff + /// either of those isn't `Micheline::Seq`. If the number is suffixed with + /// `last_seq`, only the last argument will get the special treatment for + /// `Seq`. /// /// This is useful for the last "catchall" pattern for invalid Micheline to /// recover some measure of totality. @@ -541,6 +543,9 @@ pub(crate) fn typecheck_instruction<'a>( (2) => { [] | [_] | [_, _, _, ..] }; + (3) => { + [] | [_] | [_, _] | [_, _, _, _, ..] + }; (1 seq) => { expect_args!(1) | [micheline_non_seq!()] }; @@ -550,6 +555,9 @@ pub(crate) fn typecheck_instruction<'a>( | [Micheline::Seq(..), micheline_non_seq!()] | [micheline_non_seq!(), Micheline::Seq(..)] }; + (3 last_seq) => { + expect_args!(3) | [_, _, micheline_non_seq!()] + }; } ctx.gas.consume(gas::tc_cost::INSTR_STEP)?; @@ -1107,6 +1115,15 @@ pub(crate) fn typecheck_instruction<'a>( (App(RIGHT, [_ty_left], _), []) => no_overload!(RIGHT, len 1), (App(RIGHT, expect_args!(1), _), _) => unexpected_micheline!(), + (App(prim @ (LAMBDA | LAMBDA_REC), [ty1, ty2, Seq(instrs)], _), ..) => { + let in_ty = parse_ty(ctx, ty1)?; + let out_ty = parse_ty(ctx, ty2)?; + stack.push(Type::new_lambda(in_ty.clone(), out_ty.clone())); + let res = typecheck_lambda(instrs, ctx, in_ty, out_ty, matches!(prim, LAMBDA_REC))?; + I::Lambda(res) + } + (App(LAMBDA | LAMBDA_REC, expect_args!(3 last_seq), _), _) => unexpected_micheline!(), + (App(other, ..), _) => todo!("Unhandled instruction {other}"), (Seq(nested), _) => I::Seq(typecheck(nested, ctx, self_entrypoints, opt_stack)?), @@ -1449,6 +1466,7 @@ fn ensure_ty_eq(ctx: &mut Ctx, ty1: &Type, ty2: &Type) -> Result<(), TcError> { #[cfg(test)] mod typecheck_tests { + use super::Lambda; use crate::ast::micheline::test_helpers::*; use crate::ast::michelson_address as addr; use crate::gas::Gas; @@ -4170,6 +4188,15 @@ mod typecheck_tests { code: vec![Drop(None), Unit] }))) ); + assert_eq!( + parse("LAMBDA unit unit { DROP ; UNIT }") + .unwrap() + .typecheck_instruction(&mut Ctx::default(), None, &[]), + Ok(Lambda(Lambda::Lambda { + micheline_code: seq! { app!(DROP); app!(UNIT) }, + code: vec![Drop(None), Unit] + })) + ); } #[test] @@ -4184,6 +4211,16 @@ mod typecheck_tests { TypesNotEqual(Type::Unit, Type::Int).into() )) ); + assert_eq!( + parse("LAMBDA unit int { DROP ; UNIT }") + .unwrap() + .typecheck_instruction(&mut Ctx::default(), None, &[]), + Err(TcError::StacksNotEqual( + stk![Type::Unit], + stk![Type::Int], + TypesNotEqual(Type::Unit, Type::Int).into() + )) + ); } #[test] @@ -4198,6 +4235,16 @@ mod typecheck_tests { reason: Some(TypesNotEqual(Type::Bool, Type::Int).into()) }) ); + assert_eq!( + parse("LAMBDA int unit { IF { UNIT } { UNIT } }") + .unwrap() + .typecheck_instruction(&mut Ctx::default(), None, &[]), + Err(TcError::NoMatchingOverload { + instr: Prim::IF, + stack: stk![Type::Int], + reason: Some(TypesNotEqual(Type::Bool, Type::Int).into()) + }) + ); } #[test] @@ -4208,6 +4255,12 @@ mod typecheck_tests { .typecheck_instruction(&mut Ctx::default(), Some(&app!(unit)), &[]), Err(TcError::SelfForbidden) ); + assert_eq!( + parse("LAMBDA unit unit { SELF }") + .unwrap() + .typecheck_instruction(&mut Ctx::default(), Some(&app!(unit)), &[]), + Err(TcError::SelfForbidden) + ); } #[test] @@ -4218,6 +4271,12 @@ mod typecheck_tests { .typecheck_instruction(&mut Ctx::default(), Some(&app!(unit)), &[]), Err(TcError::SelfForbidden) ); + assert_eq!( + parse("LAMBDA_REC unit unit { SELF }") + .unwrap() + .typecheck_instruction(&mut Ctx::default(), Some(&app!(unit)), &[]), + Err(TcError::SelfForbidden) + ); } #[test] @@ -4231,6 +4290,15 @@ mod typecheck_tests { code: vec![Dip(None, vec![Drop(None)])] }))) ); + assert_eq!( + parse("LAMBDA_REC unit unit { DIP { DROP } }") + .unwrap() + .typecheck_instruction(&mut Ctx::default(), None, &[]), + Ok(Lambda(Lambda::LambdaRec { + micheline_code: seq! { app!(DIP[seq! { app!(DROP) } ]) }, + code: vec![Dip(None, vec![Drop(None)])] + })) + ); } #[test] @@ -4245,6 +4313,16 @@ mod typecheck_tests { TypesNotEqual(Type::new_lambda(Type::Unit, Type::Unit), Type::Unit).into() )) ); + assert_eq!( + parse("LAMBDA_REC unit unit { DROP }") + .unwrap() + .typecheck_instruction(&mut Ctx::default(), None, &[]), + Err(TcError::StacksNotEqual( + stk![Type::new_lambda(Type::Unit, Type::Unit)], + stk![Type::Unit], + TypesNotEqual(Type::new_lambda(Type::Unit, Type::Unit), Type::Unit).into() + )) + ); } #[test] @@ -4259,5 +4337,15 @@ mod typecheck_tests { reason: Some(TypesNotEqual(Type::Bool, Type::Int).into()) }) ); + assert_eq!( + parse("LAMBDA_REC int unit { IF { UNIT } { UNIT }; DIP { DROP } }") + .unwrap() + .typecheck_instruction(&mut Ctx::default(), None, &[]), + Err(TcError::NoMatchingOverload { + instr: Prim::IF, + stack: stk![Type::new_lambda(Type::Int, Type::Unit), Type::Int], + reason: Some(TypesNotEqual(Type::Bool, Type::Int).into()) + }) + ); } } -- GitLab