diff --git a/.gitignore b/.gitignore index 34f20c8c80f..beb07d34a9c 100644 --- a/.gitignore +++ b/.gitignore @@ -88,3 +88,5 @@ Source/IntegrationTests/TestFiles/LitTests/LitTest/**/*.deps.json Source/IntegrationTests/TestFiles/LitTests/LitTest/**/*.csproj /Source/IntegrationTests/TestFiles/LitTests/LitTest/pythonmodule/multimodule/PythonModule2 /Source/IntegrationTests/TestFiles/LitTests/LitTest/pythonmodule/singlemodule/dafnysource/PythonModule1 +/Source/DafnyCore/Prelude/DafnyPrelude.bpl +/Source/DafnyCore/Prelude/Sequences.bpl diff --git a/Source/DafnyCore/Backends/BoogieExtractor.cs b/Source/DafnyCore/Backends/BoogieExtractor.cs new file mode 100644 index 00000000000..86b110d7091 --- /dev/null +++ b/Source/DafnyCore/Backends/BoogieExtractor.cs @@ -0,0 +1,350 @@ +//----------------------------------------------------------------------------- +// +// Copyright by the contributors to the Dafny Project +// SPDX-License-Identifier: MIT +// +//----------------------------------------------------------------------------- + +#nullable enable + +using System; +using System.Collections.Generic; +using System.Linq; +using System.Numerics; +using System.Diagnostics.Contracts; +using Microsoft.BaseTypes; +using Microsoft.Boogie; + +namespace Microsoft.Dafny.Compilers { + public class ExtractorError : Exception { + public ExtractorError(string message) + : base(message) { + } + } + + public class BoogieExtractor : ASTVisitor { + /// + /// Says to look inside the module for contents to extract. + /// Can be applied to a module. + /// + /// Note: This attribute isn't used yet, so the use of the attribute is just a stylistic thing at the moment. + /// Similarly, one can imagine that the extractor will look at a module's export clauses, to--in some way--check that + /// the set of Boogie declarations exported are self consistent. But that isn't done yet, either. Instead, all contents + /// of all files given to the extractor are considered for extraction. + /// + private const string ExtractAttribute = "extract_boogie"; + + /// + /// Gives the Boogie name to be used in the extraction. + /// Can be applied to types and functions. + /// + private const string NameAttribute = "extract_boogie_name"; + + /// + /// Says to place the extracted axiom declaration in the "uses" block of the given function. + /// Can be applied to lemmas. + /// + private const string UsedByAttribute = "extract_used_by"; + + /// + /// Gives a matching pattern to be applied in the quantifier emitted from a lemma or from a quantifier. + /// Can be applied to lemmas and quantifiers. + /// + private const string PatternAttribute = "extract_pattern"; + + /// + /// Specifies an additional attribute to be attached to the quantifier emitted from a lemma. + /// Can be applied to lemmas. + /// + private const string AttributeAttribute = "extract_attribute"; + + /// + /// Throws an "ExtractorError" if the input is unexpected or unsupported. + /// + public static Boogie.Program Extract(Program program) { + var extractor = new BoogieExtractor(); + extractor.VisitModule(program.DefaultModule); + extractor.FixUpUsedByInformation(); + + var extractedProgram = new Boogie.Program(); + extractedProgram.AddTopLevelDeclarations(extractor.allDeclarations); + return extractedProgram; + } + + private List declarations = new(); // for the current module + private List allDeclarations = new(); // these are the declarations for all modules marked with {:extract} + private readonly Dictionary functionExtractions = new(); + private readonly List<(Boogie.Axiom, Function)> axiomUsedBy = new(); + + private BoogieExtractor() { + } + + void FixUpUsedByInformation() { + foreach (var (axiom, function) in axiomUsedBy) { + if (!functionExtractions.TryGetValue(function, out var boogieFunction)) { + throw new ExtractorError($":{UsedByAttribute} attribute mentions non-extracted function: {function.Name}"); + } + boogieFunction.OtherDefinitionAxioms.Add(axiom); + } + axiomUsedBy.Clear(); + } + + public override IASTVisitorContext GetContext(IASTVisitorContext astVisitorContext, bool inFunctionPostcondition) { + return astVisitorContext; + } + + void VisitModule(ModuleDecl module) { + var previousDeclarations = declarations; + declarations = new(); + + VisitDeclarations(module.Signature.TopLevels.Values.ToList()); + + if (Attributes.Contains(module.Signature.ModuleDef.Attributes, ExtractAttribute)) { + declarations.Sort((d0, d1) => d0.tok.pos - d1.tok.pos); + allDeclarations.AddRange(declarations); + } + declarations = previousDeclarations; + } + + protected override void VisitOneDeclaration(TopLevelDecl decl) { + if (decl is ModuleDecl moduleDecl) { + VisitModule(moduleDecl); + return; + } + + if (GetExtractName(decl.Attributes) is { } extractName) { + var ty = new Boogie.TypeCtorDecl(decl.tok, extractName, decl.TypeArgs.Count); + declarations.Add(ty); + } + + base.VisitOneDeclaration(decl); // this will visit the declaration's members + } + + public override void VisitMethod(Method method) { + if (method is not Lemma lemma) { + return; + } + + var patterns = Attributes.FindAllExpressions(lemma.Attributes, PatternAttribute); + var usedByInfo = Attributes.Find(lemma.Attributes, UsedByAttribute); + if (patterns == null && usedByInfo == null) { + return; + } + + if ((lemma.Ins.Count == 0) != (patterns == null)) { + throw new ExtractorError($"a parameterized lemma must specify at least one :{PatternAttribute}: {lemma.Name}"); + } + if (lemma.TypeArgs.Count != 0) { + throw new ExtractorError($"an extracted lemma is not allowed to have type parameters: {lemma.Name}"); + } + if (lemma.Outs.Count != 0) { + throw new ExtractorError($"an extracted lemma is not allowed to have out-parameters: {lemma.Name}"); + } + + var tok = lemma.tok; + + var boundVars = lemma.Ins.ConvertAll(formal => + (Boogie.Variable)new Boogie.BoundVariable(tok, new TypedIdent(tok, formal.Name, ExtractType(formal.Type))) + ); + + var triggers = GetTriggers(tok, patterns); + + var ante = BoogieGenerator.BplAnd(lemma.Req.ConvertAll(req => ExtractExpr(req.E))); + var post = BoogieGenerator.BplAnd(lemma.Ens.ConvertAll(ens => ExtractExpr(ens.E))); + var body = BoogieGenerator.BplImp(ante, post); + + Boogie.Expr axiomBody; + if (boundVars.Count == 0) { + axiomBody = body; + } else { + var kv = GetKeyValues(tok, lemma.Attributes); + axiomBody = new Boogie.ForallExpr(tok, new List(), boundVars, kv, triggers, body); + } + var axiom = new Boogie.Axiom(tok, axiomBody); + declarations.Add(axiom); + + if (usedByInfo != null) { + if (usedByInfo.Args.Count == 1 && usedByInfo.Args[0].Resolved is MemberSelectExpr { Member: Function function }) { + axiomUsedBy.Add((axiom, function)); + } else { + throw new ExtractorError($":{UsedByAttribute} argument on lemma '{lemma.Name}' is expected to be an extracted function"); + } + } + } + + private Trigger? GetTriggers(IToken tok, List>? patterns) { + if (patterns == null) { + return null; + } + + Boogie.Trigger? triggers = null; + for (var i = 0; i < patterns.Count; i++) { + var terms = patterns![i].ConvertAll(ExtractExpr); + triggers = new Boogie.Trigger(tok, true, terms, triggers); + } + + return triggers; + } + + private QKeyValue? GetKeyValues(IToken tok, Attributes attributes) { + Boogie.QKeyValue kv = null; + var extractAttributes = Attributes.FindAllExpressions(attributes, AttributeAttribute); + if (extractAttributes != null) { + if (extractAttributes.Count == 0) { + throw new ExtractorError($"first argument to :{AttributeAttribute} is expected to be a literal string; got no arguments"); + } + for (var i = extractAttributes.Count; 0 <= --i;) { + string? attrName = null; + var parameters = new List(); + foreach (var argument in extractAttributes[i]) { + if (attrName != null) { + parameters.Add(ExtractExpr(argument)); + } else if (argument is StringLiteralExpr { Value: string name }) { + attrName = name; + } else { + throw new ExtractorError($"first argument to :{AttributeAttribute} is expected to be a literal string; got: {argument}"); + } + } + + kv = new Boogie.QKeyValue(tok, attrName, parameters, kv); + } + } + + return kv; + } + + public override void VisitFunction(Function function) { + if (GetExtractName(function.Attributes) is { } extractName) { + var tok = function.tok; + if (function.TypeArgs.Count != 0) { + throw new ExtractorError($"an extracted function is not allowed to have type parameters: {function.Name}"); + } + var inParams = function.Ins.ConvertAll(formal => + (Boogie.Variable)new Boogie.Formal(tok, new TypedIdent(tok, formal.Name, ExtractType(formal.Type)), true) + ); + var result = new Boogie.Formal(tok, new TypedIdent(tok, TypedIdent.NoName, ExtractType(function.ResultType)), false); + var fn = new Boogie.Function(tok, extractName, inParams, result); + declarations.Add(fn); + functionExtractions.Add(function, fn); + } + } + + private Boogie.Type ExtractType(Type type) { + switch (type) { + case IntType: + return Boogie.Type.Int; + case BoolType: + return Boogie.Type.Bool; + case UserDefinedType udt: { + var cl = udt.ResolvedClass; + var name = GetExtractName(cl.Attributes) ?? cl.Name; + return new Boogie.UnresolvedTypeIdentifier(Boogie.Token.NoToken, name, udt.TypeArgs.ConvertAll(ExtractType)); + } + default: + throw new ExtractorError($"type not supported by extractor: {type}"); + } + } + + private string? GetExtractName(Attributes attributes) { + if (Attributes.Find(attributes, NameAttribute) is { } extractNameAttribute) { + if (extractNameAttribute.Args.Count == 1 && extractNameAttribute.Args[0] is StringLiteralExpr { Value: string extractName }) { + return extractName; + } + } + return null; + } + + private Boogie.Expr ExtractExpr(Expression expr) { + expr = expr.Resolved; + var tok = expr.tok; + switch (expr) { + case LiteralExpr literalExpr: { + if (literalExpr.Value is bool boolValue) { + // use the specific literals, rather than Boogie.LiteralExpr(bool), in order for the + // peephole optimizations to kick in + return boolValue ? Boogie.Expr.True : Boogie.Expr.False; + } else if (literalExpr.Value is BigInteger intValue) { + var n = BigNum.FromBigInt(intValue); + return Boogie.Expr.Literal(n); + } + break; + } + + case IdentifierExpr identifierExpr: + return new Boogie.IdentifierExpr(tok, identifierExpr.Name); + + case FunctionCallExpr functionCallExpr: { + var function = functionCallExpr.Function; + var functionName = GetExtractName(function.Attributes) ?? function.Name; + Contract.Assert(function.IsStatic); + var arguments = functionCallExpr.Args.ConvertAll(ExtractExpr); + return new Boogie.NAryExpr(tok, new Boogie.FunctionCall(new Boogie.IdentifierExpr(tok, functionName)), arguments); + } + + case BinaryExpr binaryExpr: { + var e0 = ExtractExpr(binaryExpr.E0); + var e1 = ExtractExpr(binaryExpr.E1); + switch (binaryExpr.ResolvedOp) { + case BinaryExpr.ResolvedOpcode.EqCommon: + return Boogie.Expr.Eq(e0, e1); + case BinaryExpr.ResolvedOpcode.NeqCommon: + return Boogie.Expr.Neq(e0, e1); + case BinaryExpr.ResolvedOpcode.Iff: + return BoogieGenerator.BplIff(e0, e1); + case BinaryExpr.ResolvedOpcode.Imp: + return BoogieGenerator.BplImp(e0, e1); + case BinaryExpr.ResolvedOpcode.And: + return BoogieGenerator.BplAnd(e0, e1); + case BinaryExpr.ResolvedOpcode.Or: + return BoogieGenerator.BplOr(e0, e1); + case BinaryExpr.ResolvedOpcode.Le: + return Boogie.Expr.Le(e0, e1); + case BinaryExpr.ResolvedOpcode.Lt: + return Boogie.Expr.Lt(e0, e1); + case BinaryExpr.ResolvedOpcode.Add: + return Boogie.Expr.Add(e0, e1); + case BinaryExpr.ResolvedOpcode.Sub: + return Boogie.Expr.Sub(e0, e1); + default: + break; + } + break; + } + + case UnaryOpExpr unaryOpExpr: + if (unaryOpExpr.ResolvedOp == UnaryOpExpr.ResolvedOpcode.BoolNot) { + var e = ExtractExpr(unaryOpExpr.E); + return Boogie.Expr.Not(e); + } else { + throw new ExtractorError($"extractor does not support unary operator {unaryOpExpr.ResolvedOp}"); + } + + case QuantifierExpr quantifierExpr: { + var boundVars = quantifierExpr.BoundVars.ConvertAll(boundVar => + (Boogie.Variable)new Boogie.BoundVariable(tok, new TypedIdent(tok, boundVar.Name, ExtractType(boundVar.Type))) + ); + + var patterns = Attributes.FindAllExpressions(quantifierExpr.Attributes, PatternAttribute); + if (patterns.Count == 0) { + throw new ExtractorError($"extraction expects every quantifier to specify at least one :{PatternAttribute}"); + } + var triggers = GetTriggers(tok, patterns); + + var kv = GetKeyValues(tok, quantifierExpr.Attributes); + var body = ExtractExpr(quantifierExpr.LogicalBody()); + if (quantifierExpr is ExistsExpr) { + return new Boogie.ExistsExpr(tok, new List(), boundVars, kv, triggers, body); + } else { + Contract.Assert(quantifierExpr is ForallExpr); + return new Boogie.ForallExpr(tok, new List(), boundVars, kv, triggers, body); + } + } + + default: + break; + } + + throw new ExtractorError($"extraction does not support expression of type {expr.GetType()}: {expr}"); + } + } +} diff --git a/Source/DafnyCore/DafnyOptions.cs b/Source/DafnyCore/DafnyOptions.cs index 40f29a3b3b9..e6c6b0a3c4c 100644 --- a/Source/DafnyCore/DafnyOptions.cs +++ b/Source/DafnyCore/DafnyOptions.cs @@ -320,6 +320,7 @@ public enum ContractTestingMode { public PrintModes PrintMode = PrintModes.Everything; // Default to printing everything public bool DafnyVerify = true; public string DafnyPrintResolvedFile = null; + public string BoogieExtractionTargetFile = null; public List DafnyPrintExportedViews = new List(); public bool Compile = true; public List MainArgs = new List(); diff --git a/Source/DafnyCore/DafnyPrelude.bpl b/Source/DafnyCore/DafnyPrelude.bpl index d82cd33cc1c..12857ef3ff5 100644 --- a/Source/DafnyCore/DafnyPrelude.bpl +++ b/Source/DafnyCore/DafnyPrelude.bpl @@ -117,7 +117,7 @@ axiom (forall x: real :: { $Box(LitReal(x)) } $Box(LitReal(x)) == Lit($Box(x)) ) #if UNICODE_CHAR function {:inline} char#IsChar(n: int): bool { - (0 <= n && n < 55296 /* 0xD800 */) || + (0 <= n && n < 55296 /* 0xD800 */) || (57344 /* 0xE000 */ <= n && n < 1114112 /* 0x11_0000 */ ) } #else @@ -263,7 +263,7 @@ axiom (forall v: Map, t0: Ty, t1: Ty :: Map#Domain(v)[bx] ==> $IsBox(Map#Elements(v)[bx], t1) && $IsBox(bx, t0))); - + axiom (forall v: Map, t0: Ty, t1: Ty :: { $Is(v, TMap(t0, t1)) } $Is(v, TMap(t0, t1)) ==> @@ -291,9 +291,9 @@ axiom(forall h : Heap, v : real :: { $IsAlloc(v,TReal,h) } $IsAlloc(v,TReal,h)); axiom(forall h : Heap, v : bool :: { $IsAlloc(v,TBool,h) } $IsAlloc(v,TBool,h)); axiom(forall h : Heap, v : char :: { $IsAlloc(v,TChar,h) } $IsAlloc(v,TChar,h)); axiom(forall h : Heap, v : ORDINAL :: { $IsAlloc(v,TORDINAL,h) } $IsAlloc(v,TORDINAL,h)); - + axiom (forall v: Bv0, h: Heap :: { $IsAlloc(v, TBitvector(0), h) } $IsAlloc(v, TBitvector(0), h)); - + axiom (forall v: Set, t0: Ty, h: Heap :: { $IsAlloc(v, TSet(t0), h) } $IsAlloc(v, TSet(t0), h) <==> (forall bx: Box :: { v[bx] } @@ -320,7 +320,7 @@ axiom (forall v: Map, t0: Ty, t1: Ty, h: Heap :: Map#Domain(v)[bx] ==> $IsAllocBox(Map#Elements(v)[bx], t1, h) && $IsAllocBox(bx, t0, h))); - + axiom (forall v: IMap, t0: Ty, t1: Ty, h: Heap :: { $IsAlloc(v, TIMap(t0, t1), h) } $IsAlloc(v, TIMap(t0, t1), h) @@ -958,150 +958,221 @@ axiom (forall s: Seq, x: Box :: { MultiSet#FromSeq(s)[x] } // -- Axiomatization of sequences -------------------------------- // --------------------------------------------------------------- + + type Seq; -function Seq#Length(Seq): int; +function Seq#Length(s: Seq) : int; + axiom (forall s: Seq :: { Seq#Length(s) } 0 <= Seq#Length(s)); -function Seq#Empty(): Seq uses { - axiom (Seq#Length(Seq#Empty(): Seq) == 0); +function Seq#Empty() : Seq +uses { +axiom Seq#Length(Seq#Empty()) == 0; } -axiom (forall s: Seq :: { Seq#Length(s) } - (Seq#Length(s) == 0 ==> s == Seq#Empty()) + +axiom (forall s: Seq :: { Seq#Length(s) } Seq#Length(s) == 0 ==> s == Seq#Empty()); // The following would be a nice fact to include, because it would enable verifying the // GenericPick.SeqPick* methods in Test/dafny0/SmallTests.dfy. However, it substantially // slows down performance on some other tests, including running seemingly forever on // some. -// && (Seq#Length(s) != 0 ==> (exists x: Box :: Seq#Contains(s, x))) - ); - -// The empty sequence $Is any type -//axiom (forall t: Ty :: {$Is(Seq#Empty(): Seq, TSeq(t))} $Is(Seq#Empty(): Seq, TSeq(t))); +// axiom (forall s: Seq :: { Seq#Length(s) } +// (Seq#Length(s) != 0 ==> (exists x: Box :: Seq#Contains(s, x))) +// ); -function Seq#Singleton(Box): Seq; -axiom (forall t: Box :: { Seq#Length(Seq#Singleton(t)) } Seq#Length(Seq#Singleton(t)) == 1); +function Seq#Build(s: Seq, val: Box) : Seq; -function Seq#Build(s: Seq, val: Box): Seq; function Seq#Build_inv0(s: Seq) : Seq; + function Seq#Build_inv1(s: Seq) : Box; + axiom (forall s: Seq, val: Box :: { Seq#Build(s, val) } - Seq#Build_inv0(Seq#Build(s, val)) == s && - Seq#Build_inv1(Seq#Build(s, val)) == val); + Seq#Build_inv0(Seq#Build(s, val)) == s + && Seq#Build_inv1(Seq#Build(s, val)) == val); axiom (forall s: Seq, v: Box :: - { Seq#Build(s,v) } - Seq#Length(Seq#Build(s,v)) == 1 + Seq#Length(s)); -axiom (forall s: Seq, i: int, v: Box :: { Seq#Index(Seq#Build(s,v), i) } - (i == Seq#Length(s) ==> Seq#Index(Seq#Build(s,v), i) == v) && - (i != Seq#Length(s) ==> Seq#Index(Seq#Build(s,v), i) == Seq#Index(s, i))); + { Seq#Build(s, v) } + Seq#Length(Seq#Build(s, v)) == 1 + Seq#Length(s)); -// Build preserves $Is -axiom (forall s: Seq, bx: Box, t: Ty :: { $Is(Seq#Build(s,bx),TSeq(t)) } - $Is(s,TSeq(t)) && $IsBox(bx,t) ==> $Is(Seq#Build(s,bx),TSeq(t))); +axiom (forall s: Seq, i: int, v: Box :: + { Seq#Index(Seq#Build(s, v), i) } + (i == Seq#Length(s) ==> Seq#Index(Seq#Build(s, v), i) == v) + && (i != Seq#Length(s) ==> Seq#Index(Seq#Build(s, v), i) == Seq#Index(s, i))); -function Seq#Create(ty: Ty, heap: Heap, len: int, init: HandleType): Seq; -axiom (forall ty: Ty, heap: Heap, len: int, init: HandleType :: - { Seq#Length(Seq#Create(ty, heap, len, init): Seq) } - $IsGoodHeap(heap) && 0 <= len ==> - Seq#Length(Seq#Create(ty, heap, len, init): Seq) == len); -axiom (forall ty: Ty, heap: Heap, len: int, init: HandleType, i: int :: - { Seq#Index(Seq#Create(ty, heap, len, init), i) } - $IsGoodHeap(heap) && 0 <= i && i < len ==> - Seq#Index(Seq#Create(ty, heap, len, init), i) == Apply1(TInt, ty, heap, init, $Box(i))); +axiom (forall s0: Seq, s1: Seq :: + { Seq#Length(Seq#Append(s0, s1)) } + Seq#Length(Seq#Append(s0, s1)) == Seq#Length(s0) + Seq#Length(s1)); + +function Seq#Index(s: Seq, i: int) : Box; + +axiom (forall s0: Seq, s1: Seq, n: int :: + { Seq#Index(Seq#Append(s0, s1), n) } + (n < Seq#Length(s0) ==> Seq#Index(Seq#Append(s0, s1), n) == Seq#Index(s0, n)) + && (Seq#Length(s0) <= n + ==> Seq#Index(Seq#Append(s0, s1), n) == Seq#Index(s1, n - Seq#Length(s0)))); + +function Seq#Update(s: Seq, i: int, val: Box) : Seq; + +axiom (forall s: Seq, i: int, v: Box :: + { Seq#Length(Seq#Update(s, i, v)) } + 0 <= i && i < Seq#Length(s) ==> Seq#Length(Seq#Update(s, i, v)) == Seq#Length(s)); + +axiom (forall s: Seq, i: int, v: Box, n: int :: + { Seq#Index(Seq#Update(s, i, v), n) } + 0 <= n && n < Seq#Length(s) + ==> (i == n ==> Seq#Index(Seq#Update(s, i, v), n) == v) + && (i != n ==> Seq#Index(Seq#Update(s, i, v), n) == Seq#Index(s, n))); + +function Seq#Append(s0: Seq, s1: Seq) : Seq; + +function Seq#Contains(s: Seq, val: Box) : bool; + +axiom (forall s: Seq, x: Box :: + { Seq#Contains(s, x) } + Seq#Contains(s, x) + <==> (exists i: int :: + { Seq#Index(s, i) } + 0 <= i && i < Seq#Length(s) && Seq#Index(s, i) == x)); -function Seq#Append(Seq, Seq): Seq; -axiom (forall s0: Seq, s1: Seq :: { Seq#Length(Seq#Append(s0,s1)) } - Seq#Length(Seq#Append(s0,s1)) == Seq#Length(s0) + Seq#Length(s1)); - -function Seq#Index(Seq, int): Box; -axiom (forall t: Box :: { Seq#Index(Seq#Singleton(t), 0) } Seq#Index(Seq#Singleton(t), 0) == t); -axiom (forall s0: Seq, s1: Seq, n: int :: { Seq#Index(Seq#Append(s0,s1), n) } - (n < Seq#Length(s0) ==> Seq#Index(Seq#Append(s0,s1), n) == Seq#Index(s0, n)) && - (Seq#Length(s0) <= n ==> Seq#Index(Seq#Append(s0,s1), n) == Seq#Index(s1, n - Seq#Length(s0)))); - -function Seq#Update(Seq, int, Box): Seq; -axiom (forall s: Seq, i: int, v: Box :: { Seq#Length(Seq#Update(s,i,v)) } - 0 <= i && i < Seq#Length(s) ==> Seq#Length(Seq#Update(s,i,v)) == Seq#Length(s)); -axiom (forall s: Seq, i: int, v: Box, n: int :: { Seq#Index(Seq#Update(s,i,v),n) } - 0 <= n && n < Seq#Length(s) ==> - (i == n ==> Seq#Index(Seq#Update(s,i,v),n) == v) && - (i != n ==> Seq#Index(Seq#Update(s,i,v),n) == Seq#Index(s,n))); - -function Seq#Contains(Seq, Box): bool; -axiom (forall s: Seq, x: Box :: { Seq#Contains(s,x) } - Seq#Contains(s,x) <==> - (exists i: int :: { Seq#Index(s,i) } 0 <= i && i < Seq#Length(s) && Seq#Index(s,i) == x)); axiom (forall x: Box :: { Seq#Contains(Seq#Empty(), x) } !Seq#Contains(Seq#Empty(), x)); axiom (forall s0: Seq, s1: Seq, x: Box :: { Seq#Contains(Seq#Append(s0, s1), x) } - Seq#Contains(Seq#Append(s0, s1), x) <==> - Seq#Contains(s0, x) || Seq#Contains(s1, x)); + Seq#Contains(Seq#Append(s0, s1), x) + <==> Seq#Contains(s0, x) || Seq#Contains(s1, x)); -axiom (forall s: Seq, v: Box, x: Box :: // needed to prove things like '4 in [2,3,4]', see method TestSequences0 in SmallTests.dfy +// needed to prove things like '4 in [2,3,4]', see method TestSequences0 in SmallTests.dfy +axiom (forall s: Seq, v: Box, x: Box :: { Seq#Contains(Seq#Build(s, v), x) } - Seq#Contains(Seq#Build(s, v), x) <==> (v == x || Seq#Contains(s, x))); + Seq#Contains(Seq#Build(s, v), x) <==> v == x || Seq#Contains(s, x)); axiom (forall s: Seq, n: int, x: Box :: { Seq#Contains(Seq#Take(s, n), x) } - Seq#Contains(Seq#Take(s, n), x) <==> - (exists i: int :: { Seq#Index(s, i) } + Seq#Contains(Seq#Take(s, n), x) + <==> (exists i: int :: + { Seq#Index(s, i) } 0 <= i && i < n && i < Seq#Length(s) && Seq#Index(s, i) == x)); + axiom (forall s: Seq, n: int, x: Box :: { Seq#Contains(Seq#Drop(s, n), x) } - Seq#Contains(Seq#Drop(s, n), x) <==> - (exists i: int :: { Seq#Index(s, i) } + Seq#Contains(Seq#Drop(s, n), x) + <==> (exists i: int :: + { Seq#Index(s, i) } 0 <= n && n <= i && i < Seq#Length(s) && Seq#Index(s, i) == x)); -function Seq#Equal(Seq, Seq): bool; -axiom (forall s0: Seq, s1: Seq :: { Seq#Equal(s0,s1) } - Seq#Equal(s0,s1) <==> - Seq#Length(s0) == Seq#Length(s1) && - (forall j: int :: { Seq#Index(s0,j) } { Seq#Index(s1,j) } - 0 <= j && j < Seq#Length(s0) ==> Seq#Index(s0,j) == Seq#Index(s1,j))); -axiom (forall a: Seq, b: Seq :: { Seq#Equal(a,b) } // extensionality axiom for sequences - Seq#Equal(a,b) ==> a == b); - -function Seq#SameUntil(Seq, Seq, int): bool; -axiom (forall s0: Seq, s1: Seq, n: int :: { Seq#SameUntil(s0,s1,n) } - Seq#SameUntil(s0,s1,n) <==> - (forall j: int :: { Seq#Index(s0,j) } { Seq#Index(s1,j) } - 0 <= j && j < n ==> Seq#Index(s0,j) == Seq#Index(s1,j))); - -function Seq#Take(s: Seq, howMany: int): Seq; -axiom (forall s: Seq, n: int :: { Seq#Length(Seq#Take(s,n)) } - 0 <= n && n <= Seq#Length(s) ==> Seq#Length(Seq#Take(s,n)) == n); +function Seq#Equal(s0: Seq, s1: Seq) : bool; + +axiom (forall s0: Seq, s1: Seq :: + { Seq#Equal(s0, s1) } + Seq#Equal(s0, s1) + <==> Seq#Length(s0) == Seq#Length(s1) + && (forall j: int :: + { Seq#Index(s0, j) } { Seq#Index(s1, j) } + 0 <= j && j < Seq#Length(s0) ==> Seq#Index(s0, j) == Seq#Index(s1, j))); + +// extensionality axiom for sequences +axiom (forall a: Seq, b: Seq :: { Seq#Equal(a, b) } Seq#Equal(a, b) ==> a == b); + +function Seq#SameUntil(s0: Seq, s1: Seq, n: int) : bool; + +axiom (forall s0: Seq, s1: Seq, n: int :: + { Seq#SameUntil(s0, s1, n) } + Seq#SameUntil(s0, s1, n) + <==> (forall j: int :: + { Seq#Index(s0, j) } { Seq#Index(s1, j) } + 0 <= j && j < n ==> Seq#Index(s0, j) == Seq#Index(s1, j))); + +function Seq#Take(s: Seq, howMany: int) : Seq; + +axiom (forall s: Seq, n: int :: + { Seq#Length(Seq#Take(s, n)) } + 0 <= n && n <= Seq#Length(s) ==> Seq#Length(Seq#Take(s, n)) == n); + axiom (forall s: Seq, n: int, j: int :: - {:weight 25} - { Seq#Index(Seq#Take(s,n), j) } - { Seq#Index(s, j), Seq#Take(s,n) } - 0 <= j && j < n && j < Seq#Length(s) ==> - Seq#Index(Seq#Take(s,n), j) == Seq#Index(s, j)); - -function Seq#Drop(s: Seq, howMany: int): Seq; -axiom (forall s: Seq, n: int :: { Seq#Length(Seq#Drop(s,n)) } - 0 <= n && n <= Seq#Length(s) ==> Seq#Length(Seq#Drop(s,n)) == Seq#Length(s) - n); + {:weight 25} { Seq#Index(Seq#Take(s, n), j) } { Seq#Index(s, j), Seq#Take(s, n) } + 0 <= j && j < n && j < Seq#Length(s) + ==> Seq#Index(Seq#Take(s, n), j) == Seq#Index(s, j)); + +function Seq#Drop(s: Seq, howMany: int) : Seq; + +axiom (forall s: Seq, n: int :: + { Seq#Length(Seq#Drop(s, n)) } + 0 <= n && n <= Seq#Length(s) ==> Seq#Length(Seq#Drop(s, n)) == Seq#Length(s) - n); + axiom (forall s: Seq, n: int, j: int :: - {:weight 25} - { Seq#Index(Seq#Drop(s,n), j) } - 0 <= n && 0 <= j && j < Seq#Length(s)-n ==> - Seq#Index(Seq#Drop(s,n), j) == Seq#Index(s, j+n)); + {:weight 25} { Seq#Index(Seq#Drop(s, n), j) } + 0 <= n && 0 <= j && j < Seq#Length(s) - n + ==> Seq#Index(Seq#Drop(s, n), j) == Seq#Index(s, j + n)); + axiom (forall s: Seq, n: int, k: int :: - {:weight 25} - { Seq#Index(s, k), Seq#Drop(s,n) } - 0 <= n && n <= k && k < Seq#Length(s) ==> - Seq#Index(Seq#Drop(s,n), k-n) == Seq#Index(s, k)); - -axiom (forall s, t: Seq, n: int :: - { Seq#Take(Seq#Append(s, t), n) } - { Seq#Drop(Seq#Append(s, t), n) } + {:weight 25} { Seq#Index(s, k), Seq#Drop(s, n) } + 0 <= n && n <= k && k < Seq#Length(s) + ==> Seq#Index(Seq#Drop(s, n), k - n) == Seq#Index(s, k)); + +axiom (forall s: Seq, t: Seq, n: int :: + { Seq#Take(Seq#Append(s, t), n) } { Seq#Drop(Seq#Append(s, t), n) } n == Seq#Length(s) - ==> - Seq#Take(Seq#Append(s, t), n) == s && - Seq#Drop(Seq#Append(s, t), n) == t); + ==> Seq#Take(Seq#Append(s, t), n) == s && Seq#Drop(Seq#Append(s, t), n) == t); + +// Commutability of Take and Drop with Update. +axiom (forall s: Seq, i: int, v: Box, n: int :: + { Seq#Take(Seq#Update(s, i, v), n) } + 0 <= i && i < n && n <= Seq#Length(s) + ==> Seq#Take(Seq#Update(s, i, v), n) == Seq#Update(Seq#Take(s, n), i, v)); + +axiom (forall s: Seq, i: int, v: Box, n: int :: + { Seq#Take(Seq#Update(s, i, v), n) } + n <= i && i < Seq#Length(s) + ==> Seq#Take(Seq#Update(s, i, v), n) == Seq#Take(s, n)); + +axiom (forall s: Seq, i: int, v: Box, n: int :: + { Seq#Drop(Seq#Update(s, i, v), n) } + 0 <= n && n <= i && i < Seq#Length(s) + ==> Seq#Drop(Seq#Update(s, i, v), n) == Seq#Update(Seq#Drop(s, n), i - n, v)); + +axiom (forall s: Seq, i: int, v: Box, n: int :: + { Seq#Drop(Seq#Update(s, i, v), n) } + 0 <= i && i < n && n <= Seq#Length(s) + ==> Seq#Drop(Seq#Update(s, i, v), n) == Seq#Drop(s, n)); + +// drop commutes with build. +axiom (forall s: Seq, v: Box, n: int :: + { Seq#Drop(Seq#Build(s, v), n) } + 0 <= n && n <= Seq#Length(s) + ==> Seq#Drop(Seq#Build(s, v), n) == Seq#Build(Seq#Drop(s, n), v)); + +// Additional axioms about common things +axiom (forall s: Seq, n: int :: { Seq#Drop(s, n) } n == 0 ==> Seq#Drop(s, n) == s); + +axiom (forall s: Seq, n: int :: + { Seq#Take(s, n) } + n == 0 ==> Seq#Take(s, n) == Seq#Empty()); + +axiom (forall s: Seq, m: int, n: int :: + { Seq#Drop(Seq#Drop(s, m), n) } + 0 <= m && 0 <= n && m + n <= Seq#Length(s) + ==> Seq#Drop(Seq#Drop(s, m), n) == Seq#Drop(s, m + n)); + + +// The empty sequence $Is any type +//axiom (forall t: Ty :: {$Is(Seq#Empty(): Seq, TSeq(t))} $Is(Seq#Empty(): Seq, TSeq(t))); + +// Build preserves $Is +axiom (forall s: Seq, bx: Box, t: Ty :: { $Is(Seq#Build(s, bx), TSeq(t)) } + $Is(s, TSeq(t)) && $IsBox(bx, t) ==> $Is(Seq#Build(s, bx), TSeq(t))); + +function Seq#Create(ty: Ty, heap: Heap, len: int, init: HandleType): Seq; +axiom (forall ty: Ty, heap: Heap, len: int, init: HandleType :: + { Seq#Length(Seq#Create(ty, heap, len, init): Seq) } + $IsGoodHeap(heap) && 0 <= len ==> + Seq#Length(Seq#Create(ty, heap, len, init): Seq) == len); +axiom (forall ty: Ty, heap: Heap, len: int, init: HandleType, i: int :: + { Seq#Index(Seq#Create(ty, heap, len, init), i) } + $IsGoodHeap(heap) && 0 <= i && i < len ==> + Seq#Index(Seq#Create(ty, heap, len, init), i) == Apply1(TInt, ty, heap, init, $Box(i))); function Seq#FromArray(h: Heap, a: ref): Seq; axiom (forall h: Heap, a: ref :: @@ -1128,27 +1199,10 @@ axiom (forall h: Heap, i: int, v: Box, a: ref :: { Seq#FromArray(update(h, a, IndexField(i), v), a) } 0 <= i && i < _System.array.Length(a) ==> Seq#FromArray(update(h, a, IndexField(i), v), a) == Seq#Update(Seq#FromArray(h, a), i, v) ); -// Commutability of Take and Drop with Update. -axiom (forall s: Seq, i: int, v: Box, n: int :: - { Seq#Take(Seq#Update(s, i, v), n) } - 0 <= i && i < n && n <= Seq#Length(s) ==> Seq#Take(Seq#Update(s, i, v), n) == Seq#Update(Seq#Take(s, n), i, v) ); -axiom (forall s: Seq, i: int, v: Box, n: int :: - { Seq#Take(Seq#Update(s, i, v), n) } - n <= i && i < Seq#Length(s) ==> Seq#Take(Seq#Update(s, i, v), n) == Seq#Take(s, n)); -axiom (forall s: Seq, i: int, v: Box, n: int :: - { Seq#Drop(Seq#Update(s, i, v), n) } - 0 <= n && n <= i && i < Seq#Length(s) ==> Seq#Drop(Seq#Update(s, i, v), n) == Seq#Update(Seq#Drop(s, n), i-n, v) ); -axiom (forall s: Seq, i: int, v: Box, n: int :: - { Seq#Drop(Seq#Update(s, i, v), n) } - 0 <= i && i < n && n <= Seq#Length(s) ==> Seq#Drop(Seq#Update(s, i, v), n) == Seq#Drop(s, n)); // Extension axiom, triggers only on Takes from arrays. axiom (forall h: Heap, a: ref, n0, n1: int :: { Seq#Take(Seq#FromArray(h, a), n0), Seq#Take(Seq#FromArray(h, a), n1) } n0 + 1 == n1 && 0 <= n0 && n1 <= _System.array.Length(a) ==> Seq#Take(Seq#FromArray(h, a), n1) == Seq#Build(Seq#Take(Seq#FromArray(h, a), n0), read(h, a, IndexField(n0): Field)) ); -// drop commutes with build. -axiom (forall s: Seq, v: Box, n: int :: - { Seq#Drop(Seq#Build(s, v), n) } - 0 <= n && n <= Seq#Length(s) ==> Seq#Drop(Seq#Build(s, v), n) == Seq#Build(Seq#Drop(s, n), v) ); function Seq#Rank(Seq): int; axiom (forall s: Seq, i: int :: @@ -1164,15 +1218,6 @@ axiom (forall s: Seq, i: int, j: int :: { Seq#Rank(Seq#Append(Seq#Take(s, i), Seq#Drop(s, j))) } 0 <= i && i < j && j <= Seq#Length(s) ==> Seq#Rank(Seq#Append(Seq#Take(s, i), Seq#Drop(s, j))) < Seq#Rank(s) ); -// Additional axioms about common things -axiom (forall s: Seq, n: int :: { Seq#Drop(s, n) } - n == 0 ==> Seq#Drop(s, n) == s); -axiom (forall s: Seq, n: int :: { Seq#Take(s, n) } - n == 0 ==> Seq#Take(s, n) == Seq#Empty()); -axiom (forall s: Seq, m, n: int :: { Seq#Drop(Seq#Drop(s, m), n) } - 0 <= m && 0 <= n && m+n <= Seq#Length(s) ==> - Seq#Drop(Seq#Drop(s, m), n) == Seq#Drop(s, m+n)); - // --------------------------------------------------------------- // -- Axiomatization of Maps ------------------------------------- // --------------------------------------------------------------- @@ -1501,3 +1546,4 @@ axiom (forall x, y, z: int :: #endif // ------------------------------------------------------------------------- + diff --git a/Source/DafnyCore/Makefile b/Source/DafnyCore/Makefile index e05f6554ae2..32190f29bb0 100644 --- a/Source/DafnyCore/Makefile +++ b/Source/DafnyCore/Makefile @@ -27,3 +27,7 @@ format: check-format: ../../Scripts/dafny format . --check + +extract: + (cd Prelude; make; cd ..) + cp Prelude/DafnyPrelude.bpl . diff --git a/Source/DafnyCore/Prelude/Boxes.dfy b/Source/DafnyCore/Prelude/Boxes.dfy new file mode 100644 index 00000000000..660c8d71426 --- /dev/null +++ b/Source/DafnyCore/Prelude/Boxes.dfy @@ -0,0 +1,8 @@ +module Boxes { + export + provides Box, arbitrary + + type Box(==,0) + + const arbitrary: Box +} diff --git a/Source/DafnyCore/Prelude/Lists.dfy b/Source/DafnyCore/Prelude/Lists.dfy new file mode 100644 index 00000000000..17d505d3b8c --- /dev/null +++ b/Source/DafnyCore/Prelude/Lists.dfy @@ -0,0 +1,112 @@ +module Lists { + export + reveals List, List.Length, List.At, List.Append, List.Take, List.Drop, List.Split + provides List.LengthAppend, List.AppendAt, List.AboutDrop + provides List.AppendTake, List.TakeFromAppend, List.AppendDrop, List.DropFromAppend + provides List.AppendTakeDrop, List.LengthTakeDrop + + datatype List = Nil | Cons(head: X, tail: List) + { + function Length(): nat { + if Nil? then 0 else 1 + tail.Length() + } + + function Append(xs: List): List { + match this + case Nil => xs + case Cons(x, tail) => Cons(x, tail.Append(xs)) + } + + lemma LengthAppend(xs: List) + ensures Append(xs).Length() == Length() + xs.Length() + { + } + + function At(i: nat): X + requires i < Length() + { + if i == 0 then head else tail.At(i - 1) + } + + lemma AppendAt(xs: List, i: nat) + requires i < Append(xs).Length() + ensures Append(xs).At(i) == + if i < Length() then At(i) else (LengthAppend(xs); xs.At(i - Length())) + { + } + + function Take(n: nat): List + requires n <= Length() + { + if n == 0 then Nil else Cons(head, tail.Take(n - 1)) + } + + function Drop(n: nat): List + requires n <= Length() + { + if n == 0 then this else tail.Drop(n - 1) + } + + function Split(n: nat): (split: (List, List)) + requires n <= Length() + ensures split.0.Append(split.1) == this + { + AppendTakeDrop(n); + (Take(n), Drop(n)) + } + + lemma AboutDrop(n: nat) + requires n < Length() + ensures Drop(n).Cons? + { + } + + lemma AppendTake(xs: List) + ensures (LengthAppend(xs); Append(xs).Take(Length()) == this) + { + match this + case Nil => + case Cons(x, tail) => + LengthAppend(xs); + } + + lemma TakeFromAppend(xs: List, n: nat) + requires n <= Length() + xs.Length() + ensures (LengthAppend(xs); + Append(xs).Take(n) == + if n <= Length() then Take(n) else Append(xs.Take(n - Length()))) + { + LengthAppend(xs); + } + + lemma AppendDrop(xs: List) + ensures (LengthAppend(xs); Append(xs).Drop(Length()) == xs) + { + match this + case Nil => + case Cons(x, tail) => + LengthAppend(xs); + } + + lemma DropFromAppend(xs: List, n: nat) + requires n <= Length() + xs.Length() + ensures (LengthAppend(xs); + Append(xs).Drop(n) == + if n <= Length() then Drop(n).Append(xs) else xs.Drop(n - Length())) + { + LengthAppend(xs); + } + + lemma AppendTakeDrop(i: nat) + requires i <= Length() + ensures Take(i).Append(Drop(i)) == this + { + } + + lemma LengthTakeDrop(i: nat) + requires i <= Length() + ensures Take(i).Length() == i && Drop(i).Length() == Length() - i + { + } + } +} diff --git a/Source/DafnyCore/Prelude/Makefile b/Source/DafnyCore/Prelude/Makefile new file mode 100644 index 00000000000..94e8c4b8341 --- /dev/null +++ b/Source/DafnyCore/Prelude/Makefile @@ -0,0 +1,20 @@ +DAFNY=../../../Scripts/dafny + +all: DafnyPrelude.bpl + +DafnyPrelude.bpl: PreludeCore.bpl Sequences.bpl + # cpp is allergic to primes, so we have to do a song and dance around it + sed -e "s|'|PRIME|g" -i "" PreludeCore.bpl Sequences.bpl + # also, we need to disable preprocessing of Boogie things + sed -e "s|^#if|//#if|" -i "" PreludeCore.bpl + sed -e "s|^#e|//#e|" -i "" PreludeCore.bpl + # Extract Boogie from the model verified in Dafny + cpp -C -P PreludeCore.bpl DafnyPrelude.bpl + # Undo the song and dance with primes and Boogie preprocessing directives + sed -e "s|^//#|#|" -i "" PreludeCore.bpl DafnyPrelude.bpl + sed -e "s|PRIME|'|g" -i "" PreludeCore.bpl Sequences.bpl DafnyPrelude.bpl + +Sequences.bpl: Lists.dfy Boxes.dfy Sequences.dfy + $(DAFNY) verify Lists.dfy Boxes.dfy Sequences.dfy --extract:Sequences.bpl + # Remove trailing spaces that the Boogie pretty printer emits + sed -e "s| *$$||" -i "" Sequences.bpl diff --git a/Source/DafnyCore/Prelude/PreludeCore.bpl b/Source/DafnyCore/Prelude/PreludeCore.bpl new file mode 100644 index 00000000000..b40823328f9 --- /dev/null +++ b/Source/DafnyCore/Prelude/PreludeCore.bpl @@ -0,0 +1,1351 @@ +// Dafny prelude +// Created 9 February 2008 by Rustan Leino. +// Converted to Boogie 2 on 28 June 2008. +// Edited sequence axioms 20 October 2009 by Alex Summers. +// Modified 2014 by Dan Rosen. +// Copyright (c) 2008-2014, Microsoft. +// Copyright by the contributors to the Dafny Project +// SPDX-License-Identifier: MIT + +const $$Language$Dafny: bool uses { // To be recognizable to the ModelViewer as + axiom $$Language$Dafny; // coming from a Dafny program. +} + +// --------------------------------------------------------------- +// -- Types ------------------------------------------------------ +// --------------------------------------------------------------- + +type Ty; +type Bv0 = int; + +const unique TBool : Ty uses { + axiom Tag(TBool) == TagBool; +} +const unique TChar : Ty uses { + axiom Tag(TChar) == TagChar; +} +const unique TInt : Ty uses { + axiom Tag(TInt) == TagInt; +} +const unique TReal : Ty uses { + axiom Tag(TReal) == TagReal; +} +const unique TORDINAL : Ty uses { + axiom Tag(TORDINAL) == TagORDINAL; +} +// See for which axioms we can make use of the trigger to determine the connection. +function TBitvector(int) : Ty; +axiom (forall w: int :: { TBitvector(w) } Inv0_TBitvector(TBitvector(w)) == w); + +function TSet(Ty) : Ty; +axiom (forall t: Ty :: { TSet(t) } Inv0_TSet(TSet(t)) == t); +axiom (forall t: Ty :: { TSet(t) } Tag(TSet(t)) == TagSet); + +function TISet(Ty) : Ty; +axiom (forall t: Ty :: { TISet(t) } Inv0_TISet(TISet(t)) == t); +axiom (forall t: Ty :: { TISet(t) } Tag(TISet(t)) == TagISet); + +function TMultiSet(Ty) : Ty; +axiom (forall t: Ty :: { TMultiSet(t) } Inv0_TMultiSet(TMultiSet(t)) == t); +axiom (forall t: Ty :: { TMultiSet(t) } Tag(TMultiSet(t)) == TagMultiSet); + +function TSeq(Ty) : Ty; +axiom (forall t: Ty :: { TSeq(t) } Inv0_TSeq(TSeq(t)) == t); +axiom (forall t: Ty :: { TSeq(t) } Tag(TSeq(t)) == TagSeq); + +function TMap(Ty, Ty) : Ty; +axiom (forall t, u: Ty :: { TMap(t,u) } Inv0_TMap(TMap(t,u)) == t); +axiom (forall t, u: Ty :: { TMap(t,u) } Inv1_TMap(TMap(t,u)) == u); +axiom (forall t, u: Ty :: { TMap(t,u) } Tag(TMap(t,u)) == TagMap); + +function TIMap(Ty, Ty) : Ty; +axiom (forall t, u: Ty :: { TIMap(t,u) } Inv0_TIMap(TIMap(t,u)) == t); +axiom (forall t, u: Ty :: { TIMap(t,u) } Inv1_TIMap(TIMap(t,u)) == u); +axiom (forall t, u: Ty :: { TIMap(t,u) } Tag(TIMap(t,u)) == TagIMap); + + +function Inv0_TBitvector(Ty) : int; +function Inv0_TSet(Ty) : Ty; +function Inv0_TISet(Ty) : Ty; +function Inv0_TSeq(Ty) : Ty; +function Inv0_TMultiSet(Ty) : Ty; +function Inv0_TMap(Ty) : Ty; +function Inv1_TMap(Ty) : Ty; +function Inv0_TIMap(Ty) : Ty; +function Inv1_TIMap(Ty) : Ty; + +// -- Classes and Datatypes -- + +// -- Type Tags -- +type TyTag; +function Tag(Ty) : TyTag; + +const unique TagBool : TyTag; +const unique TagChar : TyTag; +const unique TagInt : TyTag; +const unique TagReal : TyTag; +const unique TagORDINAL : TyTag; +const unique TagSet : TyTag; +const unique TagISet : TyTag; +const unique TagMultiSet : TyTag; +const unique TagSeq : TyTag; +const unique TagMap : TyTag; +const unique TagIMap : TyTag; +const unique TagClass : TyTag; + +type TyTagFamily; +function TagFamily(Ty): TyTagFamily; + +// --------------------------------------------------------------- +// -- Literals --------------------------------------------------- +// --------------------------------------------------------------- +function {:identity} Lit(x: T): T { x } +axiom (forall x: T :: { $Box(Lit(x)) } $Box(Lit(x)) == Lit($Box(x)) ); + +// Specialize Lit to concrete types. +// These aren't logically required, but on some examples improve +// verification speed +function {:identity} LitInt(x: int): int { x } +axiom (forall x: int :: { $Box(LitInt(x)) } $Box(LitInt(x)) == Lit($Box(x)) ); + +function {:identity} LitReal(x: real): real { x } +axiom (forall x: real :: { $Box(LitReal(x)) } $Box(LitReal(x)) == Lit($Box(x)) ); + +// --------------------------------------------------------------- +// -- Characters ------------------------------------------------- +// --------------------------------------------------------------- + +#if UNICODE_CHAR +function {:inline} char#IsChar(n: int): bool { + (0 <= n && n < 55296 /* 0xD800 */) || + (57344 /* 0xE000 */ <= n && n < 1114112 /* 0x11_0000 */ ) +} +#else +function {:inline} char#IsChar(n: int): bool { + 0 <= n && n < 65536 +} +#endif + +type char; +function char#FromInt(int): char; +axiom (forall n: int :: + { char#FromInt(n) } + char#IsChar(n) ==> char#ToInt(char#FromInt(n)) == n); + +function char#ToInt(char): int; +axiom (forall ch: char :: + { char#ToInt(ch) } + char#FromInt(char#ToInt(ch)) == ch && + char#IsChar(char#ToInt(ch))); + +function char#Plus(char, char): char; +axiom (forall a: char, b: char :: + { char#Plus(a, b) } + char#Plus(a, b) == char#FromInt(char#ToInt(a) + char#ToInt(b))); + +function char#Minus(char, char): char; +axiom (forall a: char, b: char :: + { char#Minus(a, b) } + char#Minus(a, b) == char#FromInt(char#ToInt(a) - char#ToInt(b))); + +// --------------------------------------------------------------- +// -- References ------------------------------------------------- +// --------------------------------------------------------------- + +type ref; +const null: ref; + +// --------------------------------------------------------------- +// -- Boxing and unboxing ---------------------------------------- +// --------------------------------------------------------------- + +type Box; +const $ArbitraryBoxValue: Box; + +function $Box(T): Box; +function $Unbox(Box): T; +axiom (forall x : T :: { $Box(x) } $Unbox($Box(x)) == x); +axiom (forall x : Box :: { $Unbox(x): T} $Box($Unbox(x): T) == x); + + +// Corresponding entries for boxes... +// This could probably be solved by having Box also inhabit Ty +function $IsBox(Box,Ty): bool; +function $IsAllocBox(Box,Ty,Heap): bool; + +axiom (forall bx : Box :: + { $IsBox(bx, TInt) } + ( $IsBox(bx, TInt) ==> $Box($Unbox(bx) : int) == bx && $Is($Unbox(bx) : int, TInt))); +axiom (forall bx : Box :: + { $IsBox(bx, TReal) } + ( $IsBox(bx, TReal) ==> $Box($Unbox(bx) : real) == bx && $Is($Unbox(bx) : real, TReal))); +axiom (forall bx : Box :: + { $IsBox(bx, TBool) } + ( $IsBox(bx, TBool) ==> $Box($Unbox(bx) : bool) == bx && $Is($Unbox(bx) : bool, TBool))); +axiom (forall bx : Box :: + { $IsBox(bx, TChar) } + ( $IsBox(bx, TChar) ==> $Box($Unbox(bx) : char) == bx && $Is($Unbox(bx) : char, TChar))); + +// Since each bitvector type is a separate type in Boogie, the Box/Unbox axioms for bitvectors are +// generated programmatically. Except, Bv0 is given here. +axiom (forall bx : Box :: + { $IsBox(bx, TBitvector(0)) } + ( $IsBox(bx, TBitvector(0)) ==> $Box($Unbox(bx) : Bv0) == bx && $Is($Unbox(bx) : Bv0, TBitvector(0)))); + +axiom (forall bx : Box, t : Ty :: + { $IsBox(bx, TSet(t)) } + ( $IsBox(bx, TSet(t)) ==> $Box($Unbox(bx) : Set) == bx && $Is($Unbox(bx) : Set, TSet(t)))); +axiom (forall bx : Box, t : Ty :: + { $IsBox(bx, TISet(t)) } + ( $IsBox(bx, TISet(t)) ==> $Box($Unbox(bx) : ISet) == bx && $Is($Unbox(bx) : ISet, TISet(t)))); +axiom (forall bx : Box, t : Ty :: + { $IsBox(bx, TMultiSet(t)) } + ( $IsBox(bx, TMultiSet(t)) ==> $Box($Unbox(bx) : MultiSet) == bx && $Is($Unbox(bx) : MultiSet, TMultiSet(t)))); +axiom (forall bx : Box, t : Ty :: + { $IsBox(bx, TSeq(t)) } + ( $IsBox(bx, TSeq(t)) ==> $Box($Unbox(bx) : Seq) == bx && $Is($Unbox(bx) : Seq, TSeq(t)))); +axiom (forall bx : Box, s : Ty, t : Ty :: + { $IsBox(bx, TMap(s, t)) } + ( $IsBox(bx, TMap(s, t)) ==> $Box($Unbox(bx) : Map) == bx && $Is($Unbox(bx) : Map, TMap(s, t)))); +axiom (forall bx : Box, s : Ty, t : Ty :: + { $IsBox(bx, TIMap(s, t)) } + ( $IsBox(bx, TIMap(s, t)) ==> $Box($Unbox(bx) : IMap) == bx && $Is($Unbox(bx) : IMap, TIMap(s, t)))); + +axiom (forall v : T, t : Ty :: + { $IsBox($Box(v), t) } + ( $IsBox($Box(v), t) <==> $Is(v,t) )); +axiom (forall v : T, t : Ty, h : Heap :: + { $IsAllocBox($Box(v), t, h) } + ( $IsAllocBox($Box(v), t, h) <==> $IsAlloc(v,t,h) )); + +// --------------------------------------------------------------- +// -- Is and IsAlloc --------------------------------------------- +// --------------------------------------------------------------- + +// Type-argument to $Is is the /representation type/, +// the second value argument to $Is is the actual type. +function $Is(T,Ty): bool; // no heap for now +axiom(forall v : int :: { $Is(v,TInt) } $Is(v,TInt)); +axiom(forall v : real :: { $Is(v,TReal) } $Is(v,TReal)); +axiom(forall v : bool :: { $Is(v,TBool) } $Is(v,TBool)); +axiom(forall v : char :: { $Is(v,TChar) } $Is(v,TChar)); +axiom(forall v : ORDINAL :: { $Is(v,TORDINAL) } $Is(v,TORDINAL)); + +// Since every bitvector type is a separate type in Boogie, the $Is/$IsAlloc axioms +// for bitvectors are generated programatically. Except, TBitvector(0) is given here. +axiom (forall v: Bv0 :: { $Is(v, TBitvector(0)) } $Is(v, TBitvector(0))); + +axiom (forall v: Set, t0: Ty :: { $Is(v, TSet(t0)) } + $Is(v, TSet(t0)) <==> + (forall bx: Box :: { v[bx] } + v[bx] ==> $IsBox(bx, t0))); +axiom (forall v: ISet, t0: Ty :: { $Is(v, TISet(t0)) } + $Is(v, TISet(t0)) <==> + (forall bx: Box :: { v[bx] } + v[bx] ==> $IsBox(bx, t0))); +axiom (forall v: MultiSet, t0: Ty :: { $Is(v, TMultiSet(t0)) } + $Is(v, TMultiSet(t0)) <==> + (forall bx: Box :: { v[bx] } + 0 < v[bx] ==> $IsBox(bx, t0))); +axiom (forall v: MultiSet, t0: Ty :: { $Is(v, TMultiSet(t0)) } + $Is(v, TMultiSet(t0)) ==> $IsGoodMultiSet(v)); +axiom (forall v: Seq, t0: Ty :: { $Is(v, TSeq(t0)) } + $Is(v, TSeq(t0)) <==> + (forall i : int :: { Seq#Index(v, i) } + 0 <= i && i < Seq#Length(v) ==> + $IsBox(Seq#Index(v, i), t0))); + +axiom (forall v: Map, t0: Ty, t1: Ty :: + { $Is(v, TMap(t0, t1)) } + $Is(v, TMap(t0, t1)) + <==> (forall bx: Box :: + { Map#Elements(v)[bx] } { Map#Domain(v)[bx] } + Map#Domain(v)[bx] ==> + $IsBox(Map#Elements(v)[bx], t1) && + $IsBox(bx, t0))); + +axiom (forall v: Map, t0: Ty, t1: Ty :: + { $Is(v, TMap(t0, t1)) } + $Is(v, TMap(t0, t1)) ==> + $Is(Map#Domain(v), TSet(t0)) && + $Is(Map#Values(v), TSet(t1)) && + $Is(Map#Items(v), TSet(Tclass._System.Tuple2(t0, t1)))); +axiom (forall v: IMap, t0: Ty, t1: Ty :: + { $Is(v, TIMap(t0, t1)) } + $Is(v, TIMap(t0, t1)) + <==> (forall bx: Box :: + { IMap#Elements(v)[bx] } { IMap#Domain(v)[bx] } + IMap#Domain(v)[bx] ==> + $IsBox(IMap#Elements(v)[bx], t1) && + $IsBox(bx, t0))); +axiom (forall v: IMap, t0: Ty, t1: Ty :: + { $Is(v, TIMap(t0, t1)) } + $Is(v, TIMap(t0, t1)) ==> + $Is(IMap#Domain(v), TISet(t0)) && + $Is(IMap#Values(v), TISet(t1)) && + $Is(IMap#Items(v), TISet(Tclass._System.Tuple2(t0, t1)))); + +function $IsAlloc(T,Ty,Heap): bool; +axiom(forall h : Heap, v : int :: { $IsAlloc(v,TInt,h) } $IsAlloc(v,TInt,h)); +axiom(forall h : Heap, v : real :: { $IsAlloc(v,TReal,h) } $IsAlloc(v,TReal,h)); +axiom(forall h : Heap, v : bool :: { $IsAlloc(v,TBool,h) } $IsAlloc(v,TBool,h)); +axiom(forall h : Heap, v : char :: { $IsAlloc(v,TChar,h) } $IsAlloc(v,TChar,h)); +axiom(forall h : Heap, v : ORDINAL :: { $IsAlloc(v,TORDINAL,h) } $IsAlloc(v,TORDINAL,h)); + +axiom (forall v: Bv0, h: Heap :: { $IsAlloc(v, TBitvector(0), h) } $IsAlloc(v, TBitvector(0), h)); + +axiom (forall v: Set, t0: Ty, h: Heap :: { $IsAlloc(v, TSet(t0), h) } + $IsAlloc(v, TSet(t0), h) <==> + (forall bx: Box :: { v[bx] } + v[bx] ==> $IsAllocBox(bx, t0, h))); +axiom (forall v: ISet, t0: Ty, h: Heap :: { $IsAlloc(v, TISet(t0), h) } + $IsAlloc(v, TISet(t0), h) <==> + (forall bx: Box :: { v[bx] } + v[bx] ==> $IsAllocBox(bx, t0, h))); +axiom (forall v: MultiSet, t0: Ty, h: Heap :: { $IsAlloc(v, TMultiSet(t0), h) } + $IsAlloc(v, TMultiSet(t0), h) <==> + (forall bx: Box :: { v[bx] } + 0 < v[bx] ==> $IsAllocBox(bx, t0, h))); +axiom (forall v: Seq, t0: Ty, h: Heap :: { $IsAlloc(v, TSeq(t0), h) } + $IsAlloc(v, TSeq(t0), h) <==> + (forall i : int :: { Seq#Index(v, i) } + 0 <= i && i < Seq#Length(v) ==> + $IsAllocBox(Seq#Index(v, i), t0, h))); + +axiom (forall v: Map, t0: Ty, t1: Ty, h: Heap :: + { $IsAlloc(v, TMap(t0, t1), h) } + $IsAlloc(v, TMap(t0, t1), h) + <==> (forall bx: Box :: + { Map#Elements(v)[bx] } { Map#Domain(v)[bx] } + Map#Domain(v)[bx] ==> + $IsAllocBox(Map#Elements(v)[bx], t1, h) && + $IsAllocBox(bx, t0, h))); + +axiom (forall v: IMap, t0: Ty, t1: Ty, h: Heap :: + { $IsAlloc(v, TIMap(t0, t1), h) } + $IsAlloc(v, TIMap(t0, t1), h) + <==> (forall bx: Box :: + { IMap#Elements(v)[bx] } { IMap#Domain(v)[bx] } + IMap#Domain(v)[bx] ==> + $IsAllocBox(IMap#Elements(v)[bx], t1, h) && + $IsAllocBox(bx, t0, h))); + + +function $AlwaysAllocated(Ty): bool; + axiom (forall ty: Ty :: { $AlwaysAllocated(ty) } + $AlwaysAllocated(ty) ==> + (forall h: Heap, v: Box :: { $IsAllocBox(v, ty, h) } $IsBox(v, ty) ==> $IsAllocBox(v, ty, h))); + +function $OlderTag(Heap): bool; + +// --------------------------------------------------------------- +// -- Encoding of type names ------------------------------------- +// --------------------------------------------------------------- + +type ClassName; +const unique class._System.int: ClassName; +const unique class._System.bool: ClassName; +const unique class._System.set: ClassName; +const unique class._System.seq: ClassName; +const unique class._System.multiset: ClassName; + +function Tclass._System.object?(): Ty; +function Tclass._System.Tuple2(Ty, Ty): Ty; + +function /*{:never_pattern true}*/ dtype(ref): Ty; // changed from ClassName to Ty + +function TypeTuple(a: ClassName, b: ClassName): ClassName; +function TypeTupleCar(ClassName): ClassName; +function TypeTupleCdr(ClassName): ClassName; +// TypeTuple is injective in both arguments: +axiom (forall a: ClassName, b: ClassName :: { TypeTuple(a,b) } + TypeTupleCar(TypeTuple(a,b)) == a && + TypeTupleCdr(TypeTuple(a,b)) == b); + +// -- Function handles ------------------------------------------- + +type HandleType; + +function SetRef_to_SetBox(s: [ref]bool): Set; +axiom (forall s: [ref]bool, bx: Box :: { SetRef_to_SetBox(s)[bx] } + SetRef_to_SetBox(s)[bx] == s[$Unbox(bx): ref]); +axiom (forall s: [ref]bool :: { SetRef_to_SetBox(s) } + $Is(SetRef_to_SetBox(s), TSet(Tclass._System.object?()))); + +// Functions ApplyN, RequiresN, and ReadsN are generated on demand by the translator, +// but Apply1 is referred to in the prelude, so its definition is hardcoded here. +function Apply1(Ty, Ty, Heap, HandleType, Box): Box; + +// --------------------------------------------------------------- +// -- Datatypes -------------------------------------------------- +// --------------------------------------------------------------- + +type DatatypeType; + +type DtCtorId; +function DatatypeCtorId(DatatypeType): DtCtorId; + +function DtRank(DatatypeType): int; +function BoxRank(Box): int; + +axiom (forall d: DatatypeType :: {BoxRank($Box(d))} BoxRank($Box(d)) == DtRank(d)); + +// --------------------------------------------------------------- +// -- Big Ordinals ----------------------------------------------- +// --------------------------------------------------------------- + +type ORDINAL = Box; // :| There are more big ordinals than boxes + +// The following two functions give an abstracton over all ordinals. +// Function ORD#IsNat returns true when the ordinal is one of the natural +// numbers. Function ORD#Offset gives how many successors (that is, +// +1 operations) an ordinal is above the nearest lower limit ordinal. +// That is, if the ordinal is \lambda+n, then ORD#Offset returns n. +function ORD#IsNat(ORDINAL): bool; +function ORD#Offset(ORDINAL): int; +axiom (forall o:ORDINAL :: { ORD#Offset(o) } 0 <= ORD#Offset(o)); + +function {:inline} ORD#IsLimit(o: ORDINAL): bool { ORD#Offset(o) == 0 } +function {:inline} ORD#IsSucc(o: ORDINAL): bool { 0 < ORD#Offset(o) } + +function ORD#FromNat(int): ORDINAL; +axiom (forall n:int :: { ORD#FromNat(n) } + 0 <= n ==> ORD#IsNat(ORD#FromNat(n)) && ORD#Offset(ORD#FromNat(n)) == n); +axiom (forall o:ORDINAL :: { ORD#Offset(o) } { ORD#IsNat(o) } + ORD#IsNat(o) ==> o == ORD#FromNat(ORD#Offset(o))); + +function ORD#Less(ORDINAL, ORDINAL): bool; +axiom (forall o,p: ORDINAL :: { ORD#Less(o,p) } + (ORD#Less(o,p) ==> o != p) && // irreflexivity + (ORD#IsNat(o) && !ORD#IsNat(p) ==> ORD#Less(o,p)) && + (ORD#IsNat(o) && ORD#IsNat(p) ==> ORD#Less(o,p) == (ORD#Offset(o) < ORD#Offset(p))) && + (ORD#Less(o,p) && ORD#IsNat(p) ==> ORD#IsNat(o))); +// ORD#Less is trichotomous: +axiom (forall o,p: ORDINAL :: { ORD#Less(o,p), ORD#Less(p,o) } + ORD#Less(o,p) || o == p || ORD#Less(p,o)); +// ORD#Less is transitive: +axiom (forall o,p,r: ORDINAL :: + { ORD#Less(o,p), ORD#Less(p,r) } + { ORD#Less(o,p), ORD#Less(o,r) } + ORD#Less(o,p) && ORD#Less(p,r) ==> ORD#Less(o,r)); + +// ORD#LessThanLimit is a synonym of ORD#Less, introduced for more selected triggering +function ORD#LessThanLimit(ORDINAL, ORDINAL): bool; +axiom (forall o,p: ORDINAL :: { ORD#LessThanLimit(o, p) } + ORD#LessThanLimit(o, p) == ORD#Less(o, p)); + +function ORD#Plus(ORDINAL, ORDINAL): ORDINAL; +axiom (forall o,p: ORDINAL :: { ORD#Plus(o,p) } + (ORD#IsNat(ORD#Plus(o,p)) ==> ORD#IsNat(o) && ORD#IsNat(p)) && + (ORD#IsNat(p) ==> + ORD#IsNat(ORD#Plus(o,p)) == ORD#IsNat(o) && + ORD#Offset(ORD#Plus(o,p)) == ORD#Offset(o) + ORD#Offset(p))); +axiom (forall o,p: ORDINAL :: { ORD#Plus(o,p) } + (o == ORD#Plus(o, p) || ORD#Less(o, ORD#Plus(o, p))) && + (p == ORD#Plus(o, p) || ORD#Less(p, ORD#Plus(o, p)))); +axiom (forall o,p: ORDINAL :: { ORD#Plus(o,p) } + (o == ORD#FromNat(0) ==> ORD#Plus(o, p) == p) && + (p == ORD#FromNat(0) ==> ORD#Plus(o, p) == o)); + +function ORD#Minus(ORDINAL, ORDINAL): ORDINAL; +axiom (forall o,p: ORDINAL :: { ORD#Minus(o,p) } + ORD#IsNat(p) && ORD#Offset(p) <= ORD#Offset(o) ==> + ORD#IsNat(ORD#Minus(o,p)) == ORD#IsNat(o) && + ORD#Offset(ORD#Minus(o,p)) == ORD#Offset(o) - ORD#Offset(p)); +axiom (forall o,p: ORDINAL :: { ORD#Minus(o,p) } + ORD#IsNat(p) && ORD#Offset(p) <= ORD#Offset(o) ==> + (p == ORD#FromNat(0) && ORD#Minus(o, p) == o) || + (p != ORD#FromNat(0) && ORD#Less(ORD#Minus(o, p), o))); + +// o+m+n == o+(m+n) +axiom (forall o: ORDINAL, m,n: int :: + { ORD#Plus(ORD#Plus(o, ORD#FromNat(m)), ORD#FromNat(n)) } + 0 <= m && 0 <= n ==> + ORD#Plus(ORD#Plus(o, ORD#FromNat(m)), ORD#FromNat(n)) == ORD#Plus(o, ORD#FromNat(m+n))); +// o-m-n == o+(m+n) +axiom (forall o: ORDINAL, m,n: int :: + { ORD#Minus(ORD#Minus(o, ORD#FromNat(m)), ORD#FromNat(n)) } + 0 <= m && 0 <= n && m+n <= ORD#Offset(o) ==> + ORD#Minus(ORD#Minus(o, ORD#FromNat(m)), ORD#FromNat(n)) == ORD#Minus(o, ORD#FromNat(m+n))); +// o+m-n == EITHER o+(m-n) OR o-(n-m) +axiom (forall o: ORDINAL, m,n: int :: + { ORD#Minus(ORD#Plus(o, ORD#FromNat(m)), ORD#FromNat(n)) } + 0 <= m && 0 <= n && n <= ORD#Offset(o) + m ==> + (0 <= m - n ==> ORD#Minus(ORD#Plus(o, ORD#FromNat(m)), ORD#FromNat(n)) == ORD#Plus(o, ORD#FromNat(m-n))) && + (m - n <= 0 ==> ORD#Minus(ORD#Plus(o, ORD#FromNat(m)), ORD#FromNat(n)) == ORD#Minus(o, ORD#FromNat(n-m)))); +// o-m+n == EITHER o-(m-n) OR o+(n-m) +axiom (forall o: ORDINAL, m,n: int :: + { ORD#Plus(ORD#Minus(o, ORD#FromNat(m)), ORD#FromNat(n)) } + 0 <= m && 0 <= n && n <= ORD#Offset(o) + m ==> + (0 <= m - n ==> ORD#Plus(ORD#Minus(o, ORD#FromNat(m)), ORD#FromNat(n)) == ORD#Minus(o, ORD#FromNat(m-n))) && + (m - n <= 0 ==> ORD#Plus(ORD#Minus(o, ORD#FromNat(m)), ORD#FromNat(n)) == ORD#Plus(o, ORD#FromNat(n-m)))); + +// --------------------------------------------------------------- +// -- Axiom contexts --------------------------------------------- +// --------------------------------------------------------------- + +// used to make sure function axioms are not used while their consistency is being checked +const $ModuleContextHeight: int; +const $FunctionContextHeight: int; + +// --------------------------------------------------------------- +// -- Layers of function encodings ------------------------------- +// --------------------------------------------------------------- + +type LayerType; +const $LZ: LayerType; +function $LS(LayerType): LayerType; +function AsFuelBottom(LayerType) : LayerType; + +function AtLayer([LayerType]A, LayerType): A; +axiom (forall f : [LayerType]A, ly : LayerType :: { AtLayer(f,ly) } AtLayer(f,ly) == f[ly]); +axiom (forall f : [LayerType]A, ly : LayerType :: { AtLayer(f,$LS(ly)) } AtLayer(f,$LS(ly)) == AtLayer(f,ly)); + +// --------------------------------------------------------------- +// -- Fields ----------------------------------------------------- +// --------------------------------------------------------------- + +type Field; + +function FDim(Field): int uses { + axiom FDim(alloc) == 0; +} + +function IndexField(int): Field; +axiom (forall i: int :: { IndexField(i) } FDim(IndexField(i)) == 1); +function IndexField_Inverse(Field): int; +axiom (forall i: int :: { IndexField(i) } IndexField_Inverse(IndexField(i)) == i); + +function MultiIndexField(Field, int): Field; +axiom (forall f: Field, i: int :: { MultiIndexField(f,i) } FDim(MultiIndexField(f,i)) == FDim(f) + 1); +function MultiIndexField_Inverse0(Field): Field; +function MultiIndexField_Inverse1(Field): int; +axiom (forall f: Field, i: int :: { MultiIndexField(f,i) } + MultiIndexField_Inverse0(MultiIndexField(f,i)) == f && + MultiIndexField_Inverse1(MultiIndexField(f,i)) == i); + +function DeclType(Field): ClassName; + +type NameFamily; +function DeclName(Field): NameFamily uses { + axiom DeclName(alloc) == allocName; +} +function FieldOfDecl(ClassName, NameFamily): Field; +axiom (forall cl : ClassName, nm: NameFamily :: + {FieldOfDecl(cl, nm): Field} + DeclType(FieldOfDecl(cl, nm): Field) == cl && DeclName(FieldOfDecl(cl, nm): Field) == nm); + +function $IsGhostField(Field): bool uses { + axiom $IsGhostField(alloc); // treat as ghost field, since it is allowed to be changed by ghost code +} +axiom (forall h: Heap, k: Heap :: { $HeapSuccGhost(h,k) } + $HeapSuccGhost(h,k) ==> + $HeapSucc(h,k) && + (forall o: ref, f: Field :: { read(k, o, f) } + !$IsGhostField(f) ==> read(h, o, f) == read(k, o, f))); + +// --------------------------------------------------------------- +// -- Allocatedness and Heap Succession -------------------------- +// --------------------------------------------------------------- + + +// $IsAlloc and $IsAllocBox are monotonic + +axiom (forall h, k : Heap, v : T, t : Ty :: + { $HeapSucc(h, k), $IsAlloc(v, t, h) } + $HeapSucc(h, k) ==> $IsAlloc(v, t, h) ==> $IsAlloc(v, t, k)); +axiom (forall h, k : Heap, bx : Box, t : Ty :: + { $HeapSucc(h, k), $IsAllocBox(bx, t, h) } + $HeapSucc(h, k) ==> $IsAllocBox(bx, t, h) ==> $IsAllocBox(bx, t, k)); + +// No axioms for $Is and $IsBox since they don't talk about the heap. + +const unique alloc: Field; +const unique allocName: NameFamily; + +// --------------------------------------------------------------- +// -- Arrays ----------------------------------------------------- +// --------------------------------------------------------------- + +function _System.array.Length(a: ref): int; +axiom (forall o: ref :: {_System.array.Length(o)} 0 <= _System.array.Length(o)); + + +// --------------------------------------------------------------- +// -- Reals ------------------------------------------------------ +// --------------------------------------------------------------- + +function Int(x: real): int { int(x) } +function Real(x: int): real { real(x) } +axiom (forall i: int :: { Int(Real(i)) } Int(Real(i)) == i); + +function {:inline} _System.real.Floor(x: real): int { Int(x) } + +// --------------------------------------------------------------- +// -- The heap --------------------------------------------------- +// --------------------------------------------------------------- +type Heap = [ref][Field]Box; +function {:inline} read(H: Heap, r: ref, f: Field) : Box { H[r][f] } +function {:inline} update(H:Heap, r:ref, f: Field, v: Box) : Heap { H[r := H[r][f := v]] } + +function $IsGoodHeap(Heap): bool; +function $IsHeapAnchor(Heap): bool; +var $Heap: Heap where $IsGoodHeap($Heap) && $IsHeapAnchor($Heap); + +// The following is used as a reference heap in places where the translation needs a heap +// but the expression generated is really one that is (at least in a correct program) +// independent of the heap. +const $OneHeap: Heap uses { + axiom $IsGoodHeap($OneHeap); +} + +function $HeapSucc(Heap, Heap): bool; +axiom (forall h: Heap, r: ref, f: Field, x: Box :: { update(h, r, f, x) } + $IsGoodHeap(update(h, r, f, x)) ==> + $HeapSucc(h, update(h, r, f, x))); +axiom (forall a,b,c: Heap :: { $HeapSucc(a,b), $HeapSucc(b,c) } + a != c ==> $HeapSucc(a,b) && $HeapSucc(b,c) ==> $HeapSucc(a,c)); +axiom (forall h: Heap, k: Heap :: { $HeapSucc(h,k) } + $HeapSucc(h,k) ==> (forall o: ref :: { read(k, o, alloc) } $Unbox(read(h, o, alloc)) ==> $Unbox(read(k, o, alloc)))); + +function $HeapSuccGhost(Heap, Heap): bool; + +// --------------------------------------------------------------- +// -- Useful macros ---------------------------------------------- +// --------------------------------------------------------------- + +// havoc everything in $Heap, except {this}+rds+nw +procedure $YieldHavoc(this: ref, rds: Set, nw: Set); + modifies $Heap; + ensures (forall $o: ref, $f: Field :: { read($Heap, $o, $f) } + $o != null && $Unbox(read(old($Heap), $o, alloc)) ==> + $o == this || rds[$Box($o)] || nw[$Box($o)] ==> + read($Heap, $o, $f) == read(old($Heap), $o, $f)); + ensures $HeapSucc(old($Heap), $Heap); + +// havoc everything in $Heap, except rds-modi-{this} +procedure $IterHavoc0(this: ref, rds: Set, modi: Set); + modifies $Heap; + ensures (forall $o: ref, $f: Field :: { read($Heap, $o, $f) } + $o != null && $Unbox(read(old($Heap), $o, alloc)) ==> + rds[$Box($o)] && !modi[$Box($o)] && $o != this ==> + read($Heap, $o, $f) == read(old($Heap), $o, $f)); + ensures $HeapSucc(old($Heap), $Heap); + +// havoc $Heap at {this}+modi+nw +procedure $IterHavoc1(this: ref, modi: Set, nw: Set); + modifies $Heap; + ensures (forall $o: ref, $f: Field :: { read($Heap, $o, $f) } + $o != null && $Unbox(read(old($Heap), $o, alloc)) ==> + read($Heap, $o, $f) == read(old($Heap), $o, $f) || + $o == this || modi[$Box($o)] || nw[$Box($o)]); + ensures $HeapSucc(old($Heap), $Heap); + +procedure $IterCollectNewObjects(prevHeap: Heap, newHeap: Heap, this: ref, NW: Field) + returns (s: Set); + ensures (forall bx: Box :: { s[bx] } s[bx] <==> + ($Unbox(read(newHeap, this, NW)) : Set)[bx] || + ($Unbox(bx) != null && !$Unbox(read(prevHeap, $Unbox(bx):ref, alloc)) && $Unbox(read(newHeap, $Unbox(bx):ref, alloc)))); + +// --------------------------------------------------------------- +// -- Axiomatizations -------------------------------------------- +// --------------------------------------------------------------- + +// --------------------------------------------------------------- +// -- Axiomatization of sets ------------------------------------- +// --------------------------------------------------------------- + +type Set = [Box]bool; + +function Set#Card(Set): int; +axiom (forall s: Set :: { Set#Card(s) } 0 <= Set#Card(s)); + +function Set#Empty(): Set; +axiom (forall o: Box :: { Set#Empty()[o] } !Set#Empty()[o]); +axiom (forall s: Set :: { Set#Card(s) } + (Set#Card(s) == 0 <==> s == Set#Empty()) && + (Set#Card(s) != 0 ==> (exists x: Box :: s[x]))); + +// the empty set could be of anything +//axiom (forall t: Ty :: { $Is(Set#Empty() : [Box]bool, TSet(t)) } $Is(Set#Empty() : [Box]bool, TSet(t))); + +function Set#Singleton(Box): Set; +axiom (forall r: Box :: { Set#Singleton(r) } Set#Singleton(r)[r]); +axiom (forall r: Box, o: Box :: { Set#Singleton(r)[o] } Set#Singleton(r)[o] <==> r == o); +axiom (forall r: Box :: { Set#Card(Set#Singleton(r)) } Set#Card(Set#Singleton(r)) == 1); + +function Set#UnionOne(Set, Box): Set; +axiom (forall a: Set, x: Box, o: Box :: { Set#UnionOne(a,x)[o] } + Set#UnionOne(a,x)[o] <==> o == x || a[o]); +axiom (forall a: Set, x: Box :: { Set#UnionOne(a, x) } + Set#UnionOne(a, x)[x]); +axiom (forall a: Set, x: Box, y: Box :: { Set#UnionOne(a, x), a[y] } + a[y] ==> Set#UnionOne(a, x)[y]); +axiom (forall a: Set, x: Box :: { Set#Card(Set#UnionOne(a, x)) } + a[x] ==> Set#Card(Set#UnionOne(a, x)) == Set#Card(a)); +axiom (forall a: Set, x: Box :: { Set#Card(Set#UnionOne(a, x)) } + !a[x] ==> Set#Card(Set#UnionOne(a, x)) == Set#Card(a) + 1); + +function Set#Union(Set, Set): Set; +axiom (forall a: Set, b: Set, o: Box :: { Set#Union(a,b)[o] } + Set#Union(a,b)[o] <==> a[o] || b[o]); +axiom (forall a, b: Set, y: Box :: { Set#Union(a, b), a[y] } + a[y] ==> Set#Union(a, b)[y]); +axiom (forall a, b: Set, y: Box :: { Set#Union(a, b), b[y] } + b[y] ==> Set#Union(a, b)[y]); +axiom (forall a, b: Set :: { Set#Union(a, b) } + Set#Disjoint(a, b) ==> + Set#Difference(Set#Union(a, b), a) == b && + Set#Difference(Set#Union(a, b), b) == a); +// Follows from the general union axiom, but might be still worth including, because disjoint union is a common case: +// axiom (forall a, b: Set :: { Set#Card(Set#Union(a, b)) } +// Set#Disjoint(a, b) ==> +// Set#Card(Set#Union(a, b)) == Set#Card(a) + Set#Card(b)); + +function Set#Intersection(Set, Set): Set; +axiom (forall a: Set, b: Set, o: Box :: { Set#Intersection(a,b)[o] } + Set#Intersection(a,b)[o] <==> a[o] && b[o]); + +axiom (forall a, b: Set :: { Set#Union(Set#Union(a, b), b) } + Set#Union(Set#Union(a, b), b) == Set#Union(a, b)); +axiom (forall a, b: Set :: { Set#Union(a, Set#Union(a, b)) } + Set#Union(a, Set#Union(a, b)) == Set#Union(a, b)); +axiom (forall a, b: Set :: { Set#Intersection(Set#Intersection(a, b), b) } + Set#Intersection(Set#Intersection(a, b), b) == Set#Intersection(a, b)); +axiom (forall a, b: Set :: { Set#Intersection(a, Set#Intersection(a, b)) } + Set#Intersection(a, Set#Intersection(a, b)) == Set#Intersection(a, b)); +axiom (forall a, b: Set :: { Set#Card(Set#Union(a, b)) }{ Set#Card(Set#Intersection(a, b)) } + Set#Card(Set#Union(a, b)) + Set#Card(Set#Intersection(a, b)) == Set#Card(a) + Set#Card(b)); + +function Set#Difference(Set, Set): Set; +axiom (forall a: Set, b: Set, o: Box :: { Set#Difference(a,b)[o] } + Set#Difference(a,b)[o] <==> a[o] && !b[o]); +axiom (forall a, b: Set, y: Box :: { Set#Difference(a, b), b[y] } + b[y] ==> !Set#Difference(a, b)[y] ); +axiom (forall a, b: Set :: + { Set#Card(Set#Difference(a, b)) } + Set#Card(Set#Difference(a, b)) + Set#Card(Set#Difference(b, a)) + + Set#Card(Set#Intersection(a, b)) + == Set#Card(Set#Union(a, b)) && + Set#Card(Set#Difference(a, b)) == Set#Card(a) - Set#Card(Set#Intersection(a, b))); + +function Set#Subset(Set, Set): bool; +axiom (forall a: Set, b: Set :: { Set#Subset(a,b) } + Set#Subset(a,b) <==> (forall o: Box :: {a[o]} {b[o]} a[o] ==> b[o])); +// axiom(forall a: Set, b: Set :: +// { Set#Subset(a,b), Set#Card(a), Set#Card(b) } // very restrictive trigger +// Set#Subset(a,b) ==> Set#Card(a) <= Set#Card(b)); + + +function Set#Equal(Set, Set): bool; +axiom (forall a: Set, b: Set :: { Set#Equal(a,b) } + Set#Equal(a,b) <==> (forall o: Box :: {a[o]} {b[o]} a[o] <==> b[o])); +axiom (forall a: Set, b: Set :: { Set#Equal(a,b) } // extensionality axiom for sets + Set#Equal(a,b) ==> a == b); + +function Set#Disjoint(Set, Set): bool; +axiom (forall a: Set, b: Set :: { Set#Disjoint(a,b) } + Set#Disjoint(a,b) <==> (forall o: Box :: {a[o]} {b[o]} !a[o] || !b[o])); + +// --------------------------------------------------------------- +// -- Axiomatization of isets ------------------------------------- +// --------------------------------------------------------------- + +type ISet = [Box]bool; + +function ISet#Empty(): Set; +axiom (forall o: Box :: { ISet#Empty()[o] } !ISet#Empty()[o]); + +// the empty set could be of anything +//axiom (forall t: Ty :: { $Is(ISet#Empty() : [Box]bool, TISet(t)) } $Is(ISet#Empty() : [Box]bool, TISet(t))); + + +function ISet#UnionOne(ISet, Box): ISet; +axiom (forall a: ISet, x: Box, o: Box :: { ISet#UnionOne(a,x)[o] } + ISet#UnionOne(a,x)[o] <==> o == x || a[o]); +axiom (forall a: ISet, x: Box :: { ISet#UnionOne(a, x) } + ISet#UnionOne(a, x)[x]); +axiom (forall a: ISet, x: Box, y: Box :: { ISet#UnionOne(a, x), a[y] } + a[y] ==> ISet#UnionOne(a, x)[y]); + +function ISet#Union(ISet, ISet): ISet; +axiom (forall a: ISet, b: ISet, o: Box :: { ISet#Union(a,b)[o] } + ISet#Union(a,b)[o] <==> a[o] || b[o]); +axiom (forall a, b: ISet, y: Box :: { ISet#Union(a, b), a[y] } + a[y] ==> ISet#Union(a, b)[y]); +axiom (forall a, b: Set, y: Box :: { ISet#Union(a, b), b[y] } + b[y] ==> ISet#Union(a, b)[y]); +axiom (forall a, b: ISet :: { ISet#Union(a, b) } + ISet#Disjoint(a, b) ==> + ISet#Difference(ISet#Union(a, b), a) == b && + ISet#Difference(ISet#Union(a, b), b) == a); + +function ISet#Intersection(ISet, ISet): ISet; +axiom (forall a: ISet, b: ISet, o: Box :: { ISet#Intersection(a,b)[o] } + ISet#Intersection(a,b)[o] <==> a[o] && b[o]); + +axiom (forall a, b: ISet :: { ISet#Union(ISet#Union(a, b), b) } + ISet#Union(ISet#Union(a, b), b) == ISet#Union(a, b)); +axiom (forall a, b: Set :: { ISet#Union(a, ISet#Union(a, b)) } + ISet#Union(a, ISet#Union(a, b)) == ISet#Union(a, b)); +axiom (forall a, b: ISet :: { ISet#Intersection(ISet#Intersection(a, b), b) } + ISet#Intersection(ISet#Intersection(a, b), b) == ISet#Intersection(a, b)); +axiom (forall a, b: ISet :: { ISet#Intersection(a, ISet#Intersection(a, b)) } + ISet#Intersection(a, ISet#Intersection(a, b)) == ISet#Intersection(a, b)); + + +function ISet#Difference(ISet, ISet): ISet; +axiom (forall a: ISet, b: ISet, o: Box :: { ISet#Difference(a,b)[o] } + ISet#Difference(a,b)[o] <==> a[o] && !b[o]); +axiom (forall a, b: ISet, y: Box :: { ISet#Difference(a, b), b[y] } + b[y] ==> !ISet#Difference(a, b)[y] ); + +function ISet#Subset(ISet, ISet): bool; +axiom (forall a: ISet, b: ISet :: { ISet#Subset(a,b) } + ISet#Subset(a,b) <==> (forall o: Box :: {a[o]} {b[o]} a[o] ==> b[o])); + +function ISet#Equal(ISet, ISet): bool; +axiom (forall a: ISet, b: ISet :: { ISet#Equal(a,b) } + ISet#Equal(a,b) <==> (forall o: Box :: {a[o]} {b[o]} a[o] <==> b[o])); +axiom (forall a: ISet, b: ISet :: { ISet#Equal(a,b) } // extensionality axiom for sets + ISet#Equal(a,b) ==> a == b); + +function ISet#Disjoint(ISet, ISet): bool; +axiom (forall a: ISet, b: ISet :: { ISet#Disjoint(a,b) } + ISet#Disjoint(a,b) <==> (forall o: Box :: {a[o]} {b[o]} !a[o] || !b[o])); + +// --------------------------------------------------------------- +// -- Axiomatization of multisets -------------------------------- +// --------------------------------------------------------------- + +function Math#min(a: int, b: int): int; +axiom (forall a: int, b: int :: { Math#min(a, b) } a <= b <==> Math#min(a, b) == a); +axiom (forall a: int, b: int :: { Math#min(a, b) } b <= a <==> Math#min(a, b) == b); +axiom (forall a: int, b: int :: { Math#min(a, b) } Math#min(a, b) == a || Math#min(a, b) == b); + +function Math#clip(a: int): int; +axiom (forall a: int :: { Math#clip(a) } 0 <= a ==> Math#clip(a) == a); +axiom (forall a: int :: { Math#clip(a) } a < 0 ==> Math#clip(a) == 0); + +type MultiSet = [Box]int; + +function $IsGoodMultiSet(ms: MultiSet): bool; +// ints are non-negative, used after havocing, and for conversion from sequences to multisets. +axiom (forall ms: MultiSet :: { $IsGoodMultiSet(ms) } + $IsGoodMultiSet(ms) <==> + (forall bx: Box :: { ms[bx] } 0 <= ms[bx] && ms[bx] <= MultiSet#Card(ms))); + +function MultiSet#Card(MultiSet): int; +axiom (forall s: MultiSet :: { MultiSet#Card(s) } 0 <= MultiSet#Card(s)); +axiom (forall s: MultiSet, x: Box, n: int :: { MultiSet#Card(s[x := n]) } + 0 <= n ==> MultiSet#Card(s[x := n]) == MultiSet#Card(s) - s[x] + n); + +function MultiSet#Empty(): MultiSet; +axiom (forall o: Box :: { MultiSet#Empty()[o] } MultiSet#Empty()[o] == 0); +axiom (forall s: MultiSet :: { MultiSet#Card(s) } + (MultiSet#Card(s) == 0 <==> s == MultiSet#Empty()) && + (MultiSet#Card(s) != 0 ==> (exists x: Box :: 0 < s[x]))); + +function MultiSet#Singleton(Box): MultiSet; +axiom (forall r: Box, o: Box :: { MultiSet#Singleton(r)[o] } (MultiSet#Singleton(r)[o] == 1 <==> r == o) && + (MultiSet#Singleton(r)[o] == 0 <==> r != o)); +axiom (forall r: Box :: { MultiSet#Singleton(r) } MultiSet#Singleton(r) == MultiSet#UnionOne(MultiSet#Empty(), r)); + +function MultiSet#UnionOne(MultiSet, Box): MultiSet; +// pure containment axiom (in the original multiset or is the added element) +axiom (forall a: MultiSet, x: Box, o: Box :: { MultiSet#UnionOne(a,x)[o] } + 0 < MultiSet#UnionOne(a,x)[o] <==> o == x || 0 < a[o]); +// union-ing increases count by one +axiom (forall a: MultiSet, x: Box :: { MultiSet#UnionOne(a, x) } + MultiSet#UnionOne(a, x)[x] == a[x] + 1); +// non-decreasing +axiom (forall a: MultiSet, x: Box, y: Box :: { MultiSet#UnionOne(a, x), a[y] } + 0 < a[y] ==> 0 < MultiSet#UnionOne(a, x)[y]); +// other elements unchanged +axiom (forall a: MultiSet, x: Box, y: Box :: { MultiSet#UnionOne(a, x), a[y] } + x != y ==> a[y] == MultiSet#UnionOne(a, x)[y]); +axiom (forall a: MultiSet, x: Box :: { MultiSet#Card(MultiSet#UnionOne(a, x)) } + MultiSet#Card(MultiSet#UnionOne(a, x)) == MultiSet#Card(a) + 1); + + +function MultiSet#Union(MultiSet, MultiSet): MultiSet; +// union-ing is the sum of the contents +axiom (forall a: MultiSet, b: MultiSet, o: Box :: { MultiSet#Union(a,b)[o] } + MultiSet#Union(a,b)[o] == a[o] + b[o]); +axiom (forall a: MultiSet, b: MultiSet :: { MultiSet#Card(MultiSet#Union(a,b)) } + MultiSet#Card(MultiSet#Union(a,b)) == MultiSet#Card(a) + MultiSet#Card(b)); + +function MultiSet#Intersection(MultiSet, MultiSet): MultiSet; +axiom (forall a: MultiSet, b: MultiSet, o: Box :: { MultiSet#Intersection(a,b)[o] } + MultiSet#Intersection(a,b)[o] == Math#min(a[o], b[o])); + +// left and right pseudo-idempotence +axiom (forall a, b: MultiSet :: { MultiSet#Intersection(MultiSet#Intersection(a, b), b) } + MultiSet#Intersection(MultiSet#Intersection(a, b), b) == MultiSet#Intersection(a, b)); +axiom (forall a, b: MultiSet :: { MultiSet#Intersection(a, MultiSet#Intersection(a, b)) } + MultiSet#Intersection(a, MultiSet#Intersection(a, b)) == MultiSet#Intersection(a, b)); + +// multiset difference, a - b. clip() makes it positive. +function MultiSet#Difference(MultiSet, MultiSet): MultiSet; +axiom (forall a: MultiSet, b: MultiSet, o: Box :: { MultiSet#Difference(a,b)[o] } + MultiSet#Difference(a,b)[o] == Math#clip(a[o] - b[o])); +axiom (forall a, b: MultiSet, y: Box :: { MultiSet#Difference(a, b), b[y], a[y] } + a[y] <= b[y] ==> MultiSet#Difference(a, b)[y] == 0 ); +axiom (forall a, b: MultiSet :: + { MultiSet#Card(MultiSet#Difference(a, b)) } + MultiSet#Card(MultiSet#Difference(a, b)) + MultiSet#Card(MultiSet#Difference(b, a)) + + 2 * MultiSet#Card(MultiSet#Intersection(a, b)) + == MultiSet#Card(MultiSet#Union(a, b)) && + MultiSet#Card(MultiSet#Difference(a, b)) == MultiSet#Card(a) - MultiSet#Card(MultiSet#Intersection(a, b))); + +// multiset subset means a must have at most as many of each element as b +function MultiSet#Subset(MultiSet, MultiSet): bool; +axiom (forall a: MultiSet, b: MultiSet :: { MultiSet#Subset(a,b) } + MultiSet#Subset(a,b) <==> (forall o: Box :: {a[o]} {b[o]} a[o] <= b[o])); + +function MultiSet#Equal(MultiSet, MultiSet): bool; +axiom (forall a: MultiSet, b: MultiSet :: { MultiSet#Equal(a,b) } + MultiSet#Equal(a,b) <==> (forall o: Box :: {a[o]} {b[o]} a[o] == b[o])); +// extensionality axiom for multisets +axiom (forall a: MultiSet, b: MultiSet :: { MultiSet#Equal(a,b) } + MultiSet#Equal(a,b) ==> a == b); + +function MultiSet#Disjoint(MultiSet, MultiSet): bool; +axiom (forall a: MultiSet, b: MultiSet :: { MultiSet#Disjoint(a,b) } + MultiSet#Disjoint(a,b) <==> (forall o: Box :: {a[o]} {b[o]} a[o] == 0 || b[o] == 0)); + +// conversion to a multiset. each element in the original set has duplicity 1. +function MultiSet#FromSet(Set): MultiSet; +axiom (forall s: Set, a: Box :: { MultiSet#FromSet(s)[a] } + (MultiSet#FromSet(s)[a] == 0 <==> !s[a]) && + (MultiSet#FromSet(s)[a] == 1 <==> s[a])); +axiom (forall s: Set :: { MultiSet#Card(MultiSet#FromSet(s)) } + MultiSet#Card(MultiSet#FromSet(s)) == Set#Card(s)); + +// conversion to a multiset, from a sequence. +function MultiSet#FromSeq(Seq): MultiSet uses { + axiom MultiSet#FromSeq(Seq#Empty(): Seq) == MultiSet#Empty(): MultiSet; +} + +// conversion produces a good map. +axiom (forall s: Seq :: { MultiSet#FromSeq(s) } $IsGoodMultiSet(MultiSet#FromSeq(s)) ); +// cardinality axiom +axiom (forall s: Seq :: + { MultiSet#Card(MultiSet#FromSeq(s)) } + MultiSet#Card(MultiSet#FromSeq(s)) == Seq#Length(s)); +// building axiom +axiom (forall s: Seq, v: Box :: + { MultiSet#FromSeq(Seq#Build(s, v)) } + MultiSet#FromSeq(Seq#Build(s, v)) == MultiSet#UnionOne(MultiSet#FromSeq(s), v) + ); + +// concatenation axiom +axiom (forall a: Seq, b: Seq :: + { MultiSet#FromSeq(Seq#Append(a, b)) } + MultiSet#FromSeq(Seq#Append(a, b)) == MultiSet#Union(MultiSet#FromSeq(a), MultiSet#FromSeq(b)) ); + +// update axiom +axiom (forall s: Seq, i: int, v: Box, x: Box :: + { MultiSet#FromSeq(Seq#Update(s, i, v))[x] } + 0 <= i && i < Seq#Length(s) ==> + MultiSet#FromSeq(Seq#Update(s, i, v))[x] == + MultiSet#Union(MultiSet#Difference(MultiSet#FromSeq(s), MultiSet#Singleton(Seq#Index(s,i))), MultiSet#Singleton(v))[x] ); + // i.e. MS(Update(s, i, v)) == MS(s) - {{s[i]}} + {{v}} +axiom (forall s: Seq, x: Box :: { MultiSet#FromSeq(s)[x] } + (exists i : int :: { Seq#Index(s,i) } 0 <= i && i < Seq#Length(s) && x == Seq#Index(s,i)) <==> 0 < MultiSet#FromSeq(s)[x] ); + +// --------------------------------------------------------------- +// -- Axiomatization of sequences -------------------------------- +// --------------------------------------------------------------- + +#include "Sequences.bpl" + +// The empty sequence $Is any type +//axiom (forall t: Ty :: {$Is(Seq#Empty(): Seq, TSeq(t))} $Is(Seq#Empty(): Seq, TSeq(t))); + +// Build preserves $Is +axiom (forall s: Seq, bx: Box, t: Ty :: { $Is(Seq#Build(s, bx), TSeq(t)) } + $Is(s, TSeq(t)) && $IsBox(bx, t) ==> $Is(Seq#Build(s, bx), TSeq(t))); + +function Seq#Create(ty: Ty, heap: Heap, len: int, init: HandleType): Seq; +axiom (forall ty: Ty, heap: Heap, len: int, init: HandleType :: + { Seq#Length(Seq#Create(ty, heap, len, init): Seq) } + $IsGoodHeap(heap) && 0 <= len ==> + Seq#Length(Seq#Create(ty, heap, len, init): Seq) == len); +axiom (forall ty: Ty, heap: Heap, len: int, init: HandleType, i: int :: + { Seq#Index(Seq#Create(ty, heap, len, init), i) } + $IsGoodHeap(heap) && 0 <= i && i < len ==> + Seq#Index(Seq#Create(ty, heap, len, init), i) == Apply1(TInt, ty, heap, init, $Box(i))); + +function Seq#FromArray(h: Heap, a: ref): Seq; +axiom (forall h: Heap, a: ref :: + { Seq#Length(Seq#FromArray(h,a)) } + Seq#Length(Seq#FromArray(h, a)) == _System.array.Length(a)); +axiom (forall h: Heap, a: ref :: + { Seq#FromArray(h, a) } + (forall i: int :: + // it's important to include both triggers, so that assertions about the + // the relation between the array and the sequence can be proved in either + // direction + { read(h, a, IndexField(i)) } + { Seq#Index(Seq#FromArray(h, a): Seq, i) } + 0 <= i && + i < Seq#Length(Seq#FromArray(h, a)) // this will trigger the previous axiom to get a connection with _System.array.Length(a) + ==> + Seq#Index(Seq#FromArray(h, a), i) == read(h, a, IndexField(i)))); +axiom (forall h0, h1: Heap, a: ref :: + { Seq#FromArray(h1, a), $HeapSucc(h0, h1) } + $IsGoodHeap(h0) && $IsGoodHeap(h1) && $HeapSucc(h0, h1) && h0[a] == h1[a] + ==> + Seq#FromArray(h0, a) == Seq#FromArray(h1, a)); +axiom (forall h: Heap, i: int, v: Box, a: ref :: + { Seq#FromArray(update(h, a, IndexField(i), v), a) } + 0 <= i && i < _System.array.Length(a) ==> Seq#FromArray(update(h, a, IndexField(i), v), a) == Seq#Update(Seq#FromArray(h, a), i, v) ); + +// Extension axiom, triggers only on Takes from arrays. +axiom (forall h: Heap, a: ref, n0, n1: int :: + { Seq#Take(Seq#FromArray(h, a), n0), Seq#Take(Seq#FromArray(h, a), n1) } + n0 + 1 == n1 && 0 <= n0 && n1 <= _System.array.Length(a) ==> Seq#Take(Seq#FromArray(h, a), n1) == Seq#Build(Seq#Take(Seq#FromArray(h, a), n0), read(h, a, IndexField(n0): Field)) ); + +function Seq#Rank(Seq): int; +axiom (forall s: Seq, i: int :: + { DtRank($Unbox(Seq#Index(s, i)): DatatypeType) } + 0 <= i && i < Seq#Length(s) ==> DtRank($Unbox(Seq#Index(s, i)): DatatypeType) < Seq#Rank(s) ); +axiom (forall s: Seq, i: int :: + { Seq#Rank(Seq#Drop(s, i)) } + 0 < i && i <= Seq#Length(s) ==> Seq#Rank(Seq#Drop(s, i)) < Seq#Rank(s) ); +axiom (forall s: Seq, i: int :: + { Seq#Rank(Seq#Take(s, i)) } + 0 <= i && i < Seq#Length(s) ==> Seq#Rank(Seq#Take(s, i)) < Seq#Rank(s) ); +axiom (forall s: Seq, i: int, j: int :: + { Seq#Rank(Seq#Append(Seq#Take(s, i), Seq#Drop(s, j))) } + 0 <= i && i < j && j <= Seq#Length(s) ==> Seq#Rank(Seq#Append(Seq#Take(s, i), Seq#Drop(s, j))) < Seq#Rank(s) ); + +// --------------------------------------------------------------- +// -- Axiomatization of Maps ------------------------------------- +// --------------------------------------------------------------- + +type Map; + +// A Map is defined by three functions, Map#Domain, Map#Elements, and #Map#Card. + +function Map#Domain(Map) : Set; + +function Map#Elements(Map) : [Box]Box; + +function Map#Card(Map) : int; + +axiom (forall m: Map :: { Map#Card(m) } 0 <= Map#Card(m)); + +axiom (forall m: Map :: + { Map#Card(m) } + Map#Card(m) == 0 <==> m == Map#Empty()); + +axiom (forall m: Map :: + { Map#Domain(m) } + m == Map#Empty() || (exists k: Box :: Map#Domain(m)[k])); +axiom (forall m: Map :: + { Map#Values(m) } + m == Map#Empty() || (exists v: Box :: Map#Values(m)[v])); +axiom (forall m: Map :: + { Map#Items(m) } + m == Map#Empty() || (exists k, v: Box :: Map#Items(m)[$Box(#_System._tuple#2._#Make2(k, v))])); + +axiom (forall m: Map :: + { Set#Card(Map#Domain(m)) } { Map#Card(m) } + Set#Card(Map#Domain(m)) == Map#Card(m)); +axiom (forall m: Map :: + { Set#Card(Map#Values(m)) } { Map#Card(m) } + Set#Card(Map#Values(m)) <= Map#Card(m)); +axiom (forall m: Map :: + { Set#Card(Map#Items(m)) } { Map#Card(m) } + Set#Card(Map#Items(m)) == Map#Card(m)); + +// The set of Values of a Map can be obtained by the function Map#Values, which is +// defined as follows. Remember, a Set is defined by membership (using Boogie's +// square brackets) and Map#Card, so we need to define what these mean for the Set +// returned by Map#Values. + +function Map#Values(Map) : Set; + +axiom (forall m: Map, v: Box :: { Map#Values(m)[v] } + Map#Values(m)[v] == + (exists u: Box :: { Map#Domain(m)[u] } { Map#Elements(m)[u] } + Map#Domain(m)[u] && + v == Map#Elements(m)[u])); + +// The set of Items--that is, (key,value) pairs--of a Map can be obtained by the +// function Map#Items. Again, we need to define membership of Set#Card for this +// set. Everywhere else in this axiomatization, Map is parameterized by types U V, +// even though Dafny only ever instantiates U V with Box Box. This makes the +// axiomatization more generic. Function Map#Items, however, returns a set of +// pairs, and the axiomatization of pairs is Dafny specific. Therefore, the +// definition of Map#Items here is to be considered Dafny specific. Also, note +// that it relies on the two destructors for 2-tuples. + +function Map#Items(Map) : Set; + +function #_System._tuple#2._#Make2(Box, Box) : DatatypeType; +function _System.Tuple2._0(DatatypeType) : Box; +function _System.Tuple2._1(DatatypeType) : Box; + +axiom (forall m: Map, item: Box :: { Map#Items(m)[item] } + Map#Items(m)[item] <==> + Map#Domain(m)[_System.Tuple2._0($Unbox(item))] && + Map#Elements(m)[_System.Tuple2._0($Unbox(item))] == _System.Tuple2._1($Unbox(item))); + +// Here are the operations that produce Map values. + +function Map#Empty(): Map; +axiom (forall u: Box :: + { Map#Domain(Map#Empty(): Map)[u] } + !Map#Domain(Map#Empty(): Map)[u]); + +function Map#Glue([Box]bool, [Box]Box, Ty): Map; +axiom (forall a: [Box]bool, b: [Box]Box, t: Ty :: + { Map#Domain(Map#Glue(a, b, t)) } + Map#Domain(Map#Glue(a, b, t)) == a); +axiom (forall a: [Box]bool, b: [Box]Box, t: Ty :: + { Map#Elements(Map#Glue(a, b, t)) } + Map#Elements(Map#Glue(a, b, t)) == b); +axiom (forall a: [Box]bool, b: [Box]Box, t0, t1: Ty :: + { Map#Glue(a, b, TMap(t0, t1)) } + // In the following line, no trigger needed, since the quantifier only gets used in negative contexts + (forall bx: Box :: a[bx] ==> $IsBox(bx, t0) && $IsBox(b[bx], t1)) + ==> + $Is(Map#Glue(a, b, TMap(t0, t1)), TMap(t0, t1))); + + +//Build is used in displays, and for map updates +function Map#Build(Map, Box, Box): Map; +/*axiom (forall m: Map, u: Box, v: Box :: + { Map#Domain(Map#Build(m, u, v))[u] } { Map#Elements(Map#Build(m, u, v))[u] } + Map#Domain(Map#Build(m, u, v))[u] && Map#Elements(Map#Build(m, u, v))[u] == v);*/ + +axiom (forall m: Map, u: Box, u': Box, v: Box :: + { Map#Domain(Map#Build(m, u, v))[u'] } { Map#Elements(Map#Build(m, u, v))[u'] } + (u' == u ==> Map#Domain(Map#Build(m, u, v))[u'] && + Map#Elements(Map#Build(m, u, v))[u'] == v) && + (u' != u ==> Map#Domain(Map#Build(m, u, v))[u'] == Map#Domain(m)[u'] && + Map#Elements(Map#Build(m, u, v))[u'] == Map#Elements(m)[u'])); +axiom (forall m: Map, u: Box, v: Box :: { Map#Card(Map#Build(m, u, v)) } + Map#Domain(m)[u] ==> Map#Card(Map#Build(m, u, v)) == Map#Card(m)); +axiom (forall m: Map, u: Box, v: Box :: { Map#Card(Map#Build(m, u, v)) } + !Map#Domain(m)[u] ==> Map#Card(Map#Build(m, u, v)) == Map#Card(m) + 1); + +// Map operations +function Map#Merge(Map, Map): Map; +axiom (forall m: Map, n: Map :: + { Map#Domain(Map#Merge(m, n)) } + Map#Domain(Map#Merge(m, n)) == Set#Union(Map#Domain(m), Map#Domain(n))); +axiom (forall m: Map, n: Map, u: Box :: + { Map#Elements(Map#Merge(m, n))[u] } + Map#Domain(Map#Merge(m, n))[u] ==> + (!Map#Domain(n)[u] ==> Map#Elements(Map#Merge(m, n))[u] == Map#Elements(m)[u]) && + (Map#Domain(n)[u] ==> Map#Elements(Map#Merge(m, n))[u] == Map#Elements(n)[u])); + +function Map#Subtract(Map, Set): Map; +axiom (forall m: Map, s: Set :: + { Map#Domain(Map#Subtract(m, s)) } + Map#Domain(Map#Subtract(m, s)) == Set#Difference(Map#Domain(m), s)); +axiom (forall m: Map, s: Set, u: Box :: + { Map#Elements(Map#Subtract(m, s))[u] } + Map#Domain(Map#Subtract(m, s))[u] ==> + Map#Elements(Map#Subtract(m, s))[u] == Map#Elements(m)[u]); + +//equality for maps +function Map#Equal(Map, Map): bool; +axiom (forall m: Map, m': Map:: + { Map#Equal(m, m') } + Map#Equal(m, m') <==> (forall u : Box :: Map#Domain(m)[u] == Map#Domain(m')[u]) && + (forall u : Box :: Map#Domain(m)[u] ==> Map#Elements(m)[u] == Map#Elements(m')[u])); +// extensionality +axiom (forall m: Map, m': Map:: + { Map#Equal(m, m') } + Map#Equal(m, m') ==> m == m'); + +function Map#Disjoint(Map, Map): bool; +axiom (forall m: Map, m': Map :: + { Map#Disjoint(m, m') } + Map#Disjoint(m, m') <==> (forall o: Box :: {Map#Domain(m)[o]} {Map#Domain(m')[o]} !Map#Domain(m)[o] || !Map#Domain(m')[o])); + +// --------------------------------------------------------------- +// -- Axiomatization of IMaps ------------------------------------ +// --------------------------------------------------------------- + +type IMap; + +// A IMap is defined by two functions, Map#Domain and Map#Elements. + +function IMap#Domain(IMap) : Set; + +function IMap#Elements(IMap) : [Box]Box; + +axiom (forall m: IMap :: + { IMap#Domain(m) } + m == IMap#Empty() || (exists k: Box :: IMap#Domain(m)[k])); +axiom (forall m: IMap :: + { IMap#Values(m) } + m == IMap#Empty() || (exists v: Box :: IMap#Values(m)[v])); +axiom (forall m: IMap :: + { IMap#Items(m) } + m == IMap#Empty() || (exists k, v: Box :: IMap#Items(m)[$Box(#_System._tuple#2._#Make2(k, v))])); + +axiom (forall m: IMap :: + { IMap#Domain(m) } + m == IMap#Empty() <==> IMap#Domain(m) == ISet#Empty()); +axiom (forall m: IMap :: + { IMap#Values(m) } + m == IMap#Empty() <==> IMap#Values(m) == ISet#Empty()); +axiom (forall m: IMap :: + { IMap#Items(m) } + m == IMap#Empty() <==> IMap#Items(m) == ISet#Empty()); + +// The set of Values of a IMap can be obtained by the function IMap#Values, which is +// defined as follows. Remember, a ISet is defined by membership (using Boogie's +// square brackets) so we need to define what these mean for the Set +// returned by Map#Values. + +function IMap#Values(IMap) : Set; + +axiom (forall m: IMap, v: Box :: { IMap#Values(m)[v] } + IMap#Values(m)[v] == + (exists u: Box :: { IMap#Domain(m)[u] } { IMap#Elements(m)[u] } + IMap#Domain(m)[u] && + v == IMap#Elements(m)[u])); + +// The set of Items--that is, (key,value) pairs--of a Map can be obtained by the +// function IMap#Items. +// Everywhere else in this axiomatization, IMap is parameterized by types U V, +// even though Dafny only ever instantiates U V with Box Box. This makes the +// axiomatization more generic. Function IMap#Items, however, returns a set of +// pairs, and the axiomatization of pairs is Dafny specific. Therefore, the +// definition of IMap#Items here is to be considered Dafny specific. Also, note +// that it relies on the two destructors for 2-tuples. + +function IMap#Items(IMap) : Set; + +axiom (forall m: IMap, item: Box :: { IMap#Items(m)[item] } + IMap#Items(m)[item] <==> + IMap#Domain(m)[_System.Tuple2._0($Unbox(item))] && + IMap#Elements(m)[_System.Tuple2._0($Unbox(item))] == _System.Tuple2._1($Unbox(item))); + +// Here are the operations that produce Map values. +function IMap#Empty(): IMap; +axiom (forall u: Box :: + { IMap#Domain(IMap#Empty(): IMap)[u] } + !IMap#Domain(IMap#Empty(): IMap)[u]); + +function IMap#Glue([Box] bool, [Box]Box, Ty): IMap; +axiom (forall a: [Box]bool, b: [Box]Box, t: Ty :: + { IMap#Domain(IMap#Glue(a, b, t)) } + IMap#Domain(IMap#Glue(a, b, t)) == a); +axiom (forall a: [Box]bool, b: [Box]Box, t: Ty :: + { IMap#Elements(IMap#Glue(a, b, t)) } + IMap#Elements(IMap#Glue(a, b, t)) == b); +axiom (forall a: [Box]bool, b: [Box]Box, t0, t1: Ty :: + { IMap#Glue(a, b, TIMap(t0, t1)) } + // In the following line, no trigger needed, since the quantifier only gets used in negative contexts + (forall bx: Box :: a[bx] ==> $IsBox(bx, t0) && $IsBox(b[bx], t1)) + ==> + $Is(Map#Glue(a, b, TIMap(t0, t1)), TIMap(t0, t1))); + +//Build is used in displays +function IMap#Build(IMap, Box, Box): IMap; +/*axiom (forall m: IMap, u: Box, v: Box :: + { IMap#Domain(IMap#Build(m, u, v))[u] } { IMap#Elements(IMap#Build(m, u, v))[u] } + IMap#Domain(IMap#Build(m, u, v))[u] && IMap#Elements(IMap#Build(m, u, v))[u] == v);*/ + +axiom (forall m: IMap, u: Box, u': Box, v: Box :: + { IMap#Domain(IMap#Build(m, u, v))[u'] } { IMap#Elements(IMap#Build(m, u, v))[u'] } + (u' == u ==> IMap#Domain(IMap#Build(m, u, v))[u'] && + IMap#Elements(IMap#Build(m, u, v))[u'] == v) && + (u' != u ==> IMap#Domain(IMap#Build(m, u, v))[u'] == IMap#Domain(m)[u'] && + IMap#Elements(IMap#Build(m, u, v))[u'] == IMap#Elements(m)[u'])); + +//equality for imaps +function IMap#Equal(IMap, IMap): bool; +axiom (forall m: IMap, m': IMap:: + { IMap#Equal(m, m') } + IMap#Equal(m, m') <==> (forall u : Box :: IMap#Domain(m)[u] == IMap#Domain(m')[u]) && + (forall u : Box :: IMap#Domain(m)[u] ==> IMap#Elements(m)[u] == IMap#Elements(m')[u])); +// extensionality +axiom (forall m: IMap, m': IMap:: + { IMap#Equal(m, m') } + IMap#Equal(m, m') ==> m == m'); + +// IMap operations +function IMap#Merge(IMap, IMap): IMap; +axiom (forall m: IMap, n: IMap :: + { IMap#Domain(IMap#Merge(m, n)) } + IMap#Domain(IMap#Merge(m, n)) == Set#Union(IMap#Domain(m), IMap#Domain(n))); +axiom (forall m: IMap, n: IMap, u: Box :: + { IMap#Elements(IMap#Merge(m, n))[u] } + IMap#Domain(IMap#Merge(m, n))[u] ==> + (!IMap#Domain(n)[u] ==> IMap#Elements(IMap#Merge(m, n))[u] == IMap#Elements(m)[u]) && + (IMap#Domain(n)[u] ==> IMap#Elements(IMap#Merge(m, n))[u] == IMap#Elements(n)[u])); + +function IMap#Subtract(IMap, Set): IMap; +axiom (forall m: IMap, s: Set :: + { IMap#Domain(IMap#Subtract(m, s)) } + IMap#Domain(IMap#Subtract(m, s)) == Set#Difference(IMap#Domain(m), s)); +axiom (forall m: IMap, s: Set, u: Box :: + { IMap#Elements(IMap#Subtract(m, s))[u] } + IMap#Domain(IMap#Subtract(m, s))[u] ==> + IMap#Elements(IMap#Subtract(m, s))[u] == IMap#Elements(m)[u]); + +// ------------------------------------------------------------------------- +// -- Provide arithmetic wrappers to improve triggering and non-linear math +// ------------------------------------------------------------------------- + +function INTERNAL_add_boogie(x:int, y:int) : int { x + y } +function INTERNAL_sub_boogie(x:int, y:int) : int { x - y } +function INTERNAL_mul_boogie(x:int, y:int) : int { x * y } +function INTERNAL_div_boogie(x:int, y:int) : int { x div y } +function INTERNAL_mod_boogie(x:int, y:int) : int { x mod y } +function {:never_pattern true} INTERNAL_lt_boogie(x:int, y:int) : bool { x < y } +function {:never_pattern true} INTERNAL_le_boogie(x:int, y:int) : bool { x <= y } +function {:never_pattern true} INTERNAL_gt_boogie(x:int, y:int) : bool { x > y } +function {:never_pattern true} INTERNAL_ge_boogie(x:int, y:int) : bool { x >= y } + +function Mul(x, y: int): int { x * y } +function Div(x, y: int): int { x div y } +function Mod(x, y: int): int { x mod y } +function Add(x, y: int): int { x + y } +function Sub(x, y: int): int { x - y } + +#if ARITH_DISTR +axiom (forall x, y, z: int :: + { Mul(Add(x, y), z) } + Mul(Add(x, y), z) == Add(Mul(x, z), Mul(y, z))); +axiom (forall x,y,z: int :: + { Mul(x, Add(y, z)) } + Mul(x, Add(y, z)) == Add(Mul(x, y), Mul(x, z))); +//axiom (forall x, y, z: int :: +// { Mul(Sub(x, y), z) } +// Mul(Sub(x, y), z) == Sub(Mul(x, z), Mul(y, z))); +#endif +#if ARITH_MUL_DIV_MOD +axiom (forall x, y: int :: + { Div(x, y), Mod(x, y) } + { Mul(Div(x, y), y) } + y != 0 ==> + Mul(Div(x, y), y) + Mod(x, y) == x); +#endif +#if ARITH_MUL_SIGN +axiom (forall x, y: int :: + { Mul(x, y) } + ((0 <= x && 0 <= y) || (x <= 0 && y <= 0) ==> 0 <= Mul(x, y))); +#endif +#if ARITH_MUL_COMM +axiom (forall x, y: int :: + { Mul(x, y) } + Mul(x, y) == Mul(y, x)); +#endif +#if ARITH_MUL_ASSOC +axiom (forall x, y, z: int :: + { Mul(x, Mul(y, z)) } + Mul(y, z) != z && Mul(y, z) != y ==> Mul(x, Mul(y, z)) == Mul(Mul(x, y), z)); +#endif + +// ------------------------------------------------------------------------- diff --git a/Source/DafnyCore/Prelude/Sequences.dfy b/Source/DafnyCore/Prelude/Sequences.dfy new file mode 100644 index 00000000000..d4ea7c2e86e --- /dev/null +++ b/Source/DafnyCore/Prelude/Sequences.dfy @@ -0,0 +1,796 @@ +module {:extract_boogie} Sequences { + export + provides Lists, Boxes + provides Seq, Length, AboutLength + provides Empty, LengthEmpty0, LengthEmpty1 + provides Index, Append, IndexAppend + provides Build, BuildInv0, BuildInv1, BuildInjective, LengthBuild + provides Update, IndexUpdate, LengthUpdate + provides Contains, SeqContainsItsElements, EmptyContainsNothing, AppendContains, BuildContains + provides Equal, AboutEqual, Extensionality + provides SameUntil, AboutSameUntil + provides Take, LengthTake, IndexTake + provides Drop, LengthDrop, IndexDrop0, IndexDrop1 + provides TakeContains, DropContains, AppendTakeDrop + provides DropNothing, TakeNothing, DropDrop + provides TakeUpdate0, TakeUpdate1, DropUpdate0, DropUpdate1, DropBuild + + import opened Lists + import opened Boxes + + // boogie: type Seq; + type {:extract_boogie_name "Seq"} Seq = List + + // boogie: function Seq#Length(Seq): int; + function {:extract_boogie_name "Seq#Length"} Length(s: Seq): int { + s.Length() + } + + // boogie: axiom (forall s: Seq :: { Seq#Length(s) } 0 <= Seq#Length(s)); + lemma {:extract_pattern Length(s)} AboutLength(s: Seq) + ensures 0 <= Length(s) + { + } + + // boogie: function Seq#Empty(): Seq; + function {:extract_boogie_name "Seq#Empty"} Empty(): Seq { + Nil + } + + // boogie: axiom Seq#Length(Seq#Empty()) == 0; + lemma {:extract_used_by Empty} LengthEmpty0() + ensures Length(Empty()) == 0 + { + } + + // boogie axiom (forall s: Seq :: { Seq#Length(s) } Seq#Length(s) == 0 ==> s == Seq#Empty()); + lemma {:extract_pattern Length(s)} LengthEmpty1(s: Seq) + requires Length(s) == 0 + ensures s == Empty() + { + } + + // boogie: + // The following would be a nice fact to include, because it would enable verifying the + // GenericPick.SeqPick* methods in Test/dafny0/SmallTests.dfy. However, it substantially + // slows down performance on some other tests, including running seemingly forever on + // some. + // axiom (forall s: Seq :: { Seq#Length(s) } + // Seq#Length(s) != 0 ==> (exists x: Box :: Seq#Contains(s, x))); + + // boogie: function Seq#Build(s: Seq, val: Box): Seq; + function {:extract_boogie_name "Seq#Build"} Build(s: Seq, val: Box): Seq { + s.Append(Cons(val, Nil)) + } + + // boogie: function Seq#Build_inv0(s: Seq) : Seq; + function {:extract_boogie_name "Seq#Build_inv0"} BuildInv0(s: Seq): Seq { + if s.Nil? then Nil else s.Take(s.Length() - 1) + } + // boogie: function Seq#Build_inv1(s: Seq) : Box; + function {:extract_boogie_name "Seq#Build_inv1"} BuildInv1(s: Seq): Box { + if s.Nil? then + Boxes.arbitrary + else + s.AboutDrop(s.Length() - 1); + s.Drop(s.Length() - 1).head + } + + // boogie: + // axiom (forall s: Seq, val: Box :: + // { Seq#Build(s, val) } + // Seq#Build_inv0(Seq#Build(s, val)) == s && + // Seq#Build_inv1(Seq#Build(s, val)) == val); + lemma {:extract_pattern Build(s, val)} BuildInjective(s: Seq, val: Box) + ensures BuildInv0(Build(s, val)) == s + ensures BuildInv1(Build(s, val)) == val + { + var b := Build(s, val); + var valList := Cons(val, Nil); + assert b == s.Append(valList) != Nil; + assert L: b.Length() == s.Length() + 1 by { + s.LengthAppend(valList); + } + + calc { + BuildInv0(b); + s.Append(valList).Take(b.Length() - 1); + { reveal L; } + s.Append(valList).Take(s.Length()); + { s.AppendTake(valList); } + s; + } + + calc { + BuildInv1(b); + { b.AboutDrop(b.Length() - 1); } + b.Drop(b.Length() - 1).head; + { reveal L; } + s.Append(valList).Drop(s.Length()).head; + { s.AppendDrop(valList); } + valList.head; + val; + } + } + + // boogie: + // axiom (forall s: Seq, v: Box :: + // { Seq#Build(s,v) } + // Seq#Length(Seq#Build(s,v)) == 1 + Seq#Length(s)); + lemma {:extract_pattern Build(s, v)} LengthBuild(s: Seq, v: Box) + ensures Length(Build(s, v)) == 1 + Length(s) + { + var valList := Cons(v, Nil); + assert valList.Length() == 1; + s.LengthAppend(valList); + } + + // boogie: + // axiom (forall s: Seq, i: int, v: Box :: { Seq#Index(Seq#Build(s,v), i) } + // (i == Seq#Length(s) ==> Seq#Index(Seq#Build(s,v), i) == v) && + // (i != Seq#Length(s) ==> Seq#Index(Seq#Build(s,v), i) == Seq#Index(s, i))); + lemma {:extract_pattern Index(Build(s, v), i)} IndexBuild(s: Seq, i: int, v: Box) + ensures i == Length(s) ==> Index(Build(s, v), i) == v + ensures i != Length(s) ==> Index(Build(s, v), i) == Index(s, i) + { + var b := Build(s, v); + var valList := Cons(v, Nil); + assert b == s.Append(valList) != Nil; + assert b.Length() == s.Length() + 1 by { + s.LengthAppend(valList); + } + + if 0 <= i < b.Length() { + calc { + Index(Build(s, v), i); + Index(s.Append(valList), i); + s.Append(valList).At(i); + { s.AppendAt(valList, i); } + if i < Length(s) then s.At(i) else valList.At(0); + } + } + } + + // boogie: + // axiom (forall s0: Seq, s1: Seq :: { Seq#Length(Seq#Append(s0,s1)) } + // Seq#Length(Seq#Append(s0,s1)) == Seq#Length(s0) + Seq#Length(s1)); + lemma {:extract_pattern Length(Append(s0, s1))} LengthAppend(s0: Seq, s1: Seq) + ensures Length(Append(s0, s1)) == Length(s0) + Length(s1) + { + s0.LengthAppend(s1); + } + + // boogie: function Seq#Index(Seq, int): Box; + function {:extract_boogie_name "Seq#Index"} Index(s: Seq, i: int): Box { + if 0 <= i < Length(s) then + s.At(i) + else + Boxes.arbitrary + } + + // boogie: + // axiom (forall s0: Seq, s1: Seq, n: int :: { Seq#Index(Seq#Append(s0,s1), n) } + // (n < Seq#Length(s0) ==> Seq#Index(Seq#Append(s0,s1), n) == Seq#Index(s0, n)) && + // (Seq#Length(s0) <= n ==> Seq#Index(Seq#Append(s0,s1), n) == Seq#Index(s1, n - Seq#Length(s0)))); + lemma {:extract_pattern Index(Append(s0, s1), n)} IndexAppend(s0: Seq, s1: Seq, n: int) + ensures n < Length(s0) ==> Index(Append(s0, s1), n) == Index(s0, n) + ensures Length(s0) <= n ==> Index(Append(s0, s1), n) == Index(s1, n - Length(s0)) + { + if + case n < 0 => + + case 0 <= n < Length(s0) => + if n == 0 { + calc { + Index(Append(s0, s1), 0); + Index(Cons(s0.head, Append(s0.tail, s1)), 0); + s0.head; + Index(Cons(s0.head, s0.tail), 0); + Index(s0, 0); + } + } else { + calc { + Index(Append(s0, s1), n); + // def. Append + Index(Cons(s0.head, Append(s0.tail, s1)), n); + // def. Index + Index(Append(s0.tail, s1), n - 1); + { IndexAppend(s0.tail, s1, n - 1); } + Index(s0.tail, n - 1); + // def. Index + Index(Cons(s0.head, s0.tail), n); + Index(s0, n); + } + } + + case Length(s0) <= n => + match s0 + case Nil => + calc { + Index(Append(s0, s1), n); + // def. Append + Index(s1, n); + // def. Length + Index(s1, n - Length(s0)); + } + case Cons(x, tail) => + calc { + Index(Append(s0, s1), n); + // def. Append + Index(Cons(s0.head, Append(s0.tail, s1)), n); + // def. Index + Index(Append(s0.tail, s1), n - 1); + { IndexAppend(s0.tail, s1, n - 1); } + Index(s1, n - 1 - Length(s0.tail)); + // def. Length + Index(s1, n - Length(s0)); + } + } + + // boogie: function Seq#Update(Seq, int, Box): Seq; + function {:extract_boogie_name "Seq#Update"} Update(s: Seq, i: int, val: Box): Seq { + if !(0 <= i < s.Length()) then + s + else if i == 0 then + Cons(val, s.tail) + else + Cons(s.head, Update(s.tail, i - 1, val)) + } + + // boogie: + // axiom (forall s: Seq, i: int, v: Box :: { Seq#Length(Seq#Update(s,i,v)) } + // 0 <= i && i < Seq#Length(s) ==> Seq#Length(Seq#Update(s,i,v)) == Seq#Length(s)); + lemma {:extract_pattern Length(Update(s, i, v))} LengthUpdate(s: Seq, i: int, v: Box) + requires 0 <= i < Length(s) + ensures Length(Update(s, i, v)) == Length(s) + { + } + + // boogie: + // axiom (forall s: Seq, i: int, v: Box, n: int :: { Seq#Index(Seq#Update(s,i,v),n) } + // 0 <= n && n < Seq#Length(s) ==> + // (i == n ==> Seq#Index(Seq#Update(s,i,v),n) == v) && + // (i != n ==> Seq#Index(Seq#Update(s,i,v),n) == Seq#Index(s,n))); + lemma {:extract_pattern Index(Update(s, i, v), n)} IndexUpdate(s: Seq, i: int, v: Box, n: int) + requires 0 <= n < Length(s) + ensures i == n ==> Index(Update(s, i, v), n) == v + ensures i != n ==> Index(Update(s, i, v), n) == Index(s, n) + { + if 0 == i < s.Length() { + calc { + Index(Update(s, i, v), n); + { LengthUpdate(s, i, v); } + Update(s, i, v).At(n); + Cons(v, s.tail).At(n); + } + + } else if 0 < i < s.Length() { + LengthUpdate(s, i, v); + calc { + Index(Update(s, i, v), n); + Update(s, i, v).At(n); + Cons(s.head, Update(s.tail, i - 1, v)).At(n); + } + if n == 0 { + calc { + Cons(s.head, Update(s.tail, i - 1, v)).At(n); + s.head; + Cons(s.head, s.tail).At(n); + s.At(n); + Index(s, n); + } + } else { + calc { + Cons(s.head, Update(s.tail, i - 1, v)).At(n); + Update(s.tail, i - 1, v).At(n - 1); + { IndexUpdate(s.tail, i - 1, v, n - 1); } + if i == n then v else Index(s.tail, n - 1); + if i == n then v else Index(s, n); + } + } + } + } + + // boogie: function Seq#Append(Seq, Seq): Seq; + function {:extract_boogie_name "Seq#Append"} Append(s0: Seq, s1: Seq): Seq { + s0.Append(s1) + } + + // boogie: function Seq#Contains(Seq, Box): bool; + predicate {:extract_boogie_name "Seq#Contains"} Contains(s: Seq, val: Box) { + exists i :: 0 <= i < Length(s) && Index(s, i) == val + } + + // boogie: + // axiom (forall s: Seq, x: Box :: { Seq#Contains(s,x) } + // Seq#Contains(s,x) <==> + // (exists i: int :: { Seq#Index(s,i) } 0 <= i && i < Seq#Length(s) && Seq#Index(s,i) == x)); + lemma {:extract_pattern Contains(s, x)} SeqContainsItsElements(s: Seq, x: Box) + ensures Contains(s, x) <==> + exists i: int {:extract_pattern Index(s, i)} :: 0 <= i < Length(s) && Index(s, i) == x + { + } + + // boogie: + // axiom (forall x: Box :: + // { Seq#Contains(Seq#Empty(), x) } + // !Seq#Contains(Seq#Empty(), x)); + lemma {:extract_pattern Contains(Empty(), x)} EmptyContainsNothing(x: Box) + ensures !Contains(Empty(), x) + { + } + + // boogie: + // axiom (forall s0: Seq, s1: Seq, x: Box :: + // { Seq#Contains(Seq#Append(s0, s1), x) } + // Seq#Contains(Seq#Append(s0, s1), x) <==> + // Seq#Contains(s0, x) || Seq#Contains(s1, x)); + lemma {:extract_pattern Contains(Append(s0, s1), x)} AppendContains(s0: Seq, s1: Seq, x: Box) + ensures Contains(Append(s0, s1), x) <==> Contains(s0, x) || Contains(s1, x) + { + var a := Append(s0, s1); + s0.LengthAppend(s1); + + if Contains(a, x) { + var i :| 0 <= i < Length(a) && Index(a, i) == x; + assert a.At(i) == if i < s0.Length() then s0.At(i) else s1.At(i - s0.Length()) by { + s0.AppendAt(s1, i); + } + + if i < s0.Length() { + assert Contains(s0, x) by { + assert 0 <= i < Length(s0) && Index(s0, i) == x; + } + } else { + var j := i - s0.Length(); + assert Contains(s1, x) by { + assert x == Index(s1, j); + } + } + } + + if Contains(s0, x) { + var i :| 0 <= i < Length(s0) && Index(s0, i) == x; + assert Contains(a, x) by { + assert Index(a, i) == x by { + s0.AppendAt(s1, i); + } + } + } + + if Contains(s1, x) { + var j :| 0 <= j < Length(s1) && Index(s1, j) == x; + var i := s0.Length() + j; + assert Contains(a, x) by { + assert Index(a, i) == x by { + s0.AppendAt(s1, i); + } + } + } + } + + // needed to prove things like '4 in [2,3,4]', see method TestSequences0 in SmallTests.dfy + // boogie: + // axiom (forall s: Seq, v: Box, x: Box :: + // { Seq#Contains(Seq#Build(s, v), x) } + // Seq#Contains(Seq#Build(s, v), x) <==> (v == x || Seq#Contains(s, x))); + lemma {:extract_pattern Contains(Build(s, v), x)} BuildContains(s: Seq, v: Box, x: Box) + ensures Contains(Build(s, v), x) <==> v == x || Contains(s, x) + { + var valList := Cons(v, Nil); + var b := s.Append(valList); + assert b == Build(s, v); + + assert Ping: v == x ==> Contains(valList, x) by { + assert Index(valList, 0) == v; + } + assert Pong: Contains(valList, x) ==> v == x by { + if Contains(valList, x) { + var i :| 0 <= i < valList.Length() && Index(valList, i) == x; + assert valList.Length() == 1; + } + } + + calc { + Contains(b, x); + { AppendContains(s, valList, x); } + Contains(s, x) || Contains(valList, x); + { reveal Ping, Pong; } + v == x || Contains(s, x); + } + } + + // boogie: + // axiom (forall s: Seq, n: int, x: Box :: + // { Seq#Contains(Seq#Take(s, n), x) } + // Seq#Contains(Seq#Take(s, n), x) <==> + // (exists i: int :: { Seq#Index(s, i) } + // 0 <= i && i < n && i < Seq#Length(s) && Seq#Index(s, i) == x)); + lemma {:extract_pattern Contains(Take(s, n), x)} TakeContains(s: Seq, n: int, x: Box) + ensures Contains(Take(s, n), x) <==> + exists i: int {:extract_pattern Index(s, i)} :: 0 <= i < n && i < Length(s) && Index(s, i) == x + { + if + case n < 0 => + calc { + Contains(Take(s, n), x); + { assert Take(s, n) == Empty(); } + Contains(Empty(), x); + false; + exists i :: 0 <= i < n && i < Length(s) && Index(s, i) == x; + } + + case 0 <= n <= s.Length() => + var (prefix, suffix) := s.Split(n); + var t := s.Take(n); + assert t == prefix; + assert t.Length() == n by { + s.LengthTakeDrop(n); + } + assert L: forall i :: 0 <= i < Length(t) ==> Index(t, i) == Index(s, i) by { + forall i | 0 <= i < Length(t) + ensures Index(t, i) == Index(s, i) + { + prefix.AppendAt(suffix, i); + } + } + + calc { + Contains(t, x); + exists i :: 0 <= i < Length(t) && Index(t, i) == x; + { reveal L; } + exists i :: 0 <= i < n && i < Length(s) && Index(s, i) == x; + } + + case s.Length() < n => + calc { + Contains(Take(s, n), x); + Contains(s, x); + exists i :: 0 <= i < Length(s) && Index(s, i) == x; + { assert Length(s) < n; } + exists i :: 0 <= i < n && i < Length(s) && Index(s, i) == x; + } + } + + // boogie: + // axiom (forall s: Seq, n: int, x: Box :: + // { Seq#Contains(Seq#Drop(s, n), x) } + // Seq#Contains(Seq#Drop(s, n), x) <==> + // (exists i: int :: { Seq#Index(s, i) } + // 0 <= n && n <= i && i < Seq#Length(s) && Seq#Index(s, i) == x)); + lemma {:extract_pattern Contains(Drop(s, n), x)} DropContains(s: Seq, n: int, x: Box) + ensures Contains(Drop(s, n), x) <==> + exists i: int {:extract_pattern Index(s, i)} :: 0 <= n <= i < Length(s) && Index(s, i) == x + { + if 0 <= n <= s.Length() { + var (prefix, suffix) := s.Split(n); + var t := s.Take(n); + assert t == prefix; + assert t.Length() == n by { + s.LengthTakeDrop(n); + } + assert L: forall i :: 0 <= i < Length(suffix) ==> Index(suffix, i) == Index(s, n + i) by { + forall i | 0 <= i < Length(suffix) { + calc { + Index(s, n + i); + { prefix.LengthAppend(suffix); } + s.At(n + i); + { prefix.AppendAt(suffix, n + i); } + suffix.At(i); + Index(suffix, i); + } + } + } + + if Contains(Drop(s, n), x) { + var j :| 0 <= j < Length(suffix) && Index(suffix, j) == x; + var i := n + j; + assert 0 <= n <= i < Length(s) by { + prefix.LengthAppend(suffix); + } + assert Index(s, i) == x by { + reveal L; + } + } + + if i :| 0 <= n <= i < Length(s) && Index(s, i) == x { + var j := i - n; + assert 0 <= j < Length(suffix) by { + prefix.LengthAppend(suffix); + } + assert Index(suffix, j) == x by { + reveal L; + } + } + + } else { + calc { + Contains(Drop(s, n), x); + Contains(Empty(), x); + false; + exists i :: 0 <= n <= i < Length(s) && Index(s, i) == x; + } + } + } + + // boogie: function Seq#Equal(Seq, Seq): bool; + predicate {:extract_boogie_name "Seq#Equal"} Equal(s0: Seq, s1: Seq) { + s0 == s1 + } + + // boogie: + // axiom (forall s0: Seq, s1: Seq :: { Seq#Equal(s0,s1) } + // Seq#Equal(s0,s1) <==> + // Seq#Length(s0) == Seq#Length(s1) && + // (forall j: int :: { Seq#Index(s0,j) } { Seq#Index(s1,j) } + // 0 <= j && j < Seq#Length(s0) ==> Seq#Index(s0,j) == Seq#Index(s1,j))); + lemma {:extract_pattern Equal(s0, s1)} AboutEqual(s0: Seq, s1: Seq) + ensures Equal(s0, s1) <==> + && Length(s0) == Length(s1) + && forall j: int {:extract_pattern Index(s0, j)} {:extract_pattern Index(s1, j)} :: + 0 <= j < Length(s0) ==> Index(s0, j) == Index(s1, j) + { + if Length(s0) == Length(s1) && forall j :: 0 <= j < Length(s0) ==> Index(s0, j) == Index(s1, j) { + assert forall s, i :: 0 <= i < Length(s) ==> Index(s, i) == s.At(i); + DatatypeEquality(s0, s1); + } + } + + lemma DatatypeEquality(s0: Seq, s1: Seq) + requires s0.Length() == s1.Length() + requires forall j :: 0 <= j < s0.Length() ==> s0.At(j) == s1.At(j) + ensures s0 == s1 + { + if s0.Length() != 0 { + assert s0.head == s1.head by { + assert s0.head == s0.At(0) && s1.head == s1.At(0); + } + var t0, t1 := s0.tail, s1.tail; + assert t0.Length() == t1.Length(); + assert forall i :: 0 <= i < t0.Length() ==> t0.At(i) == s0.At(i + 1); + assert forall i :: 0 <= i < t0.Length() ==> t0.At(i) == t1.At(i); + } + } + + // extensionality axiom for sequences + // boogie: + // axiom (forall a: Seq, b: Seq :: { Seq#Equal(a,b) } + // Seq#Equal(a,b) ==> a == b); + lemma {:extract_pattern Equal(a, b)} Extensionality(a: Seq, b: Seq) + requires Equal(a, b) + ensures a == b + { + } + + // boogie: function Seq#SameUntil(Seq, Seq, int): bool; + predicate {:extract_boogie_name "Seq#SameUntil"} SameUntil(s0: Seq, s1: Seq, n: int) { + forall j :: 0 <= j < n ==> Index(s0, j) == Index(s1, j) + } + + // boogie: + // axiom (forall s0: Seq, s1: Seq, n: int :: { Seq#SameUntil(s0,s1,n) } + // Seq#SameUntil(s0,s1,n) <==> + // (forall j: int :: { Seq#Index(s0,j) } { Seq#Index(s1,j) } + // 0 <= j && j < n ==> Seq#Index(s0,j) == Seq#Index(s1,j))); + lemma {:extract_pattern SameUntil(s0, s1, n)} AboutSameUntil(s0: Seq, s1: Seq, n: int) + ensures SameUntil(s0, s1, n) <==> + forall j: int {:extract_pattern Index(s0, j)} {:extract_pattern Index(s1, j)} :: + 0 <= j < n ==> Index(s0, j) == Index(s1, j) + { + } + + // boogie: function Seq#Take(s: Seq, howMany: int): Seq; + function {:extract_boogie_name "Seq#Take"} Take(s: Seq, howMany: int): Seq { + if howMany < 0 then + Empty() + else if howMany <= s.Length() then + s.Take(howMany) + else + s + } + + // boogie: + // axiom (forall s: Seq, n: int :: { Seq#Length(Seq#Take(s,n)) } + // 0 <= n && n <= Seq#Length(s) ==> Seq#Length(Seq#Take(s,n)) == n); + lemma {:extract_pattern Length(Take(s, n))} LengthTake(s: Seq, n: int) + requires 0 <= n <= Length(s) + ensures Length(Take(s, n)) == n + { + s.LengthTakeDrop(n); + } + + // boogie: + // axiom (forall s: Seq, n: int, j: int :: + // {:weight 25} + // { Seq#Index(Seq#Take(s,n), j) } + // { Seq#Index(s, j), Seq#Take(s,n) } + // 0 <= j && j < n && j < Seq#Length(s) ==> + // Seq#Index(Seq#Take(s,n), j) == Seq#Index(s, j)); + lemma {:extract_attribute "weight", 25} {:extract_pattern Index(Take(s, n), j)} {:extract_pattern Index(s, j), Take(s, n)} + IndexTake(s: Seq, n: int, j: int) + requires 0 <= j < n && j < Length(s) + ensures Index(Take(s, n), j) == Index(s, j) + { + if j != 0 && n <= s.Length() { + IndexTake(s.tail, n - 1, j - 1); + } + } + + // boogie: function Seq#Drop(s: Seq, howMany: int): Seq; + function {:extract_boogie_name "Seq#Drop"} Drop(s: Seq, howMany: int): Seq { + if 0 <= howMany <= s.Length() then + s.Drop(howMany) + else + Empty() + } + + // boogie: + // axiom (forall s: Seq, n: int :: { Seq#Length(Seq#Drop(s,n)) } + // 0 <= n && n <= Seq#Length(s) ==> Seq#Length(Seq#Drop(s,n)) == Seq#Length(s) - n); + lemma {:extract_pattern Length(Drop(s, n))} LengthDrop(s: Seq, n: int) + requires 0 <= n <= Length(s) + ensures Length(Drop(s, n)) == Length(s) - n + { + s.LengthTakeDrop(n); + } + + // boogie: + // axiom (forall s: Seq, n: int, j: int :: + // {:weight 25} + // { Seq#Index(Seq#Drop(s,n), j) } + // 0 <= n && 0 <= j && j < Seq#Length(s)-n ==> + // Seq#Index(Seq#Drop(s,n), j) == Seq#Index(s, j+n)); + lemma {:extract_attribute "weight", 25} {:extract_pattern Index(Drop(s, n), j)} IndexDrop0(s: Seq, n: int, j: int) + requires 0 <= n && 0 <= j < Length(s) - n + ensures Index(Drop(s, n), j) == Index(s, j + n) + { + IndexDrop1(s, n, j + n); + } + + // boogie: + // axiom (forall s: Seq, n: int, k: int :: + // {:weight 25} + // { Seq#Index(s, k), Seq#Drop(s,n) } + // 0 <= n && n <= k && k < Seq#Length(s) ==> + // Seq#Index(Seq#Drop(s,n), k-n) == Seq#Index(s, k)); + lemma {:extract_attribute "weight", 25} {:extract_pattern Index(s, k), Drop(s, n)} IndexDrop1(s: Seq, n: int, k: int) + requires 0 <= n <= k < Length(s) + ensures Index(Drop(s, n), k - n) == Index(s, k) + { + if n != 0 { + IndexDrop1(s.tail, n - 1, k - 1); + } + } + + // boogie: + // axiom (forall s, t: Seq, n: int :: + // { Seq#Take(Seq#Append(s, t), n) } + // { Seq#Drop(Seq#Append(s, t), n) } + // n == Seq#Length(s) + // ==> + // Seq#Take(Seq#Append(s, t), n) == s && + // Seq#Drop(Seq#Append(s, t), n) == t); + lemma {:extract_pattern Take(Append(s, t), n)} {:extract_pattern Drop(Append(s, t), n)} AppendTakeDrop(s: Seq, t: Seq, n: int) + requires n == Length(s) + ensures Take(Append(s, t), n) == s + ensures Drop(Append(s, t), n) == t + { + var a := Append(s, t); + assert 0 <= n <= Length(a) by { + s.LengthAppend(t); + } + s.AppendTake(t); + s.AppendDrop(t); + } + + // Commutativity of Take and Drop with Update. + + // boogie: + // axiom (forall s: Seq, i: int, v: Box, n: int :: + // { Seq#Take(Seq#Update(s, i, v), n) } + // 0 <= i && i < n && n <= Seq#Length(s) ==> Seq#Take(Seq#Update(s, i, v), n) == Seq#Update(Seq#Take(s, n), i, v) ); + lemma {:extract_pattern Take(Update(s, i, v), n)} TakeUpdate0(s: Seq, i: int, v: Box, n: int) + requires 0 <= i < n <= Length(s) + ensures Take(Update(s, i, v), n) == Update(Take(s, n), i, v) + decreases i + { + if i != 0 { + TakeUpdate0(s.tail, i - 1, v, n - 1); + } + } + + // boogie: + // axiom (forall s: Seq, i: int, v: Box, n: int :: + // { Seq#Take(Seq#Update(s, i, v), n) } + // n <= i && i < Seq#Length(s) ==> Seq#Take(Seq#Update(s, i, v), n) == Seq#Take(s, n)); + lemma {:extract_pattern Take(Update(s, i, v), n)} TakeUpdate1(s: Seq, i: int, v: Box, n: int) + requires n <= i < Length(s) + ensures Take(Update(s, i, v), n) == Take(s, n) + { + if 0 <= n && i != 0 { + TakeUpdate1(s.tail, i - 1, v, n - 1); + } + } + + // boogie: + // axiom (forall s: Seq, i: int, v: Box, n: int :: + // { Seq#Drop(Seq#Update(s, i, v), n) } + // 0 <= n && n <= i && i < Seq#Length(s) ==> Seq#Drop(Seq#Update(s, i, v), n) == Seq#Update(Seq#Drop(s, n), i-n, v) ); + lemma {:extract_pattern Drop(Update(s, i, v), n)} DropUpdate0(s: Seq, i: int, v: Box, n: int) + requires 0 <= n <= i < Length(s) + ensures Drop(Update(s, i, v), n) == Update(Drop(s, n), i - n, v) + { + if n != 0 { + DropUpdate0(s.tail, i - 1, v, n - 1); + } + } + + // boogie: + // axiom (forall s: Seq, i: int, v: Box, n: int :: + // { Seq#Drop(Seq#Update(s, i, v), n) } + // 0 <= i && i < n && n <= Seq#Length(s) ==> Seq#Drop(Seq#Update(s, i, v), n) == Seq#Drop(s, n)); + lemma {:extract_pattern Drop(Update(s, i, v), n)} DropUpdate1(s: Seq, i: int, v: Box, n: int) + requires 0 <= i < n <= Length(s) + ensures Drop(Update(s, i, v), n) == Drop(s, n) + { + if i != 0 { + DropUpdate1(s.tail, i - 1, v, n - 1); + } + } + + // Drop commutes with build + + // boogie: + // axiom (forall s: Seq, v: Box, n: int :: + // { Seq#Drop(Seq#Build(s, v), n) } + // 0 <= n && n <= Seq#Length(s) ==> Seq#Drop(Seq#Build(s, v), n) == Seq#Build(Seq#Drop(s, n), v) ); + lemma {:extract_pattern Drop(Build(s, v), n)} DropBuild(s: Seq, v: Box, n: int) + requires 0 <= n <= Length(s) + ensures Drop(Build(s, v), n) == Build(Drop(s, n), v) + { + if n != 0 { + calc { + Drop(Build(s, v), n); + Drop(Cons(s.head, Build(s.tail, v)), n); + Drop(Build(s.tail, v), n - 1); + { DropBuild(s.tail, v, n - 1); } + Build(Drop(s.tail, n - 1), v); + Build(Drop(s, n), v); + } + } + } + + // Additional axioms about common things + + // boogie: + // axiom (forall s: Seq, n: int :: { Seq#Drop(s, n) } + // n == 0 ==> Seq#Drop(s, n) == s); + lemma {:extract_pattern Drop(s, n)} DropNothing(s: Seq, n: int) + requires n == 0 + ensures Drop(s, n) == s + { + } + + // boogie: + // axiom (forall s: Seq, n: int :: { Seq#Take(s, n) } + // n == 0 ==> Seq#Take(s, n) == Seq#Empty()); + lemma {: extract_pattern Take(s, n)} TakeNothing(s: Seq, n: int) + requires n == 0 + ensures Take(s, n) == Empty() + { + } + + // boogie: + // axiom (forall s: Seq, m, n: int :: { Seq#Drop(Seq#Drop(s, m), n) } + // 0 <= m && 0 <= n && m+n <= Seq#Length(s) ==> + // Seq#Drop(Seq#Drop(s, m), n) == Seq#Drop(s, m+n)); + lemma {:extract_pattern Drop(Drop(s, m), n)} DropDrop(s: Seq, m: int, n: int) + requires 0 <= m && 0 <= n && m + n <= Length(s) + ensures Drop(Drop(s, m), n) == Drop(s, m + n) + { + if m != 0 { + DropDrop(s.tail, m - 1, n); + } + } + +} diff --git a/Source/DafnyCore/Verifier/BoogieGenerator.BoogieFactory.cs b/Source/DafnyCore/Verifier/BoogieGenerator.BoogieFactory.cs index 970ea4beed5..622f426aea6 100644 --- a/Source/DafnyCore/Verifier/BoogieGenerator.BoogieFactory.cs +++ b/Source/DafnyCore/Verifier/BoogieGenerator.BoogieFactory.cs @@ -684,7 +684,7 @@ static Bpl.Expr BplForall(Bpl.IToken tok, List typeParams, : new Bpl.ForallExpr(tok, typeParams, formals, kv, triggers, body, immutable); } - static Bpl.Expr BplAnd(IEnumerable conjuncts) { + public static Bpl.Expr BplAnd(IEnumerable conjuncts) { Contract.Requires(conjuncts != null); Bpl.Expr eq = Bpl.Expr.True; foreach (var c in conjuncts) { @@ -693,7 +693,7 @@ static Bpl.Expr BplAnd(IEnumerable conjuncts) { return eq; } - static Bpl.Expr BplAnd(Bpl.Expr a, Bpl.Expr b) { + public static Bpl.Expr BplAnd(Bpl.Expr a, Bpl.Expr b) { Contract.Requires(a != null); Contract.Requires(b != null); Contract.Ensures(Contract.Result() != null); @@ -712,7 +712,7 @@ static Bpl.Expr BplAnd(Bpl.Expr a, Bpl.Expr b) { } } - static Bpl.Expr BplOr(IEnumerable disjuncts) { + public static Bpl.Expr BplOr(IEnumerable disjuncts) { Contract.Requires(disjuncts != null); Bpl.Expr eq = Bpl.Expr.False; foreach (var d in disjuncts) { @@ -721,7 +721,7 @@ static Bpl.Expr BplOr(IEnumerable disjuncts) { return eq; } - static Bpl.Expr BplOr(Bpl.Expr a, Bpl.Expr b) { + public static Bpl.Expr BplOr(Bpl.Expr a, Bpl.Expr b) { Contract.Requires(a != null); Contract.Requires(b != null); Contract.Ensures(Contract.Result() != null); @@ -742,7 +742,7 @@ static Bpl.Expr BplOr(Bpl.Expr a, Bpl.Expr b) { } } - static Bpl.Expr BplIff(Bpl.Expr a, Bpl.Expr b) { + public static Bpl.Expr BplIff(Bpl.Expr a, Bpl.Expr b) { Contract.Requires(a != null); Contract.Requires(b != null); Contract.Ensures(Contract.Result() != null); @@ -767,7 +767,7 @@ static Bpl.Expr BplIff(Bpl.Expr a, Bpl.Expr b) { } } - static Bpl.Expr BplImp(Bpl.Expr a, Bpl.Expr b) { + public static Bpl.Expr BplImp(Bpl.Expr a, Bpl.Expr b) { Contract.Requires(a != null); Contract.Requires(b != null); Contract.Ensures(Contract.Result() != null); diff --git a/Source/DafnyDriver/Commands/VerifyCommand.cs b/Source/DafnyDriver/Commands/VerifyCommand.cs index 95df95fe4a2..8a19922ba93 100644 --- a/Source/DafnyDriver/Commands/VerifyCommand.cs +++ b/Source/DafnyDriver/Commands/VerifyCommand.cs @@ -10,6 +10,7 @@ using DafnyCore.Options; using DafnyDriver.Commands; using Microsoft.Boogie; +using Microsoft.Dafny.Compilers; namespace Microsoft.Dafny; @@ -21,6 +22,13 @@ static VerifyCommand() { OptionRegistry.RegisterOption(FilterSymbol, OptionScope.Cli); OptionRegistry.RegisterOption(FilterPosition, OptionScope.Cli); OptionRegistry.RegisterOption(PerformanceStatisticsOption, OptionScope.Cli); + OptionRegistry.RegisterOption(ExtractTarget, OptionScope.Cli); + + DafnyOptions.RegisterLegacyBinding(ExtractTarget, (options, f) => { + options.BoogieExtractionTargetFile = f; + options.ExpandFilename(options.BoogieExtractionTargetFile, x => options.BoogieExtractionTargetFile = x, options.LogPrefix, + options.FileTimestamp); + }); } public static readonly Option PerformanceStatisticsOption = new("--performance-stats", @@ -35,6 +43,13 @@ static VerifyCommand() { public static readonly Option FilterPosition = new("--filter-position", @"Filter what gets verified based on a source location. The location is specified as a file path suffix, optionally followed by a colon and a line number. For example, `dafny verify dfyconfig.toml --filter-position=source1.dfy:5` will only verify things that range over line 5 in the file `source1.dfy`. In combination with `--isolate-assertions`, individual assertions can be verified by filtering on the line that contains them. When processing a single file, the filename can be skipped, for example: `dafny verify MyFile.dfy --filter-position=:23`"); + public static readonly Option ExtractTarget = new("--extract", @" +Extract Dafny types, functions, and lemmas to Boogie. +(use - as to output to console.)".TrimStart()) { + IsHidden = true, + ArgumentHelpName = "file", + }; + public static Command Create() { var result = new Command("verify", "Verify the program."); result.AddArgument(DafnyCommands.FilesArgument); @@ -50,6 +65,7 @@ public static Command Create() { PerformanceStatisticsOption, FilterSymbol, FilterPosition, + ExtractTarget, DafnyFile.DoNotVerifyDependencies }.Concat(DafnyCommands.VerificationOptions). Concat(DafnyCommands.ConsoleOutputOptions). @@ -76,6 +92,18 @@ public static async Task HandleVerification(DafnyOptions options) { await verificationSummarized; await verificationResultsLogged; await proofDependenciesReported; + + if (!resolution.HasErrors && options.BoogieExtractionTargetFile != null) { + using (var engine = ExecutionEngine.CreateWithoutSharedCache(options)) { + try { + var extractedProgram = BoogieExtractor.Extract(resolution.ResolvedProgram); + engine.PrintBplFile(options.BoogieExtractionTargetFile, extractedProgram, true, pretty: true); + } catch (ExtractorError extractorError) { + options.OutputWriter.WriteLine($"Boogie axiom extraction error: {extractorError.Message}"); + return 1; + } + } + } } return await compilation.GetAndReportExitCode(); diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/Fuel.legacy.dfy.expect b/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/Fuel.legacy.dfy.expect index cedc561422a..a13a5837473 100755 --- a/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/Fuel.legacy.dfy.expect +++ b/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/Fuel.legacy.dfy.expect @@ -21,19 +21,19 @@ Fuel.legacy.dfy(324,21): Related location Fuel.legacy.dfy(313,41): Related location Fuel.legacy.dfy(335,26): Error: function precondition could not be proved Fuel.legacy.dfy(324,21): Related location -Fuel.legacy.dfy(314,72): Related location +Fuel.legacy.dfy(312,43): Related location Fuel.legacy.dfy(335,26): Error: function precondition could not be proved Fuel.legacy.dfy(324,21): Related location -Fuel.legacy.dfy(314,93): Related location +Fuel.legacy.dfy(312,58): Related location Fuel.legacy.dfy(335,26): Error: function precondition could not be proved Fuel.legacy.dfy(324,21): Related location Fuel.legacy.dfy(314,46): Related location Fuel.legacy.dfy(335,26): Error: function precondition could not be proved Fuel.legacy.dfy(324,21): Related location -Fuel.legacy.dfy(312,43): Related location +Fuel.legacy.dfy(314,72): Related location Fuel.legacy.dfy(335,26): Error: function precondition could not be proved Fuel.legacy.dfy(324,21): Related location -Fuel.legacy.dfy(312,58): Related location +Fuel.legacy.dfy(314,93): Related location Fuel.legacy.dfy(335,49): Error: destructor 't' can only be applied to datatype values constructed by 'VTuple' Fuel.legacy.dfy(335,50): Error: index out of range Fuel.legacy.dfy(336,38): Error: index out of range @@ -46,16 +46,16 @@ Fuel.legacy.dfy(329,21): Related location Fuel.legacy.dfy(312,43): Related location Fuel.legacy.dfy(336,45): Error: function precondition could not be proved Fuel.legacy.dfy(329,21): Related location -Fuel.legacy.dfy(314,72): Related location +Fuel.legacy.dfy(313,41): Related location Fuel.legacy.dfy(336,45): Error: function precondition could not be proved Fuel.legacy.dfy(329,21): Related location -Fuel.legacy.dfy(314,93): Related location +Fuel.legacy.dfy(312,58): Related location Fuel.legacy.dfy(336,45): Error: function precondition could not be proved Fuel.legacy.dfy(329,21): Related location -Fuel.legacy.dfy(313,41): Related location +Fuel.legacy.dfy(314,72): Related location Fuel.legacy.dfy(336,45): Error: function precondition could not be proved Fuel.legacy.dfy(329,21): Related location -Fuel.legacy.dfy(312,58): Related location +Fuel.legacy.dfy(314,93): Related location Fuel.legacy.dfy(336,71): Error: index out of range Fuel.legacy.dfy(397,22): Error: assertion might not hold Fuel.legacy.dfy(398,22): Error: assertion might not hold diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/SubsetTypes.dfy.expect b/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/SubsetTypes.dfy.expect index 69fdfc5c714..7890ca1c5ff 100644 --- a/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/SubsetTypes.dfy.expect +++ b/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/SubsetTypes.dfy.expect @@ -91,5 +91,5 @@ SubsetTypes.dfy(459,15): Error: assertion might not hold SubsetTypes.dfy(464,13): Error: assertion might not hold Dafny program verifier finished with 13 verified, 91 errors -Total resources used is 738370 +Total resources used is 738020 Max resources used by VC is 67520 diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny1/SchorrWaite.dfy b/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny1/SchorrWaite.dfy index 1ba97fbbe11..103443605ef 100644 --- a/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny1/SchorrWaite.dfy +++ b/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny1/SchorrWaite.dfy @@ -166,7 +166,7 @@ ghost predicate ReachableVia(source: Node, older p: Path, sink: Node, S: set n in S && sink in n.children && ReachableVia(source, prefix, n, S) } -method SchorrWaite(root: Node, ghost S: set) +method {:isolate_assertions} SchorrWaite(root: Node, ghost S: set) requires root in S // S is closed under 'children': requires forall n :: n in S ==> @@ -262,18 +262,13 @@ method SchorrWaite(root: Node, ghost S: set) if p == null { return; } - assert {:split_here} true; var oldP := p.children[p.childrenVisited]; p.children := p.children[p.childrenVisited := t]; - assert {:split_here} true; t := p; p := oldP; stackNodes := stackNodes[..|stackNodes| - 1]; - assert {:split_here} true; t.childrenVisited := t.childrenVisited + 1; path := t.pathFromRoot; - assert {:split_here} true; - } else if t.children[t.childrenVisited] == null || t.children[t.childrenVisited].marked { assert {:focus} true; // just advance to next child diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny1/SchorrWaite.dfy.expect b/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny1/SchorrWaite.dfy.expect index f75e2c47c50..c97911df812 100644 --- a/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny1/SchorrWaite.dfy.expect +++ b/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny1/SchorrWaite.dfy.expect @@ -1,4 +1,4 @@ -Dafny program verifier finished with 19 verified, 0 errors -Total resources used is 36712308 -Max resources used by VC is 24415515 +Dafny program verifier finished with 272 verified, 0 errors +Total resources used is 33995995 +Max resources used by VC is 4344173 diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny1/SchorrWaite.dfy.refresh.expect b/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny1/SchorrWaite.dfy.refresh.expect index 359b55e55f3..a5d11a8c0b8 100644 --- a/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny1/SchorrWaite.dfy.refresh.expect +++ b/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny1/SchorrWaite.dfy.refresh.expect @@ -1,4 +1,4 @@ -Dafny program verifier finished with 19 verified, 0 errors -Total resources used is 24189140 -Max resources used by VC is 13054890 +Dafny program verifier finished with 276 verified, 0 errors +Total resources used is 32464776 +Max resources used by VC is 2154535 diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-2026.dfy b/Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-2026.dfy index 9c250624fb8..9c6c1ff274d 100644 --- a/Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-2026.dfy +++ b/Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-2026.dfy @@ -15,8 +15,8 @@ method foo(n: nat) returns (ret: array) var i := 0; while i < n - 1 invariant 0 <= i < n - invariant forall j :: 0 <= j < i ==> j % 2 == 0 ==> ret[j] == "even" invariant forall j :: 0 <= j < i ==> j % 2 == 1 ==> ret[j] == "odd" + invariant forall j :: 0 <= j < i ==> j % 2 == 0 ==> ret[j] == "even" { if i % 2 == 0 { ret[i] := "odd"; diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-2026.dfy.expect b/Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-2026.dfy.expect index cad8bc15090..83094f7432c 100644 --- a/Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-2026.dfy.expect +++ b/Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-2026.dfy.expect @@ -1,4 +1,4 @@ -git-issue-2026.dfy(18,18): Error: this invariant could not be proved to be maintained by the loop +git-issue-2026.dfy(19,18): Error: this invariant could not be proved to be maintained by the loop Related message: loop invariant violation Related counterexample: WARNING: the following counterexample may be inconsistent or invalid. See dafny.org/dafny/DafnyRef/DafnyRef#sec-counterexamples diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/server/counterexample_commandline.dfy.expect b/Source/IntegrationTests/TestFiles/LitTests/LitTest/server/counterexample_commandline.dfy.expect index 1a0deba5dfa..e13eaa030b7 100644 --- a/Source/IntegrationTests/TestFiles/LitTests/LitTest/server/counterexample_commandline.dfy.expect +++ b/Source/IntegrationTests/TestFiles/LitTests/LitTest/server/counterexample_commandline.dfy.expect @@ -4,13 +4,13 @@ counterexample_commandline.dfy(31,20): Error: a postcondition could not be prove Temporary variables to describe counterexamples: ghost var counterexampleLoopGuard0 : bool := false; counterexample_commandline.dfy(21,8): initial state: - assume this != null && |this.p| > 0 && |s| > 0 && 1 == |s| && '\U{0002}' == s[0] && 1 == |this.p| && '?' == this.p[0]; + assume this != null && |this.p| > 0 && |s| > 0 && 1 == |s| && '\0' == s[0] && 1 == |this.p| && '?' == this.p[0]; counterexample_commandline.dfy(22,22): - assume this != null && |this.p| > 0 && |s| > 0 && 1 == |s| && '\U{0002}' == s[0] && false == b && 1 == |this.p| && '?' == this.p[0]; + assume this != null && |this.p| > 0 && |s| > 0 && 1 == |s| && '\0' == s[0] && false == b && 1 == |this.p| && '?' == this.p[0]; counterexample_commandline.dfy(23,22): - assume this != null && |this.p| > 0 && |s| > 0 && 1 == |s| && '\U{0002}' == s[0] && false == b && 0 == i && '?' == this.p[0] && 1 == |this.p|; + assume this != null && |this.p| > 0 && |s| > 0 && 1 == |s| && '\0' == s[0] && false == b && 0 == i && '?' == this.p[0] && 1 == |this.p|; counterexample_commandline.dfy(24,12): after some loop iterations: - counterexampleLoopGuard0 := this != null && |this.p| > 0 && |s| > 0 && 1 == |s| && '\U{0002}' == s[0] && false == b && 0 == i && '?' == this.p[0] && 1 == |this.p|; + counterexampleLoopGuard0 := this != null && |this.p| > 0 && |s| > 0 && 1 == |s| && '\0' == s[0] && false == b && 0 == i && '?' == this.p[0] && 1 == |this.p|; counterexample_commandline.dfy(18,22): Related location: this is the postcondition that could not be proved diff --git a/docs/dev/news/5621.feat b/docs/dev/news/5621.feat new file mode 100644 index 00000000000..0c7705f9a5e --- /dev/null +++ b/docs/dev/news/5621.feat @@ -0,0 +1,41 @@ +New feature: model extractor + +### CLI option + +The `dafny verify` command now has an option `--extract:`, where (just like for the various print options) `` is allowed to be `-` to denote standard output. + +### Extract mechanism + +Upon successful verification, the new extract mechanism visits the AST of the given program. For any module marked with `{:extract}`, the extract-worthy material from the module is output. The output declarations will be in the same order as they appear textually in the module (in particular, the fact that module-level Dafny declarations are collected in an internal class `_default` has no bearing on the output order). + +Three kinds of declarations are extract-worthy: + +* A type declaration `A` that bears an attribute `{:extract_name B}` is extracted into a Boogie type declaration `type B _ _ _;`. + + The definition of the type is ignored. (The intended usage for an extracted type is that the Dafny program give a definition for the type, which goes to show the existence of such a type.) + +* A function declaration `F(x: X, y: Y): Z` that bears an attribute `{:extract_name G}` is extracted into a Boogie function declaration `function G(x: X, y: Y): Z;`. + + The body of the Dafny function is ignored. (The intended usage for an extracted function is that the Dafny program give a definition for the function, which goes to show the existence of such a function.) + +* A lemma declaration `L(x: X, y: Y) requires P ensures Q` that bears an attribute `{:extract_pattern ...}` or an attribute `{:extract_used_by ...}` is extracted into a Boogie `axiom`. The axiom has the basic form `axiom (forall x: X, y: Y :: P ==> Q);`. + + If the lemma has an attribute `{:extract_used_by F}`, then the axiom will be emitted into the `uses` clause of the Boogie function generated for Dafny function `F`. + + If the lemma has no in-parameters, the axiom is just `P ==> Q`. + + If the lemma has in-parameters, then any attribute `{:extract_pattern E, F, G}` adds a matching pattern `{ E, F, G }` to the emitted quantifier. Also, any attribute `{:extract_attribute "name", E, F, G}` adds an attribute `{:name E, F, G}` to the quantifier. + +### Expressions + +The pre- and postconditions of extracted lemmas turn into analogous Boogie expressions, and the types of function/lemma parameters and bound variables are extracted into analogous Boogie types. The intended usage of the extract mechanism is that these expressions and types do indeed have analogous Boogie types. + +At this time, only a limited set of expressions and types are supported, but more can be added in the future. + +Any `forall` and `exists` quantifiers in expressions are allowed to use `:extract_pattern` and `:extract_attribute` attributes, as described above for lemmas. + +Some extracted expressions are simplified. For example, `true && !!P` is simplified to `P`. + +### Soundness + +The Dafny program that is used as input for the extraction is treated like any other Dafny program. The intended usage of the extraction mechanism is to prove parts of the axiomatization in `DafnyPrelude.bpl` to be logically consistent. Whether or not the extracted Boogie declarations meet this goal depends on the given Dafny program. For example, if the given Dafny program formalizes sequences in terms of maps and formalizes maps in terms of sequences, then the extraction probably does not provide guarantees of consistency.