New Pure Function Encoding by jaspergeer · Pull Request #163 · Aurel300/prusti-dev

jaspergeer · 2026-03-28T00:56:06Z

This PR re-implements the encoding of pure functions. It solves two problems:

Previously, we were verifying both the impure encoding and pure encoding of each function. It was possible that the impure encoding verified while the pure encoding did not.
Functions on references to recursive data structures would not be unfolded along with their argument's referent, causing programs to fail to verify without extra annotation.

Changes

There are changes to existing encoders in this PR:

TyPure now generates a trig function for every type, which takes a snapshot and returns a boolean.
TyUsePure's interface exposes some utility functions for calling trig functions.
MirLocalDefEnc also generates a trig function application. For ADTs, this applies the type's trig function to the local's snapshot. For Refs, this applies the referent type's trig function to the referent's snapshot.
MirImpure emits, when encoding a place, inhales of trig applications for that place and any projections whose type is an ADT. When encoding an Aggregate rvalue, an instance of trig applied to the snapshot of the aggregate value is emitted.
FunctionEnc now encodes functions using a manual axiomatization, which is described in the next section.

This PR adds some tests:

verify/pass/pure-fn/list-enum.rs
verify/pass/pure-fn/list-enum-poly.rs
verify/pass/pure-fn/pure-spec.rs
verify/fail/pure-fn/list-enum-fail.rs
verify/fail/pure-fn/pure-spec-fail.rs

The first two tests fail to verify in the current version of Prusti because they rely on function definitions being unfolded alongside the referent of an argument. The second two tests exist as a smoke test for soundness bugs.

In addition, the following were moved to tests:

tests_old/verify/fail/demos/append-sorted-error-{1,2,4}.rs
tests_old/verify/pass/demos/append-sorted.rs passes

Design

The encoding of a pure function:

#[pure]
#[requires(<pre>)]
#[ensures(<post>)]
f(arg0: T0, ... argn: Tn): Tr 
{
	<body>
}

is as follows:

domain PureFns {
    function unlimited_f(arg0: [T0], ..., argn: [Tn]): [Tr]
	
    function limited_f(arg0: [T0], ..., argn: [Tn]): [Tr]
	
    axiom Defn_f {
        forall arg0: [T0], ..., argn: [Tn] ::
        { unlimited_f(arg0, ..., argn) }
        <arg0-triggers>
        ...
        <argn-triggers>
        unlimited_f(arg0, ..., argn) ==
            [<body>](arg0, ..., argn)
    }
    
    axiom Limited_f {
        forall arg0: [T0], ..., argn: [Tn] ::
        { unlimited_f(arg0, ..., argn) }
        unlimited_f(arg0, ..., argn) == limited_f(arg0, ..., argn)
    }
	
    <trig-fns>
}

function caller_f(arg0: [T0], ..., argn: [Tn]): [Tr]
    requires [<pre>](arg0, ..., argn)
    ensures [ [<post>](arg0, ..., argn, <result>), true ]
{
    unlimited_f(arg0, ..., argn)
}

where:

[T] refers to the snapshot-based encoding of T.

[<body>](arg0, ..., argn) is the pure encoding of <body> with free variable substitutions arg0, ..., argn.
The free variables of a body are the ordered function arguments followed by the 'return place', if it can be referenced.
Note that the pure encoding will be modified to encode recursive calls to f as calls to limited_f.

<trig-fns> contains an opaque function function trig_s_T([T]): Bool for each ADT T.

<argi-triggers> is { limited_f(arg0, ..., argn), trig_s_T(make_concrete_s_T(argi.s_Ref_immutable_1)) } if Ti is an immutable reference type and T is an ADT such that &T = Ti.
<argi-triggers> is { limited_f(arg0, ..., argn), trig_s_Ti(argi) } if Ti is an ADT.
<argi-triggers> is empty otherwise.

Note: here I take the naive approach of triggering on the unfolding of any ADT parameter - if it turns out that this has too much of a performance impact, we could try analyzing type definitions to restrict triggers to recursive types and try analyzing the body of a pure function to identify which parameters are unfolded around a recursive call

[<pre>](arg0, ..., argn) and [<post>](arg0, ..., argn, ret) and [<post>](arg0, ..., argn, <result>) are the pure encodings of <pre> and <post> with free variable substitutions.
Observe that the encoding of the post condition appears inside of an inhale-exhale statement. As a result, Viper will trust that the body of caller_f satisfies the spec.

Impure Encoding

When a pure function f is called from impure code, this is encoded as a call to caller_f.

We inhale instances of trig_s_T for instances of s_T which occur in assignment statement rvalues (they may be projections of the root place).
We also inhale an instance of trig_s_T for the snapshot encoding of Aggregate rvalues, which correspond to ADT constructions.
We also inhale an instance of trig_s_T for the PCG operation RepackExpand.

Aurel300 · 2026-04-10T13:39:08Z

Re: tests, do the tests in the second category mentioned here (the ones which mention "better recursive pure functions") now verify?

jaspergeer · 2026-04-23T22:37:18Z

Re: tests, do the tests in the second category mentioned here (the ones which mention "better recursive pure functions") now verify?

tests_old/verify/fail/demos/append-sorted-error-{1,2,4}.rs all fail correctly
tests_old/verify/pass/demos/append-sorted.rs passes

The remaining 3 cause panics but they do on rewrite-2023 as well.

jaspergeer added 13 commits January 26, 2026 10:07

add test for overflows in pure functions

84a76ac

implement new encoding

08a0fe3

cleanup

484a7d5

implement limited/unlimited

a53d02f

generate valid fns for each adt

7d40bcd

generate valid triggers

81d1b2d

implement triggers (not yet working)

25c0bb6

generate triggers a different way

8706e59

cleanup

b910093

rename to "trig" and generate triggers for places in rvalues

c73f411

generate spec fns

4a75a6d

cleanup, document

ab7a3a9

add tests

f55f3ee

jaspergeer marked this pull request as draft March 28, 2026 00:56

jaspergeer added 13 commits March 27, 2026 18:04

un-modify a test

79cad1e

new overflow test is redundant

40c123e

Merge branch 'rewrite-2023' into pure-fns

d95c0ba

get to compile

5bfe08f

cleanup and small fixes

86c6b97

Merge branch 'rewrite-2023' into pure-fns

e2e0186

appease clippy

2fc9a2c

fix panic when generating triggers

0cb828d

call caller functions in the right places

063ca40

WIP

7089670

add poly tests

8a0b6bc

call caller fn in impure code in trait impls

856cc2b

don't trigger on non-adt args

9a32f1b

jaspergeer force-pushed the pure-fns branch from 55e2a5f to 9a32f1b Compare April 8, 2026 03:52

jaspergeer added 2 commits April 8, 2026 09:10

formatting

3e6b672

move test

01e90c4

inhale trig on RepackExpand

1dc1167

jaspergeer marked this pull request as ready for review April 24, 2026 00:56

jaspergeer marked this pull request as draft April 24, 2026 03:07

jaspergeer added 2 commits April 24, 2026 14:03

emit triggers only on RepackExpand, not Collapse

8c6220a

appease clippy

b135b2c

jaspergeer marked this pull request as ready for review April 24, 2026 21:54

JonasAlaif requested review from Aurel300 and JonasAlaif May 4, 2026 15:12

document fail-tests

ae3577d

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

New Pure Function Encoding#163

New Pure Function Encoding#163
jaspergeer wants to merge 32 commits into
Aurel300:rewrite-2023from
jaspergeer:pure-fns

jaspergeer commented Mar 28, 2026 •

edited

Loading

Uh oh!

Aurel300 commented Apr 10, 2026

Uh oh!

jaspergeer commented Apr 23, 2026 •

edited

Loading

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

2 participants

Conversation

jaspergeer commented Mar 28, 2026 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Changes

Design

Impure Encoding

Uh oh!

Aurel300 commented Apr 10, 2026

Uh oh!

jaspergeer commented Apr 23, 2026 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

2 participants

jaspergeer commented Mar 28, 2026 •

edited

Loading

jaspergeer commented Apr 23, 2026 •

edited

Loading