<commit_before><commit_msg>SDGSimple passes<commit_after>{-@ LIQUID "--reflection"     @-}
{-@ LIQUID "--ple"            @-}
{-@ LIQUID "--no-termination" @-}

module SGDSimple where

{-@ relational update ~ update :: x1:_ -> _ ~ x2:_ -> _ ~~ x1 < x2 => r1 x1 < r2 x2 @-}
update :: Int -> Int
update x = x + 1

-- TODO: add x1 x2 to the env
-- TODO: support fo precs for functions
{-@ relational bind ~ bind :: x1:_ -> f1:(z1:_ -> _) -> _ 
                            ~ x2:_ -> f2:(z2:_ -> _) -> _ 
                           ~~ x1 < x2 => (z1 < z2 => r1 < r2) => r1 x1 f1 < r2 x2 f2 @-}
bind :: Int -> (Int -> Int) -> Int
bind x f = f x

{-@ relational bind1 ~ bind1 :: x1:_ -> _ 
                              ~ x2:_ -> _
                             ~~ x1 < x2 => r1 x1 < r2 x2 @-}
bind1 :: Int -> Int
bind1 x = x + 1

{-@ relational choice ~ choice :: x1:_ -> _ ~ x2:_ -> _ ~~ x1 < x2 => r1 < r2 @-}
choice :: Int -> Int
choice x = x + 1 

{-@ relational sgd ~ sgd :: x1:_ -> _ ~ x2:_ -> _ ~~ x1 < x2 => r1 x1 < r2 x2 @-}
sgd :: Int -> Int
sgd x = choice (bind x update)

{'fraction_non_alphanumeric': 0.19813953488372094, 'fraction_numerical': 0.053023255813953486, 'mean_word_length': 1.5927710843373495, 'pattern_counts': {'":': 0, '<': 15, '<?xml version=': 0, '>': 31, 'https://': 0, 'lorem ipsum': 0, 'www.': 0, 'xml': 0}, 'pii_count': 0, 'substrings_counts': 0, 'word_list_counts': {'cursed_substrings.json': 0, 'profanity_word_list.json': 0, 'sexual_word_list.json': 0, 'zh_pornsignals.json': 0}}
{'dir': 'git-commits-cleaned', 'id': '2627621', 'n_tokens_mistral': 429, 'n_tokens_neox': 414, 'n_words': 125}