Encode unknown generic type parameters with `(declare-forall-sort)` - #93

Draft

coeff-aij wants to merge 154 commits into

coord-e:mainfrom

coeff-aij:forall-sort

Commits on Jun 8, 2026

add: ForallSort
coeff-aij
committed
4eae892
change: translate param type using ForallSortIdx
coeff-aij
committed
2e330a3
change: translate Type::Param into chc::Sort::Forall
coeff-aij
committed
f95cfde
change: use forall sort instead of deferred type
coeff-aij
committed
debaa61
add: output (define-forall-sort)
coeff-aij
committed
03d7932
fix: duplication of ForallSortIdx for the same parameter
coeff-aij
committed
0d47cc8
add test cases using unknown type parameters with trait bounds
coeff-aij
committed
4e35b61
change: use DeferredType for generic functions without requires/ensures
coeff-aij
committed
2ef31cb
change: prevent overwriting concrete types with deferred types
coeff-aij
committed
f42debf
change: disable DeferredType completely
coeff-aij
committed
0a2cc17
remove all extern_spec in std.rs temporarily
coeff-aij
committed
dc9b0e9
add: imcomplete support for alias types
coeff-aij
committed
6d82bfb
change: use Type::Param and chc::Sort::Forall for type prameters
coeff-aij
committed
a0df8dc
add: ForallPred represents unresolved user-defined predicates
coeff-aij
committed
85d9e01
change: replace unresolved user-defined predicates with ForallPred
coeff-aij
committed
4d381fc
fix: distinguish different type parameters in subtyping
coeff-aij
committed
14170e7
change: store the def_id of the corresponding function in TypeBuilder
coeff-aij
committed
6ee71de
fix: identify type parameters using the DefId of the owner(e.g. `fn f<T>` for `T` in the body)
coeff-aij
committed
6c8add1
fix: wrong conditionals to insert forall predicates
coeff-aij
committed
af226a4
fix: normalize thrust::Model::Ty
coeff-aij
committed
3888011
fix: propagate the DefId for the owner function of formula_fn and
coeff-aij
committed
968a4a7
fix: use both TypeParamIdx and ForallSortIdx for type parameters
coeff-aij
committed
87969f2
add: insert declarations of universally quantified predicate variables
coeff-aij
committed
2855cc5
add: analyze and output dependencies between predicates
coeff-aij
committed
8127496
add: translate alias type into forall sort
coeff-aij
committed
23187ce
add: tests for unknown type parameters
coeff-aij
committed
01f9f6c
fix: propagate owner_fn_id of type parameters
coeff-aij
committed
743bcda
add: debug print for AliasTy
coeff-aij
committed
d5cdefb
fix: propagate owner_fn_id of type parameters
coeff-aij
committed
0dc245d
add: translate <ParamTy as Model>::Ty into ParamTy
coeff-aij
committed
5d50264
add: register_generic_def() for substitution of generic args from call
coeff-aij
committed
516cbd5
fix: instantiate generic type parameters contained in args of predicate
coeff-aij
committed
6de74be
add: distinguish calls of forall-predicates with different type
coeff-aij
committed
b921e2c
fix: skip expected_ty() for trait methods without MIR body
coeff-aij
committed
59f401c

Commits on Jun 9, 2026

change: try to bypass the instantiation of unknown generic args on
coeff-aij
committed
e4ed770

Commits on Jun 11, 2026

Commits on Jun 12, 2026

Commits on Jun 13, 2026

Commits on Jun 14, 2026

add: opaque type handling for Box and Vec
coeff-aij
committed
c4cb3bc
fix: use try_normalize_erasing_regions to avoid panic
coeff-aij
committed
b6db754
fix: relax &mut restriction to allow any element type
coeff-aij
committed
b1ad064
revert: commenting out most of extern_spec in std.rs
coeff-aij
committed
2077ab7
add: annotations for fold() (WIP)
coeff-aij
committed
92764b7
Merge branch 'main' into forall-sort
coeff-aij
committed
7fc03cd
fix annotations on fold() (WIP)
coeff-aij
committed
312f362
add test codes for reproducing/avoiding annotation errors
coeff-aij
committed
848f511

Commits on Jun 15, 2026

fix: annotations on fold()
coeff-aij
committed
555106e

Commits on Jun 17, 2026

fix: incorrect signature and duplication of ForallPred
coeff-aij
committed
9d1db19
Merge branch 'main' into forall-sort
coeff-aij
committed
7675b06

Commits on Jun 20, 2026

Merge branch 'main' into forall-sort
coeff-aij
committed
20349c1
fix: propagete owner_fn_id to AnnotFnTranslator
coeff-aij
committed
77a562e
fix: runtime error with borrowing RefCell
coeff-aij
committed
9027871
add: translate AliasTy with TemplateTypeBuilder
coeff-aij
committed
164e771
change: use deferred type for generic functions whose annotations and
coeff-aij
committed
3bafc78
fix: wrong abi for closure
coeff-aij
committed
481829f

Commits on Jun 24, 2026

fix: insert ForallPred for the last argument of closure
coeff-aij
committed
45d0bc4
add: positive test cases for traits
coeff-aij
committed
9eac0a5
Merge branch 'main' into forall-sort
coeff-aij
committed
8f6e2fb

Commits on Jun 25, 2026

Commits on Jun 26, 2026

fix: try to normalize alias projections and allocate the same
coeff-aij
committed
7595088
fix: use impl block's DefId for recognition of type parameters in impl<T>
coeff-aij
committed
e27f7ad
change: use GenericDefTy for unannotated generic functions
coeff-aij
committed
2b696ce
remove: instantiation which breaks alias types which are already
coeff-aij
committed
083f312
add: gather closure param type from parent impl block
coeff-aij
committed
d4252d9
fix: unboxing ForallPred
coeff-aij
committed
018444c
fix: replace commas and whitespaces contained in `Map<I, F>` as
coeff-aij
committed
2458b2e

Commits on Jun 27, 2026

Commits on Jun 28, 2026

Commits on Jul 5, 2026

Merge branch 'main' into forall-sort
coeff-aij
committed
57dbc0d

Commits on Aug 16, 2026

Merge branch 'main' into forall-sort
coeff-aij
committed
3db3950
tests: configure extended CoAR solver
coeff-aij
committed
e2a2d43
fix: include caller in generic type cache keys
coeff-aij
committed
5b2d3bf
improve forall sort type formatting
coeff-aij
committed
e18fba1
test: cover forall sort type formatting
coeff-aij
committed
7993e4b
fix: handle singleton refinement values
coeff-aij
committed
ceb4d03
fix: add forall sort default values
coeff-aij
committed
5eef717
fix: handle unresolved trait method calls
coeff-aij
committed
015bda2
test: specify trait update invariant
coeff-aij
committed
6457860
tests: configure solver for remaining polymorphic cases
coeff-aij
committed
1d814ff

Commits on Aug 25, 2026

Merge branch 'main' into forall-sort
coeff-aij
committed
267233d

Commits on Aug 30, 2026

Merge branch 'main' into forall-sort
coeff-aij
committed
9e49de6
Rename ResolvedCallable::Closure to Concrete
coeff-aij
committed
cf01d7b
test: add solver configuration environmental variables
coeff-aij
committed
bb83b7b

Commits on Sep 2, 2026

add: test for impl and generic function using trait
coeff-aij
committed
5094a69

Commits on Sep 4, 2026

Merge branch 'main' into forall-sort
coeff-aij
committed
ce6bcae

Commits on Sep 5, 2026

Replace invariant_context with context in annot_simple_loop_self.rs

coeff-aij
and
claude
committed
50f63ef
Add fail counterparts for the pass/traits tests

coeff-aij
and
claude
committed
fb6dff0
Add probe tests for the language features used by iterator adapters

coeff-aij
and
claude
committed
ebfa167

Commits on Sep 6, 2026

Mark the match-&mut probes as passing with the rebuilt PCSat

coeff-aij
and
claude
committed
cbf05cf
Find closure bounds declared on the enclosing impl or trait

coeff-aij
and
claude
committed
1b59fcf
Declare the sorts used only in forall and user-defined predicate signatures

coeff-aij
and
claude
committed
8bb1439
Resolve trait predicate calls on concrete types in non-generic functions

coeff-aij
and
claude
committed
4b4f0ac
Fix the simple_loop_call_multi.rs example and add its fail twin

coeff-aij
and
claude
committed
1707162
Merge branch 'fix/concrete-trait-pred-in-nongeneric-fn' into forall-sort
coeff-aij
committed
8bfbcfc
Fix simple_loop_self_mut.rs and add the simple_loop_self fail twins

coeff-aij
and
claude
committed
622b67e

Commits on Sep 8, 2026

Drop the probe_ prefix from the adapter feature tests

coeff-aij
and
claude
committed
323a3b8
Pin impl predicate resolution on a generic ADT from a generic owner

coeff-aij
and
claude
committed
d7ddf81
Regenerate the predicate hashes broken by dropping the probe_ prefix

coeff-aij
and
claude
committed
7828fb1
Trim the comments of the adapter feature tests

coeff-aij
and
claude
committed
cfcb2c5
Merge branch 'main' into forall-sort
coeff-aij
committed
b748267
Drop the annotation-error probe tests

coeff-aij
and
claude
committed
af978e4
Add the fold_noloop, id, and take adapter test pairs

coeff-aij
and
claude
committed
e4acd6a
Lower `Ghost<T>` through its content instead of trait normalization

coeff-aij
and
claude
committed
56219a2
Add the annotated variants of the two-loop trait tests

coeff-aij
and
claude
committed
1e4deb1
Add the annotated variants of the fixed-filter tests

coeff-aij
and
claude
committed
26bf976
fix: track generic fn call results by re-analyzing bodies at concrete args
coeff-aij
committed
d4ddb53
Note what ties a generic body's re-analysis to its caller

coeff-aij
and
claude
committed
5b9d65e
Pin how a generic function's contract reaches a generic caller

coeff-aij
and
claude
committed
8acdcdc

Commits on Sep 9, 2026

Declare the forall default an empty array references

coeff-aij
and
claude
committed
9301494
Keep a `Self::Assoc` projection resolvable when lifted out of a trait impl

coeff-aij
and
claude
committed
c0cfee5
Resolve an impl's closure type parameter at the caller's arguments

coeff-aij
and
claude
committed
79c5315
Let an `FnMut` precondition name the closure's current upvars

coeff-aij
and
claude
committed
09d408e
Adopt the ghost-history test pairs from iterator-adapters

coeff-aij
and
claude
committed
1ae7725
Break the item_ok propagation in ghost_produced's fail twin

coeff-aij
and
claude
committed
c702e41

Commits on Sep 10, 2026

Check a trait postcondition at the impl, not in the default body

coeff-aij
and
claude
committed
1128385