Advent of Code 2021 day 3 solution in F*

welcome to solving advent of code problems in f-star f-star is a dependently typed language that lets you prove that properties about your program at the same time as you're writing it uh speaking of which i wanted to show the thing that had tripped the solution to the thing that tripped me up last night so um had a problem where i was trying to say that the forward function uh increments the horizontal direction and i could only prove that if i eliminated the depth statement and the reason that was the case is i had neglected to include this condition up here in the preconditions of the function so we've got you know and the argument's the function here and we we put a condition on d that says has to be greater than zero uh this is the return type and the effect and we can say these preconditions have to be true before we can call the function and after we call the function the insurers conditions are true so the state stateful reasoning in f-star uses the state effect which is based on a heap so we just say you know the two variables we need need to be in the heap and the important part i was missing is and they're not the same variable they're not pointers to the same location they don't alias because if they did alias then this function might not increase uh horizontal it might decrease it because aim could be negative um it doesn't know i didn't tell it it couldn't be and so when we put that in when i put that in then the function would would finally type check and this created a little bit of problems because uh the types of these global variables are not specific enough to say that they're not all aliases of each other so i just put it in as an assumption in the start of the program i think the what's part of what's going on here is uh is that uh this is not really the way you're supposed to do things is have global variables and have these functions reference them you're supposed to pass in the references in good functional fashion so maybe there's some way to get around that i tried a couple things but they didn't work but i was i was glad that i was able to you know prove this fairly obvious thing that hey horizontal increases if you add a positive number to it even if you do something else in the meantime so looking forward to what seemingly trivial thing will cause me problems today uh that is part of the fun of learning learning the language we've got about a minute 30 to go so uh thanks to everybody who uh showed up last night in a raid and got very confused uh i also want to thank my employer akita software who is sponsoring advent of code this year we are hiring uh we'd love to to have people who are interested in programming languages join our pl heavy heavy group but i'm a systems person by training so uh we we need uh back-end engineers front-end engineers uh we're looking for a developer advocate i'd love to have you apply there's a there's a link in my my uh on my stream page where you go to uh akita software software dot if i can type ketosoftware.com jobs got about 30 seconds to go i am screen sharing not can make the same mistake twice i am trying a new chat front end that will give me a signal when somebody is chatting so i won't ignore people for for 20 minutes at time either all right here we go [Music] hi gene yes i heard that hi mirdly all right first parameter check is the power consumption okay each bit in the gamma ray can be determined by finding the most common bit in the corresponding position of all numbers in the diagnostic report so it's the it's the majority function majority bitwise function okay so that gives us the gamma rate which we convert to decimal okay the epsilon rate is the least common bit so the the minority function all right so how big is our input uh pretty big all right i think we're gonna do i think we're gonna not just copy it in as a big input we're actually gonna do some some i o today all right so why don't we why don't we start with that copy that and i didn't didn't get set up ahead of time all right all right um module name has to be the same as the file name it's not a very flexible system um let's say we're going to need io uh we're gonna need printf at some points we're gonna need uh [Music] probably this total i don't know yeah let's let's open that uh and we're gonna need string okay so we've got a bit vector type should i use the bit vector where is that going to be completely okay it's got the conversion functions that's good uh map list of booleans to a bit vector that's good uh does it have majority it does not all right let's try using anyway [Music] hello sir skull legend so we're going to say all right so we're going to cheat and look at how long [Music] i'm just going to do everything with length twelve because they're tell me bits we got all right so type uh what did they call this in the description it's a diagnostic yes diagnostic equals bit vector uh okay bit vector dot oh it's b v t v t f all right does that all work it does all right so let's write our function to parse a string into a bit vector um so i am i am learning to code in f-star uh it's it's a new language for me i know pretty other programming languages and work as a software engineer but this is challenging to me uh because it's it's a it's a research language out of microsoft research uh it's got some rough edges uh and you know it's it's a stretch for me it's uh forces me to think about things in a different way all right so let's parse diagnostic let's take a string and the string has to have so this is a refine a refinement type we could just take a string but we'll take only strings where the length of the string is 12. and that still doesn't guarantee that's correct so it's having taken option type to either say did it succeed or did it fail to parse uh and i keep making this mistake i think i need parentheses there all right um um so we should just peel to [Music] map we should just be able to map [Music] a parse function across the list of characters but i then we then how would we tell if they were wrong all right um hmm i mean we could say the string has to only contain two characters but that would be very the two characters we care about but that would be a fairly complicated thing to express uh all right we'll just we'll just loosen up a little bit and say it oh this is not a good choice i can't type that word all right so parse bit uh given a single character becomes a boolean so so if we did so the match syntax lets us do pattern matching uh characters are pretty simple uh no all right it's just normal false uh confusing the f star has two trues and two falses it's got the boolean value false and then the the propositional type true okay these are these are wrong all right now if we try that it's going to complain that we didn't match all the characters and it says the patterns are incomplete the smt couldn't solve or couldn't prove that every character match so we're just we could parse and put an error value all the way through but we'll just say anything else is false i don't know how to tell the autocomplete to go away the emacs mode is very helpful for some things but other things i just haven't figured out yet all right so we should just call our list2bv oops on map par spit so map the parspit function over string it's not string of two list it's it's list of string there it is yes all right does that type check oh length all right it does it's it's happy that um we it it managed to reason that if we start with the string of length 12 and then we map it then that list has the same length and that's the one that lists two to bv so if we use the wrong value uh it won't type check it says i expect hey i expected a list of length 12 and you just gave me some random link list of bulls i'm sorry i can't make the the bottom of the screen all right um so so what we're gonna do is take a uh i'm gonna [Music] look at one of my previous attempts at i o and copy that um so we don't actually care what uh we don't care for part one what order these are in since we're just doing the majority minority so if we reverse it that's that's fine um all right so it's going to take a file descriptor it's open for reading and um sure let's let's uh now let's let's let's write this way so we're going to take a listed diagnostics and return [Music] so i switched effects here these are these functions are both total they always terminate and they don't do any i o ml is on the completely opposite side a function with the ml effect marked can do io can fail to terminate can throw exceptions and we're gonna we're gonna take full use of that except i didn't import that type all right reload our dependencies everything's look good okay uh let rex means where it's recursive uh the arrow is the wrong thing that's for types okay so uh one of the things i didn't find in the tutorial was how to catch exceptions and it turns out it's the uh exactly like you do in in uh ml uh so okay you know camel so f star reads an awful lot like ocam it's got some extra stuff but if you if you ever say i don't know how to do this a good bet is look up how to do it on camel which has much better tutorials a lot more resources and that will give you the clue so so if we need to check this line has the right length so if this length is not equal to 13 uh it'll just fail otherwise we want to parse the rest of the input and [Music] cons this onto the header list which as i said will give us the wrong order but that's okay of course okay so there's a special character for cons we'll use that okay and then to find the end of file is signaled by an exception which is not real uh convenient but we'll just return the list of the list we've been building up and if it's any other error then we'll fill with all right parse i don't know i said parse order there we go uh strewlin of line oh uh okay gotta check the right value and said you gave me a line that wasn't a length 12. there we go so it can tell that if we're in the else clause then this must be true and that's what we required parse diagnostic to get so everything's happy there all right let's we could try this out i'm fairly confident i haven't screwed up yet so let's build our majority and minority functions on the list of bit vectors how we're gonna do this all right let's build something that all right let's build something that takes a list of bulls if we're really fancy we can take the majority and minority at the same time um and let's try to write a fancy type which is usually where i get in trouble uh so this should be a boolean but it should be a special boolean uh let me look at the list documentation effect so we have something that counts it doesn't look like we have anything that counts [Music] [Music] okay so i guess we build that first so what i want to say is uh that the output should so the number of b in input is greater than or equal to [Music] uh is greater than the length of the input divided by two so that's that's what the specification is um the thing that bothers me is can we guarantee that it exists and that's true only if our the length of the list uh is odd otherwise we could split 50 50. this this is looking very complicated let's see how far we get [Music] so we're gonna we're gonna need a helper function that uh no let's let's count them all right so let true count equals number of we haven't written that yet true in the input and let the false count equals the number of false in the input so we'll take we'll take it take two part passes over but all right so if true greater than false count then uh true else false so we could we could just uh we just uh we could just do that sure all right so let's write the function we need so number of and we'll we'll make it a general type but one it has to be a type that uh has equality so a list of a's and the value that's a itself and this returns a natural number uh we should probably if we've been rigorous to find that number but um we'll we'll make do so we're going to match the list and let's be a little fancy here so if the list is uh hmm i don't know how to do this what i want to match is the literal the value that's in v but i'm worried it will bind me to a new variable all right let's be less fancy okay so if there's got to be a way to do that i'm going to i'm going to check the tutorial a second there they're two torturers one that's not all the way written and one that is they've deprecated and made hard to find okay [Music] okay those are all pretty simple yeah we can match any is it copied from oh camel it is okay i mean there's there's the pattern we saw hmm all right let's try it see if it works so the syntax is head tail uh when that's a key word all right looking good when head equals v then it's one plus the number of those in the rest of the list and otherwise uh it's just the number in the rest the list and if we reach the end then it's zero all right let's see if it likes that okay the pound uh says this is in we didn't define this recursive function the pound says this is a aha it says when clauses are not yet supported in verify mode they will be someday oh dear all right i got i gotta copy that for posterity okay i do this the old-fashioned way all right if head equals v uh single equal uh f star also has two equals uh i'll guess to javascript people it's no big loop uh but it's got equals which is an operator and then that does equal equality comparison then it's got double equals which is propositional equality which is something you you prove so if it's single equals it is also double equals but not necessarily the reverse all right all right that type checks uh i keep forgetting the closing curly brace length input i don't know why his emacs has got itself in a bad way for that oh uh what okay it's using the wrong length both string and list define their own length functions we gotta qualify it if number uh do i define this backwards yeah i wanted i wanted to do it this way and that'll number of that in that [Music] uh and so what we're going to have to do uh to prove that this function terminates is say that each time we decrease the length there we go okay okay so it couldn't prove that this return type which is bool matches our fancy type um all right so what do we need to prove that um so what for one thing you know it doesn't know that the true count and the false count because i shouldn't have i'm pretty sure it doesn't know that yes we haven't told it yeah it says i can't i can't prove that so let's prove that with a lemma so lem is just a function in f star uh but a funny function not one that actually gets executed so true and false partition the list so given a list bool and it may be important that it's and [Music] no no we do we don't that's true even if it's even all right so we can say this is a lemma that ensures that number of true nl number of false in l equals all right so how do we prove this uh by induction so if it's an empty list then it's true and we we say the the double print is the unit value it's it's just a singleton type that's the only thing that has unit value and in this contest it basically means figured out yourself so we'll check that it can actually number of that actually okay so it can figure that case out and it says well if you prove it for the other case then you've proved it in general so uh all right the easiest thing to do is just say well can you figure it out from the tail uh which we need to make this a recursive function it can all right we're done all we had to do is tell it hey you use induction and you're done uh it can it can reason from uh our definition of number of and the things it knows about lists uh so we're good all right so now we can add this in as a lemma at added in like it's a function call about our input function and so now that's all we needed all right pretty cool uh so it s3 calls out to a a smt solver it uses z3 and that solver can prove things about simple arithmetic and about this and and it doesn't actually do induction itself but but it it can do it can figure out the induct what the inductive step it what if if we give it uh this piece of information you can say based on that can i prove the thing you wanted me to prove um which is almost as good as it being able to do induct uh induction by itself all right so let's flip everything around here and it's not happy okay uh so it might okay we should uh we need to [Music] all right if it's 5 then this should be 2 but length of input divided by 2 this is euclidean division so it should be oh all right it is less than or equal to there we go all right raw so let's all right what we're actually trying to do we're trying to count we're trying to take our list and apply these to each bit all right so let's do that um so gamma on our list of a list of diagnostic what it was called in the [Music] uh tote stands for uh total um it that means it's uh it's a function so i used it up here you know to say this function is a total function so it's defined on all its inputs it always terminates it doesn't have any side effects so it's a pure and total function uh the reason we have to use it here is because f star does not have effect polymorphism so there's a bunch of list functions that work uh you know like take map and map has to be a total function and there's a separate set that's list dot something else uh what is it sorry this is my home brewed this is my homebrew documentation i i ran the documentation generator i can't just go to the website so there's another one which is just pure uh so tote says i'm using the one that's what works with total functions not the ones that have a weaker condition okay um [Music] okay so we're going to take a list diagnostic and we're going to turn an integer and i'm going to do that by creating a new bit vector oh god i'm not going to get into interranges again in my warm-up i spent like days getting an interrange function work we don't have to be general here we can just hard code it all right so go back to bit vector we're going to take what i want is a 12-way zip i'm not sure that's gonna happen all right but we can build this from the inside out so we're gonna build a new bit vector and we're going to do list2bv on it and that's going to be applying the majority function to all the zeroth bits and then all the one bit and then okay so we're going to do map i'll just put in placeholder there apply majority to everything first to [Music] the list and this is where i'm being really cheesy uh 12 numbers yes uh there's not a built-in range function i was surprised but so this is a list literal of the numbers 0-11 instead okay so those are the index we want and so for each index we're going to [Music] take the majority of the list created by taking the [Music] nth ith element uh of everything in the list so something map something of uh [Music] yeah just of l okay so what's our something i really should break this out let's let's break this out uh what is this operation called so all it's going to be i th element i so let's uh that seems like it should already have a name i'm kind of surprised it doesn't [Music] preview to int into vv tv extension [Music] huh [Music] why doesn't this exist who knows all right so i've got a [Music] a diagnostic and an integer i that is that's a natural number less than 12. we get a bull back so we get the index uh not the string index but the list index of okay what's that defined that's defined as list first so bv to list what's it called bv spv2 list let's hear it for library consistency uh of d i all right does that work that works does this work oh uh we need to do it in the other order so we can curry the function it's a little unfortunate oh did again [Music] oh uh okay and then we need to take our bit vector and we need to turn it into an int okay bv to [Music] it of all that wow field tree i'm gonna have to take a look at this this may be uh where this may be where using bit vectors bites us failed to resolve implicit argument of type position introduced for flex flex quasi okay uh so we can give it its implicit argument so list2bv takes all right it's implicit argument is the length of the list so its length is twelve oh we gotta say pound twelve okay we need to tell it that this list is odd and then it will know the mapped list is also odd so yes this is not well defined if my first [Music] l equals okay all right uh it says it doesn't know that the list is 12 elements long although it should so what we're going to do is we're just going to prove it so we're going to say uh 0 to 11 is a list of natural numbers and the length of our val length of zero to element equals twelve we might have to do a little more work i guess i guess we can't use the freeze the element name i'm at 11. um all right here's what we're gonna do is we're just gonna pack that up but we're going to ask it to prove via normalization which just means expand the expand the definitions until you're done so list.length 2 eleven okay where's our syntax here ah oh oh uh we didn't we didn't put we didn't put the list back in okay that's that's why we're getting the syntax here because i deleted that i should only stick with words i can actually type hmm i've had this problem with a certain arm before is it check things but it doesn't necessarily make them available gosh i'm always surprised by what's the what's the tough part of the night and tonight is proving that the list has 12 elements in it okay uh [Laughter] [Music] all right what if we make it a function it is actually equal to 12 right yeah okay wow [Music] maybe if increasing fuel would actually help here so fuel is how many times it's willing to undo a recursive definition but this should be fine uh because it should be all be given to the solver as one unit all right you know what i'm just i've i've checked it twice even that's not enough wow am i gonna have to pull in int range just so i can define this i mean i got it to work eventually all right uh let's do zero to n and that returns ah i don't care what order they're in either i do care what order i have to preserve the order okay uh i screwed this all up oh all right l is a list of gnats such that n minus one okay so lists all right match all right if n equals one then our list is zero else zero two n one n minus one i just i just feel like this is going to bite bite us because all right let's just build in reverse order which will be easier for it to reason about then we can reverse it else in all right good so let's call this one to zero and then we want to reverse the order tell them please tell me we have reverse all these things you you get used to just having and then all right there's a rev here somewhere there we go reverse okay oh oh we didn't call that here all right well it's not called anywhere n minus one to zero out of 12. all right uh and okay so it's a list of oh this is why i wanted to avoid this okay so it's complaining that our list is not bounded by 12 like it needs to be that the elements of list are not themselves bounded and so we could put in something here that says this is a list of numbers x such that x is less than n but i don't think it's oh it's telling it's telling us we got it wrong uh the top number needs to be n minus one [Music] it says got type in but it should know that if n is greater than zero and it's not zero okay parenthesis wrong uh what am i missing here okay [Music] if that's true then n minus 1 is greater than or equal to zero right n sub one equals n minus one in what uh [Music] okay yeah this is probably ran into before that this list recursively has everything less than or equal to one and all right fine no that's not it which one was it okay it did all this work to prove that okay this is so dumb why am i doing this all right so this this is a bunch of limits to basically prove that everything's in the right range and it has the length that we expect it to have all right so let zero to eleven this returns a list list of numbers all of which are below 12. and that list has has length 12. 0 to 12. oh um all right so this sm tp pat is is supposed to say whenever you use uh whenever you use this function give this lemma so that you don't so i have to specify it by default okay uh all right so is the problem that that was the problem okay i had used the just like there are two types of equal and uh two types of lots of other things there's two all right so is that enough to satisfy this function oh suit eleven i made it a function all right it works we had to write three lemmas and two functions to prove that it list had the length that we gave it but i don't know how to get the literal to work this is ridiculous there's got to be a better way to do this but uh let's try to finish up part one because it's after midnight already so this is the minority great so i think we've got all the pieces we wrote our parser we wrote the two functions we're supposed to calculate let us write our main function then uh let's write a function that opens the file so i'm going to take a file name open the file for reading [Music] uh okay [Music] diagnostics is parse input of the file descriptor and the empty list let equals epsilon yes and i don't think there's any way to define more than one thing in the same let statement but maybe i just don't know what it is uh again ideas in print string [Music] we have to use the function off multiply unless we import a special package because uh star is reserved for pair types okay so it says how do you know that your input is of odd length like you promised so we'll check it so if uh list is not one then all right so it kept us honest let's compile this and try it out on the tutorial first on the example first so go back here oh no does that does the tutorial have a different it does have a different length all right we're just we're just screwed i'm not going back and fixing all that uh so better hope this is right i mean we should have some confidence right it's it type checks we we asserted that it behaved the way it was expected to so it's entirely possible i might oops i misunderstood the program the the problem or misinterpreted something copy a make file over so f star is better save it f-star is rechecking everything uh that we checked interactively and writing out ocamel and then we compile the ocamel file and i made the same mistake i've made two nights in a row which is that i didn't actually call this function we wrote so calc part one of input.text fortunately the compilation is a little a little faster tonight than it was last night well this is a stupid uh assumption for me to make it's exactly a thousand lines so it's not guaranteed to have a majority but it does anyway hmm [Music] that's most unfortunate i should have checked at the start uh so let's see if it's well defined then adding a zero at the end can't change anything so this is a gross hack the only way it matters is if there's even values but if there's even numbers then it doesn't matter then then the problem is not well defined okay uh if we just charge the head without writing any types then we wouldn't be in this situation let's see if we're okay all right that's right answer alright on to part two all right so we're gonna filter by the most common value that's going to cause us even more grief because we could have have sub lists that are of even length and so our function can't guarantee that okay so we're gonna we're gonna have to loosen our specification we're just gonna have to say if it's evenly matched then it's it's um we pick a value arbitrarily [Music] [Music] so we'll get rid of that constraint and [Music] to change the module name okay good still type type checked minority is less than or equal to okay good good all right so let me check this again so we're going to if zero and one are equally common keep values with a one all right so this is where this might actually be helpful so we can encode that as a type and it's easy to get wrong so it's worth doing so we can say either it's greater than the input length v2 or uh b is true and [Music] number of true equals two and one are equally common and the least common we need to go the other way all right a number of true number of true input why is it on oh underscore all right uh so is subtract is it failing for a dumb reason or because we didn't actually do this well we didn't actually do it right because we only got okay we should use the other ore all right so this should be greater than or equal to to make that true good that's helpful it's the first time we've actually gotten i think some mileage out of this all right so let's say this is true is i mean we really lonely like to have this come into play for odd numbers i think it didn't matter too much on the other one but let's right so it should be less than half rounded up or it should be false and the number of falses is exactly [Music] okay okay i'm feeling pretty good so let's define the filter criteria be easier if we could loop okay so all right so let's say we're going to filter by position i and i is a natural number less than 12 and we're going to take and take the list of diagnostic and we're going to return a list of another list of diagnostic which i mean theory we could show that it's non-empty but that would be really gross i think okay so let's um okay take everything take the eighth element of the bit vector across everything take the majority that okay good just uh filter removes everything where fx does not hold removed okay so filter uh if element for each diagnostic the ith element of d has to be equal to bit okay we need the same for minority good okay so we need to go from [Music] is it from first yeah from first bit to the last bit so um this returns an integer so if n equals 12 then we can't do this anymore um we'll say greater equal 12 to make it easier on the solver then just return an error uh value you should probably make this an an option in but it's fine else uh if equals one then we just do bv2 into that else we recursively call with n plus one and we we can't really put the condition and it's less than 12 because how do we prove that it actually terminates it might not on some inputs uh so it's kind of kind of sketchy but uh i don't see a way to do better here so we're gonna filter majority by position and which we know is less than 12 at this point in the control flow of the list oh uh extra colon wrong quality wrong syntax can you tell i've been programming python today oh uh so we need to do [Music] this to pv uh uh oh no so we need we need to grab the first element of the list uh that's not right so this decreases 12 minus n it doesn't decrease n we need to prove okay we need to prove that the function terminates uh uh maybe we should do [Music] oh no we mean circle all the way around okay that's all right i mean i wish crud i should have more confidence that uh if it type checks then it will terminate that's what it was yelling at me before about okay so that's o2 and the co2 is the same thing with the minority and you know if we're cool functional programmers we've abstracted this operation across the the filtering uh the filtering criteria which we could we could do but all right let's get rid of our hack let's get o2 starting at zero and co2 is turning at zero all right having type checks let's try it out i'm not as confident we got everything right nope nope something's wrong all right double check all right first bit first pit okay [Music] [Music] all right we can get rid of all this stuff don't need that anymore so it seems likely that there's a problem we screwed up the definition of maturity minority but i spent some time [Music] writing these conditions i kind of believe they're correct and they and they type checked so so [Music] let's let's write some unit tests so we believe that majority of one one uh [Music] false false true true equals true oh uh that's that's the wrong syntax that's tool syntax not list syntax okay looks good this be false and this is that what it says when you're looking for the minority yeah we want to keep values f of zero okay so we didn't screw up on the parity we did screw up on the parody oh no that's that's the right thing no that's a bad test case all right hmm well so let's write let's use the example input and just extend it out that's five bits so we need one two three four five six seven more except the value the value is going to be off by a factor of two to the seventh [Music] oh uh the problem was that i ran part one again [Laughter] getting tired i guess all right let's try running the part two code on the real input okay that's not so good but at least we're running the right program now [Music] seven six eight three two two by two seventh 230. okay so we're correct on the example and just we're just getting a zero on the big one which is telling us that probably that we're hitting this case let's let's put something more ugh all right if we reach there then we return the none type otherwise we return the sum type okay so i feel one with uh i'm running on letters all right so [Music] okay matches two with none next one interesting okay so it's our majority [Music] you know one of these is not doing the right thing uh the majority i'm pretty confident in now we both proved it and unit tested it uh so i don't think we're doing anything silly there a small test case worked okay [Music] all right we'll make this a non-total function so we can print out what is our length at the end uh nobody in the chat is jumping up and saying i know where the bug is [Music] oh [Music] okay that makes sense uh we should just check these in the opposite order we got all the way down to one on the very last bit so it was a bounce check i don't it's a good how could we uh how could we write a type for this that would uh would it caught that i don't know else if it's good looks guys let's make part two hurrah okay it only took me an hour and 45 minutes tonight so a little about a half hour longer than last night that's not a good trend but uh we did it thanks for staying up with me i'm gonna call tonight unless there any questions i didn't see any in the chat beyond what does torch stand for which explained so have a good rest of your evening

Channel: Mark Gritter

Views: 60

Keywords: FStarLang, Programming

Id: lroPbn5cc8w

Length: 111min 19sec (6679 seconds)

Published: Fri Dec 03 2021