feat: Introduce :older attribute

RELEASE_NOTES.md

@@ -18,6 +18,7 @@
 - fix: Fix initialization of non-auto-init in-parameters in C#/JavaScript/Go compilers (https://github.com/dafny-lang/dafny/pull/1935)
 - fix: Resolution of static functions-by-method (https://github.com/dafny-lang/dafny/pull/2023)
 - fix: Export sets did not work with inner modules (https://github.com/dafny-lang/dafny/pull/2025)
+- feat: The new `:older` attribute indicates that a predicate ensures the allocatedness of some of its arguments. This allows more functions to show that their quantifiers do not depend on the allocation state. See `/attrHelp` for more information.
 
 
 # 3.5.0

Source/Dafny/AST/DafnyAst.cs

@@ -6013,10 +6013,11 @@ public override bool IsMutable {
  public readonly bool IsOld;
  public readonly Expression DefaultValue;
  public readonly bool IsNameOnly;
+ public readonly bool IsOlder;
  public readonly string NameForCompilation;
 
  public Formal(IToken tok, string name, Type type, bool inParam, bool isGhost, Expression defaultValue,
- bool isOld = false, bool isNameOnly = false, string nameForCompilation = null)
+ bool isOld = false, bool isNameOnly = false, bool isOlder = false, string nameForCompilation = null)
  : base(tok, name, type, isGhost) {
  Contract.Requires(tok != null);
  Contract.Requires(name != null);
@@ -6027,6 +6028,7 @@ public Formal(IToken tok, string name, Type type, bool inParam, bool isGhost, Ex
  IsOld = isOld;
  DefaultValue = defaultValue;
  IsNameOnly = isNameOnly;
+ IsOlder = isOlder;
  NameForCompilation = nameForCompilation ?? name;
  }
 
@@ -11421,6 +11423,7 @@ public enum PoolVirtues { None = 0, Finite = 1, Enumerable = 2, IndependentOfAll
  /// 0: AllocFreeBoundedPool
  /// 0: ExplicitAllocatedBoundedPool
  /// 0: SpecialAllocIndependenceAllocatedBoundedPool
+ /// 0: OlderBoundedPool
  ///
  /// 1: WiggleWaggleBound
  ///
@@ -11691,6 +11694,13 @@ public class DatatypeInclusionBoundedPool : BoundedPool {
  public override int Preference() => 2;
  }
 
+ public class OlderBoundedPool : BoundedPool {
+ public OlderBoundedPool() {
+ }
+ public override PoolVirtues Virtues => PoolVirtues.IndependentOfAlloc | PoolVirtues.IndependentOfAlloc_or_ExplicitAlloc;
+ public override int Preference() => 0;
+ }
+
  [FilledInDuringResolution] public List<BoundedPool> Bounds;
  // invariant Bounds == null || Bounds.Count == BoundVars.Count;
 

Source/Dafny/AST/Printer.cs

@@ -1014,6 +1014,10 @@ void PrintFormal(Formal f, bool showNewKeyword) {
  if (showNewKeyword && !f.IsOld) {
  wr.Write("new ");
  }
+ if (f.IsOlder) {
+ Contract.Assert(f.HasName);
+ wr.Write("older ");
+ }
  if (f.IsGhost) {
  wr.Write("ghost ");
  }

Source/Dafny/Cloner.cs

@@ -199,7 +199,7 @@ public virtual Type CloneType(Type t) {
 
  public Formal CloneFormal(Formal formal) {
  Formal f = new Formal(Tok(formal.tok), formal.Name, CloneType(formal.Type), formal.InParam, formal.IsGhost,
- CloneExpr(formal.DefaultValue), formal.IsOld, formal.IsNameOnly, formal.NameForCompilation);
+ CloneExpr(formal.DefaultValue), formal.IsOld, formal.IsNameOnly, formal.IsOlder, formal.NameForCompilation);
  return f;
  }
 

Source/Dafny/Dafny.atg

@@ -191,7 +191,7 @@ public Parser(Scanner/*!*/ scanner, Errors/*!*/ errors, Include include, ModuleD
 }
 
 bool IsIdentifier(int kind) {
- return kind == _ident || kind == _least || kind == _greatest;
+ return kind == _ident || kind == _least || kind == _greatest || kind == _older;
 }
 
 bool IsLabel(bool allowLabel) {
@@ -203,6 +203,18 @@ bool IsLabel(bool allowLabel) {
  return (IsIdentifier(la.kind) || la.kind == _digits) && x.kind == _colon;
 }
 
+bool IsKeywordForFormal() {
+ scanner.ResetPeek();
+ if (la.kind == _ghost || la.kind == _new || la.kind == _nameonly) {
+ return true;
+ } else if (la.kind == _older) {
+ // "older" is just a contextual keyword, so don't recognize it as a keyword if it must be an identifier
+ IToken x = scanner.Peek();
+ return x.kind != _colon;
+ }
+ return false;
+}
+
 bool IsBinding() {
  scanner.ResetPeek();
  IToken x = scanner.Peek();
@@ -824,6 +836,9 @@ TOKENS
  requires = "requires".
  ensures = "ensures".
  ghost = "ghost".
+ new = "new".
+ nameonly = "nameonly".
+ older = "older". /* a keyword only when it appears as a modifier to a parameter of a non-extreme function */
  witness = "witness".
  lbracecolon = "{:".
  lbrace = '{'.
@@ -1436,15 +1451,19 @@ SynonymTypeDecl<DeclModifierData dmod, ModuleDefinition module, out TopLevelDecl
  .
 
 /*------------------------------------------------------------------------*/
-GIdentType<bool allowGhostKeyword, bool allowNewKeyword, bool allowNameOnlyKeyword,
- out IToken/*!*/ id, out Type/*!*/ ty, out bool isGhost, out bool isOld, out bool isNameOnly>
+GIdentType<bool allowGhostKeyword, bool allowNewKeyword, bool allowNameOnlyKeyword, bool allowOlderKeyword,
+ out IToken/*!*/ id, out Type/*!*/ ty, out bool isGhost, out bool isOld, out bool isNameOnly, out bool isOlder>
 /* isGhost always returns as false if allowGhostKeyword is false */
 = (. Contract.Ensures(Contract.ValueAtReturn(out id)!=null);
  Contract.Ensures(Contract.ValueAtReturn(out ty)!=null);
- isGhost = false; isOld = allowNewKeyword; isNameOnly = false; .)
- { "ghost" (. if (allowGhostKeyword) { isGhost = true; } else { SemErr(t, "formal cannot be declared 'ghost' in this context"); } .)
- | "new" (. if (allowNewKeyword) { isOld = false; } else { SemErr(t, "formal cannot be declared 'new' in this context"); } .)
- | "nameonly" (. if (allowNameOnlyKeyword) { isNameOnly = true; } else { SemErr(t, "formal cannot be declared 'nameonly' in this context"); } .)
+ isGhost = false; isOld = allowNewKeyword; isNameOnly = false; isOlder = false;
+ .)
+ { IF(IsKeywordForFormal())
+ ( "ghost" (. if (allowGhostKeyword) { isGhost = true; } else { SemErr(t, "formal cannot be declared 'ghost' in this context"); } .)
+ | "new" (. if (allowNewKeyword) { isOld = false; } else { SemErr(t, "formal cannot be declared 'new' in this context"); } .)
+ | "nameonly" (. if (allowNameOnlyKeyword) { isNameOnly = true; } else { SemErr(t, "formal cannot be declared 'nameonly' in this context"); } .)
+ | "older" (. if (allowOlderKeyword) { isOlder = true; } else { SemErr(t, "formal cannot be declared 'older' in this context"); } .)
+ )
  }
  IdentType<out id, out ty, false>
  .
@@ -1570,11 +1589,11 @@ IteratorDecl<DeclModifierData dmod, ModuleDefinition module, out IteratorDecl/*!
  IteratorName<out id>
  (
  [ GenericParameters<typeArgs, true> ]
- Formals<true, true, false, ins>
+ Formals<true, true, false, false, ins>
  [ ( "yields"
  | "returns" (. SemErr(t, "iterators don't have a 'returns' clause; did you mean 'yields'?"); .)
  )
- Formals<false, true, false, outs>
+ Formals<false, true, false, false, outs>
  ]
  | ellipsis (. signatureEllipsis = t; .)
  )
@@ -1733,9 +1752,9 @@ MethodDecl<DeclModifierData dmod, bool allowConstructor, out Method/*!*/ m>
  [ KType<ref kType> (. if (!(isGreatestLemma || isLeastLemma)) { SemErr(t, "type of _k can only be specified for least and greatest lemmas"); } .)
  ]
  (. var isCompilable = (isPlainOlMethod || isConstructor) && !dmod.IsGhost; .)
- Formals<true, isCompilable, isTwoStateLemma, ins>
+ Formals<true, isCompilable, isTwoStateLemma, false, ins>
  [ "returns" (. if (isConstructor) { SemErr(t, "constructors cannot have out-parameters"); } .)
- Formals<false, isCompilable, false, outs>
+ Formals<false, isCompilable, false, false, outs>
  ]
  | ellipsis (. signatureEllipsis = t; .)
  )
@@ -1889,23 +1908,24 @@ IteratorSpec<.List<FrameExpression/*!*/>/*!*/ reads, List<FrameExpression/*!*/>/
  .
 
 /*------------------------------------------------------------------------*/
-Formals<.bool incoming, bool allowGhostKeyword, bool allowNewKeyword, List<Formal> formals.>
+Formals<.bool incoming, bool allowGhostKeyword, bool allowNewKeyword, bool allowOlderKeyword, List<Formal> formals.>
 = (. Contract.Requires(cce.NonNullElements(formals));
  IToken id;
  Type ty;
  bool isGhost;
  bool isOld;
  Expression defaultValue;
  bool isNameOnly;
+ bool isOlder;
  .)
  "("
  [
- GIdentType<allowGhostKeyword, allowNewKeyword, incoming, out id, out ty, out isGhost, out isOld, out isNameOnly>
+ GIdentType<allowGhostKeyword, allowNewKeyword, incoming, allowOlderKeyword, out id, out ty, out isGhost, out isOld, out isNameOnly, out isOlder>
  ParameterDefaultValue<incoming, out defaultValue>
- (. formals.Add(new Formal(id, id.val, ty, incoming, isGhost, defaultValue, isOld, isNameOnly)); .)
- { "," GIdentType<allowGhostKeyword, allowNewKeyword, incoming, out id, out ty, out isGhost, out isOld, out isNameOnly>
+ (. formals.Add(new Formal(id, id.val, ty, incoming, isGhost, defaultValue, isOld, isNameOnly, isOlder)); .)
+ { "," GIdentType<allowGhostKeyword, allowNewKeyword, incoming, allowOlderKeyword, out id, out ty, out isGhost, out isOld, out isNameOnly, out isOlder>
  ParameterDefaultValue<incoming, out defaultValue>
- (. formals.Add(new Formal(id, id.val, ty, incoming, isGhost, defaultValue, isOld, isNameOnly)); .)
+ (. formals.Add(new Formal(id, id.val, ty, incoming, isGhost, defaultValue, isOld, isNameOnly, isOlder)); .)
  }
  ]
  ")"
@@ -2190,12 +2210,12 @@ FunctionDecl<DeclModifierData dmod, out Function/*!*/ f>
  MethodFunctionName<out id>
  (
  [ GenericParameters<typeArgs, false> ]
- Formals<true, true, isTwoState, formals>
+ Formals<true, true, isTwoState, true, formals>
  ":"
  ( IF(FollowedByColon())
  "("
- GIdentType<false, false, false, out var resultId, out var ty, out var resultIsGhost, out var isOld, out var isNameOnly>
- (. Contract.Assert(!resultIsGhost && !isOld && !isNameOnly);
+ GIdentType<false, false, false, false, out var resultId, out var ty, out var resultIsGhost, out var isOld, out var isNameOnly, out var isOlder>
+ (. Contract.Assert(!resultIsGhost && !isOld && !isNameOnly && !isOlder);
  result = new Formal(resultId, resultId.val, ty, false, false, null, false);
  .)
  ")"
@@ -2212,7 +2232,7 @@ FunctionDecl<DeclModifierData dmod, out Function/*!*/ f>
  MethodFunctionName<out id>
  (
  [ GenericParameters<typeArgs, false> ]
- [ Formals<true, true, isTwoState, formals>
+ [ Formals<true, true, isTwoState, true, formals>
  ]
  [ ":" Type<out returnType> (. SemErr(t, "predicates do not have an explicitly declared return type; it is always bool"); .)
  ]
@@ -2232,7 +2252,7 @@ FunctionDecl<DeclModifierData dmod, out Function/*!*/ f>
  (
  [ GenericParameters<typeArgs, false> ]
  [ KType<ref kType> ]
- Formals<true, false, false, formals>
+ Formals<true, false, false, false, formals>
  [ ":" (. SemErr(t, "least predicates do not have an explicitly declared return type; it is always bool"); .)
  ]
  | ellipsis (. signatureEllipsis = t; .)
@@ -2250,7 +2270,7 @@ FunctionDecl<DeclModifierData dmod, out Function/*!*/ f>
  (
  [ GenericParameters<typeArgs, false> ]
  [ KType<ref kType> ]
- Formals<true, false, false, formals>
+ Formals<true, false, false, false, formals>
  [ ":" (. SemErr(t, "greatest predicates do not have an explicitly declared return type; it is always bool"); .)
  ]
  | ellipsis (. signatureEllipsis = t; .)
@@ -4732,6 +4752,7 @@ Ident<out IToken/*!*/ x>
  ( ident
  | "least" (. t.kind = _ident; .) // convert it to an ident
  | "greatest" (. t.kind = _ident; .) // convert it to an ident
+ | "older" (. t.kind = _ident; .) // convert it to an ident
  )
  (. x = t; .)
  .

Source/Dafny/DafnyPrelude.bpl

@@ -329,6 +329,8 @@ function $AlwaysAllocated(Ty): bool uses {
  (forall h: Heap, v: Box :: { $IsAllocBox(v, ty, h) } $IsBox(v, ty) ==> $IsAllocBox(v, ty, h)));
 }
 
+function $OlderTag(Heap): bool;
+
 // ---------------------------------------------------------------
 // -- Encoding of type names -------------------------------------
 // ---------------------------------------------------------------

Source/Dafny/RefinementTransformer.cs

@@ -934,9 +934,13 @@ void CheckAgreement_Parameters(IToken tok, List<Formal> old, List<Formal> nw, st
  } else if (o.IsGhost && !n.IsGhost) {
  Reporter.Error(MessageSource.RefinementTransformer, n.tok, "{0} '{1}' of {2} {3} cannot be changed, compared to the corresponding {2} in the module it refines, from ghost to non-ghost", parameterKind, n.Name, thing, name);
  } else if (!o.IsOld && n.IsOld) {
- Reporter.Error(MessageSource.RefinementTransformer, n.tok, "{0} '{1}' of {2} {3} cannot be changed, compared to the corresponding {2} in the module it refines, from non-new to new", parameterKind, n.Name, thing, name);
- } else if (o.IsOld && !n.IsOld) {
  Reporter.Error(MessageSource.RefinementTransformer, n.tok, "{0} '{1}' of {2} {3} cannot be changed, compared to the corresponding {2} in the module it refines, from new to non-new", parameterKind, n.Name, thing, name);
+ } else if (o.IsOld && !n.IsOld) {
+ Reporter.Error(MessageSource.RefinementTransformer, n.tok, "{0} '{1}' of {2} {3} cannot be changed, compared to the corresponding {2} in the module it refines, from non-new to new", parameterKind, n.Name, thing, name);
+ } else if (!o.IsOlder && n.IsOlder) {
+ Reporter.Error(MessageSource.RefinementTransformer, n.tok, "{0} '{1}' of {2} {3} cannot be changed, compared to the corresponding {2} in the module it refines, from non-older to older", parameterKind, n.Name, thing, name);
+ } else if (o.IsOlder && !n.IsOlder) {
+ Reporter.Error(MessageSource.RefinementTransformer, n.tok, "{0} '{1}' of {2} {3} cannot be changed, compared to the corresponding {2} in the module it refines, from older to non-older", parameterKind, n.Name, thing, name);
  } else if (!TypesAreSyntacticallyEqual(o.Type, n.Type)) {
  Reporter.Error(MessageSource.RefinementTransformer, n.tok, "the type of {0} '{1}' is different from the type of the same {0} in the corresponding {2} in the module it refines ('{3}' instead of '{4}')", parameterKind, n.Name, thing, n.Type, o.Type);
  } else if (n.DefaultValue != null) {