@@ -453,7 +453,7 @@ def test_match_body_is_tier3(self) -> None:
453453 assert result .summary .tier1_verified >= 2
454454
455455 def test_recursive_call_is_tier3 (self ) -> None :
456- """Recursive function bodies can't be translated to Z3 ."""
456+ """Recursive functions still have Tier 3 for decreases ."""
457457 result = _verify ("""
458458fn factorial(@Nat -> @Nat)
459459 requires(true)
@@ -465,7 +465,7 @@ def test_recursive_call_is_tier3(self) -> None:
465465 else { @Nat.0 * factorial(@Nat.0 - 1) }
466466}
467467""" )
468- # ensures(@Nat.result >= 1) — body has recursive call → Tier 3
468+ # ensures(@Nat.result >= 1) — now Tier 1 via modular verification
469469 # decreases — always Tier 3 for now
470470 assert result .summary .tier3_runtime >= 1
471471
@@ -576,7 +576,8 @@ def test_mixed_tiers(self) -> None:
576576}
577577""" )
578578 # requires(true) → Tier 1 trivial
579- # ensures with recursive body → Tier 3
579+ # ensures — now Tier 1 via modular verification (recursive call
580+ # returns fresh Nat var with assumed postcondition)
580581 # decreases → Tier 3
581582 assert result .summary .total >= 3
582583 assert result .summary .tier1_verified >= 1
@@ -652,3 +653,242 @@ def test_boolean_logic_in_contract(self) -> None:
652653 effects(pure)
653654{ @Int.0 }
654655""" )
656+
657+
658+ # =====================================================================
659+ # Call-site precondition verification (C6b)
660+ # =====================================================================
661+
662+ class TestCallSiteVerification :
663+ """Modular verification: callee preconditions checked at call sites."""
664+
665+ def test_call_satisfied_precondition (self ) -> None :
666+ """Calling with a literal that satisfies requires(@Int.0 != 0)."""
667+ _verify_ok ("""
668+ fn non_zero(@Int -> @Int)
669+ requires(@Int.0 != 0)
670+ ensures(true)
671+ effects(pure)
672+ { @Int.0 }
673+
674+ fn caller(@Unit -> @Int)
675+ requires(true)
676+ ensures(true)
677+ effects(pure)
678+ { non_zero(1) }
679+ """ )
680+
681+ def test_call_violated_precondition (self ) -> None :
682+ """Calling with literal 0 violates requires(@Int.0 != 0)."""
683+ _verify_err ("""
684+ fn non_zero(@Int -> @Int)
685+ requires(@Int.0 != 0)
686+ ensures(true)
687+ effects(pure)
688+ { @Int.0 }
689+
690+ fn bad_caller(@Unit -> @Int)
691+ requires(true)
692+ ensures(true)
693+ effects(pure)
694+ { non_zero(0) }
695+ """ , "precondition" )
696+
697+ def test_call_precondition_forwarded (self ) -> None :
698+ """Caller's precondition implies callee's — passes."""
699+ _verify_ok ("""
700+ fn non_zero(@Int -> @Int)
701+ requires(@Int.0 != 0)
702+ ensures(true)
703+ effects(pure)
704+ { @Int.0 }
705+
706+ fn safe_caller(@Int -> @Int)
707+ requires(@Int.0 != 0)
708+ ensures(true)
709+ effects(pure)
710+ { non_zero(@Int.0) }
711+ """ )
712+
713+ def test_call_postcondition_assumed (self ) -> None :
714+ """Caller's ensures relies on callee's postcondition."""
715+ _verify_ok ("""
716+ fn succ(@Int -> @Int)
717+ requires(true)
718+ ensures(@Int.result == @Int.0 + 1)
719+ effects(pure)
720+ { @Int.0 + 1 }
721+
722+ fn add_two(@Int -> @Int)
723+ requires(true)
724+ ensures(@Int.result == @Int.0 + 2)
725+ effects(pure)
726+ { succ(succ(@Int.0)) }
727+ """ )
728+
729+ def test_recursive_call_uses_postcondition (self ) -> None :
730+ """Recursive factorial: ensures(@Nat.result >= 1) now Tier 1.
731+
732+ The postcondition is assumed at the recursive call site,
733+ and base case returns 1, so result >= 1 is provable.
734+ """
735+ result = _verify ("""
736+ fn factorial(@Nat -> @Nat)
737+ requires(true)
738+ ensures(@Nat.result >= 1)
739+ decreases(@Nat.0)
740+ effects(pure)
741+ {
742+ if @Nat.0 == 0 then { 1 }
743+ else { @Nat.0 * factorial(@Nat.0 - 1) }
744+ }
745+ """ )
746+ errors = [d for d in result .diagnostics if d .severity == "error" ]
747+ assert errors == [], f"Expected no errors, got: { [e .description for e in errors ]}
748+ # ensures now Tier 1 (modular verification), decreases still Tier 3
749+ assert result .summary .tier1_verified >= 2
750+
751+ def test_call_trivial_precondition (self ) -> None :
752+ """Callee with requires(true) — always satisfied."""
753+ _verify_ok ("""
754+ fn id(@Int -> @Int)
755+ requires(true)
756+ ensures(@Int.result == @Int.0)
757+ effects(pure)
758+ { @Int.0 }
759+
760+ fn caller(@Int -> @Int)
761+ requires(true)
762+ ensures(@Int.result == @Int.0)
763+ effects(pure)
764+ { id(@Int.0) }
765+ """ )
766+
767+ def test_call_in_let_binding (self ) -> None :
768+ """Call result used via let binding, passed to second call."""
769+ _verify_ok ("""
770+ fn succ(@Int -> @Int)
771+ requires(true)
772+ ensures(@Int.result == @Int.0 + 1)
773+ effects(pure)
774+ { @Int.0 + 1 }
775+
776+ fn add_two_let(@Int -> @Int)
777+ requires(true)
778+ ensures(@Int.result == @Int.0 + 2)
779+ effects(pure)
780+ {
781+ let @Int = succ(@Int.0);
782+ succ(@Int.0)
783+ }
784+ """ )
785+
786+ def test_where_block_call (self ) -> None :
787+ """Call to a where-block helper function."""
788+ _verify_ok ("""
789+ fn outer(@Int -> @Int)
790+ requires(true)
791+ ensures(@Int.result == @Int.0 + 1)
792+ effects(pure)
793+ { helper(@Int.0) }
794+ where {
795+ fn helper(@Int -> @Int)
796+ requires(true)
797+ ensures(@Int.result == @Int.0 + 1)
798+ effects(pure)
799+ { @Int.0 + 1 }
800+ }
801+ """ )
802+
803+ def test_generic_call_falls_to_tier3 (self ) -> None :
804+ """Calls to generic functions bail to Tier 3."""
805+ result = _verify ("""
806+ forall<T>
807+ fn id(@T -> @T)
808+ requires(true)
809+ ensures(@T.result == @T.0)
810+ effects(pure)
811+ { @T.0 }
812+
813+ fn caller(@Int -> @Int)
814+ requires(true)
815+ ensures(true)
816+ effects(pure)
817+ { id(@Int.0) }
818+ """ )
819+ # id's contracts → Tier 3 (generic)
820+ # caller's body has generic call → body_expr is None
821+ # Since caller's ensures is trivial, it doesn't matter
822+ assert result .summary .tier3_runtime >= 1
823+
824+ def test_multiple_preconditions_all_checked (self ) -> None :
825+ """Two requires on callee, second one violated."""
826+ _verify_err ("""
827+ fn guarded(@Int -> @Int)
828+ requires(@Int.0 > 0)
829+ requires(@Int.0 < 100)
830+ ensures(true)
831+ effects(pure)
832+ { @Int.0 }
833+
834+ fn bad_caller(@Int -> @Int)
835+ requires(@Int.0 > 0)
836+ ensures(true)
837+ effects(pure)
838+ { guarded(@Int.0) }
839+ """ , "precondition" )
840+
841+ def test_precondition_via_caller_requires (self ) -> None :
842+ """Caller's requires forwards two constraints to satisfy callee."""
843+ _verify_ok ("""
844+ fn guarded(@Int -> @Int)
845+ requires(@Int.0 > 0)
846+ requires(@Int.0 < 100)
847+ ensures(true)
848+ effects(pure)
849+ { @Int.0 }
850+
851+ fn good_caller(@Int -> @Int)
852+ requires(@Int.0 > 0)
853+ requires(@Int.0 < 100)
854+ ensures(true)
855+ effects(pure)
856+ { guarded(@Int.0) }
857+ """ )
858+
859+ def test_multiple_calls_in_sequence (self ) -> None :
860+ """Two calls in sequence, each gets a fresh return variable."""
861+ _verify_ok ("""
862+ fn inc(@Int -> @Int)
863+ requires(true)
864+ ensures(@Int.result == @Int.0 + 1)
865+ effects(pure)
866+ { @Int.0 + 1 }
867+
868+ fn add_two_seq(@Int -> @Int)
869+ requires(true)
870+ ensures(@Int.result == @Int.0 + 2)
871+ effects(pure)
872+ {
873+ let @Int = inc(@Int.0);
874+ inc(@Int.0)
875+ }
876+ """ )
877+
878+ def test_violation_error_mentions_callee_name (self ) -> None :
879+ """Error message includes the callee function name."""
880+ errors = _verify_err ("""
881+ fn non_zero(@Int -> @Int)
882+ requires(@Int.0 != 0)
883+ ensures(true)
884+ effects(pure)
885+ { @Int.0 }
886+
887+ fn bad(@Int -> @Int)
888+ requires(true)
889+ ensures(true)
890+ effects(pure)
891+ { non_zero(0) }
892+ """ , "precondition" )
893+ # Check that the error mentions the callee name
894+ assert any ("non_zero" in e .description for e in errors )
0 commit comments